From 2faf6c1d71de054f4630e3489efb4631a0f320b5 Mon Sep 17 00:00:00 2001 From: Samuel Balco Date: Thu, 15 Aug 2024 16:02:11 +0100 Subject: [PATCH 1/2] Add `--smt-arg` to kore (#4025) Fixes #4024 --------- Co-authored-by: rv-jenkins --- booster/tools/booster/Server.hs | 5 ++++- dev-tools/kore-rpc-dev/Server.hs | 2 ++ kore/app/share/GlobalMain.hs | 4 +++- kore/src/Options/SMT.hs | 10 ++++++++++ 4 files changed, 19 insertions(+), 2 deletions(-) diff --git a/booster/tools/booster/Server.hs b/booster/tools/booster/Server.hs index 32cbd99e93..c007532e94 100644 --- 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 loggerEnv@Log.LoggerEnv{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 loggerEnv@Log.LoggerEnv{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 index 54856280cf..84a8ebf2b7 100644 --- 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 index 8da152ac4a..d29f5f8c1d 100644 --- 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,7 +582,7 @@ 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 @@ -589,6 +590,7 @@ execute options metadataTools lemmas worker = , 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 index 615ee3dad7..4319e05e10 100644 --- 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 From 02ed6136e334433f0d3cc8939f646f02324d3137 Mon Sep 17 00:00:00 2001 From: github-actions Date: Thu, 15 Aug 2024 15:07:17 +0000 Subject: [PATCH 2/2] Format with fourmolu --- .../library/Booster/Syntax/Json/Internalise.hs | 11 +++++++++-- .../Booster/Syntax/ParsedKore/Internalise.hs | 18 ++++++++++++++---- 2 files changed, 23 insertions(+), 6 deletions(-) diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index ad52f701fe..5c375bb535 100644 --- 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 index 3aef3fe334..4bd05808b0 100644 --- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -877,7 +877,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 @@ -936,7 +941,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 @@ -1006,8 +1016,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