Add --smt-arg to kore (#4025)

Fixes #4024

---------

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

Author: goodlyrottenapple

booster/tools/booster/Server.hs

@@ -486,6 +486,7 @@ translateSMTOpts = \case
             , retryLimit =
                 KoreSMT.RetryLimit . maybe Unlimited (Limit . fromIntegral) $ smtOpts.retryLimit
             , tactic = fmap translateSExpr smtOpts.tactic
+            , args = smtOpts.args
             }
     Nothing ->
         defaultKoreSolverOptions{solver = KoreSMT.None}
@@ -499,6 +500,7 @@ translateSMTOpts = \case
             , prelude = KoreSMT.Prelude Nothing
             , solver = KoreSMT.Z3
             , tactic = Nothing
+            , args = []
             }
     translateSExpr :: SMT.SExpr -> KoreSMT.SExpr
     translateSExpr (SMT.Atom (SMT.SMTId x)) = KoreSMT.Atom (Text.decodeUtf8 x)
@@ -533,7 +535,7 @@ mkKoreServer [email protected]{logAction} CLOptions{definitionFile, mainMo
                 , loggerEnv
                 }
   where
-    KoreSMT.KoreSolverOptions{timeOut, retryLimit, tactic} = koreSolverOptions
+    KoreSMT.KoreSolverOptions{timeOut, retryLimit, tactic, args} = koreSolverOptions
     smtConfig :: KoreSMT.Config
     smtConfig =
         KoreSMT.defaultConfig
@@ -542,6 +544,7 @@ mkKoreServer [email protected]{logAction} CLOptions{definitionFile, mainMo
               KoreSMT.timeOut = timeOut
             , KoreSMT.retryLimit = retryLimit
             , KoreSMT.tactic = tactic
+            , KoreSMT.arguments = args <> KoreSMT.defaultConfig.arguments
             }
 
     -- SMT solver with user declared lemmas

dev-tools/kore-rpc-dev/Server.hs

@@ -304,6 +304,7 @@ translateSMTOpts = \case
             , retryLimit =
                 KoreSMT.RetryLimit . maybe Unlimited (Limit . fromIntegral) $ smtOpts.retryLimit
             , tactic = fmap translateSExpr smtOpts.tactic
+            , args = smtOpts.args
             }
     Nothing ->
         defaultKoreSolverOptions{solver = KoreSMT.None}
@@ -317,6 +318,7 @@ translateSMTOpts = \case
             , prelude = KoreSMT.Prelude Nothing
             , solver = KoreSMT.Z3
             , tactic = Nothing
+            , args = []
             }
     translateSExpr :: SMT.SExpr -> KoreSMT.SExpr
     translateSExpr (SMT.Atom (SMT.SMTId x)) = KoreSMT.Atom (Text.decodeUtf8 x)

kore/app/share/GlobalMain.hs

@@ -188,6 +188,7 @@ import SMT (
     SMT,
  )
 import SMT qualified
+import SMT qualified as SMT.Config (Config (..))
 import System.Clock (
     Clock (Monotonic),
     diffTimeSpec,
@@ -581,14 +582,15 @@ execute options metadataTools lemmas worker =
             (declareSMTLemmas metadataTools lemmas)
             worker
     withoutSMT = SMT.runNoSMT worker
-    KoreSolverOptions{timeOut, rLimit, resetInterval, prelude, solver} =
+    KoreSolverOptions{timeOut, rLimit, resetInterval, prelude, solver, args} =
         options
     config =
         SMT.defaultConfig
             { SMT.timeOut = timeOut
             , SMT.rLimit = rLimit
             , SMT.resetInterval = resetInterval
             , SMT.prelude = prelude
+            , SMT.arguments = args <> SMT.Config.arguments SMT.defaultConfig
             }
 
 data SerializedDefinition = SerializedDefinition

kore/src/Options/SMT.hs

@@ -60,6 +60,7 @@ data KoreSolverOptions = KoreSolverOptions
     , prelude :: !Prelude
     , solver :: !Solver
     , tactic :: !(Maybe SExpr)
+    , args :: [String]
     }
 
 parseKoreSolverOptions :: Parser KoreSolverOptions
@@ -72,6 +73,7 @@ parseKoreSolverOptions =
         <*> parsePrelude
         <*> parseSolver
         <*> parseTactic
+        <*> parseArgs
   where
     parseTimeOut =
         option
@@ -128,6 +130,14 @@ parseKoreSolverOptions =
                 <> value defaultTactic
             )
 
+    parseArgs =
+        many $
+            strOption
+                ( metavar "SMT_ARG"
+                    <> long "smt-arg"
+                    <> help "Argument passed to Z3"
+                )
+
     SMT.Config
         { timeOut = defaultTimeOut
         , retryLimit = defaultRetryLimit