Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Booster: Only check SMT prelude in initSolver #4040

Merged
merged 4 commits into from
Aug 19, 2024
Merged

Booster: Only check SMT prelude in initSolver #4040

Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
1ce2995
Don't check prelude
geo2a Aug 14, 2024
e470b21
Check SMT prelude consistency when initialising solver
geo2a Aug 19, 2024
a667a9e
Do not run the command the second time
geo2a Aug 19, 2024
63b1c51
kore-rpc-client: ignore model when comparing GetModel results
geo2a Aug 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 20 additions & 12 deletions booster/library/Booster/SMT/Interface.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,7 @@ import Booster.SMT.Base as SMT
import Booster.SMT.Runner as SMT
import Booster.SMT.Translate as SMT
import Booster.Syntax.Json.Externalise (externaliseTerm)
import Booster.Util (Flag (..))

data SMTError
= GeneralSMTError Text
Expand Down Expand Up @@ -98,7 +99,7 @@ initSolver def smtOptions = Log.withContext Log.CtxSMT $ do
Log.logMessage ("Starting new SMT solver" :: Text)
ctxt <- mkContext smtOptions prelude

evalSMT ctxt checkPrelude
evalSMT ctxt (runPrelude CheckSMTPrelude)
Log.logMessage ("Successfully initialised SMT solver with " <> (Text.pack . show $ smtOptions))
pure ctxt

Expand Down Expand Up @@ -130,7 +131,7 @@ hardResetSolver = do
liftIO $ do
writeIORef solverRef solver
writeIORef ctxt.solverClose $ Backend.close handle
checkPrelude
runPrelude NoCheckSMTPrelude

-- | Retry the action `cb`, first decreasing the retry counter and increasing the timeout limit, unless the retry limit has already been reached, in which case call `onTimeout`
retry :: Log.LoggerMIO io => SMT io a -> SMT io a -> SMT io a
Expand All @@ -155,21 +156,28 @@ translatePrelude def =
throwSMT $ "Unable to translate elements of the definition to SMT: " <> err
Right decls -> pure decls

checkPrelude :: Log.LoggerMIO io => SMT io ()
checkPrelude = do
pattern CheckSMTPrelude, NoCheckSMTPrelude :: Flag "CheckSMTPrelude"
pattern CheckSMTPrelude = Flag True
pattern NoCheckSMTPrelude = Flag False

runPrelude :: Log.LoggerMIO io => Flag "CheckSMTPrelude" -> SMT io ()
runPrelude doCheck = do
ctxt <- SMT get
-- set the user defined timeout for queries
setTimeout ctxt.options.timeout
Log.logMessage ("Checking definition prelude" :: Text)
-- send the commands from the definition's SMT prelude
check <- mapM_ runCmd ctxt.prelude >> runCmd CheckSat
case check of
Sat -> pure ()
other -> do
Log.logMessage $ "Initial SMT definition check returned " <> pack (show other)
closeContext ctxt
throwSMT' $
"Aborting due to potentially-inconsistent SMT setup: Initial check returned " <> show other
mapM_ runCmd ctxt.prelude
-- optionally check the prelude for consistency
when (coerce doCheck) $ do
check <- mapM_ runCmd ctxt.prelude >> runCmd CheckSat
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

you are running mapM_ runCmd ctxt.prelude twice when doCheck is true.

Suggested change
mapM_ runCmd ctxt.prelude
-- optionally check the prelude for consistency
when (coerce doCheck) $ do
check <- mapM_ runCmd ctxt.prelude >> runCmd CheckSat
mapM_ runCmd ctxt.prelude
-- optionally check the prelude for consistency
when (coerce doCheck) $ do
check <- runCmd CheckSat

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oops, good catch!

case check of
Sat -> pure ()
other -> do
Log.logMessage $ "Initial SMT definition check returned " <> pack (show other)
closeContext ctxt
throwSMT' $
"Aborting due to potentially-inconsistent SMT setup: Initial check returned " <> show other
where
setTimeout timeout = do
Log.logMessage $ "Setting SMT timeout to: " <> show timeout
Expand Down
Loading