Commit be38823e authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

dedicated norms

parent 7c5e2077
......@@ -152,5 +152,5 @@ instance PP.Pretty p => PP.Pretty (Literal p) where
instance PP.Pretty l => PP.Pretty (DNF l) where
pretty Top = PP.text "⊤"
pretty Bot = PP.text "⊥"
pretty dnf = lst " ∨ " [ lst " ∧ " [ PP.pretty l | l <- lits c] | c <- conjs dnf]
where lst s = PP.group . PP.hcat . PP.punctuate (PP.text s)
pretty dnf = lst " ∨ " [ lst " ∧ " [ PP.group (PP.pretty l) | l <- lits c] | c <- conjs dnf]
where lst s = PP.hcat . PP.punctuate (PP.text s)
......@@ -8,26 +8,41 @@ import Data.PWhile.BoolExpression hiding (variables)
import qualified Data.PWhile.BoolExpression as B
import qualified Data.PWhile.Expression as E
data GExp c = GExp BExp c E.Exp
deriving Show
-- plusG :: (Eq c, Ord c, Num c) => GExp c -> GExp c -> GExp c
-- plusG (GExp g1 e1) (GExp g2 e2) = GExp (g1 .&& g2) (e1 + e2)
data Norm = Norm BExp E.Exp
deriving (Eq, Ord, Read, Show)
norm :: BExp -> E.Exp -> Norm
norm _ e@(E.Constant _) = Norm Top e
norm g e = Norm g e
oneN :: Norm
oneN = Norm Top 1
mulG :: (Eq c, Ord c, Num c) => GExp c -> GExp c -> GExp c
mulG (GExp g1 k1 e1) (GExp g2 k2 e2) = GExp (g1 .&& g2) (k1 * k2) (e1 * e2)
plusN :: Norm -> Norm -> Norm
plusN (Norm _ 0) n@Norm{} = n
plusN n@Norm{} (Norm _ 0) = n
plusN (Norm g1 e1) (Norm g2 e2) = norm (g1 .&& g2) (e1 + e2)
-- norm :: (Eq c, Num c) => BExp c -> E.Expression c -> GExp c
-- norm g e = GExp g e' where
-- e' = fmap fromIntegral e
mulN :: Norm -> Norm -> Norm
mulN (Norm _ 1) n@Norm{} = n
mulN n@Norm{} (Norm _ 1) = n
mulN (Norm g1 e1) (Norm g2 e2) = norm (g1 .&& g2) (e1 * e2)
fromExp :: (Eq c, Num c) => E.Exp -> CExp c
fromExp = E . fmap fromIntegral
prodN :: [Norm] -> Norm
prodN = foldl mulN oneN
expN :: Norm -> Int -> Norm
expN (Norm g e) i = Norm g (product (replicate i e))
isZeroN :: Norm -> Bool
isZeroN (Norm _ e) = e == 0
isConstN :: Norm -> Bool
isConstN (Norm _ e) = null (E.variables e)
data CExp c =
E E.Exp
| Coeff c (CExp c)
N c Norm
| Div (CExp c) E.Exp
| Plus (CExp c) (CExp c)
| Sup (CExp c) (CExp c)
......@@ -35,10 +50,14 @@ data CExp c =
deriving (Eq, Ord, Read, Show)
-- fromExp :: (Eq c, Num c) => E.Exp -> CExp c
-- fromExp = E . fmap fromIntegral
traverseCoeff :: (Num c', Ord c', Applicative f) => (c -> f c') -> CExp c -> f (CExp c')
traverseCoeff f = walk where
walk (E e) = pure (E e)
walk (Coeff k c) = coeff <$> f k <*> walk c
walk (N k n) = nm <$> f k where
nm 0 = zero
nm k' = N k' n
walk (Div c e) = divBy <$> walk c <*> pure e
walk (Plus c d) = plus <$> walk c <*> walk d
walk (Sup c d) = sup <$> walk c <*> walk d
......@@ -47,27 +66,26 @@ traverseCoeff f = walk where
mapCoeff :: (Num c', Ord c') => (c -> c') -> CExp c -> CExp c'
mapCoeff f = runIdentity . traverseCoeff (pure . f)
fromNorm :: Num c => Norm -> CExp c
fromNorm = N 1
zero :: (Eq c, Num c) => CExp c
zero = E 0
zero = N 1 (Norm Top 0)
one :: (Eq c, Num c) => CExp c
one = E 1
coeff :: (Eq c, Num c) => c -> CExp c -> CExp c
coeff 0 _ = zero
coeff 1 c = c
coeff k c = Coeff k c
one = N 1 (Norm Top 1)
plus :: (Eq c, Num c, Ord c) => CExp c -> CExp c -> CExp c
plus (Coeff k1 c1) (Coeff k2 c2)
| k1 == k2 = Coeff k1 (c1 `plus` c2)
plus (Div c1 e1) (Div c2 e2)
| e1 == e2 = (c1 `plus` c2) `divBy` e1
plus (E 0) c2 = c2
plus c1 (E 0) = c1
plus (E e1) (E e2) = E (e1 + e2)
plus c1 c2 = Plus c1 c2
plus (Cond g c1 c2) (Cond g' c1' c2')
| g == g' = Cond g (c1 `plus` c1') (c2 `plus` c2')
plus (Div c1 e1) (Div c2 e2) | e1 == e2 = (c1 `plus` c2) `divBy` e1
plus (N k1 n1) (N k2 n2) | k1 == k2 = N k1 (n1 `plusN` n2)
plus c1 c2 | c1 == zero = c2
| c2 == zero = c1
| otherwise = Plus c1 c2
ramp :: Num c => E.Exp -> CExp c
ramp e = N 1 (norm (e .>= 0) e)
sum :: (Eq c, Num c, Ord c) => [CExp c] -> CExp c
sum = foldl plus zero
......@@ -78,7 +96,7 @@ sup c1 c2 | c1 == zero = c2
| c1 == c2 = c1
sup c1 c2 = Sup c1 c2
cond :: Eq c => BExp -> CExp c -> CExp c -> CExp c
cond :: (Eq c, Num c) => BExp -> CExp c -> CExp c -> CExp c
cond Top c _ = c
cond Bot _ d = d
cond _ c d
......@@ -90,15 +108,16 @@ cond g c d = Cond g c d
guarded :: (Eq c, Num c) => BExp -> CExp c -> CExp c
guarded g c = cond g c zero
oneV :: CExp c
oneV = E "@@ONE@@"
oneV :: Num c => CExp c
oneV = N 1 (Norm Top "@@ONE@@")
pred :: (Eq c, Num c) => BExp -> CExp c
pred g = cond g oneV zero
divBy :: (Eq c, Ord c, Num c) => CExp c -> E.Exp -> CExp c
divBy c _
| c == zero = zero
divBy c 1 = c
divBy (E e) f = case snd (E.factor e f) of { (e',1) -> E e'; (e',f') -> Div (E e') f' }
divBy (Div c e) f = Div c (e * f)
divBy c f = Div c f
......@@ -115,63 +134,87 @@ divBy c f = Div c f
scale :: (Eq c, Ord c, Num c) => E.Exp -> CExp c -> CExp c
scale 0 _ = zero
scale 1 c = c
scale e (Coeff k c) = Coeff k (scale e c)
scale e (E f) = E (e * f)
scale (E.Constant k) c = scaleC (fromIntegral k) c
scale e (N k n) = N k (norm (e .>= 0) e `mulN` n)
scale e (Div d f) = scale e' d `divBy` f' where (_,(e',f')) = E.factor e f
scale e (Plus d1 d2) = scale e d1 `plus` scale e d2
scale e (Sup d1 d2) = scale e d1 `sup` scale e d2
scale e (Cond g d1 d2) = cond g (scale e d1) (scale e d2)
scaleC :: (Eq c, Ord c, Num c) => c -> CExp c -> CExp c
scaleC 0 _ = zero
scaleC 1 c = c
scaleC k c = mapCoeff (*k) c
-- toExp :: (Eq c, Num c) => CExp c -> Maybe (E.Expression c)
-- toExp (E f) = Just f
-- toExp (Plus d1 d2) = (+) <$> toExp d1 <*> toExp d2
-- toExp _ = Nothing
gExps :: (Eq c, Num c) => CExp c -> [GExp c]
gExps = walk B.Top 1 where
walk B.Bot _ _ = []
walk b k (E e) = [GExp b k e]
walk b k (Coeff l c) = walk b (k * l) c
walk b k (Div c _) = walk b k c
walk b k (Plus c d) = walk b k c ++ walk b k d
walk b k (Sup c d) = walk b k c ++ walk b k d
walk b k (Cond g c d) = walk (b .&& g) k c ++ walk (b .&& neg g) k d
fromGExp :: (Eq c, Ord c, Num c) => GExp c -> CExp c
fromGExp (GExp g k e)
| k == 0 || e == 0 = zero
| otherwise = guarded g (coeff k (E e))
variables :: CExp c -> S.Set E.Var
variables (E e) = E.variables e
variables (Coeff _ c) = variables c
variables (Div c f) = variables c `S.union` E.variables f
variables (Plus c d) = variables c `S.union` variables d
variables (Sup c d) = variables c `S.union` variables d
variables (Cond g c d) = B.variables g `S.union` variables c `S.union` variables d
variables (N _ (Norm _ e)) = E.variables e
variables (Div c f) = variables c `S.union` E.variables f
variables (Plus c d) = variables c `S.union` variables d
variables (Sup c d) = variables c `S.union` variables d
variables (Cond g c d) = B.variables g `S.union` variables c `S.union` variables d
instance E.Substitutable Norm where
substitute s e (Norm g f) = norm (E.substitute s e g) (E.substitute s e f)
instance (Eq c, Ord c, Num c) => E.Substitutable (CExp c) where
substitute s e (E f) = E (E.substitute s e f)
substitute s e (Coeff k c) = Coeff k (E.substitute s e c)
substitute s e (N k n) = N k (E.substitute s e n)
substitute s e (Div c f) = E.substitute s e c `divBy` E.substitute s e f
substitute s e (Plus c d) = E.substitute s e c `plus` E.substitute s e d
substitute s e (Sup c d) = E.substitute s e c `sup` E.substitute s e d
substitute s e (Cond b c d) = cond (E.substitute s e b) (E.substitute s e c) (E.substitute s e d)
instance PP.Pretty Norm where
pretty (Norm g e) = PP.brackets (PP.hang 0 (PP.pretty e PP.</> PP.text "|" PP.<+> PP.pretty g))
instance (PP.Pretty c, Eq c, Num c) => PP.Pretty (CExp c) where
pretty = pp id where
pp _ (E e) = ppFun "E" [PP.pretty e]
pp _ (Coeff k c) = ppFun "mul" [PP.pretty k, PP.pretty c]
pp _ (Div c e) = ppFun "div" [ PP.pretty c, PP.pretty e ]
pp _ (Plus c d) = ppFun "plus" [ PP.pretty c, PP.pretty d ]
-- pp par (Div c e) = PP.parens (infx (pp id c) "/" (PP.pretty e))
-- pp par (Plus c d) = PP.parens (infx (pp PP.parens c) "+" (pp PP.parens d))
pp _ (Sup c d) = ppFun "sup" [ pp id c, pp id d ]
pp par (N 1 n) = par (ppNorm n)
pp par (N k n) = PP.pretty k PP.<> PP.text "·" PP.<> par (ppNorm n)
pp par (Div c e) = par (infx (pp id c) "/" (PP.pretty e))
pp _ (Plus c d) = infx (pp PP.parens c) "+" (pp PP.parens d)
pp _ (Sup c d) = ppFun "sup" [ PP.pretty c, PP.pretty d ]
pp _ (Cond g c d)
| d == zero = PP.brackets (PP.pretty g) PP.</> PP.parens (PP.pretty c)
| otherwise = PP.text "ite" PP.<> PP.tupled [ PP.pretty g, pp id c, pp id d ]
-- infx d1 s d2 = d1 PP.</> PP.text s PP.<+> d2
| d == zero = PP.hang 1 (PP.brackets (PP.pretty g) PP.<> PP.text "·" PP.<> pp PP.parens c)
| otherwise = PP.text "ite" PP.<> PP.tupled [ PP.pretty g, pp id c, pp id d ]
ppFun f ls = PP.text f PP.<> PP.tupled ls
infx l s r = PP.hang 1 (l PP.</> PP.text s PP.<+> r)
ppNorm (Norm _ e) = PP.pretty e
-- guarded norms
data GNorm c = GNorm BExp c Norm
deriving Show
isConstGN :: (Eq c, Num c) => GNorm c -> Bool
isConstGN (GNorm g c n)
| c == 0 = True
| isZeroN n = True
| g == Bot = True
| otherwise = isConstN n && S.null (B.variables g)
mulG :: (Eq c, Ord c, Num c) => GNorm c -> GNorm c -> GNorm c
mulG (GNorm g1 k1 n1) (GNorm g2 k2 n2) = GNorm (g1 .&& g2) (k1 * k2) (n1 `mulN` n2)
fromGNorm :: (Eq c, Ord c, Num c) => GNorm c -> CExp c
fromGNorm (GNorm Bot _ _) = zero
fromGNorm (GNorm _ 0 _) = zero
fromGNorm (GNorm _ _ (Norm _ 0)) = zero
fromGNorm (GNorm g k n) = guarded g (N k n)
gNorms :: (Eq c, Num c) => CExp c -> [GNorm c]
gNorms = walk B.Top 1 where
walk B.Bot _ _ = []
walk b k (N _ e) = [GNorm b k e]
walk b k (Div c _) = walk b k c
walk b k (Plus c d) = walk b k c ++ walk b k d
walk b k (Sup c d) = walk b k c ++ walk b k d
walk b k (Cond g c d) = walk (b .&& g) k c ++ walk (b .&& neg g) k d
instance (PP.Pretty c, Eq c, Ord c, Num c) => PP.Pretty (GExp c) where
pretty = PP.pretty . fromGExp
instance (PP.Pretty c, Eq c, Ord c, Num c) => PP.Pretty (GNorm c) where
pretty = PP.pretty . fromGNorm
......@@ -154,15 +154,8 @@ runAny m = listToMaybe <$> run Any m
-- cost functions
----------------------------------------------------------------------
ramp :: (Eq c, Num c) => E.Exp -> C.CExp c
ramp e = C.guarded (e .>= 0) (C.fromExp e)
isConstGExp (C.GExp _ _ 0) = True
isConstGExp (C.GExp Bot _ _) = True
isConstGExp (C.GExp g _ e) = null (E.variables e) && S.null (B.variables g)
varGExps :: (Eq c, Num c) => C.CExp c -> [C.GExp c]
varGExps = filter (not . isConstGExp) . C.gExps
varGNorms :: (Eq c, Num c) => C.CExp c -> [C.GNorm c]
varGNorms = filter (not . C.isConstGN) . C.gNorms
-- estimating expectations
----------------------------------------------------------------------
......@@ -195,17 +188,17 @@ boundedSum f (l,o) = logBlkIdM msg $ bs fi where
inv = o .>= vi
, cnd = vi .>= l
, cost = g
, step = (E.substitute i (vi - 1) . C.fromGExp) `map` ns
, step = (E.substitute i (vi - 1) . C.fromNorm) `map` ns
, cont = C.zero
, limt = ns }
uiUp = UpperInvariant {
inv = vi .>= l
, cnd = o .>= vi
, cost = g
, step = (E.substitute i (vi + 1) . C.fromGExp) `map` ns
, step = (E.substitute i (vi + 1) . C.fromNorm) `map` ns
, cont = C.zero
, limt = ns }
ns = varGExps g
ns = [n | C.GNorm _ _ n <- varGNorms g]
expectation :: E.Dist E.Exp -> (E.Exp -> CExp) -> SolveM CExp
......@@ -262,7 +255,9 @@ expectation (E.Rand n) f =
-- Expectation Transformer
----------------------------------------------------------------------
extractRanking :: C -> BExp -> BExp -> CExp -> CExp -> SolveM [C.GExp Rational]
type NormPoly = P.Polynomial C.Norm Int
extractRanking :: C -> BExp -> BExp -> CExp -> CExp -> SolveM [C.Norm]
extractRanking body i c g f = do
combine <-
(logMsg "additive" >> pure additive)
......@@ -271,46 +266,49 @@ extractRanking body i c g f = do
(logMsg "optimistic" >> pure (ranksFromBExpWith optimistic))
<|> (logMsg "shift" >> pure (ranksFromBExpWith shift))
<|> (logMsg "squared-optimistic" >> pure (squared (ranksFromBExpWith optimistic)))
gRanks <- filter (not . isConstGExp) <$> combine rankFromBExp (c .&& i) (varGExps g)
return (C.GExp Top 1 1 : varGExps f ++ gRanks) -- ++ fRanks'
gRanks <- combine rankFromBExp (c .&& i) (varGNorms g)
fRanks <- pure (sum (fromGNorm `map` C.gNorms f))
return (toNormList (norm 1 + fRanks + gRanks)) -- ++ fRanks'
where
ranksFromBExpWith sel bexp = mapM sel (S.toList (literals bexp))
toNormList p = filter (not . zeroN) [ C.prodN [ C.expN n i | (n,i) <- P.toPowers m ]
| (_,m) <- P.toMonos p]
where zeroN (C.Norm _ e) = e == 0
norm e = P.variable (C.Norm (e .>= 0) e)
fromGNorm (C.GNorm _ _ n) = P.variable n
additive fromBExp b gexps = do
grdRanks <- fromBExp (b .&& bigAnd [ b' | C.GExp b' _ _ <- gexps ])
return (grdRanks ++ [ C.GExp (e .>= 0) k e | C.GExp _ k e <- gexps ])
ranksFromBExpWith sel bexp = sum <$> mapM sel (S.toList (literals bexp))
multiplicative fromBExp b gexps =
concat <$> sequence [ map (C.mulG (C.GExp (e .>= 0) k e)) <$> fromBExp (b .&& b')
| C.GExp b' k e <- gexps]
additive fromBExp b gexps =
(+) (sum (fromGNorm `map` gexps))
<$> fromBExp (b .&& bigAnd [ b' | C.GNorm b' _ _ <- gexps ])
guarded :: BExp -> E.Exp -> C.GExp Rational
guarded g = C.GExp g 1
multiplicative fromBExp b gexps =
(+) <$> additive fromBExp b gexps
<*> (sum <$> sequence [ (*) (P.variable n) <$> fromBExp (b .&& b')
| C.GNorm b' _ n <- gexps])
optimistic (a :>=: b) = pure $ guarded (a .>= b) (a - b + 1)
optimistic (a :>=: b) = pure $ norm (a - b + 1)
-- optimistic' i (a :>=: b) = pure $ guarded (a .>= b) (a - b + i)
squared m x = do
gs <- m x
return [C.GExp b (k*k) (e * e) | C.GExp b k e <- gs]
squared m x = sq <$> m x where sq n = n * n
-- delta (C.Norm e) = do
-- ns <- S.toList <$> C.norms <$> evt body (C.fromNorm (C.norm e) :: C.NormPoly Rational)
-- return $ C.Norm $ maxE [ ne | C.Norm ne <- ns ] - e
shift l@(a :>=: b) = do
mkNorm <$> maxE <$> concatMap diffs <$> C.gExps <$> evt body (C.pred (a .>= b))
-- TODO: this is a mess; maybe define wp for non-recursive language?
mkNorm <$> maxE <$> concatMap diffs <$> C.gNorms <$> evt body (C.pred (a .>= b))
where
maxE [] = 0
maxE es = foldl1 (P.zipCoefficientsWith (max 0) (max 0) max) es
diffs (C.GExp gd _ e)
| e /= 0 = [ (a' - b') - (a - b) | a' :>=: b' <- S.toList (literals gd) ]
| otherwise = []
mkNorm (E.AddConst _ df) = guarded (e .>= 0) e
where e = a - b + 1 + E.constant df
diffs (C.GNorm gd _ n)
| not (C.isZeroN n) = [ (a' - b') - (a - b) | a' :>=: b' <- S.toList (literals gd) ]
| otherwise = []
-- TODO
mkNorm (E.AddConst _ df) = norm (a - b + 1 + E.constant df)
isConstantWrt :: CExp -> C -> Bool
f `isConstantWrt` c = C.variables f `S.disjoint` vs where
......@@ -364,7 +362,7 @@ et Evt c (C.Plus f1 f2)
et _ Abort _ = return C.zero
et _ Skip f = return f
et Evt (Tic _) f = return f
et Ect (Tic e) f = return $ ramp e `C.plus` f
et Ect (Tic e) f = return $ C.ramp e `C.plus` f
et _ (Ass v d) f = expectation d (\ e -> E.substitute v e f)
et t (NonDet e1 e2) f = C.sup <$> etM t e1 f <*> etM t e2 f
et t (Choice ls) f = discreteExpectation ls (\ c -> etM t c f)
......@@ -381,7 +379,7 @@ et t (While _ i b c) f =
ns <- extractRanking c i b g f
logMsg2 "Norms" ns
-- TODO: filter those ni's for which hi cannot be computed?
hs <- traverse (evt c . C.fromGExp) ns
hs <- traverse (evt c . C.fromNorm) ns
let ui = UpperInvariant { inv = i
, cnd = b
, cost = g
......
......@@ -23,7 +23,7 @@ data UpperInvariant =
, cost :: CExp Rational
, step :: [CExp Rational]
, cont :: CExp Rational
, limt :: [GExp Rational]}
, limt :: [Norm]}
deriving Show
class InvariantSolver s where
......@@ -52,4 +52,4 @@ instance Pretty UpperInvariant where
ppCont = ppPrem (inv ui .&& neg (cnd ui)) <+> pretty (cont ui)
</> ppLeq <+> ppHi (limt ui)
ppPrem b = pretty b <+> ppImp
ppHi gi = PP.char 'h' <> PP.tupled (fmap pretty gi)
ppHi gi = PP.char 'h' <> PP.tupled (fmap (PP.group . pretty) gi)
......@@ -268,7 +268,7 @@ entailsSmtK i p c k =
applyTemplate :: (Num c, Ord c, Eq c) => [c] -> [C.CExp c] -> C.CExp c
applyTemplate qs cs = C.sum (zipWith C.Coeff qs cs)
applyTemplate qs cs = C.sum (zipWith C.scaleC qs cs)
-- elimination of cost expression
......@@ -276,9 +276,7 @@ applyTemplate qs cs = C.sum (zipWith C.Coeff qs cs)
-- toFrac :: AExp -> (AExp, Exp)
toFrac :: (Eq c, Ord c, Num c) => C.CExp c -> (C.CExp c, E.Exp)
toFrac c@C.E{} = (c,1)
toFrac (C.Coeff k c) = (C.Coeff k d, f) where
(d,f) = toFrac c
toFrac c@C.N{} = (c,1)
toFrac (C.Div c e) = (d,e*f) where
(d,f) = toFrac c
toFrac (C.Sup c1 c2) = (C.scale f2 d1 `C.sup` C.scale f1 d2, f1 * f2 * f) where
......@@ -302,37 +300,41 @@ reduce (GEQ c (toFrac -> (lhs,f1)) (toFrac -> (rhs,f2))) = do
return [GEQ g (fromExp f2' * l) (fromExp f1' * r) | GEQ g l r <- cs, r /= 0]
where
(_,(f1',f2')) = E.factor f1 f2
branch (fromBExp -> g) m c1 c2 ctx k =
branch (fromBExp -> g) m1 m2 ctx k =
entailsSmtK 1 ctx g $ \ entailed ->
if entailed
then m c1 (ctx .&! g) k -- debugPA (PP.pretty ctx <> PP.text "=>" <> PP.pretty g) =<<
then m1 (ctx .&! g) k -- debugPA (PP.pretty ctx <> PP.text "=>" <> PP.pretty g) =<<
else entailsSmtK 1 ctx (neg' g) $ \ negEntailed ->
if negEntailed
then m c2 (ctx .&! neg' g) k -- debugPA (PP.pretty ctx <> PP.text "=>" <> PP.pretty (neg' g)) =<<
else (++) <$> m c1 (ctx .&! g) k
<*> m c2 (ctx .&! neg' g) k
then m2 (ctx .&! neg' g) k -- debugPA (PP.pretty ctx <> PP.text "=>" <> PP.pretty (neg' g)) =<<
else (++) <$> m1 (ctx .&! g) k
<*> m2 (ctx .&! neg' g) k
add m c1 c2 ctx k =
m c1 ctx $ \ e1 ctx' ->
m c2 ctx' $ \ e2 ->
norm (C.Norm g e) =
branch g (\ ctx' k' -> k' (fromExp e) ctx')
(\ ctx' k' -> k' 0 ctx')
add m1 m2 ctx k =
m1 ctx $ \ e1 ctx' ->
m2 ctx' $ \ e2 ->
k (e1 + e2)
scale l m c1 ctx k =
m c1 ctx $ \ e -> k (P.coefficient l * e)
scale l m ctx k =
m ctx $ \ e -> k (P.coefficient l * e)
walkLhs _ Bot _ = return []
walkLhs (C.E e) ctx k = k (fromExp e) ctx
walkLhs (C.Coeff l c1) ctx k = scale l walkLhs c1 ctx k
walkLhs (C.Cond g c1 c2) ctx k = branch g walkLhs c1 c2 ctx k
walkLhs (C.Plus c1 c2) ctx k = add walkLhs c1 c2 ctx k
walkLhs (C.N c' n) ctx k = scale c' (norm n) ctx k
walkLhs (C.Cond g c1 c2) ctx k =
branch g (walkLhs c1) (walkLhs c2) ctx k
walkLhs (C.Plus c1 c2) ctx k = add (walkLhs c1) (walkLhs c2) ctx k
walkLhs C.Div {} _ _ = error "InvariantSolver.Naive.reduce: div on lhs"
walkLhs C.Sup {} _ _ = error "InvariantSolver.Naive.reduce: sup on lhs"
walkRhs _ Bot _ = return []
walkRhs (C.E e) ctx k = k (fromExp e) ctx
walkRhs (C.Coeff l c1) ctx k = scale l walkRhs c1 ctx k
walkRhs (C.Cond g c1 c2) ctx k = branch g walkRhs c1 c2 ctx k
walkRhs (C.Plus c1 c2) ctx k = add walkRhs c1 c2 ctx k
walkRhs (C.N c' n) ctx k = scale c' (norm n) ctx k
walkRhs (C.Cond g c1 c2) ctx k = branch g (walkRhs c1) (walkRhs c2) ctx k
walkRhs (C.Plus c1 c2) ctx k = add (walkRhs c1) (walkRhs c2) ctx k
walkRhs C.Div {} _ _ = error "InvariantSolver.Naive.reduce: div on rhs"
walkRhs (C.Sup c1 c2) ctx k =
(++) <$> walkRhs c1 ctx k <*> walkRhs c2 ctx k
......@@ -343,12 +345,11 @@ debug = debugMsg "SmtSolver"
-- debugPA :: (Applicative f, PP.Pretty msg, PP.Pretty e) => msg -> e -> f e
-- debugPA = debugMsgA "SmtSolver" . renderPretty
upperInvariant :: NaiveSolver -> UpperInvariant -> SmtM (Maybe CExp)
upperInvariant s UpperInvariant{..} = do
qs <- traverse (const freshACoeff) step
let
f = applyTemplate qs [ encode (C.fromGExp l) | l <- limt]
f = applyTemplate qs [ encode (C.fromNorm l) | l <- limt]
g = C.cond cnd (encode cost `C.plus` applyTemplate qs (encode `map` step)) (encode cont)
initial = debug "initial" (GEQ (fromBExp inv) f g)
cs <- debug "final" <$> reduce initial
......
......@@ -55,8 +55,8 @@ evalBExp (Disj ds) st = any (\(Conj cs) -> all isGte cs) ds where
evalCExp :: C.CExp Rational -> Store -> Rational
evalCExp cexp st = ev cexp where
ev (C.E e) = fromIntegral (evalExp e st)
ev (C.Coeff k d) = k * ev d
ev (C.N k (C.Norm _ e)) = k * fromIntegral (evalExp e st)
-- ev (C.Coeff k d) = k * ev d
ev (C.Div c e) = ev c / fromIntegral (evalExp e st)
ev (C.Plus c d) = ev c + ev d
ev (C.Sup c d) = ev c `max` ev d
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment