Add support for CVC5

.github/ci.sh

@@ -80,7 +80,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
 }
 
 build_cryptol() {
@@ -127,6 +127,7 @@ zip_dist_with_solvers() {
   # dependencies) as the SAW binaries.
   cp "$BIN/abc"        dist/bin/
   cp "$BIN/cvc4"       dist/bin/
+  cp "$BIN/cvc5"       dist/bin/
   cp "$BIN/yices"      dist/bin/
   cp "$BIN/yices-smt2" dist/bin/
   # Z3 4.8.14 has been known to nondeterministically time out with the AWSLC

.github/workflows/ci.yml

@@ -573,9 +573,6 @@ jobs:
           docker-compose pull
           grep -h '^FROM' docker/*.dockerfile | sort -u | awk '{print $2}' | xargs -n1 -P8 docker pull
 
-      - uses: jpribyl/[email protected]
-        continue-on-error: true
-
       - shell: bash
         name: "make s2n"
         working-directory: s2nTests
@@ -606,9 +603,6 @@ jobs:
           name: "${{ runner.os }}-bins"
           path: ./exercises/bin
 
-      - uses: jpribyl/[email protected]
-        continue-on-error: true
-
       - shell: bash
         name: "make exercises container"
         working-directory: exercises

CHANGES.md

@@ -90,6 +90,11 @@
   allows verification certain kinds of simple loops by using a
   user-provided loop invariant.
 
+* Add a `cvc5` family of proof scripts that use the CVC5 SMT solver.
+  (Note that the `sbv_cvc5` and `sbv_unint_cvc5` are non-functional
+  on Windows at this time due to a downstream issue with CVC5 1.0.4 and
+  earlier.)
+
 # Version 0.9
 
 ## New Features

cabal.GHC-8.10.7.config

@@ -1,5 +1,6 @@
 active-repositories: hackage.haskell.org:merge
-constraints: any.Cabal ==3.2.1.0,
+constraints: any.BoundedChan ==1.0.3.0,
+             any.Cabal ==3.2.1.0,
              any.Glob ==0.10.2,
              any.GraphSCC ==1.0.4,
              GraphSCC -use-maps,
@@ -248,6 +249,7 @@ constraints: any.Cabal ==3.2.1.0,
              optparse-applicative +process,
              any.optparse-simple ==0.1.1.4,
              optparse-simple -build-example,
+             any.ordered-containers ==0.2.3,
              any.panic ==0.4.0.1,
              any.parallel ==3.2.2.0,
              parameterized-utils +unsafe-operations,
@@ -284,7 +286,7 @@ constraints: any.Cabal ==3.2.1.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,
@@ -329,7 +331,7 @@ constraints: any.Cabal ==3.2.1.0,
              any.tasty-hunit ==0.10.0.3,
              any.tasty-quickcheck ==0.10.2,
              any.tasty-smallcheck ==0.8.2,
-             any.tasty-sugar ==1.3.0.2,
+             any.tasty-sugar ==2.0.1.0,
              any.template-haskell ==2.16.0.0,
              any.temporary ==1.3,
              any.terminal-size ==0.3.3,

cabal.GHC-8.8.4.config

@@ -1,5 +1,6 @@
 active-repositories: hackage.haskell.org:merge
-constraints: any.Cabal ==3.0.1.0,
+constraints: any.BoundedChan ==1.0.3.0,
+             any.Cabal ==3.0.1.0,
              any.Glob ==0.10.2,
              any.GraphSCC ==1.0.4,
              GraphSCC -use-maps,
@@ -249,6 +250,7 @@ constraints: any.Cabal ==3.0.1.0,
              optparse-applicative +process,
              any.optparse-simple ==0.1.1.4,
              optparse-simple -build-example,
+             any.ordered-containers ==0.2.3,
              any.panic ==0.4.0.1,
              any.parallel ==3.2.2.0,
              parameterized-utils +unsafe-operations,
@@ -285,7 +287,7 @@ constraints: any.Cabal ==3.0.1.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,
@@ -330,7 +332,7 @@ constraints: any.Cabal ==3.0.1.0,
              any.tasty-hunit ==0.10.0.3,
              any.tasty-quickcheck ==0.10.2,
              any.tasty-smallcheck ==0.8.2,
-             any.tasty-sugar ==1.3.0.2,
+             any.tasty-sugar ==2.0.1.0,
              any.template-haskell ==2.15.0.0,
              any.temporary ==1.3,
              any.terminal-size ==0.3.3,

cabal.GHC-9.2.7.config

@@ -1,5 +1,6 @@
 active-repositories: hackage.haskell.org:merge
-constraints: any.Cabal ==3.6.3.0,
+constraints: any.BoundedChan ==1.0.3.0,
+             any.Cabal ==3.6.3.0,
              any.Glob ==0.10.2,
              any.GraphSCC ==1.0.4,
              GraphSCC -use-maps,
@@ -249,6 +250,7 @@ constraints: any.Cabal ==3.6.3.0,
              optparse-applicative +process,
              any.optparse-simple ==0.1.1.4,
              optparse-simple -build-example,
+             any.ordered-containers ==0.2.3,
              any.panic ==0.4.0.1,
              any.parallel ==3.2.2.0,
              parameterized-utils +unsafe-operations,
@@ -285,7 +287,7 @@ constraints: any.Cabal ==3.6.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,
@@ -330,7 +332,7 @@ constraints: any.Cabal ==3.6.3.0,
              any.tasty-hunit ==0.10.0.3,
              any.tasty-quickcheck ==0.10.2,
              any.tasty-smallcheck ==0.8.2,
-             any.tasty-sugar ==1.3.0.2,
+             any.tasty-sugar ==2.0.1.0,
              any.template-haskell ==2.18.0.0,
              any.temporary ==1.3,
              any.terminal-size ==0.3.3,

doc/manual/manual.md

@@ -1131,7 +1131,7 @@ sawscript> sat_print abc {{ \(x:[8]) -> x+x == x*2 }}
 Sat: [x = 0]
 ~~~~
 
-In addition to these, the `boolector`, `cvc4`, `mathsat`, and `yices`
+In addition to these, the `boolector`, `cvc4`, `cvc5`, `mathsat`, and `yices`
 provers are available. The internal decision procedure `rme`, short for
 Reed-Muller Expansion, is an automated prover that works particularly
 well on the Galois field operations that show up, for example, in AES.
@@ -1199,6 +1199,8 @@ named subterms should be represented as uninterpreted functions.
 
 * `unint_cvc4 : [String] -> ProofScript ()`
 
+* `unint_cvc5 : [String] -> ProofScript ()`
+
 * `unint_yices : [String] -> ProofScript ()`
 
 * `unint_z3 : [String] -> ProofScript ()`
@@ -1218,6 +1220,8 @@ library to represent and solve SMT queries:
 
 * `sbv_unint_cvc4 : [String] -> ProofScript ()`
 
+* `sbv_unint_cvc5 : [String] -> ProofScript ()`
+
 * `sbv_unint_yices : [String] -> ProofScript ()`
 
 * `sbv_unint_z3 : [String] -> ProofScript ()`
@@ -1226,6 +1230,8 @@ The `w4_`-prefixed tactics make use of the What4 library instead of SBV:
 
 * `w4_unint_cvc4 : [String] -> ProofScript ()`
 
+* `w4_unint_cvc5 : [String] -> ProofScript ()`
+
 * `w4_unint_yices : [String] -> ProofScript ()`
 
 * `w4_unint_z3 : [String] -> ProofScript ()`

doc/tutorial/tutorial.md

@@ -296,7 +296,7 @@ passes the given term through unchanged, because it might be used for
 either satisfiability or validity checking.
 
 The SMT-Lib export capabilities in SAWScript make use of the Haskell
-SBV package, and support ABC, Boolector, CVC4, MathSAT, Yices, and Z3.
+SBV package, and support ABC, Boolector, CVC4, CVC5, MathSAT, Yices, and Z3.
 
 \newpage
 

intTests/test_cvc5/test.saw

@@ -0,0 +1,9 @@
+let
+{{
+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)
+}};
+
+prove (w4_unint_cvc5 []) {{ add_mul_lemma }};

intTests/test_cvc5/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

saw-core-sbv/saw-core-sbv.cabal

@@ -20,7 +20,7 @@ library
     lens,
     mtl,
     saw-core,
-    sbv >= 8.10 && < 9.1,
+    sbv >= 9.1 && < 9.3,
     text,
     transformers,
     vector

saw-remote-api/python/saw_client/proofscript.py

@@ -45,6 +45,10 @@ class CVC4(UnintProver):
   def __init__(self, unints : List[str]) -> None:
     super().__init__("w4-cvc4", unints)
 
+class CVC5(UnintProver):
+  def __init__(self, unints : List[str]) -> None:
+    super().__init__("w4-cvc5", unints)
+
 class Yices(UnintProver):
   def __init__(self, unints : List[str]) -> None:
     super().__init__("w4-yices", unints)
@@ -57,6 +61,10 @@ class CVC4_SBV(UnintProver):
   def __init__(self, unints : List[str]) -> None:
     super().__init__("sbv-cvc4", unints)
 
+class CVC5_SBV(UnintProver):
+  def __init__(self, unints : List[str]) -> None:
+    super().__init__("sbv-cvc5", unints)
+
 class Yices_SBV(UnintProver):
   def __init__(self, unints : List[str]) -> None:
     super().__init__("sbv-yices", unints)
@@ -121,6 +129,9 @@ def to_json(self) -> Any:
 def cvc4(unints : List[str]) -> ProofTactic:
   return UseProver(CVC4(unints))
 
+def cvc5(unints : List[str]) -> ProofTactic:
+  return UseProver(CVC5(unints))
+
 def yices(unints : List[str]) -> ProofTactic:
   return UseProver(Yices(unints))
 

saw-remote-api/src/SAWServer/ProofScript.hs

@@ -57,13 +57,15 @@ data Prover
   | SBV_ABC_SMTLib
   | SBV_Boolector [String]
   | SBV_CVC4 [String]
+  | SBV_CVC5 [String]
   | SBV_MathSAT [String]
   | SBV_Yices [String]
   | SBV_Z3 [String]
   | W4_ABC_SMTLib
   | W4_ABC_Verilog
   | W4_Boolector [String]
   | W4_CVC4 [String]
+  | W4_CVC5 [String]
   | W4_Yices [String]
   | W4_Z3 [String]
 
@@ -87,18 +89,21 @@ instance FromJSON Prover where
         "abc"            -> pure W4_ABC_SMTLib
         "boolector"      -> SBV_Boolector <$> unints
         "cvc4"           -> SBV_CVC4  <$> unints
+        "cvc5"           -> SBV_CVC5  <$> unints
         "mathsat"        -> SBV_MathSAT <$> unints
         "rme"            -> pure RME
         "sbv-abc"        -> pure SBV_ABC_SMTLib
         "sbv-boolector"  -> SBV_Boolector <$> unints
         "sbv-cvc4"       -> SBV_CVC4  <$> unints
+        "sbv-cvc5"       -> SBV_CVC5  <$> unints
         "sbv-mathsat"    -> SBV_MathSAT <$> unints
         "sbv-yices"      -> SBV_Yices <$> unints
         "sbv-z3"         -> SBV_Z3    <$> unints
         "w4-abc-smtlib"  -> pure W4_ABC_SMTLib
         "w4-abc-verilog" -> pure W4_ABC_Verilog
         "w4-boolector"   -> W4_Boolector <$> unints
         "w4-cvc4"        -> W4_CVC4   <$> unints
+        "w4-cvc5"        -> W4_CVC5   <$> unints
         "w4-yices"       -> W4_Yices  <$> unints
         "w4-z3"          -> W4_Z3     <$> unints
         "yices"          -> SBV_Yices <$> unints
@@ -273,13 +278,15 @@ interpretProofScript (ProofScript ts) = go ts
             SBV_ABC_SMTLib        -> return $ SB.proveABC_SBV
             SBV_Boolector unints  -> return $ SB.proveUnintBoolector unints
             SBV_CVC4 unints       -> return $ SB.proveUnintCVC4 unints
+            SBV_CVC5 unints       -> return $ SB.proveUnintCVC5 unints
             SBV_MathSAT unints    -> return $ SB.proveUnintMathSAT unints
             SBV_Yices unints      -> return $ SB.proveUnintYices unints
             SBV_Z3 unints         -> return $ SB.proveUnintZ3 unints
             W4_ABC_SMTLib         -> return $ SB.w4_abc_smtlib2
             W4_ABC_Verilog        -> return $ SB.w4_abc_verilog
             W4_Boolector unints   -> return $ SB.w4_unint_boolector unints
             W4_CVC4 unints        -> return $ SB.w4_unint_cvc4 unints
+            W4_CVC5 unints        -> return $ SB.w4_unint_cvc5 unints
             W4_Yices unints       -> return $ SB.w4_unint_yices unints
             W4_Z3 unints          -> return $ SB.w4_unint_z3 unints
         go [Trivial]                  = return $ SB.trivial

saw-script.cabal

@@ -80,7 +80,7 @@ library
     , saw-core-coq
     , saw-core-sbv
     , saw-core-what4
-    , sbv >= 8.10 && < 9.1
+    , sbv >= 9.1 && < 9.3
     , split
     , temporary
     , template-haskell

src/SAWScript/Builtins.hs

@@ -1005,6 +1005,9 @@ proveZ3 = proveSBV SBV.z3
 proveCVC4 :: ProofScript ()
 proveCVC4 = proveSBV SBV.cvc4
 
+proveCVC5 :: ProofScript ()
+proveCVC5 = proveSBV SBV.cvc5
+
 proveMathSAT :: ProofScript ()
 proveMathSAT = proveSBV SBV.mathSAT
 
@@ -1020,6 +1023,9 @@ proveUnintZ3 = proveUnintSBV SBV.z3
 proveUnintCVC4 :: [String] -> ProofScript ()
 proveUnintCVC4 = proveUnintSBV SBV.cvc4
 
+proveUnintCVC5 :: [String] -> ProofScript ()
+proveUnintCVC5 = proveUnintSBV SBV.cvc5
+
 proveUnintMathSAT :: [String] -> ProofScript ()
 proveUnintMathSAT = proveUnintSBV SBV.mathSAT
 
@@ -1040,6 +1046,9 @@ w4_z3 = wrapW4Prover Prover.proveWhat4_z3 []
 w4_cvc4 :: ProofScript ()
 w4_cvc4 = wrapW4Prover Prover.proveWhat4_cvc4 []
 
+w4_cvc5 :: ProofScript ()
+w4_cvc5 = wrapW4Prover Prover.proveWhat4_cvc5 []
+
 w4_yices :: ProofScript ()
 w4_yices = wrapW4Prover Prover.proveWhat4_yices []
 
@@ -1055,6 +1064,9 @@ w4_unint_z3_using tactic = wrapW4Prover (Prover.proveWhat4_z3_using tactic)
 w4_unint_cvc4 :: [String] -> ProofScript ()
 w4_unint_cvc4 = wrapW4Prover Prover.proveWhat4_cvc4
 
+w4_unint_cvc5 :: [String] -> ProofScript ()
+w4_unint_cvc5 = wrapW4Prover Prover.proveWhat4_cvc5
+
 w4_unint_yices :: [String] -> ProofScript ()
 w4_unint_yices = wrapW4Prover Prover.proveWhat4_yices
 
@@ -1066,6 +1078,10 @@ offline_w4_unint_cvc4 :: [String] -> String -> ProofScript ()
 offline_w4_unint_cvc4 unints path =
      wrapW4ProveExporter Prover.proveExportWhat4_cvc4 unints path ".smt2"
 
+offline_w4_unint_cvc5 :: [String] -> String -> ProofScript ()
+offline_w4_unint_cvc5 unints path =
+     wrapW4ProveExporter Prover.proveExportWhat4_cvc5 unints path ".smt2"
+
 offline_w4_unint_yices :: [String] -> String -> ProofScript ()
 offline_w4_unint_yices unints path =
      wrapW4ProveExporter Prover.proveExportWhat4_yices unints path ".smt2"