Retry SMT queries in Booster when deciding predicates (#3889)

Fixes #3884 

- refactor the SMT modules to allow re-initializing the solver
dynamically:
  - `SMTContext` now carries the prelude and `SMTOptions`
- the `closeContext` function only closes the solver handle, and does
not close the solver transcript handle. The new `destroyContext`
function does both.
- The `SMT` monad is is changed to have `StateT SMTContext`. The
`Booster.SMT.Interface.restartSolver` function restarts the solver with
modified options, altering the context. Note that it does not touch the
transcript handle, i.e. it will persist the sovler restarts.

- the `getModelFor` and `checkPredicates` functions now have logic to
retry with doubled timeout when the solver returns unknown.

I'm checking-in the integration test that I was using when developing. I
ran the server with `--smt-timeout 1` to observe the retry mechanism
kicking-in, but I do not think it is a good idea to try to force it to
retry the queries in CI. The test may still be useful when working on
the SMT code in future.

---------

Co-authored-by: github-actions <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

Author: 3 people

booster/library/Booster/JsonRpc.hs

@@ -17,6 +17,7 @@ module Booster.JsonRpc (
 
 import Control.Applicative ((<|>))
 import Control.Concurrent (MVar, putMVar, readMVar, takeMVar)
+import Control.Exception qualified as Exception
 import Control.Monad
 import Control.Monad.Extra (whenJust)
 import Control.Monad.IO.Class
@@ -148,7 +149,7 @@ respond stateVar =
                     solver <- traverse (SMT.initSolver def) mSMTOptions
                     result <-
                         performRewrite doTracing def mLlvmLibrary solver mbDepth cutPoints terminals substPat
-                    whenJust solver SMT.closeSolver
+                    whenJust solver SMT.finaliseSolver
                     stop <- liftIO $ getTime Monotonic
                     let duration =
                             if fromMaybe False req.logTiming
@@ -309,7 +310,7 @@ respond stateVar =
                                         pure $ Right (addHeader $ Syntax.KJAnd predicateSort result)
                                     (Left something, _) ->
                                         pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty something
-            whenJust solver SMT.closeSolver
+            whenJust solver SMT.finaliseSolver
             stop <- liftIO $ getTime Monotonic
 
             let duration =
@@ -389,12 +390,12 @@ respond stateVar =
                                         "No predicates or substitutions given, returning Unknown"
                                     pure $ Left SMT.Unknown
                                 else do
-                                    solver <-
-                                        SMT.initSolver def smtOptions
-                                    smtResult <-
-                                        SMT.getModelFor solver boolPs suppliedSubst
-                                    SMT.closeSolver solver
-                                    pure smtResult
+                                    solver <- SMT.initSolver def smtOptions
+                                    result <- SMT.getModelFor solver boolPs suppliedSubst
+                                    SMT.finaliseSolver solver
+                                    case result of
+                                        Left err -> liftIO $ Exception.throw err -- fail hard on SMT errors
+                                        Right response -> pure response
                         Log.logOtherNS "booster" (Log.LevelOther "SMT") $
                             "SMT result: " <> pack (either show (("Subst: " <>) . show . Map.size) smtResult)
                         pure . Right . RpcTypes.GetModel $ case smtResult of
@@ -573,7 +574,7 @@ handleSmtError = JsonRpcHandler $ \case
     SMT.GeneralSMTError err -> runtimeError "problem" err
     SMT.SMTTranslationError err -> runtimeError "translation" err
     SMT.SMTSolverUnknown reason premises preds -> do
-        Log.logErrorNS "booster" "SMT returned `Unknown'"
+        Log.logErrorNS "booster" ("SMT returned `Unknown' with reason " <> reason)
 
         let bool = externaliseSort Pattern.SortBool -- predicates are terms of sort Bool
             externalise = Syntax.KJAnd bool . map (externalisePredicate bool) . Set.toList