Booster: Only check SMT prelude in initSolver (#4040)

Fixes #4036
runtimeverification · Aug 19, 2024 · aa22475 · aa22475
1 parent f1d156f
commit aa22475
Show file tree

Hide file tree

Showing 2 changed files with 27 additions and 12 deletions.
diff --git a/booster/library/Booster/JsonRpc/Utils.hs b/booster/library/Booster/JsonRpc/Utils.hs
@@ -52,6 +52,10 @@ diffJson file1 file2 =
         -- useful when comparing responses of `kore-rpc` and `kore-rpc-booster`
         (contents1@(RpcResponse (Execute res1)), RpcResponse (Execute res2))
             | sameModuloBranchOrder res1 res2 -> Identical $ rpcTypeOf contents1
+        -- special case for GetModel results: only compare the satisfiable fields,
+        -- ignore variable assignments if present
+        (contents1@(RpcResponse (GetModel res1)), RpcResponse (GetModel res2))
+            | sameModuloModel res1 res2 -> Identical $ rpcTypeOf contents1
         (contents1, contents2)
             | contents1 == contents2 ->
                 Identical $ rpcTypeOf contents1
@@ -78,6 +82,9 @@ diffJson file1 file2 =
                 _ -> False
         | otherwise = False
 
+    sameModuloModel :: GetModelResult -> GetModelResult -> Bool
+    sameModuloModel res1 res2 = res1.satisfiable == res2.satisfiable
+
 data DiffResult
     = Identical KoreRpcType
     | DifferentType KoreRpcType KoreRpcType

diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs
@@ -57,6 +57,7 @@ import Booster.SMT.Base as SMT
 import Booster.SMT.Runner as SMT
 import Booster.SMT.Translate as SMT
 import Booster.Syntax.Json.Externalise (externaliseTerm)
+import Booster.Util (Flag (..))
 
 data SMTError
     = GeneralSMTError Text
@@ -98,7 +99,7 @@ initSolver def smtOptions = Log.withContext Log.CtxSMT $ do
     Log.logMessage ("Starting new SMT solver" :: Text)
     ctxt <- mkContext smtOptions prelude
 
-    evalSMT ctxt checkPrelude
+    evalSMT ctxt (runPrelude CheckSMTPrelude)
     Log.logMessage ("Successfully initialised SMT solver with " <> (Text.pack . show $ smtOptions))
     pure ctxt
 
@@ -130,7 +131,7 @@ hardResetSolver = do
             liftIO $ do
                 writeIORef solverRef solver
                 writeIORef ctxt.solverClose $ Backend.close handle
-            checkPrelude
+            runPrelude NoCheckSMTPrelude
 
 -- | Retry the action `cb`, first decreasing the retry counter and increasing the timeout limit, unless the retry limit has already been reached, in which case call `onTimeout`
 retry :: Log.LoggerMIO io => SMT io a -> SMT io a -> SMT io a
@@ -155,21 +156,28 @@ translatePrelude def =
                 throwSMT $ "Unable to translate elements of the definition to SMT: " <> err
             Right decls -> pure decls
 
-checkPrelude :: Log.LoggerMIO io => SMT io ()
-checkPrelude = do
+pattern CheckSMTPrelude, NoCheckSMTPrelude :: Flag "CheckSMTPrelude"
+pattern CheckSMTPrelude = Flag True
+pattern NoCheckSMTPrelude = Flag False
+
+runPrelude :: Log.LoggerMIO io => Flag "CheckSMTPrelude" -> SMT io ()
+runPrelude doCheck = do
     ctxt <- SMT get
     -- set the user defined timeout for queries
     setTimeout ctxt.options.timeout
     Log.logMessage ("Checking definition prelude" :: Text)
     -- send the commands from the definition's SMT prelude
-    check <- mapM_ runCmd ctxt.prelude >> runCmd CheckSat
-    case check of
-        Sat -> pure ()
-        other -> do
-            Log.logMessage $ "Initial SMT definition check returned " <> pack (show other)
-            closeContext ctxt
-            throwSMT' $
-                "Aborting due to potentially-inconsistent SMT setup: Initial check returned " <> show other
+    mapM_ runCmd ctxt.prelude
+    -- optionally check the prelude for consistency
+    when (coerce doCheck) $ do
+        check <- runCmd CheckSat
+        case check of
+            Sat -> pure ()
+            other -> do
+                Log.logMessage $ "Initial SMT definition check returned " <> pack (show other)
+                closeContext ctxt
+                throwSMT' $
+                    "Aborting due to potentially-inconsistent SMT setup: Initial check returned " <> show other
   where
     setTimeout timeout = do
         Log.logMessage $ "Setting SMT timeout to: " <> show timeout