merge origin

runtimeverification · Aug 16, 2024 · 9e4a8d2 · 9e4a8d2
2 parents 743d5f8 + 02ed613
commit 9e4a8d2
Show file tree

Hide file tree

Showing 6 changed files with 42 additions and 9 deletions.
diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs
@@ -215,8 +215,15 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi
                     variableSort <- lookupInternalSort sortVars definition.sorts p sort
                     let variableName = textToBS var.getId
                     pure $ Internal.Variable{variableSort, variableName}
-                (term, preds, ceilConditions, subst, unknown) <- internalisePattern allowAlias checkSubsorts sortVars definition p
-                pure $ IsPattern (existentialVars, Internal.Pattern{term,constraints = Set.fromList preds, ceilConditions}, subst, unknown)
+                (term, preds, ceilConditions, subst, unknown) <-
+                    internalisePattern allowAlias checkSubsorts sortVars definition p
+                pure $
+                    IsPattern $
+                        ( existentialVars
+                        , Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions}
+                        , subst
+                        , unknown
+                        )
   where
     isTop = \case
         [Syntax.KJTop{sort}] -> Just $ IsTop sort

diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs
@@ -878,7 +878,12 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do
             | v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v
             | otherwise = Util.modifyVarName Util.markAsRuleVar v
     (rhs, ensures) <-
-        internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDefinition ref Nothing renameVariable right
+        internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported
+            partialDefinition
+            ref
+            Nothing
+            renameVariable
+            right
     let notPreservesDefinednessReasons =
             -- users can override the definedness computation by an explicit attribute
             if coerce axAttributes.preserving
@@ -937,7 +942,12 @@ internaliseRewriteRule partialDefinition exs aliasName aliasArgs right axAttribu
             | v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v
             | otherwise = Util.modifyVarName Util.markAsRuleVar v
     (rhs, ensures) <-
-        internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDefinition ref Nothing renameVariable right
+        internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported
+            partialDefinition
+            ref
+            Nothing
+            renameVariable
+            right
 
     let notPreservesDefinednessReasons =
             -- users can override the definedness computation by an explicit attribute
@@ -1007,8 +1017,8 @@ internaliseSimpleEquation partialDef precond left right sortVars attrs
                 partialDef
                 (sourceRef attrs)
                 (Just sortVars)
-                (Util.modifyVarName ("Eq#" <>)) $
-                Syntax.KJAnd left.sort [left, precond]
+                (Util.modifyVarName ("Eq#" <>))
+                $ Syntax.KJAnd left.sort [left, precond]
         (rhs, ensures) <-
             internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported
                 partialDef
@@ -1052,7 +1062,6 @@ internaliseSimpleEquation partialDef precond left right sortVars attrs
 removeTrueBools :: [Def.Term] -> [Def.Term]
 removeTrueBools = filter (/= TrueBool)
 
-
 internaliseCeil ::
     KoreDefinition -> -- context
     Syntax.KorePattern -> -- LHS of ceil

diff --git a/booster/tools/booster/Server.hs b/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

diff --git a/dev-tools/kore-rpc-dev/Server.hs b/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)

diff --git a/kore/app/share/GlobalMain.hs b/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

diff --git a/kore/src/Options/SMT.hs b/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