add support for bitwuzla #438
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
d-xo
commented
Jan 14, 2024
Comment on lines
+279
to
+288
| (readout, writeout) <- createPipe | ||
| let cmd | ||
| = (proc (show solver) (fmap T.unpack $ solverArgs solver timeout)) | ||
| { std_in = CreatePipe | ||
| , std_out = UseHandle writeout | ||
| , std_err = UseHandle writeout | ||
| } | ||
| (Just stdin, Nothing, Nothing, process) <- createProcess cmd | ||
| hSetBuffering stdin (BlockBuffering (Just 1000000)) | ||
| let solverInstance = SolverInstance solver stdin stdout stderr process | ||
| let solverInstance = SolverInstance solver stdin readout process |
There was a problem hiding this comment.
This sends stdout and stderr from the solvers into the same pipe so we can react to both when doing solver interaction...
zoep
reviewed
Jan 15, 2024
| @@ -160,11 +160,11 @@ declareIntermediates bufs stores = | |||
| where | |||
| compareFst (l, _) (r, _) = compare l r | |||
| encodeBuf n expr = | |||
| SMT2 ["(define-const buf" <> (fromString . show $ n) <> " Buf " <> exprToSMT expr <> ")\n"] mempty mempty mempty <> encodeBufLen n expr | |||
| SMT2 ["(define-fun buf" <> (fromString . show $ n) <> "() Buf " <> exprToSMT expr <> ")\n"] mempty mempty mempty <> encodeBufLen n expr | |||
There was a problem hiding this comment.
Why fun and not const? Is this bitwuzla related?
There was a problem hiding this comment.
yeah, bitwuzla doesn't support define-const, and it's just a macro around define-fun
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
Adds support for Bitwuzla. This is the same as the old PR, but uses a new bitwuzla version (0.3.0), which has support for timeouts This pr also messes with the smt generation less (only real change is replacing
define-constwithdefine-fun).It currently can't pass the full test suite (currently 9 failures due to issues support for comparison of constant arrays), but I enabled it for a few tests where it doesn't error out to make sure we're exercising it in CI.
Checklist