Remove support for cvc4

.github/ci.sh

@@ -217,7 +217,6 @@ zip_dist_with_solvers() {
   cp "$BIN/abc"        dist/bin/
   cp "$BIN/bitwuzla"   dist/bin/
   cp "$BIN/boolector"  dist/bin/
-  cp "$BIN/cvc4"       dist/bin/
   cp "$BIN/cvc5"       dist/bin/
   cp "$BIN/yices"      dist/bin/
   cp "$BIN/yices-smt2" dist/bin/

CHANGES.md

@@ -76,7 +76,9 @@ This release supports [version
 * Fix a bug that would cause the `offline_w4_unint_yices` proof script to
   always throw an error.
 
-## Deprecations
+## Removals / Deprecations
+
+* Support for CVC4 has been removed. Use CVC5.
 
 * The `assume_unsat` builtin has been deprecated, after five years' notice
   that this was coming.

doc/llvm-java-verification-with-saw/code/NQueens.cry

@@ -8,7 +8,7 @@
   :sat nQueens : (Solution n)
   where n is the board-size
 
-  You may find that cvc4 takes a long time for solutions bigger than 5.
+  You may find that cvc5 takes a long time for solutions bigger than 18.
   For those sizes, we have had good luck with both Yices and Z3.  
 
   To do that,

doc/llvm-java-verification-with-saw/using-smt-lib-solvers.md

@@ -38,5 +38,4 @@ 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, Bitwuzla, Boolector, CVC4, CVC5, MathSAT, Yices, and
-Z3.
+package, and support ABC, Bitwuzla, Boolector, CVC5, MathSAT, Yices, and Z3.

doc/saw-lexer/src/saw_lexer.py

@@ -86,7 +86,7 @@ class SAWScriptLexer(RegexLexer):
                 r"prove|prove_print|sat|"
                 r"unfolding|simplify|normalize_term|goal_normalize|"
                 r"goal_apply|admit|"
-                r"abc|bitwuzla|boolector|cvc4|cvc5|z3|mathsat|yices|rme|"
+                r"abc|bitwuzla|boolector|cvc5|z3|mathsat|yices|rme|"
                 r"offline_rocq|"
                 r"empty_ss|basic_ss|cryptol_ss|addsimp|rewrite|"
                 r"parse_core|"

doc/saw-user-manual/installing-saw.md

@@ -112,7 +112,6 @@ In addition, it is capable of using the following other external solvers:
  - [Bitwuzla](https://github.com/bitwuzla/bitwuzla)
  - [Boolector](https://github.com/Boolector/boolector) (superseded upstream by bitwuzla, deprecated in SAW)
  - [CVC5](https://github.com/cvc5/cvc5)
- - [CVC4](https://github.com/CVC4/CVC4-archived) (superseded upstream by cvc5, deprecated in SAW)
  - MathSAT
  - [Yices](https://github.com/SRI-CSL/yices2)
 

doc/saw-user-manual/interactive-proofs.md

@@ -373,7 +373,7 @@ sawscript> sat_print abc {{ \(x:[8]) -> x+x == x*2 }}
 Sat: [x = 0]
 :::
 
-In addition to these, the `bitwuzla`, `boolector`, `cvc4`, `cvc5`, `mathsat`,
+In addition to these, the `bitwuzla`, `boolector`, `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.
@@ -441,8 +441,6 @@ named subterms should be represented as uninterpreted functions.
 
 - `unint_bitwuzla : [String] -> ProofScript ()`
 
-- `unint_cvc4 : [String] -> ProofScript ()`
-
 - `unint_cvc5 : [String] -> ProofScript ()`
 
 - `unint_yices : [String] -> ProofScript ()`
@@ -464,8 +462,6 @@ library to represent and solve SMT queries:
 
 - `sbv_unint_bitwuzla : [String] -> ProofScript ()`
 
-- `sbv_unint_cvc4 : [String] -> ProofScript ()`
-
 - `sbv_unint_cvc5 : [String] -> ProofScript ()`
 
 - `sbv_unint_yices : [String] -> ProofScript ()`
@@ -476,8 +472,6 @@ The `w4_`-prefixed tactics make use of the What4 library instead of SBV:
 
 - `w4_unint_bitwuzla : [String] -> ProofScript ()`
 
-- `w4_unint_cvc4 : [String] -> ProofScript ()`
-
 - `w4_unint_cvc5 : [String] -> ProofScript ()`
 
 - `w4_unint_yices : [String] -> ProofScript ()`
@@ -500,7 +494,7 @@ proof development and CI, where the same proof scripts are often run repeatedly
 without changes.
 
 This caching is available for all tactics which call out to automated provers
-at runtime: `abc`, `boolector`, `cvc4`, `cvc5`, `mathsat`, `yices`, `z3`,
+at runtime: `abc`, `boolector`, `cvc5`, `mathsat`, `yices`, `z3`,
 `rme`, and the family of `unint` tactics described in the previous section.
 
 When solver caching is enabled and one of the tactics mentioned above is

examples/misc/external_sat.saw

@@ -3,4 +3,4 @@ let picosat = external_cnf_solver "picosat" ["%f"];
 sat_print abc thm;
 sat_print picosat thm;
 sat_print yices thm;
-sat_print cvc4 thm;
+sat_print cvc5 thm;

examples/misc/symbolic_function.saw

@@ -19,5 +19,5 @@ let {{
 
 enc <- fresh_symbolic "enc" {| [64] -> [64] |};
 
-prove_print cvc4 {{ prop1 enc : [64] -> [100][64] -> Bit }};
-prove_print cvc4 {{ prop2 enc : [64] -> [100][64] -> Bit }};
+prove_print cvc5 {{ prop1 enc : [64] -> [100][64] -> Bit }};
+prove_print cvc5 {{ prop2 enc : [64] -> [100][64] -> Bit }};

intTests/test1646/test15.log.good

@@ -91,7 +91,6 @@ cryptol_extract : CryptolModule -> String -> TopLevel Term
 cryptol_load : String -> TopLevel CryptolModule
 cryptol_prims : () -> CryptolModule
 cryptol_ss : () -> Simpset
-cvc4 : ProofScript ()
 cvc5 : ProofScript ()
 declare_ghost_state : String -> TopLevel Ghost
 default_x86_preserved_reg : TopLevel ()
@@ -359,7 +358,6 @@ offline_smtlib2 : String -> ProofScript ()
 offline_unint_smtlib2 : [String] -> String -> ProofScript ()
 offline_w4_smtlib2 : String -> ProofScript ()
 offline_w4_unint_bitwuzla : [String] -> String -> ProofScript ()
-offline_w4_unint_cvc4 : [String] -> String -> ProofScript ()
 offline_w4_unint_cvc5 : [String] -> String -> ProofScript ()
 offline_w4_unint_yices : [String] -> String -> ProofScript ()
 offline_w4_unint_z3 : [String] -> String -> ProofScript ()
@@ -399,11 +397,9 @@ save_aig_as_cnf : String -> AIG -> TopLevel ()
 sbv_abc : ProofScript ()
 sbv_bitwuzla : ProofScript ()
 sbv_boolector : ProofScript ()
-sbv_cvc4 : ProofScript ()
 sbv_cvc5 : ProofScript ()
 sbv_mathsat : ProofScript ()
 sbv_unint_bitwuzla : [String] -> ProofScript ()
-sbv_unint_cvc4 : [String] -> ProofScript ()
 sbv_unint_cvc5 : [String] -> ProofScript ()
 sbv_unint_yices : [String] -> ProofScript ()
 sbv_unint_z3 : [String] -> ProofScript ()
@@ -450,7 +446,6 @@ unfold_term : [String] -> Term -> Term
 unfolding : [String] -> ProofScript ()
 unfolding_fix_once : [String] -> ProofScript ()
 unint_bitwuzla : [String] -> ProofScript ()
-unint_cvc4 : [String] -> ProofScript ()
 unint_cvc5 : [String] -> ProofScript ()
 unint_yices : [String] -> ProofScript ()
 unint_z3 : [String] -> ProofScript ()
@@ -460,7 +455,6 @@ w4_abc_smtlib2 : ProofScript ()
 w4_abc_verilog : ProofScript ()
 w4_offline_smtlib2 : String -> ProofScript ()
 w4_unint_bitwuzla : [String] -> ProofScript ()
-w4_unint_cvc4 : [String] -> ProofScript ()
 w4_unint_cvc5 : [String] -> ProofScript ()
 w4_unint_rme : [String] -> ProofScript ()
 w4_unint_yices : [String] -> ProofScript ()

intTests/test_search/search03.log.good

@@ -19,7 +19,6 @@ crucible_llvm_verify :
    ProofScript () ->
    TopLevel LLVMSpec
    (DEPRECATED AND WILL WARN)
-cvc4 : ProofScript ()  (DEPRECATED AND WILL WARN)
 cvc5 : ProofScript ()
 external_aig_solver :
    String -> [String] -> ProofScript ()
@@ -68,9 +67,6 @@ offline_smtlib2 : String -> ProofScript ()
 offline_unint_smtlib2 : [String] -> String -> ProofScript ()
 offline_w4_smtlib2 : String -> ProofScript ()
 offline_w4_unint_bitwuzla : [String] -> String -> ProofScript ()
-offline_w4_unint_cvc4 :
-   [String] -> String -> ProofScript ()
-   (DEPRECATED AND WILL WARN)
 offline_w4_unint_cvc5 : [String] -> String -> ProofScript ()
 offline_w4_unint_yices : [String] -> String -> ProofScript ()
 offline_w4_unint_z3 : [String] -> String -> ProofScript ()
@@ -93,13 +89,9 @@ sat_print : ProofScript () -> Term -> TopLevel ()
 sbv_abc : ProofScript ()
 sbv_bitwuzla : ProofScript ()
 sbv_boolector : ProofScript ()  (DEPRECATED AND WILL WARN)
-sbv_cvc4 : ProofScript ()  (DEPRECATED AND WILL WARN)
 sbv_cvc5 : ProofScript ()
 sbv_mathsat : ProofScript ()
 sbv_unint_bitwuzla : [String] -> ProofScript ()
-sbv_unint_cvc4 :
-   [String] -> ProofScript ()
-   (DEPRECATED AND WILL WARN)
 sbv_unint_cvc5 : [String] -> ProofScript ()
 sbv_unint_yices : [String] -> ProofScript ()
 sbv_unint_z3 : [String] -> ProofScript ()
@@ -111,9 +103,6 @@ trivial : ProofScript ()
 unfolding : [String] -> ProofScript ()
 unfolding_fix_once : [String] -> ProofScript ()
 unint_bitwuzla : [String] -> ProofScript ()
-unint_cvc4 :
-   [String] -> ProofScript ()
-   (DEPRECATED AND WILL WARN)
 unint_cvc5 : [String] -> ProofScript ()
 unint_yices : [String] -> ProofScript ()
 unint_z3 : [String] -> ProofScript ()
@@ -125,9 +114,6 @@ w4_offline_smtlib2 :
    String -> ProofScript ()
    (DEPRECATED AND WILL WARN)
 w4_unint_bitwuzla : [String] -> ProofScript ()
-w4_unint_cvc4 :
-   [String] -> ProofScript ()
-   (DEPRECATED AND WILL WARN)
 w4_unint_cvc5 : [String] -> ProofScript ()
 w4_unint_rme : [String] -> ProofScript ()
 w4_unint_yices : [String] -> ProofScript ()
@@ -159,7 +145,6 @@ crucible_llvm_verify :
    ProofScript () ->
    TopLevel LLVMSpec
    (DEPRECATED AND WILL WARN)
-cvc4 : ProofScript ()  (DEPRECATED AND WILL WARN)
 cvc5 : ProofScript ()
 external_aig_solver :
    String -> [String] -> ProofScript ()
@@ -208,9 +193,6 @@ offline_smtlib2 : String -> ProofScript ()
 offline_unint_smtlib2 : [String] -> String -> ProofScript ()
 offline_w4_smtlib2 : String -> ProofScript ()
 offline_w4_unint_bitwuzla : [String] -> String -> ProofScript ()
-offline_w4_unint_cvc4 :
-   [String] -> String -> ProofScript ()
-   (DEPRECATED AND WILL WARN)
 offline_w4_unint_cvc5 : [String] -> String -> ProofScript ()
 offline_w4_unint_yices : [String] -> String -> ProofScript ()
 offline_w4_unint_z3 : [String] -> String -> ProofScript ()
@@ -233,13 +215,9 @@ sat_print : ProofScript () -> Term -> TopLevel ()
 sbv_abc : ProofScript ()
 sbv_bitwuzla : ProofScript ()
 sbv_boolector : ProofScript ()  (DEPRECATED AND WILL WARN)
-sbv_cvc4 : ProofScript ()  (DEPRECATED AND WILL WARN)
 sbv_cvc5 : ProofScript ()
 sbv_mathsat : ProofScript ()
 sbv_unint_bitwuzla : [String] -> ProofScript ()
-sbv_unint_cvc4 :
-   [String] -> ProofScript ()
-   (DEPRECATED AND WILL WARN)
 sbv_unint_cvc5 : [String] -> ProofScript ()
 sbv_unint_yices : [String] -> ProofScript ()
 sbv_unint_z3 : [String] -> ProofScript ()
@@ -251,9 +229,6 @@ trivial : ProofScript ()
 unfolding : [String] -> ProofScript ()
 unfolding_fix_once : [String] -> ProofScript ()
 unint_bitwuzla : [String] -> ProofScript ()
-unint_cvc4 :
-   [String] -> ProofScript ()
-   (DEPRECATED AND WILL WARN)
 unint_cvc5 : [String] -> ProofScript ()
 unint_yices : [String] -> ProofScript ()
 unint_z3 : [String] -> ProofScript ()
@@ -265,9 +240,6 @@ w4_offline_smtlib2 :
    String -> ProofScript ()
    (DEPRECATED AND WILL WARN)
 w4_unint_bitwuzla : [String] -> ProofScript ()
-w4_unint_cvc4 :
-   [String] -> ProofScript ()
-   (DEPRECATED AND WILL WARN)
 w4_unint_cvc5 : [String] -> ProofScript ()
 w4_unint_rme : [String] -> ProofScript ()
 w4_unint_yices : [String] -> ProofScript ()

saw-central/src/SAWCentral/Builtins.hs

@@ -93,35 +93,30 @@ module SAWCentral.Builtins (
     proveBitwuzla,
     proveBoolector,
     proveZ3,
-    proveCVC4,
     proveCVC5,
     proveMathSAT,
     proveYices,
     proveUnintBitwuzla,
     proveUnintBoolector,
     proveUnintZ3,
-    proveUnintCVC4,
     proveUnintCVC5,
     proveUnintMathSAT,
     proveUnintYices,
     w4_abc_smtlib2,
     w4_bitwuzla,
     w4_boolector,
     w4_z3,
-    w4_cvc4,
     w4_cvc5,
     w4_yices,
     w4_unint_bitwuzla,
     w4_unint_rme,
     w4_unint_boolector,
     w4_unint_z3,
     w4_unint_z3_using,
-    w4_unint_cvc4,
     w4_unint_cvc5,
     w4_unint_yices,
     offline_w4_unint_bitwuzla,
     offline_w4_unint_z3,
-    offline_w4_unint_cvc4,
     offline_w4_unint_cvc5,
     offline_w4_unint_yices,
     offline_aig,
@@ -1234,9 +1229,6 @@ proveBoolector = proveSBV SBV.boolector
 proveZ3 :: ProofScript ()
 proveZ3 = proveSBV SBV.z3
 
-proveCVC4 :: ProofScript ()
-proveCVC4 = proveSBV SBV.cvc4
-
 proveCVC5 :: ProofScript ()
 proveCVC5 = proveSBV SBV.cvc5
 
@@ -1255,9 +1247,6 @@ proveUnintBoolector = proveUnintSBV SBV.boolector
 proveUnintZ3 :: [Text] -> ProofScript ()
 proveUnintZ3 = proveUnintSBV SBV.z3
 
-proveUnintCVC4 :: [Text] -> ProofScript ()
-proveUnintCVC4 = proveUnintSBV SBV.cvc4
-
 proveUnintCVC5 :: [Text] -> ProofScript ()
 proveUnintCVC5 = proveUnintSBV SBV.cvc5
 
@@ -1283,10 +1272,6 @@ w4_boolector = wrapW4Prover Boolector [] Prover.proveWhat4_boolector []
 w4_z3 :: ProofScript ()
 w4_z3 = wrapW4Prover Z3 [] Prover.proveWhat4_z3 []
 
--- XXX not accessable from sawscript (only w4_unint_cvc4 is)
-w4_cvc4 :: ProofScript ()
-w4_cvc4 = wrapW4Prover CVC4 [] Prover.proveWhat4_cvc4 []
-
 -- XXX not accessable from sawscript (only w4_unint_cvc5 is)
 w4_cvc5 :: ProofScript ()
 w4_cvc5 = wrapW4Prover CVC5 [] Prover.proveWhat4_cvc5 []
@@ -1313,9 +1298,6 @@ w4_unint_z3_using tactic =
   let tactic' = Text.unpack tactic in
   wrapW4Prover Z3 [W4_Tactic tactic'] (Prover.proveWhat4_z3_using tactic')
 
-w4_unint_cvc4 :: [Text] -> ProofScript ()
-w4_unint_cvc4 = wrapW4Prover CVC4 [] Prover.proveWhat4_cvc4
-
 w4_unint_cvc5 :: [Text] -> ProofScript ()
 w4_unint_cvc5 = wrapW4Prover CVC5 [] Prover.proveWhat4_cvc5
 
@@ -1330,10 +1312,6 @@ offline_w4_unint_z3 :: [Text] -> FilePath -> ProofScript ()
 offline_w4_unint_z3 unints path =
   wrapW4ProveExporter Prover.proveExportWhat4_z3 unints path ".smt2"
 
-offline_w4_unint_cvc4 :: [Text] -> FilePath -> ProofScript ()
-offline_w4_unint_cvc4 unints path =
-  wrapW4ProveExporter Prover.proveExportWhat4_cvc4 unints path ".smt2"
-
 offline_w4_unint_cvc5 :: [Text] -> FilePath -> ProofScript ()
 offline_w4_unint_cvc5 unints path =
   wrapW4ProveExporter Prover.proveExportWhat4_cvc5 unints path ".smt2"

saw-central/src/SAWCentral/Prover/SBV.hs

@@ -3,7 +3,7 @@ module SAWCentral.Prover.SBV
   ( proveUnintSBV
   , proveUnintSBVIO
   , SBV.SMTConfig
-  , SBV.z3, SBV.cvc4, SBV.cvc5, SBV.yices, SBV.mathSAT, SBV.boolector, SBV.bitwuzla
+  , SBV.z3, SBV.cvc5, SBV.yices, SBV.mathSAT, SBV.boolector, SBV.bitwuzla
   ) where
 
 import           Control.Monad