--- a/Admin/components/main Thu Jan 30 22:29:45 2025 +0100
+++ b/Admin/components/main Wed Jan 08 15:19:37 2025 +0100
@@ -3,7 +3,7 @@
bash_process-20240326
bib2xhtml-20190409
csdp-6.1.1
-cvc4-1.8
+cvc5-1.2.0-1
e-3.1-1
elm-0.19.1
easychair-3.5
--- a/NEWS Thu Jan 30 22:29:45 2025 +0100
+++ b/NEWS Wed Jan 08 15:19:37 2025 +0100
@@ -245,6 +245,7 @@
* Sledgehammer:
- Update of bundled provers:
. E 3.1 -- with patch on Windows/Cygwin for proper interrupts
+ . cvc5 1.2.0 -- with support for arm64-linux
- Added instantiations of facts using the "of" attribute
(e.g. "assms(1)[of x]"), which can be activated using the
Sledgehammer option "instantiate" (default: smart, i.e. only if
--- a/src/HOL/Nunchaku.thy Thu Jan 30 22:29:45 2025 +0100
+++ b/src/HOL/Nunchaku.thy Wed Jan 08 15:19:37 2025 +0100
@@ -11,7 +11,7 @@
The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to
the directory containing the "nunchaku" executable. The Isabelle components
-for CVC4, Kodkodi, and SMBC are necessary to use these backend solvers.
+for cvc5, Kodkodi, and SMBC are necessary to use these backend solvers.
*)
theory Nunchaku
--- a/src/HOL/TPTP/atp_problem_import.ML Thu Jan 30 22:29:45 2025 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Wed Jan 08 15:19:37 2025 +0100
@@ -239,7 +239,7 @@
(auto_tac lthy THEN ALLGOALS (atp_tac lthy 0 [] (timeout div 5) assms ATP_Proof.spassN))
ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac lthy i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" lthy i)
- ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc4" (smt_solver_tac "cvc4" lthy i)
+ ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc5" (smt_solver_tac "cvc5" lthy i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac lthy i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac lthy i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac lthy [] i)
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Jan 30 22:29:45 2025 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Jan 08 15:19:37 2025 +0100
@@ -43,7 +43,7 @@
val agsyholN : string
val alt_ergoN : string
- val cvc4N : string
+ val cvc5N : string
val eN : string
val iproverN : string
val leo2N : string
@@ -111,7 +111,7 @@
val agsyholN = "agsyhol"
val alt_ergoN = "alt_ergo"
-val cvc4N = "cvc4"
+val cvc5N = "cvc5"
val eN = "e"
val iproverN = "iprover"
val leo2N = "leo2"
--- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Thu Jan 30 22:29:45 2025 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Wed Jan 08 15:19:37 2025 +0100
@@ -30,7 +30,7 @@
("max_genuine", "1"),
("max_potential", "1"),
("overlord", "false"),
- ("solvers", "cvc4 kodkod paradox smbc"),
+ ("solvers", "cvc5 kodkod paradox smbc"),
("specialize", "true"),
("spy", "false"),
("timeout", "30"),
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Thu Jan 30 22:29:45 2025 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Wed Jan 08 15:19:37 2025 +0100
@@ -86,7 +86,7 @@
else
let
val bash_cmd =
- "PATH=\"$CVC4_HOME:$KODKODI/bin:$SMBC_HOME:$PATH\" \"$" ^
+ "PATH=\"$CVC5_HOME:$KODKODI/bin:$SMBC_HOME:$PATH\" \"$" ^
nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
(if specialize then "" else "--no-specialize ") ^
"--solvers \"" ^ space_implode "," (map Bash.string solvers) ^ "\" " ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jan 30 22:29:45 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jan 08 15:19:37 2025 +0100
@@ -388,10 +388,10 @@
val default_slice_schedule =
(* FUDGE (loosely inspired by Seventeen evaluation) *)
- [cvc4N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc4N, zipperpositionN,
- cvc4N, eN, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN, cvc4N, iproverN, zipperpositionN,
+ [cvc5N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc5N, zipperpositionN,
+ cvc5N, eN, zipperpositionN, vampireN, cvc5N, cvc5N, vampireN, cvc5N, iproverN, zipperpositionN,
spassN, vampireN, zipperpositionN, vampireN, zipperpositionN, z3N, zipperpositionN, vampireN,
- iproverN, spassN, zipperpositionN, vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N,
+ iproverN, spassN, zipperpositionN, vampireN, cvc5N, zipperpositionN, z3N, z3N, cvc5N,
zipperpositionN]
fun schedule_of_provers provers num_slices =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Jan 30 22:29:45 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Jan 08 15:19:37 2025 +0100
@@ -315,7 +315,7 @@
val leo3_config : atp_config =
{exec = (["LEO3_HOME"], ["leo3"]),
arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn problem =>
- [File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC4_SOLVER\" --atp e=\"$E_HOME\"/eprover \
+ [File.bash_path problem ^ " " ^ "--atp cvc=\"$CVC5_SOLVER\" --atp e=\"$E_HOME\"/eprover \
\-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^
(if full_proofs then "--nleq --naeq " else "")],
proof_delims = tstp_proof_delims,
--- a/src/HOL/Tools/etc/options Thu Jan 30 22:29:45 2025 +0100
+++ b/src/HOL/Tools/etc/options Wed Jan 08 15:19:37 2025 +0100
@@ -26,7 +26,7 @@
section "Miscellaneous Tools"
-public option sledgehammer_provers : string = "cvc4 verit z3 e spass vampire zipperposition"
+public option sledgehammer_provers : string = "cvc5 verit z3 e spass vampire zipperposition"
-- "provers for Sledgehammer (separated by blanks)"
public option sledgehammer_timeout : int = 30