From 98e250eeb9ba945e6a1f052212f56246208aaf32 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Fri, 16 Jan 2026 11:08:55 -0800 Subject: [PATCH 1/2] Remove support for cvc4 * update documentation to use cvc5 * remove cvc4 related functions from the codebase * update tests to use cvc5 * use placeholders where SBV mentions cvc4 * add CHANGES entry --- .github/ci.sh | 1 - CHANGES.md | 4 +- .../code/NQueens.cry | 2 +- .../using-smt-lib-solvers.md | 3 +- doc/saw-lexer/src/saw_lexer.py | 2 +- doc/saw-user-manual/installing-saw.md | 1 - doc/saw-user-manual/interactive-proofs.md | 10 +-- examples/misc/external_sat.saw | 2 +- examples/misc/symbolic_function.saw | 4 +- intTests/test1646/test15.log.good | 6 -- intTests/test_search/search03.log.good | 28 -------- saw-central/src/SAWCentral/Builtins.hs | 22 ------- saw-central/src/SAWCentral/Prover/SBV.hs | 2 +- saw-central/src/SAWCentral/Prover/What4.hs | 8 +-- saw-central/src/SAWCentral/SolverCache.hs | 2 +- saw-central/src/SAWCentral/SolverVersions.hs | 2 +- saw-python/saw_client/proofscript.py | 11 ---- saw-python/saw_client/solver_cache.py | 1 - saw-script/src/SAWScript/Interpreter.hs | 65 +------------------ saw-server/src/SAWServer/ProofScript.hs | 7 -- vim-saw/syntax/saw.vim | 2 +- 21 files changed, 18 insertions(+), 167 deletions(-) diff --git a/.github/ci.sh b/.github/ci.sh index ea03eaae36..25268b03bd 100755 --- a/.github/ci.sh +++ b/.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/ diff --git a/CHANGES.md b/CHANGES.md index 2bd61a92e4..80c0b8b066 100644 --- a/CHANGES.md +++ b/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. diff --git a/doc/llvm-java-verification-with-saw/code/NQueens.cry b/doc/llvm-java-verification-with-saw/code/NQueens.cry index b9cb340ee2..5115eb39da 100644 --- a/doc/llvm-java-verification-with-saw/code/NQueens.cry +++ b/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 5. For those sizes, we have had good luck with both Yices and Z3. To do that, diff --git a/doc/llvm-java-verification-with-saw/using-smt-lib-solvers.md b/doc/llvm-java-verification-with-saw/using-smt-lib-solvers.md index a2e73cb9db..d51e017c02 100644 --- a/doc/llvm-java-verification-with-saw/using-smt-lib-solvers.md +++ b/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. diff --git a/doc/saw-lexer/src/saw_lexer.py b/doc/saw-lexer/src/saw_lexer.py index 64bb08073a..e9c5d23cc5 100644 --- a/doc/saw-lexer/src/saw_lexer.py +++ b/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|" diff --git a/doc/saw-user-manual/installing-saw.md b/doc/saw-user-manual/installing-saw.md index 2a93347784..0ebb2ade30 100644 --- a/doc/saw-user-manual/installing-saw.md +++ b/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) diff --git a/doc/saw-user-manual/interactive-proofs.md b/doc/saw-user-manual/interactive-proofs.md index 81e406e012..e5f90f4af1 100644 --- a/doc/saw-user-manual/interactive-proofs.md +++ b/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 diff --git a/examples/misc/external_sat.saw b/examples/misc/external_sat.saw index cc35dcf2b3..377558a041 100644 --- a/examples/misc/external_sat.saw +++ b/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; diff --git a/examples/misc/symbolic_function.saw b/examples/misc/symbolic_function.saw index b1e8cb8b6c..e225951f0d 100644 --- a/examples/misc/symbolic_function.saw +++ b/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 }}; diff --git a/intTests/test1646/test15.log.good b/intTests/test1646/test15.log.good index f62ba6170e..2015856de8 100644 --- a/intTests/test1646/test15.log.good +++ b/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 () diff --git a/intTests/test_search/search03.log.good b/intTests/test_search/search03.log.good index 8ebcfb8adc..77e5cd40a5 100644 --- a/intTests/test_search/search03.log.good +++ b/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 () diff --git a/saw-central/src/SAWCentral/Builtins.hs b/saw-central/src/SAWCentral/Builtins.hs index 50f7f536a8..51c4212b0e 100644 --- a/saw-central/src/SAWCentral/Builtins.hs +++ b/saw-central/src/SAWCentral/Builtins.hs @@ -93,14 +93,12 @@ module SAWCentral.Builtins ( proveBitwuzla, proveBoolector, proveZ3, - proveCVC4, proveCVC5, proveMathSAT, proveYices, proveUnintBitwuzla, proveUnintBoolector, proveUnintZ3, - proveUnintCVC4, proveUnintCVC5, proveUnintMathSAT, proveUnintYices, @@ -108,7 +106,6 @@ module SAWCentral.Builtins ( w4_bitwuzla, w4_boolector, w4_z3, - w4_cvc4, w4_cvc5, w4_yices, w4_unint_bitwuzla, @@ -116,12 +113,10 @@ module SAWCentral.Builtins ( 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" diff --git a/saw-central/src/SAWCentral/Prover/SBV.hs b/saw-central/src/SAWCentral/Prover/SBV.hs index 6b3c0adc37..19904c0d1c 100644 --- a/saw-central/src/SAWCentral/Prover/SBV.hs +++ b/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 diff --git a/saw-central/src/SAWCentral/Prover/What4.hs b/saw-central/src/SAWCentral/Prover/What4.hs index 56c76628c4..2bf0fd29e9 100644 --- a/saw-central/src/SAWCentral/Prover/What4.hs +++ b/saw-central/src/SAWCentral/Prover/What4.hs @@ -13,7 +13,6 @@ module SAWCentral.Prover.What4 ( proveWhat4_bitwuzla, proveWhat4_rme, proveWhat4_boolector, - proveWhat4_cvc4, proveWhat4_cvc5, proveWhat4_dreal, proveWhat4_stp, @@ -23,7 +22,6 @@ module SAWCentral.Prover.What4 ( proveExportWhat4_z3, proveExportWhat4_bitwuzla, proveExportWhat4_boolector, - proveExportWhat4_cvc4, proveExportWhat4_cvc5, proveExportWhat4_dreal, proveExportWhat4_stp, @@ -154,7 +152,7 @@ proveExportWhat4_sym solver hashConsing outFilePath satq = do proveWhat4_z3, proveWhat4_bitwuzla, proveWhat4_boolector, - proveWhat4_cvc4, proveWhat4_cvc5, + proveWhat4_cvc5, proveWhat4_dreal, proveWhat4_stp, proveWhat4_yices, proveWhat4_abc, proveWhat4_rme :: Bool {- ^ Hash-consing of What4 terms -}-> @@ -165,7 +163,6 @@ proveWhat4_z3 = proveWhat4_sym z3Adapter proveWhat4_bitwuzla = proveWhat4_sym bitwuzlaAdapter proveWhat4_rme = proveWhat4_sym rmeAdapter 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 @@ -189,7 +186,7 @@ proveWhat4_z3_using tactic hashConsing satq = do proveExportWhat4_z3, proveExportWhat4_bitwuzla, proveExportWhat4_boolector, - proveExportWhat4_cvc4, proveExportWhat4_cvc5, + proveExportWhat4_cvc5, proveExportWhat4_dreal, proveExportWhat4_stp, proveExportWhat4_yices :: Bool {- ^ Hash-consing of ExportWhat4 terms -}-> FilePath {- ^ Path of file to write SMT to -}-> @@ -199,7 +196,6 @@ proveExportWhat4_z3, proveExportWhat4_z3 = proveExportWhat4_sym z3Adapter proveExportWhat4_bitwuzla = proveExportWhat4_sym bitwuzlaAdapter 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 diff --git a/saw-central/src/SAWCentral/SolverCache.hs b/saw-central/src/SAWCentral/SolverCache.hs index 9768f1ae2f..a6c5d3e5bd 100644 --- a/saw-central/src/SAWCentral/SolverCache.hs +++ b/saw-central/src/SAWCentral/SolverCache.hs @@ -189,7 +189,7 @@ data SolverBackend | ABC | Boolector | Bitwuzla - | CVC4 + | CVC4 -- NOTE: Not supported by SAW anymore | CVC5 | DReal -- NOTE: Not currently supported by SAW | MathSAT diff --git a/saw-central/src/SAWCentral/SolverVersions.hs b/saw-central/src/SAWCentral/SolverVersions.hs index 3786bbd12c..3e42a52719 100644 --- a/saw-central/src/SAWCentral/SolverVersions.hs +++ b/saw-central/src/SAWCentral/SolverVersions.hs @@ -42,7 +42,7 @@ getSolverVersion s = SBV.ABC -> (["s", "-q", "version;quit"], "UC Berkeley, ABC ") SBV.Boolector -> (["--version"] , "") SBV.Bitwuzla -> (["--version"] , "") - SBV.CVC4 -> (["--version"] , "This is CVC4 version ") + SBV.CVC4 -> nope "CVC4" SBV.CVC5 -> (["--version"] , "This is cvc5 version ") SBV.DReal -> (["--version"] , "dReal v") SBV.MathSAT -> (["-version"] , "MathSAT5 version ") diff --git a/saw-python/saw_client/proofscript.py b/saw-python/saw_client/proofscript.py index b160392b49..a4cf51c5d9 100644 --- a/saw-python/saw_client/proofscript.py +++ b/saw-python/saw_client/proofscript.py @@ -45,10 +45,6 @@ class Bitwuzla(UnintProver): def __init__(self, unints : List[str]) -> None: super().__init__("w4-bitwuzla", unints) -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) @@ -65,10 +61,6 @@ class Bitwuzla_SBV(UnintProver): def __init__(self, unints : List[str]) -> None: super().__init__("sbv-bitwuzla", unints) -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) @@ -145,9 +137,6 @@ def to_json(self) -> Any: def bitwuzla(unints : List[str]) -> ProofTactic: return UseProver(Bitwuzla(unints)) -def cvc4(unints : List[str]) -> ProofTactic: - return UseProver(CVC4(unints)) - def cvc5(unints : List[str]) -> ProofTactic: return UseProver(CVC5(unints)) diff --git a/saw-python/saw_client/solver_cache.py b/saw-python/saw_client/solver_cache.py index 907bdb1405..4687b74658 100644 --- a/saw-python/saw_client/solver_cache.py +++ b/saw-python/saw_client/solver_cache.py @@ -18,7 +18,6 @@ Literal["ABC"], Literal["Boolector"], Literal["Bitwuzla"], - Literal["CVC4"], Literal["CVC5"], Literal["DReal"], # NOTE: Not currently supported by SAW Literal["MathSAT"], diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs index f56a0b9720..a51a8cebf9 100644 --- a/saw-script/src/SAWScript/Interpreter.hs +++ b/saw-script/src/SAWScript/Interpreter.hs @@ -2477,10 +2477,6 @@ do_offline_w4_unint_z3 :: [Text] -> Text -> ProofScript () do_offline_w4_unint_z3 unints path = offline_w4_unint_z3 unints (Text.unpack path) -do_offline_w4_unint_cvc4 :: [Text] -> Text -> ProofScript () -do_offline_w4_unint_cvc4 unints path = - offline_w4_unint_cvc4 unints (Text.unpack path) - do_offline_w4_unint_cvc5 :: [Text] -> Text -> ProofScript () do_offline_w4_unint_cvc5 unints path = offline_w4_unint_cvc5 unints (Text.unpack path) @@ -4607,32 +4603,13 @@ primitives = Map.fromList $ , "as SAW 1.6." ] - -- cvc4/5 - - , prim "cvc4" "ProofScript ()" - (pureVal proveCVC4) - WarnDeprecated - [ "Use the CVC4 theorem prover to prove the current goal." - , "" - , "Expected to be hidden by default in SAW 1.6." - , "CVC4 is very obsolete and proofs should be migrated to CVC5." - ] + -- cvc5 , prim "cvc5" "ProofScript ()" (pureVal proveCVC5) Current [ "Use the CVC5 theorem prover to prove the current goal." ] - , prim "unint_cvc4" "[String] -> ProofScript ()" - (pureVal proveUnintCVC4) - WarnDeprecated - [ "Use the CVC4 theorem prover to prove the current goal. Leave the" - , "given list of names as uninterpreted." - , "" - , "Expected to be hidden by default in SAW 1.6." - , "CVC4 is very obsolete and proofs should be migrated to CVC5." - ] - , prim "unint_cvc5" "[String] -> ProofScript ()" (pureVal proveUnintCVC5) Current @@ -4640,30 +4617,11 @@ primitives = Map.fromList $ , "given list of names as uninterpreted." ] - , prim "sbv_cvc4" "ProofScript ()" - (pureVal proveCVC4) - WarnDeprecated - [ "Use the CVC4 theorem prover to prove the current goal." - , "" - , "Expected to be hidden by default in SAW 1.6." - , "CVC4 is very obsolete and proofs should be migrated to CVC5." - ] - , prim "sbv_cvc5" "ProofScript ()" (pureVal proveCVC5) Current [ "Use the CVC5 theorem prover to prove the current goal." ] - , prim "sbv_unint_cvc4" "[String] -> ProofScript ()" - (pureVal proveUnintCVC4) - WarnDeprecated - [ "Use the CVC4 theorem prover to prove the current goal. Leave the" - , "given list of names as uninterpreted." - , "" - , "Expected to be hidden by default in SAW 1.6." - , "CVC4 is very obsolete and proofs should be migrated to CVC5." - ] - , prim "sbv_unint_cvc5" "[String] -> ProofScript ()" (pureVal proveUnintCVC5) Current @@ -4671,16 +4629,6 @@ primitives = Map.fromList $ , "given list of names as uninterpreted." ] - , prim "w4_unint_cvc4" "[String] -> ProofScript ()" - (pureVal w4_unint_cvc4) - WarnDeprecated - [ "Prove the current goal using What4 (CVC4 backend). Leave the" - , "given list of names as uninterpreted." - , "" - , "Expected to be hidden by default in SAW 1.6." - , "CVC4 is very obsolete and proofs should be migrated to CVC5." - ] - , prim "w4_unint_cvc5" "[String] -> ProofScript ()" (pureVal w4_unint_cvc5) Current @@ -4688,17 +4636,6 @@ primitives = Map.fromList $ , "given list of names as uninterpreted." ] - , prim "offline_w4_unint_cvc4" "[String] -> String -> ProofScript ()" - (pureVal do_offline_w4_unint_cvc4) - WarnDeprecated - [ "Write the current goal to the given file using What4 (CVC4" - , "backend) in SMT-Lib2 format. Leave the given list of names" - , "uninterpreted." - , "" - , "Expected to be hidden by default in SAW 1.6." - , "CVC4 is very obsolete and proofs should be migrated to CVC5." - ] - , prim "offline_w4_unint_cvc5" "[String] -> String -> ProofScript ()" (pureVal do_offline_w4_unint_cvc5) Current diff --git a/saw-server/src/SAWServer/ProofScript.hs b/saw-server/src/SAWServer/ProofScript.hs index 438410ac5a..928f9b5eff 100644 --- a/saw-server/src/SAWServer/ProofScript.hs +++ b/saw-server/src/SAWServer/ProofScript.hs @@ -57,7 +57,6 @@ data Prover | SBV_ABC_SMTLib | SBV_Bitwuzla [Text] | SBV_Boolector [Text] - | SBV_CVC4 [Text] | SBV_CVC5 [Text] | SBV_MathSAT [Text] | SBV_Yices [Text] @@ -66,7 +65,6 @@ data Prover | W4_ABC_Verilog | W4_Bitwuzla [Text] | W4_Boolector [Text] - | W4_CVC4 [Text] | W4_CVC5 [Text] | W4_Yices [Text] | W4_Z3 [Text] @@ -92,14 +90,12 @@ instance FromJSON Prover where "abc" -> pure W4_ABC_SMTLib "bitwuzla" -> SBV_Bitwuzla <$> unints "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-bitwuzla" -> SBV_Bitwuzla <$> unints "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 @@ -108,7 +104,6 @@ instance FromJSON Prover where "w4-abc-verilog" -> pure W4_ABC_Verilog "w4-bitwuzla" -> W4_Bitwuzla <$> unints "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 @@ -291,7 +286,6 @@ interpretProofScript (ProofScript ts) = go ts SBV_ABC_SMTLib -> return $ SB.proveABC_SBV SBV_Bitwuzla unints -> return $ SB.proveUnintBitwuzla unints 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 @@ -300,7 +294,6 @@ interpretProofScript (ProofScript ts) = go ts W4_ABC_Verilog -> return $ SB.w4_abc_verilog W4_Bitwuzla unints -> return $ SB.w4_unint_bitwuzla unints 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 diff --git a/vim-saw/syntax/saw.vim b/vim-saw/syntax/saw.vim index cc4e30d9e9..59c2e3b891 100644 --- a/vim-saw/syntax/saw.vim +++ b/vim-saw/syntax/saw.vim @@ -7,4 +7,4 @@ highlight link SAWComment Comment setlocal formatoptions=tcqr " all SAW builtins included: -syn keyword SAWKeyword do let import abc get_opt offline_cnf abstract_symbolic goal_apply offline_cnf_external add_cryptol_defs goal_assume offline_rocq add_cryptol_eqs goal_eval offline_extcore add_prelude_defs goal_eval_unint offline_smtlib2 add_prelude_eqs goal_insert offline_unint_smtlib2 add_x86_preserved_reg goal_intro offline_verilog addsimp goal_num_ite offline_w4_unint_cvc4 addsimp' goal_num_when offline_w4_unint_yices addsimps goal_when offline_w4_unint_z3 addsimps' head parse_core admit hoist_ifs parser_printer_roundtrip approxmc include print assume_unsat java_array print_goal assume_valid java_bool print_goal_consts auto_match java_byte print_goal_depth basic_ss java_char print_goal_size beta_reduce_goal java_class print_term beta_reduce_term java_double print_term_depth boolector java_float print_type caseProofResult java_int prove caseSatResult java_load_class prove_core check_convertible java_long prove_print check_goal java_short qc_print check_term jvm_alloc_array quickcheck codegen jvm_alloc_object read_aig concat jvm_array_is read_bytes core_axiom jvm_elem_is read_core core_thm jvm_execute_func replace crucible_alloc jvm_extract return crucible_alloc_aligned jvm_field_is rewrite crucible_alloc_global jvm_fresh_var rme crucible_alloc_readonly jvm_modifies_elem run crucible_alloc_readonly_aligned jvm_modifies_field sat crucible_alloc_with_size jvm_modifies_static_field sat_print crucible_array jvm_null sbv_abc crucible_conditional_points_to jvm_postcond sbv_boolector crucible_conditional_points_to_untyped jvm_precond sbv_cvc4 crucible_declare_ghost_state jvm_return sbv_mathsat crucible_elem jvm_static_field_is sbv_unint_cvc4 crucible_equal jvm_term sbv_unint_yices crucible_execute_func jvm_unsafe_assume_spec sbv_unint_z3 crucible_field jvm_verify sbv_yices crucible_fresh_cryptol_var lambda sbv_z3 crucible_fresh_expanded_val lambdas set_ascii crucible_fresh_pointer length set_base crucible_fresh_var list_term set_color crucible_ghost_value llvm_alias set_timeout crucible_global llvm_alloc set_x86_stack_base_align crucible_global_initializer llvm_alloc_aligned sharpSAT crucible_java_extract llvm_alloc_global show crucible_llvm_array_size_profile llvm_alloc_readonly show_cfg crucible_llvm_compositional_extract llvm_alloc_readonly_aligned show_term crucible_llvm_extract llvm_alloc_with_size simplify crucible_llvm_unsafe_assume_spec llvm_array skeleton_arg crucible_llvm_verify llvm_array_size_profile skeleton_arg_index crucible_llvm_verify_x86 llvm_array_value skeleton_arg_index_pointer crucible_null llvm_boilerplate skeleton_arg_pointer crucible_packed_struct llvm_cfg skeleton_exec crucible_points_to llvm_compositional_extract skeleton_globals_post crucible_points_to_array_prefix llvm_conditional_points_to skeleton_globals_pre crucible_points_to_untyped llvm_conditional_points_to_at_type skeleton_guess_arg_sizes crucible_postcond llvm_conditional_points_to_untyped skeleton_poststate crucible_precond llvm_declare_ghost_state skeleton_prestate crucible_return llvm_double skeleton_resize_arg crucible_spec_size llvm_elem skeleton_resize_arg_index crucible_spec_solvers llvm_equal split_goal crucible_struct llvm_execute_func str_concat crucible_symbolic_alloc llvm_extract summarize_verification crucible_term llvm_field tail cryptol_add_path llvm_float term_size cryptol_extract llvm_fresh_cryptol_var term_tree_size cryptol_load llvm_fresh_expanded_val test_mr_solver cryptol_prims llvm_fresh_pointer time cryptol_ss llvm_fresh_var trivial cvc4 llvm_ghost_value true default_x86_preserved_reg llvm_global type default_x86_stack_base_align llvm_global_initializer undefined define llvm_int unfold_term disable_crucible_assert_then_assume llvm_load_module unfolding disable_crucible_profiling llvm_null unint_cvc4 disable_smt_array_memory_model llvm_packed_struct_type unint_yices disable_what4_hash_consing llvm_packed_struct_value unint_z3 disable_x86_what4_hash_consing llvm_pointer w4 dsec_print llvm_points_to w4_abc_smtlib2 dump_file_AST llvm_points_to_array_prefix w4_abc_verilog empty_ss llvm_points_to_at_type w4_offline_smtlib2 enable_crucible_assert_then_assume llvm_points_to_untyped w4_unint_cvc4 enable_crucible_profiling llvm_postcond w4_unint_yices enable_deprecated llvm_precond w4_unint_z3 enable_experimental llvm_return with_time enable_lax_arithmetic llvm_sizeof write_aig enable_smt_array_memory_model llvm_spec_size write_aig_external enable_what4_hash_consing llvm_spec_solvers write_cnf enable_x86_what4_hash_consing llvm_struct write_cnf_external env llvm_struct_type write_rocq_cryptol_module eval_bool llvm_struct_value write_rocq_cryptol_primitives_for_sawcore eval_int llvm_symbolic_alloc write_rocq_sawcore_prelude eval_list llvm_term write_rocq_term eval_size llvm_type write_core exec llvm_unsafe_assume_spec write_saig exit llvm_verify write_saig' external_aig_solver llvm_verify_x86 write_smtlib2 external_cnf_solver mathsat write_smtlib2_w4 fails module_skeleton write_verilog false nth yices for null z3 fresh_symbolic offline_aig function_skeleton offline_aig_external +syn keyword SAWKeyword do let import abc get_opt offline_cnf abstract_symbolic goal_apply offline_cnf_external add_cryptol_defs goal_assume offline_rocq add_cryptol_eqs goal_eval offline_extcore add_prelude_defs goal_eval_unint offline_smtlib2 add_prelude_eqs goal_insert offline_unint_smtlib2 add_x86_preserved_reg goal_intro offline_verilog addsimp goal_num_ite addsimp' goal_num_when offline_w4_unint_yices addsimps goal_when offline_w4_unint_z3 addsimps' head parse_core admit hoist_ifs parser_printer_roundtrip approxmc include print assume_unsat java_array print_goal assume_valid java_bool print_goal_consts auto_match java_byte print_goal_depth basic_ss java_char print_goal_size beta_reduce_goal java_class print_term beta_reduce_term java_double print_term_depth boolector java_float print_type caseProofResult java_int prove caseSatResult java_load_class prove_core check_convertible java_long prove_print check_goal java_short qc_print check_term jvm_alloc_array quickcheck codegen jvm_alloc_object read_aig concat jvm_array_is read_bytes core_axiom jvm_elem_is read_core core_thm jvm_execute_func replace crucible_alloc jvm_extract return crucible_alloc_aligned jvm_field_is rewrite crucible_alloc_global jvm_fresh_var rme crucible_alloc_readonly jvm_modifies_elem run crucible_alloc_readonly_aligned jvm_modifies_field sat crucible_alloc_with_size jvm_modifies_static_field sat_print crucible_array jvm_null sbv_abc crucible_conditional_points_to jvm_postcond sbv_boolector crucible_conditional_points_to_untyped jvm_precond crucible_declare_ghost_state jvm_return sbv_mathsat crucible_elem jvm_static_field_is crucible_equal jvm_term sbv_unint_yices crucible_execute_func jvm_unsafe_assume_spec sbv_unint_z3 crucible_field jvm_verify sbv_yices crucible_fresh_cryptol_var lambda sbv_z3 crucible_fresh_expanded_val lambdas set_ascii crucible_fresh_pointer length set_base crucible_fresh_var list_term set_color crucible_ghost_value llvm_alias set_timeout crucible_global llvm_alloc set_x86_stack_base_align crucible_global_initializer llvm_alloc_aligned sharpSAT crucible_java_extract llvm_alloc_global show crucible_llvm_array_size_profile llvm_alloc_readonly show_cfg crucible_llvm_compositional_extract llvm_alloc_readonly_aligned show_term crucible_llvm_extract llvm_alloc_with_size simplify crucible_llvm_unsafe_assume_spec llvm_array skeleton_arg crucible_llvm_verify llvm_array_size_profile skeleton_arg_index crucible_llvm_verify_x86 llvm_array_value skeleton_arg_index_pointer crucible_null llvm_boilerplate skeleton_arg_pointer crucible_packed_struct llvm_cfg skeleton_exec crucible_points_to llvm_compositional_extract skeleton_globals_post crucible_points_to_array_prefix llvm_conditional_points_to skeleton_globals_pre crucible_points_to_untyped llvm_conditional_points_to_at_type skeleton_guess_arg_sizes crucible_postcond llvm_conditional_points_to_untyped skeleton_poststate crucible_precond llvm_declare_ghost_state skeleton_prestate crucible_return llvm_double skeleton_resize_arg crucible_spec_size llvm_elem skeleton_resize_arg_index crucible_spec_solvers llvm_equal split_goal crucible_struct llvm_execute_func str_concat crucible_symbolic_alloc llvm_extract summarize_verification crucible_term llvm_field tail cryptol_add_path llvm_float term_size cryptol_extract llvm_fresh_cryptol_var term_tree_size cryptol_load llvm_fresh_expanded_val test_mr_solver cryptol_prims llvm_fresh_pointer time cryptol_ss llvm_fresh_var trivial llvm_ghost_value true default_x86_preserved_reg llvm_global type default_x86_stack_base_align llvm_global_initializer undefined define llvm_int unfold_term disable_crucible_assert_then_assume llvm_load_module unfolding disable_crucible_profiling llvm_null disable_smt_array_memory_model llvm_packed_struct_type unint_yices disable_what4_hash_consing llvm_packed_struct_value unint_z3 disable_x86_what4_hash_consing llvm_pointer w4 dsec_print llvm_points_to w4_abc_smtlib2 dump_file_AST llvm_points_to_array_prefix w4_abc_verilog empty_ss llvm_points_to_at_type w4_offline_smtlib2 enable_crucible_assert_then_assume llvm_points_to_untyped enable_crucible_profiling llvm_postcond w4_unint_yices enable_deprecated llvm_precond w4_unint_z3 enable_experimental llvm_return with_time enable_lax_arithmetic llvm_sizeof write_aig enable_smt_array_memory_model llvm_spec_size write_aig_external enable_what4_hash_consing llvm_spec_solvers write_cnf enable_x86_what4_hash_consing llvm_struct write_cnf_external env llvm_struct_type write_rocq_cryptol_module eval_bool llvm_struct_value write_rocq_cryptol_primitives_for_sawcore eval_int llvm_symbolic_alloc write_rocq_sawcore_prelude eval_list llvm_term write_rocq_term eval_size llvm_type write_core exec llvm_unsafe_assume_spec write_saig exit llvm_verify write_saig' external_aig_solver llvm_verify_x86 write_smtlib2 external_cnf_solver mathsat write_smtlib2_w4 fails module_skeleton write_verilog false nth yices for null z3 fresh_symbolic offline_aig function_skeleton offline_aig_external From d599804064c3900940ba0623cf2ead2801a20325 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Mon, 19 Jan 2026 11:02:00 -0800 Subject: [PATCH 2/2] Update comment about the nQueens problem size for CVC5 --- doc/llvm-java-verification-with-saw/code/NQueens.cry | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/llvm-java-verification-with-saw/code/NQueens.cry b/doc/llvm-java-verification-with-saw/code/NQueens.cry index 5115eb39da..66e62b4aff 100644 --- a/doc/llvm-java-verification-with-saw/code/NQueens.cry +++ b/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 cvc5 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,