-
Notifications
You must be signed in to change notification settings - Fork 126
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.
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
Add CVC5 support #1504
Add CVC5 support #1504
Conversation
fc33cbd
to
957450c
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Someday it would be nice to unify all those solver snapshot references into a single location. Somehow.
I think I've set up everything correctly, but the
Ugh. I will see if I can reproduce this locally. |
I was able to reproduce this locally. The hang happens when running the I'm not quite sure what to do about this in the mean time. Should we remove |
My vote would be to leave it in and note the issue: I doubt we'll have immediate engagement on cvc5 such that it's worth the effort to remove it now and re-add it later. Assuming you can easily add a CI bypass, that is. |
I have good news and bad news. The good news is that the underlying issue in CVC5 (cvc5/cvc5#8900) has already been fixed upstream. I have no idea when we can expect a new CVC5 release with this fix, but I'm inclined to backport the bugfix to the version of CVC5 that we include in The bad news is that we still haven't quite figured out what causes SBV to go into an infinite loop when using CVC5 on Windows. I discovered in LeventErkok/sbv#644 (comment) two things:
|
Argh, except it isn't that simple. The problem is that In the meantime, I will simply comment out the part of the test case that tests |
This patch: * Makes the necessary changes on the `cryptol` and `cryptol-remote-api` side needed add `cvc5`, `w4-cvc5`, and `sbv-cvc5` solvers. This requires SBV 9.1 or later to include the changes from LeventErkok/sbv#630, which re-exports CVC5-related functionality from all of the places that Cryptol imports from. * Adds a test case to ensure that basic CVC5 support works. * Updates the CI and Dockerfile to ensure that CVC5 is included from the `what4-solvers` bindists. Fixes #1503.
The previous version (`snapshot-20220812`) was using CVC5 1.0.1, which is too old to work properly with `what4`. I have bumped the version to `snapshot-20221212`, which includes CVC5 1.0.2.
The main payload of this commit is to bump the `what4` submodule to bring in the changes from GaloisInc/what4#204. This also brings in a variety of other submodule changes to accommodate this: * GaloisIns/crucible#1068, which ensures that everything can build against `tasty-sugar >= 2.0` (the version of the library that `what4-1.4` depends on). * GaloisInc/cryptol#1504, which adapts Cryptol to CVC5. This adjusts the lower and upper version bounds on SBV in Cryptol, so I do the same here in `saw-core.sbv.cabal` and `saw-script.cabal`. * GaloisInc/language-sally#12, which performs a similar `what4` adaptation. * GaloisInc/macaw#328, which performs a similar `what4` adaptation.
This patch:
cryptol
andcryptol-remote-api
side needed addcvc5
,w4-cvc5
, andsbv-cvc5
solvers. This requires SBV 9.1 or later to include the changes from Consistently export solvers fromData.SBV.{Dynamic,Trans}
LeventErkok/sbv#630, which re-exports CVC5-related functionality from all of the places that Cryptol imports from.what4-solvers
bindists.Fixes #1503.