🔀 Merge pull request #52 from lsrcz/fix-cegis-empty-inputs

Make cegis work like solve when no symbolic input is present
lsrcz · Feb 14, 2023 · eb30abd · eb30abd
2 parents a606a9a + 8a86e75
commit eb30abd
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 11 deletions.
diff --git a/src/Grisette/Backend/SBV/Data/SMT/Solving.hs b/src/Grisette/Backend/SBV/Data/SMT/Solving.hs
@@ -331,17 +331,22 @@ instance CEGISSolver (GrisetteSMTConfig n) SolvingFailure where
     (inputs -> CEGISCondition) ->
     IO ([inputs], Either SolvingFailure PM.Model)
   cegisMultiInputs config inputs func =
-    handle
-      ( \(x :: SBV.SBVException) -> do
-          print "An SBV Exception occurred:"
-          print x
-          print $
-            "Warning: Note that CEGIS procedures do not fully support "
-              ++ "timeouts, and will return an empty counter example list if "
-              ++ "the solver timeouts during guessing phase."
-          return ([], Left $ SolvingError x)
-      )
-      $ go1 (cexesAssertFun conInputs) conInputs (error "Should have at least one gen") [] (con True) (con True) symInputs
+    case symInputs of
+      [] -> do
+        m <- solve config (cexesAssertFun conInputs)
+        return (conInputs, m)
+      _ ->
+        handle
+          ( \(x :: SBV.SBVException) -> do
+              print "An SBV Exception occurred:"
+              print x
+              print $
+                "Warning: Note that CEGIS procedures do not fully support "
+                  ++ "timeouts, and will return an empty counter example list if "
+                  ++ "the solver timeouts during guessing phase."
+              return ([], Left $ SolvingError x)
+          )
+          $ go1 (cexesAssertFun conInputs) conInputs (error "Should have at least one gen") [] (con True) (con True) symInputs
     where
       (conInputs, symInputs) = partition (isEmptySet . extractSymbolics) inputs
       go1 :: SymBool -> [inputs] -> PM.Model -> [inputs] -> SymBool -> SymBool -> [inputs] -> IO ([inputs], Either SolvingFailure PM.Model)

diff --git a/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs b/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs
@@ -9,6 +9,8 @@ import Control.Monad.Except
 import qualified Data.HashSet as S
 import Data.Proxy
 import qualified Data.SBV as SBV
+import Data.String
+import Grisette.Backend.SBV
 import Grisette.Backend.SBV.Data.SMT.Solving
 import Grisette.Core.Control.Exception
 import Grisette.Core.Control.Monad.UnionM
@@ -64,6 +66,13 @@ cegisTests =
    in testGroup
         "CEGISTests"
         [ testGroup
+            "Regression"
+            [ testCase "Empty symbolic inputs makes cegis work like solve" $ do
+                (_, Right m1) <- cegisMultiInputs (precise z3) [1 :: Integer, 2] (\x -> cegisPostCond $ fromString $ "a" ++ show x)
+                Right m2 <- solve (precise z3) (ssym "a1" &&~ ssym "a2")
+                m1 @=? m2
+            ],
+          testGroup
             "Boolean"
             [ testCase "Basic" $ do
                 testCegis