Skip to content
GitLab
Commit 19796374 authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

fixed bug in constraint simplification of divs

parent 9faed3ec
Hide whitespace changes
Inline Side-by-side
src/Data/PWhile/Expression.hs
View file @ 19796374
......@@ -11,6 +11,7 @@ module Data.PWhile.Expression
, variable
, constant
, variables
, factor
, Substitutable (..)
-- distributions
-- , Frac (..)
......@@ -44,6 +45,11 @@ variable = P.variable
variables :: Expression c -> S.Set Var
variables = S.fromList . P.variables
factor :: (Eq c, Num c) => Expression c -> Expression c -> (Expression c, (Expression c, Expression c))
factor e1 e2 =
case P.factoriseMono [e1,e2] of
Just (m,[e1',e2']) -> (P.fromMono m, (e1',e2'))
_ -> (1,(e1,e2))
-- patterns
const_ :: (Ord v, Eq c, Num c) => P.Polynomial v c -> Maybe c
......
src/PWhile/InferEt.hs
View file @ 19796374
......@@ -200,20 +200,6 @@ boundedSum f (l,o) = logBlkIdM msg $ bs fi where
, cont = C.zero
, limt = ns }
ns = rankFromCExp g
-- where
-- fromCExp (C.E e) = fromExp e
-- fromCExp (C.Div f _) = fromCExp f
-- fromCExp (C.Plus f1 f2) = fromCExp f1 `S.union` fromCExp f2
-- fromCExp (C.Sup f1 f2) = fromCExp f1 `S.union` fromCExp f2
-- fromCExp (C.Cond g f1 f2) = S.fromList
-- [ ng `C.mulG` n1 | ng <- 1 : S.toList (fromBExp g)
-- , n1 <- S.toList (fromCExp f1)]
-- ++ [ ng `C.mulG` n2 | ng <- 1 : S.toList (fromBExp (neg g))
-- , n2 <- S.toList (fromCExp f2)]
-- fromBExp bexp = S.fromList [ C.norm (b - a - 1)
-- | (a :>=: b) <- S.toList (literals bexp)]
-- fromExp e = S.fromList [ P.fromMono m
-- | (_,m) <- P.toMonos e ]
expectation :: E.Dist E.Exp -> (E.Exp -> CExp) -> SolveM CExp
......@@ -380,7 +366,7 @@ et t (Cond _ i b c1 c2) f = C.guarded i <$> (C.cond b <$> etM t c1 f <*> etM t
et Ect (Seq c1 c2) f
| isSimple c1 = etM Ect c1 =<< etM Ect c2 f
| otherwise = C.plus <$> ect c1 C.zero <*> (evt c1 =<< ect c2 f)
et _ (Seq c1 c2) f = etM Ect c1 =<< etM Ect c2 f
et t (Seq c1 c2) f = etM t c1 =<< etM t c2 f
et t (While _ i b c) f =
-- TODO: if x not modified than x should be treated as constant, see absynthRdseql;
logBlkIdM "[While.Step]" $ do
......
src/PWhile/InvariantSolver/Naive.hs
View file @ 19796374
......@@ -33,8 +33,8 @@ type SmtFormula = SMT.SMTFormula SMT.SMTLib2
type SmtExpression = SMT.SMTExpression SMT.SMTLib2
runSmtM :: SmtM a -> a
-- runSmtM = unsafePerformIO . SMT.runSMTLib2 "z3" ["-smt2", "-in"]
runSmtM = unsafePerformIO . SMT.runSMTLib2Using "QF_LIRA" "yices-smt2" ["--incremental"]
runSmtM = unsafePerformIO . SMT.runSMTLib2 "z3" ["-smt2", "-in"]
-- runSmtM = unsafePerformIO . SMT.runSMTLib2Using "QF_LIRA" "yices-smt2" ["--incremental"]
-- runSmtM = unsafePerformIO . SMT.runSMTLib2 "yices-smt2" []
-- MS: Optimisation with OptiMathSat (version 1.6.3)
......@@ -250,20 +250,20 @@ assertEntailSmt i (Disj cs) p = forM_ cs $ \c -> SMT.assert =<< handelman i c p
assertConstraintSmt :: Int -> Constraint SmtPoly -> SmtM ()
assertConstraintSmt i (GEQ g l r) = assertEntailSmt i g (l `geqLit` r)
entailsSmtK :: Int -> DNF SmtLit -> DNF SmtLit -> (Bool -> SmtM a) -> SmtM a
entailsSmtK i p c k = anySatM (conjs c) where
anySatM [] = k False
anySatM (cs:css) = do
SMT.push
s <- allSatM (lits cs)
if s
then k True <* SMT.pop
else SMT.pop >> anySatM css
allSatM [] = return True
allSatM ls = forM ls (ent p) *> SMT.checkSat
entailsSmtK :: PP.Pretty a => Int -> DNF SmtLit -> DNF SmtLit -> (Bool -> SmtM a) -> SmtM a
entailsSmtK i p c k = k False
-- anySatM (conjs c) where
-- anySatM [] = k False
-- anySatM (cs:css) = do
-- SMT.push
-- s <- allSatM (lits cs)
-- if s then k True <* SMT.pop else SMT.pop >> anySatM css
-- allSatM [] = return True
-- allSatM ls = forM ls (ent p) *> SMT.checkSat
-- TODO: add syntactic checks and possibly assert
ent = assertEntailSmt i
-- ent = assertEntailSmt i
applyTemplate :: (Num c, Eq c) => [c] -> [C.CExp c] -> C.CExp c
......@@ -273,12 +273,31 @@ applyTemplate qs = C.sum . zipWith C.scale (E.constant `map` qs)
-- elimination of cost expression
----------------------------------------------------------------------
-- toFrac :: AExp -> (AExp, Exp)
toFrac :: (Eq c, Num c) => C.CExp c -> (C.CExp c, E.Expression c)
toFrac c@C.E{} = (c,1)
toFrac (C.Div c e) = (c,e)
toFrac (C.Sup c1 c2) = (C.scale f2 d1 `C.sup` C.scale f1 d2, f1 * f2 * f) where
(d1,e1) = toFrac c1
(d2,e2) = toFrac c2
(f,(f1,f2)) = E.factor e1 e2
toFrac (C.Plus c1 c2) = (C.scale f2 d1 `C.plus` C.scale f1 d2, f1 * f2 * f) where
(d1,e1) = toFrac c1
(d2,e2) = toFrac c2
(f,(f1,f2)) = E.factor e1 e2
toFrac (C.Cond g c1 c2) = (C.cond g (C.scale f2 d1) (C.scale f1 d2), f1 * f2 * f) where
(d1,e1) = toFrac c1
(d2,e2) = toFrac c2
(f,(f1,f2)) = E.factor e1 e2
reduce :: Constraint AExp -> SmtM [Constraint SmtPoly]
reduce (GEQ c lhs rhs) =
walkLhs lhs c (\ lhs' ctx' ->
walkRhs rhs ctx' (\ rhs' ctx'' ->
return [GEQ ctx'' lhs' rhs']))
reduce (GEQ c (toFrac -> (lhs,f1)) (toFrac -> (rhs,f2))) = do
cs <- walkLhs lhs c (\ lhs' ctx' ->
walkRhs rhs ctx' (\ rhs' ctx'' ->
return [GEQ ctx'' lhs' rhs']))
return [GEQ g (f2' * l) (f1' * r) | GEQ g l r <- cs]
where
(_,(f1',f2')) = E.factor f1 f2
branch (fromBExp -> g) m c1 c2 ctx k =
entailsSmtK 1 ctx g $ \ entailed ->
if entailed
......@@ -286,6 +305,9 @@ reduce (GEQ c lhs rhs) =
else entailsSmtK 1 ctx (neg' g) $ \ negEntailed ->
if negEntailed
then m c2 ctx k
-- TODO
-- else (++) <$> m c1 (ctx .&& g) k
-- <*> m c2 (ctx .&& neg' g) k
else (++) <$> m c1 (ctx .&! g) k
<*> m c2 (ctx .&! neg' g) k
......@@ -294,59 +316,27 @@ reduce (GEQ c lhs rhs) =
m c2 ctx' $ \ e2 ->
k (e1 + e2)
scaleLhs f cs = [ GEQ g (l * f) r | GEQ g l r <- cs]
scaleRhs f cs = [ GEQ g l (r * f) | GEQ g l r <- cs]
walkLhs _ Bot _ = return []
walkLhs (C.E e) ctx k = k e ctx
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.Div c1 f) ctx k =
walkLhs c1 ctx $ \ e ctx' -> scaleRhs f <$> k e ctx'
-- walkLhs (C.Div c1 f) ctx k =
-- walkLhs c1 ctx $ \ e ctx' -> scaleRhs f <$> k e ctx'
-- TODO: maybe specialize lhs to GExp
walkLhs C.Sup {} _ _ = error "InvariantSolver.Naive.reduce: sup on rhs"
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 0) _ _ = return []
walkRhs (C.E e) ctx k = k e ctx
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.Div c1 f) ctx k =
walkRhs c1 ctx $ \ e ctx' -> scaleLhs f <$> k e ctx'
walkRhs C.Div {} _ _ = error "InvariantSolver.Naive.reduce: div on rhs"
-- walkRhs (C.Div c1 f) ctx k =
-- walkRhs c1 ctx $ \ e ctx' -> scaleLhs f <$> k e ctx'
walkRhs (C.Sup c1 c2) ctx k =
(++) <$> walkRhs c1 ctx k <*> walkRhs c2 ctx k
fromCExp :: AExp -> SmtPoly
fromCExp (C.E e) = e
fromCExp (C.Plus c1 c2) = fromCExp c1 + fromCExp c2
fromCExp _ = error "InvariantSolver.Naive.fromCExp: undefined case"
-- eliminateMax :: Constraint l (C.MaxExp r) -> [Constraint l r]
-- eliminateMax (GEQ g l (C.Max rs)) = [GEQ g l r | r <- rs]
-- removeTrivial :: (C.CExp c) => Constraint l c -> [Constraint l c]
-- removeTrivial (GEQ _ _ r) | C.isZero r = []
-- removeTrivial (GEQ Bot _ _) = []
-- removeTrivial c = [c]
-- eliminateCond :: (Show r, Num r) => Constraint l (C.GuardedSum r) -> [Constraint l r]
-- eliminateCond (GEQ g l (C.GS s)) = [GEQ b l r | (b,r) <- walk (M.toList s)]
-- where
-- walk [] = [(g,0)]
-- walk ((b,e):ss) =
-- [ (b'', e + r) | (b',r) <- cs, let b'' = b' .&! fromBExp b, b'' /= bot]
-- ++ [ (b'', r) | (b',r) <- cs, let b'' = b' .&! neg' (fromBExp b), b'' /= bot]
-- -- ++ [ (b'', r) | (b',r) <- cs, let b'' = debug "res" $ debug "b1" b' .&! debug "b2" (neg' (fromBExp b)), b'' /= bot]
-- where cs = walk ss
-- -- eliminateFrac :: Num a => Constraint (NormPoly c) (E.Frac a) -> [Constraint a a]
-- eliminateFrac :: (Eq c, Num c) => Constraint (C.NormPoly c) (C.NormPolyFrac c) -> [Constraint (C.NormPoly c) (C.NormPoly c)]
-- eliminateFrac (GEQ g l (n C.:% d)) = [GEQ g (l * d) n]
-- concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
-- concatMapM f xs = fmap concat (mapM f xs)
-- eliminateNorm :: [Constraint (C.NormPoly SmtExpression) (C.NormPoly SmtExpression)] -> SmtM [Constraint SmtPoly SmtPoly]
-- eliminateNorm = concatMapM $ \ (GEQ g l r) -> framed $ map toConstr <$> walkPoly g (P.toMonos (l - r))
-- where
......@@ -389,10 +379,10 @@ upperInvariant s UpperInvariant{..} = do
let
f = applyTemplate qs [ fmap acoeff (C.guarded b (C.E n)) | (C.GExp b n) <- limt]
g = C.cond cnd (encode cost `C.plus` applyTemplate qs (encode `map` step)) (encode cont)
initial = GEQ (fromBExp inv) f g
initial = debug "initial" (GEQ (fromBExp inv) f g)
-- ++ maybe [] (\ u -> [GEQ (fromBExp inv) u f]) ub
-- standard = debug "standardized" [GEQ b (l - r) 0 | (GEQ b l r) <- fracFree]
cs <- reduce initial
cs <- debug "final" <$> reduce initial
checkWithSolver s
-- checkWithOptSolver qs s
(\ i -> assertConstraintSmt i `mapM_` cs)
......
src/PWhile/Testbed/Examples.hs
View file @ 19796374
......@@ -861,11 +861,11 @@ whileWithExpression = do
geo = do
b <- var "b"; x <- var "x"
assume (x .>= 0) $ do
while' (b .== 1) $ do
consume x
b .~ rand 2;
b <- var "b"
b .= 1
while' (b .> 0) $ do
consume 1;
b .~ rand 2;
-- x .= x * 2;
......
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