further entailment checks

src/PWhile/InvariantSolver/Naive.hs

@@ -239,18 +239,23 @@ handelman deg = eqCoefficientsWith $
 
 assertEntailSmt :: Int -> DNF SmtLit -> SmtLit -> SmtM ()
 -- assertEntailSmt i (Disj cs) p = forM_ cs $ \c -> SMT.assert =<< handelman i c p
-assertEntailSmt i ctx@(Disj cs) p = forM_ cs entailConj
+assertEntailSmt i (Disj cs) p = forM_ cs assertEntailConj
   where
-    entailConj c
-      | p `S.member` litsSet c = return ()
-      | otherwise              = SMT.assert =<< handelman i c p
-    -- d p = debug (show (PP.pretty ctx PP.<> PP.text " |- " PP.<> PP.pretty p)) p
+    assertEntailConj c
+      | d entailed = return ()
+      | otherwise = SMT.assert =<< handelman i c p
+      where
+        entailed = p == TT || p `S.member` litsSet c || any (`entailLit` p) c
+    Geq0 eq `entailLit` Geq0 ep
+      | E.Constant (E.Constant n) <- ep - eq = n >= 0
+    _       `entailLit` _                    = False
+    d = debug (show (PP.pretty (Disj cs) PP.<> PP.text " |- " PP.<> PP.pretty p))
 
 assertConstraintSmt :: Int -> Constraint SmtPoly -> SmtM ()
 assertConstraintSmt i (GEQ g l r) = assertEntailSmt i g (l `geqLit` r)
 
-entailsSmtK :: PP.Pretty a => Int -> DNF SmtLit -> DNF SmtLit -> (Bool -> SmtM a) -> SmtM a
-entailsSmtK i p c k = anySatM (conjs c)
+entailsSmtK :: PP.Pretty a => DNF SmtLit -> DNF SmtLit -> (Bool -> SmtM a) -> SmtM a
+entailsSmtK p c k = anySatM (conjs c)
   where
     anySatM []       = k False
     anySatM (cs:css) = do
@@ -261,7 +266,7 @@ entailsSmtK i p c k = anySatM (conjs c)
     allSatM ls = forM ls (ent p) *> SMT.checkSat
 
   -- TODO: add syntactic checks and possibly assert
-    ent = assertEntailSmt i
+    ent = assertEntailSmt 1
 
 -- elimination of cost expression
 ----------------------------------------------------------------------
@@ -293,10 +298,10 @@ reduce (GEQ c (toFrac -> (lhs,f1)) (toFrac -> (rhs,f2))) = do
     (_,(f1',f2')) = E.factor f1 f2
 
     branch (fromBExp -> g) m1 m2 ctx k =
-      entailsSmtK 1 ctx g $ \ entailed ->
+      entailsSmtK ctx g $ \ entailed ->
       if entailed
       then m1 (ctx .&! g) k -- debugPA (PP.pretty ctx <> PP.text "=>" <> PP.pretty g) =<<
-      else entailsSmtK 1 ctx (neg' g) $ \ negEntailed ->
+      else entailsSmtK ctx (neg' g) $ \ negEntailed ->
         if negEntailed
         then m2 (ctx .&! neg' g) k -- debugPA (PP.pretty ctx <> PP.text "=>" <> PP.pretty (neg' g)) =<<
         else (++) <$> m1 (ctx .&! g) k