Add CVC5 support

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.
GaloisInc · Feb 28, 2023 · fc33cbd · fc33cbd
1 parent 4c1c5fc
commit fc33cbd
Show file tree

Hide file tree

Showing 15 changed files with 39 additions and 9 deletions.
diff --git a/.github/ci.sh b/.github/ci.sh
@@ -77,7 +77,7 @@ install_system_deps() {
   cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT
   export PATH=$BIN:$PATH
   echo "$BIN" >> "$GITHUB_PATH"
-  is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" yices
+  is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" cvc5 && is_exe "$BIN" yices
 }
 
 check_docs() {
@@ -132,6 +132,7 @@ zip_dist_with_solvers() {
   sname="${name}-with-solvers"
   cp "$(which abc)"        dist/bin/
   cp "$(which cvc4)"       dist/bin/
+  cp "$(which cvc5)"       dist/bin/
   cp "$(which yices)"      dist/bin/
   cp "$(which yices-smt2)" dist/bin/
   cp "$(which z3)"         dist/bin/

diff --git a/CHANGES.md b/CHANGES.md
@@ -30,10 +30,14 @@
 * Add a syntax highlight file for Vim,
   available in `syntax-highlight/cryptol.vim`
 
-* Add `:new-seed` and `:set-seed` commands to the REPL. 
+* Add `:new-seed` and `:set-seed` commands to the REPL.
   These affect random test generation,
   and help write reproducable Cryptol scripts.
 
+* Add support for the CVC5 solver, which can be selected with
+  `:set prover=cvc5`. If you want to specify a What4 or SBV backend, you can
+  use `:set prover=w4-cvc5` or `:set prover=sbv-cvc5`, respectively.
+
 ## Bug fixes
 
 * Fix a bug in the What4 backend that could cause applications of `(@)` with

diff --git a/Dockerfile b/Dockerfile
@@ -40,6 +40,7 @@ ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH
 RUN    ! $(cryptol -c ":s prover=yices" | tail -n +2 | grep -q .) \
     #    && ! $(cryptol -c ":s prover=mathsat" | tail -n +2 | grep -q .) \
     && ! $(cryptol -c ":s prover=cvc4" | tail -n +2 | grep -q .) \
+    && ! $(cryptol -c ":s prover=cvc5" | tail -n +2 | grep -q .) \
     && ! $(cryptol -c ":s prover=abc" | tail -n +2 | grep -q .) \
     # && ! $(cryptol -c ":s prover=boolector" | tail -n +2 | grep -q .) \
     && ! $(cryptol -c ":s prover=z3" | tail -n +2 | grep -q .)

diff --git a/README.md b/README.md
@@ -25,7 +25,7 @@ predicates written in Cryptol against randomly-generated test vectors
 (in the style of
 [QuickCheck](http://hackage.haskell.org/package/QuickCheck)). There is
 also a `:prove` command, which calls out to SMT solvers, such as
-Yices, Z3, or CVC4, to prove predicates for all possible inputs.
+Yices, Z3, CVC4, or CVC5, to prove predicates for all possible inputs.
 
 # Getting Cryptol Binaries
 

diff --git a/cabal.GHC-8.10.7.config b/cabal.GHC-8.10.7.config
@@ -207,7 +207,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              s-cargot -build-example,
              any.safe ==0.3.19,
              any.safe-exceptions ==0.1.7.3,
-             any.sbv ==9.0,
+             any.sbv ==9.2,
              any.scientific ==0.3.7.0,
              scientific -bytestring-builder -integer-simple,
              any.scotty ==0.12.1,

diff --git a/cabal.GHC-9.2.4.config b/cabal.GHC-9.2.4.config
@@ -208,7 +208,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              s-cargot -build-example,
              any.safe ==0.3.19,
              any.safe-exceptions ==0.1.7.3,
-             any.sbv ==9.0,
+             any.sbv ==9.2,
              any.scientific ==0.3.7.0,
              scientific -bytestring-builder -integer-simple,
              any.scotty ==0.12.1,

diff --git a/cabal.GHC-9.4.4.config b/cabal.GHC-9.4.4.config
@@ -208,7 +208,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              s-cargot -build-example,
              any.safe ==0.3.19,
              any.safe-exceptions ==0.1.7.3,
-             any.sbv ==9.0,
+             any.sbv ==9.2,
              any.scientific ==0.3.7.0,
              scientific -bytestring-builder -integer-simple,
              any.scotty ==0.12.1,

diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst
@@ -557,7 +557,7 @@ Parameter fields
 
 
 ``prover``
-  The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any``, ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.
+  The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-cvc5``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any``, ``cvc4``, ``cvc5``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-cvc5``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.
 
 
 

diff --git a/cryptol-remote-api/python/cryptol/solver.py b/cryptol-remote-api/python/cryptol/solver.py
@@ -52,6 +52,7 @@ def without_hash_consing(self) -> 'OfflineSolver':
 # Cryptol-supported SMT configurations/solvers
 # (see Cryptol.Symbolic.SBV Haskell module)
 CVC4: OnlineSolver          = OnlineSolver("cvc4")
+CVC5: OnlineSolver          = OnlineSolver("cvc5")
 YICES: OnlineSolver         = OnlineSolver("yices")
 Z3: OnlineSolver            = OnlineSolver("z3")
 BOOLECTOR: OnlineSolver     = OnlineSolver("boolector")
@@ -60,6 +61,7 @@ def without_hash_consing(self) -> 'OfflineSolver':
 OFFLINE: OfflineSolver      = OfflineSolver("offline")
 ANY: OnlineSolver           = OnlineSolver("any")
 SBV_CVC4: OnlineSolver      = OnlineSolver("sbv-cvc4")
+SBV_CVC5: OnlineSolver      = OnlineSolver("sbv-cvc5")
 SBV_YICES: OnlineSolver     = OnlineSolver("sbv-yices")
 SBV_Z3: OnlineSolver        = OnlineSolver("sbv-z3")
 SBV_BOOLECTOR: OnlineSolver = OnlineSolver("sbv-boolector")
@@ -68,6 +70,7 @@ def without_hash_consing(self) -> 'OfflineSolver':
 SBV_OFFLINE: OfflineSolver  = OfflineSolver("sbv-offline")
 SBV_ANY: OnlineSolver       = OnlineSolver("sbv-any")
 W4_CVC4: OnlineSolver       = OnlineSolver("w4-cvc4")
+W4_CVC5: OnlineSolver       = OnlineSolver("w4-cvc5")
 W4_YICES: OnlineSolver      = OnlineSolver("w4-yices")
 W4_Z3: OnlineSolver         = OnlineSolver("w4-z3")
 W4_BOOLECTOR: OnlineSolver  = OnlineSolver("w4-boolector")

diff --git a/cryptol.cabal b/cryptol.cabal
@@ -73,7 +73,7 @@ library
                        pretty,
                        prettyprinter     >= 1.7.0,
                        process           >= 1.2,
-                       sbv               >= 8.10 && < 9.1,
+                       sbv               >= 9.1 && < 9.3,
                        simple-smt        >= 0.9.7,
                        stm               >= 2.4,
                        strict,

diff --git a/cryptol/Main.hs b/cryptol/Main.hs
@@ -200,7 +200,7 @@ displayHelp errs = do
             , "via the `:edit` command"
             ]
           )
-        , ( "SBV_{ABC,BOOLECTOR,CVC4,MATHSAT,YICES,Z3}_OPTIONS"
+        , ( "SBV_{ABC,BOOLECTOR,CVC4,CVC5,MATHSAT,YICES,Z3}_OPTIONS"
           , [ "A string of command-line arguments to be passed to the"
             , "corresponding solver invoked for `:sat` and `:prove`"
             , "when using a prover via SBV"

diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs
@@ -81,6 +81,7 @@ doSBVEval m =
 proverConfigs :: [(String, SBV.SMTConfig)]
 proverConfigs =
   [ ("cvc4"     , SBV.cvc4     )
+  , ("cvc5"     , SBV.cvc5     )
   , ("yices"    , SBV.yices    )
   , ("z3"       , SBV.z3       )
   , ("boolector", SBV.boolector)
@@ -90,6 +91,7 @@ proverConfigs =
   , ("any"      , SBV.defaultSMTCfg )
 
   , ("sbv-cvc4"     , SBV.cvc4     )
+  , ("sbv-cvc5"     , SBV.cvc5     )
   , ("sbv-yices"    , SBV.yices    )
   , ("sbv-z3"       , SBV.z3       )
   , ("sbv-boolector", SBV.boolector)

diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs
@@ -83,6 +83,7 @@ import qualified What4.SWord as SW
 import           What4.Solver
 import qualified What4.Solver.Boolector as W4
 import qualified What4.Solver.CVC4 as W4
+import qualified What4.Solver.CVC5 as W4
 import qualified What4.Solver.ExternalABC as W4
 import qualified What4.Solver.Yices as W4
 import qualified What4.Solver.Z3 as W4
@@ -161,6 +162,7 @@ data W4ProverConfig
 proverConfigs :: [(String, W4ProverConfig)]
 proverConfigs =
   [ ("w4-cvc4"      , W4ProverConfig cvc4OnlineAdapter)
+  , ("w4-cvc5"      , W4ProverConfig cvc5OnlineAdapter)
   , ("w4-yices"     , W4ProverConfig yicesOnlineAdapter)
   , ("w4-z3"        , W4ProverConfig z3OnlineAdapter)
   , ("w4-boolector" , W4ProverConfig boolectorOnlineAdapter)
@@ -186,6 +188,11 @@ cvc4OnlineAdapter =
   AnOnlineAdapter "CVC4" W4.cvc4Features W4.cvc4Options
          (Proxy :: Proxy (W4.Writer W4.CVC4))
 
+cvc5OnlineAdapter :: AnAdapter
+cvc5OnlineAdapter =
+  AnOnlineAdapter "CVC5" W4.cvc5Features W4.cvc5Options
+         (Proxy :: Proxy (W4.Writer W4.CVC5))
+
 boolectorOnlineAdapter :: AnAdapter
 boolectorOnlineAdapter =
   AnOnlineAdapter "Boolector" W4.boolectorFeatures W4.boolectorOptions
@@ -195,6 +202,7 @@ allSolvers :: W4ProverConfig
 allSolvers = W4Portfolio
   $ z3OnlineAdapter :|
   [ cvc4OnlineAdapter
+  , cvc5OnlineAdapter
   , boolectorOnlineAdapter
   , yicesOnlineAdapter
   , AnAdapter W4.externalABCAdapter

diff --git a/tests/issues/issue1503.cry b/tests/issues/issue1503.cry
@@ -0,0 +1,4 @@
+add_mul_lemma : Integer -> Integer -> Integer -> Integer -> Bit
+add_mul_lemma m n p q =
+  (0 <= m /\ 0 <= n /\ 0 <= p /\ 0 <= q /\ n < q /\ p < m) ==>
+  (m * n + p < m * q)
diff --git a/tests/issues/issue1503.icry b/tests/issues/issue1503.icry
@@ -0,0 +1,7 @@
+:l issue1503.cry
+
+:set prover=w4-cvc5
+:prove add_mul_lemma
+
+:set prover=sbv-cvc5
+:prove add_mul_lemma