Support CVC5 #1503
Labels
feature request
Asking for new or improved functionality
Comments
RyanGlScott
added a commit
that referenced
this issue
Feb 27, 2023
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.
Merged
RyanGlScott
added a commit
that referenced
this issue
Feb 27, 2023
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.
RyanGlScott
added a commit
that referenced
this issue
Feb 27, 2023
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.
RyanGlScott
added a commit
that referenced
this issue
Feb 28, 2023
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.
RyanGlScott
added a commit
that referenced
this issue
Feb 28, 2023
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.
RyanGlScott
added a commit
that referenced
this issue
Mar 6, 2023
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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Cryptol uses
what-1.4as of #1499, which means that Cryptol now has everything that it needs to support CVC5 as a solver backend, both on the What4 and SBV sides. We should add them.The text was updated successfully, but these errors were encountered: