Pass args to the smt solver via --smt-arg (#4021)

This change will let us call `z3` with `smt.ematching=false` in booster,
which seems to help with non-linear arithmetic.

---------

Co-authored-by: Jost Berthold <[email protected]>

Author: goodlyrottenapple

booster/library/Booster/CLOptions.hs

@@ -361,6 +361,15 @@ parseSMTOptions =
                                 \Example: '(check-sat-using smt)' (i.e., plain 'check-sat')"
                         )
                     )
+                <*> many
+                    ( strOption
+                        ( metavar "SMT_ARG"
+                            <> long "smt-arg"
+                            <> help
+                                ( "Arguments to be passed to the SMT solver process"
+                                )
+                        )
+                    )
             )
   where
     smtDefaults = defaultSMTOptions

booster/library/Booster/SMT/Interface.hs

@@ -126,7 +126,7 @@ hardResetSolver = do
         Just solverRef -> do
             closeContext ctxt
             Log.logMessage ("Restarting SMT solver" :: Text)
-            (solver, handle) <- connectToSolver
+            (solver, handle) <- connectToSolver ctxt.options.args
             liftIO $ do
                 writeIORef solverRef solver
                 writeIORef ctxt.solverClose $ Backend.close handle

booster/library/Booster/SMT/Runner.hs

@@ -60,6 +60,7 @@ data SMTOptions = SMTOptions
     -- ^ optional retry. Nothing for no retry, 0 for unlimited
     , tactic :: Maybe SExpr
     -- ^ optional tactic (used verbatim) to replace (check-sat)
+    , args :: [String]
     }
     deriving (Eq, Show)
 
@@ -70,6 +71,7 @@ defaultSMTOptions =
         , timeout = 125
         , retryLimit = Just 3
         , tactic = Nothing
+        , args = []
         }
 
 data SMTContext = SMTContext
@@ -97,7 +99,7 @@ mkContext ::
     io SMTContext
 mkContext opts prelude = do
     logMessage ("Starting SMT solver" :: Text)
-    (solver', handle) <- connectToSolver
+    (solver', handle) <- connectToSolver opts.args
     solver <- liftIO $ newIORef solver'
     solverClose <- liftIO $ newIORef $ Backend.close handle
     mbTranscriptHandle <- forM opts.transcript $ \path -> do
@@ -141,9 +143,9 @@ destroyContext ctxt = do
         hClose h
     liftIO $ join $ readIORef ctxt.solverClose
 
-connectToSolver :: LoggerMIO io => io (Backend.Solver, Backend.Handle)
-connectToSolver = do
-    let config = Backend.defaultConfig
+connectToSolver :: LoggerMIO io => [String] -> io (Backend.Solver, Backend.Handle)
+connectToSolver args = do
+    let config = Backend.defaultConfig{Backend.args = args <> Backend.defaultConfig.args}
     handle <- liftIO $ Backend.new config
     solver <- liftIO $ Backend.initSolver Backend.Queuing $ Backend.toBackend handle
     pure (solver, handle)