Add a solver adapter for bitwuzla #124
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
|
SBV now also supports Bitwuzla as of 8.17: https://hackage.haskell.org/package/sbv-8.17/changelog |
|
@travitch, any reason not to just merge this? Obviously, it's better to have testing set up, but I'm not sure leaving this unmerged is better. |
|
Sorry - it isn't actually working yet. Either some quirks required or... something. I remember getting some syntax errors from it |
|
OK, answers that question. I'll leave it alone for now. |
RyanGlScott
reviewed
Jan 18, 2022
RyanGlScott
added a commit
to GaloisInc/flakes
that referenced
this pull request
Jan 24, 2022
Nixpkgs currently contains bitwuzla-unstable-2021-07-01, so add it here. This will likely be useful for things like GaloisInc/what4#124.
RyanGlScott
force-pushed
the
tr/bitwuzla-adapter
branch
from
1e4929d to
59698a7
Compare
Bitwuzla is a relatively new SMT solver with support for the bitvector, floating point, array, and uninterpreted function theories. This patch adds the necessary plumbing to invoke Bitwuzla using What4. Co-authored-by: Ryan Scott <[email protected]>
RyanGlScott
force-pushed
the
tr/bitwuzla-adapter
branch
from
59698a7 to
d515e14
Compare
This was removed from the `flakes` repo in GaloisInc/flakes#7. The rationale is that odd Yices version numbers are development versions, and we only want to test release versions. `what4`'s CI was testing 2.6.1 (a development version), so let's just remove it.
kquick
approved these changes
Jan 12, 2024
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.
Bitwuzla is a relatively new SMT solver with support for the bitvector, floating
point, array, and uninterpreted function theories.