Add support for CVC5

This adds basic support for the CVC5 SMT solver by adding `cvc5` and related
proof scripts. I hae added a `test_cvc5` integration test to kick the tires.

This addresses one part of #1706.

Author: RyanGlScott

.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

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

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 cvc5 {{ add_mul_lemma }};

intTests/test_cvc5/test.sh

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

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

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"

src/SAWScript/Interpreter.hs

@@ -1918,6 +1918,11 @@ primitives = Map.fromList
     Current
     [ "Use the CVC4 theorem prover to prove the current goal." ]
 
+  , prim "cvc5"                "ProofScript ()"
+    (pureVal proveCVC5)
+    Current
+    [ "Use the CVC5 theorem prover to prove the current goal." ]
+
   , prim "z3"                  "ProofScript ()"
     (pureVal proveZ3)
     Current
@@ -1947,6 +1952,13 @@ primitives = Map.fromList
     , "given list of names as uninterpreted."
     ]
 
+  , prim "unint_cvc5"            "[String] -> ProofScript ()"
+    (pureVal proveUnintCVC5)
+    Current
+    [ "Use the CVC5 theorem prover to prove the current goal. Leave the"
+    , "given list of names as uninterpreted."
+    ]
+
   , prim "unint_yices"           "[String] -> ProofScript ()"
     (pureVal proveUnintYices)
     Current
@@ -1964,6 +1976,11 @@ primitives = Map.fromList
     Current
     [ "Use the CVC4 theorem prover to prove the current goal." ]
 
+  , prim "sbv_cvc5"            "ProofScript ()"
+    (pureVal proveCVC5)
+    Current
+    [ "Use the CVC5 theorem prover to prove the current goal." ]
+
   , prim "sbv_z3"              "ProofScript ()"
     (pureVal proveZ3)
     Current
@@ -1993,6 +2010,13 @@ primitives = Map.fromList
     , "given list of names as uninterpreted."
     ]
 
+  , prim "sbv_unint_cvc5"        "[String] -> ProofScript ()"
+    (pureVal proveUnintCVC5)
+    Current
+    [ "Use the CVC5 theorem prover to prove the current goal. Leave the"
+    , "given list of names as uninterpreted."
+    ]
+
   , prim "sbv_unint_yices"       "[String] -> ProofScript ()"
     (pureVal proveUnintYices)
     Current
@@ -2116,6 +2140,13 @@ primitives = Map.fromList
     , "given list of names as uninterpreted."
     ]
 
+  , prim "w4_unint_cvc5"         "[String] -> ProofScript ()"
+    (pureVal w4_unint_cvc5)
+    Current
+    [ "Prove the current goal using What4 (CVC5 backend). Leave the"
+    , "given list of names as uninterpreted."
+    ]
+
   , prim "w4_abc_aiger"        "ProofScript ()"
     (pureVal w4_abc_aiger)
     Current
@@ -2161,6 +2192,13 @@ primitives = Map.fromList
     ," SMT-Lib2 format. Leave the given list of names as uninterpreted."
     ]
 
+  , prim "offline_w4_unint_cvc5"  "[String] -> String -> ProofScript ()"
+    (pureVal offline_w4_unint_cvc5)
+    Current
+    [ "Write the current goal to the given file using What4 (CVC5 backend) in"
+    ," SMT-Lib2 format. Leave the given list of names as uninterpreted."
+    ]
+
   , prim "split_goal"          "ProofScript ()"
     (pureVal split_goal)
     Experimental

src/SAWScript/Prover/SBV.hs

@@ -2,7 +2,7 @@ module SAWScript.Prover.SBV
   ( proveUnintSBV
   , proveUnintSBVIO
   , SBV.SMTConfig
-  , SBV.z3, SBV.cvc4, SBV.yices, SBV.mathSAT, SBV.boolector
+  , SBV.z3, SBV.cvc4, SBV.cvc5, SBV.yices, SBV.mathSAT, SBV.boolector
   , prepNegatedSBV
   ) where
 

src/SAWScript/Prover/What4.hs

@@ -111,7 +111,8 @@ proveExportWhat4_sym solver un hashConsing outFilePath t =
      -- Assume unsat
      return (Nothing, stats)
 
-proveWhat4_z3, proveWhat4_boolector, proveWhat4_cvc4,
+proveWhat4_z3, proveWhat4_boolector,
+  proveWhat4_cvc4, proveWhat4_cvc5,
   proveWhat4_dreal, proveWhat4_stp, proveWhat4_yices,
   proveWhat4_abc ::
   Set VarIndex  {- ^ Uninterpreted functions -} ->
@@ -122,6 +123,7 @@ proveWhat4_z3, proveWhat4_boolector, proveWhat4_cvc4,
 proveWhat4_z3        = proveWhat4_sym z3Adapter
 proveWhat4_boolector = proveWhat4_sym boolectorAdapter
 proveWhat4_cvc4      = proveWhat4_sym cvc4Adapter
+proveWhat4_cvc5      = proveWhat4_sym cvc5Adapter
 proveWhat4_dreal     = proveWhat4_sym drealAdapter
 proveWhat4_stp       = proveWhat4_sym stpAdapter
 proveWhat4_yices     = proveWhat4_sym yicesAdapter
@@ -141,7 +143,8 @@ proveWhat4_z3_using tactic un hashConsing t =
           _ <- setOpt z3TacticSetting $ Text.pack tactic
           return ()
 
-proveExportWhat4_z3, proveExportWhat4_boolector, proveExportWhat4_cvc4,
+proveExportWhat4_z3, proveExportWhat4_boolector,
+  proveExportWhat4_cvc4, proveExportWhat4_cvc5,
   proveExportWhat4_dreal, proveExportWhat4_stp, proveExportWhat4_yices ::
   Set VarIndex  {- ^ Uninterpreted functions -} ->
   Bool          {- ^ Hash-consing of ExportWhat4 terms -}->
@@ -152,6 +155,7 @@ proveExportWhat4_z3, proveExportWhat4_boolector, proveExportWhat4_cvc4,
 proveExportWhat4_z3        = proveExportWhat4_sym z3Adapter
 proveExportWhat4_boolector = proveExportWhat4_sym boolectorAdapter
 proveExportWhat4_cvc4      = proveExportWhat4_sym cvc4Adapter
+proveExportWhat4_cvc5      = proveExportWhat4_sym cvc5Adapter
 proveExportWhat4_dreal     = proveExportWhat4_sym drealAdapter
 proveExportWhat4_stp       = proveExportWhat4_sym stpAdapter
 proveExportWhat4_yices     = proveExportWhat4_sym yicesAdapter