Commit 3a92ec28 authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

fixed preliminary abort in constraint reduction

parent 4d6dcf7d
......@@ -294,20 +294,17 @@ reduce :: Constraint AExp -> SmtM [Constraint SmtPoly]
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]
return [GEQ ctx'' lhs' rhs']))
return [GEQ g (f2' * l) (f1' * r) | GEQ g l r <- cs, r /= 0]
where
(_,(f1',f2')) = E.factor f1 f2
branch (fromBExp -> g) m c1 c2 ctx k =
entailsSmtK 1 ctx g $ \ entailed ->
if entailed
then m c1 ctx k
then debugPA (PP.pretty ctx <> PP.text "=>" <> PP.pretty g) =<< m c1 (ctx .&! g) k
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
then debugPA (PP.pretty ctx <> PP.text "=>" <> PP.pretty (neg' g)) =<< m c2 (ctx .&! neg' g) k
else (++) <$> m c1 (ctx .&! g) k
<*> m c2 (ctx .&! neg' g) k
......@@ -327,7 +324,7 @@ reduce (GEQ c (toFrac -> (lhs,f1)) (toFrac -> (rhs,f2))) = do
walkLhs C.Sup {} _ _ = error "InvariantSolver.Naive.reduce: sup on lhs"
walkRhs _ Bot _ = return []
walkRhs (C.E 0) _ _ = 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
......@@ -369,9 +366,12 @@ reduce (GEQ c (toFrac -> (lhs,f1)) (toFrac -> (rhs,f2))) = do
-- normalise :: (Num c1, Num c2, Eq c1, Eq c2) => Constraint (P.Polynomial v1 c1) (P.Polynomial v2 c2) -> [Constraint (P.Polynomial v1 c1) (P.Polynomial v2 c2)]
-- normalise (GEQ g l r) = [GEQ g (P.norm l) (P.norm r)]
debug :: (PP.Pretty e) => String -> e -> e
debug :: PP.Pretty e => String -> e -> e
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
......
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