# HG changeset patch
# User wenzelm
# Date 1736345977 -3600
# Node ID bbda3b4f3c99653f13b2496d62f3b17ef9c06bb0
# Parent  9601f5582f33544199fa8de854952abe43320974
switch from CVC5 to cvc5, including updates of internal tool references;

diff -r 9601f5582f33 -r bbda3b4f3c99 Admin/components/main
--- 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
diff -r 9601f5582f33 -r bbda3b4f3c99 NEWS
--- 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
diff -r 9601f5582f33 -r bbda3b4f3c99 src/HOL/Nunchaku.thy
--- 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
diff -r 9601f5582f33 -r bbda3b4f3c99 src/HOL/TPTP/atp_problem_import.ML
--- 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)
diff -r 9601f5582f33 -r bbda3b4f3c99 src/HOL/Tools/ATP/atp_proof.ML
--- 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"
diff -r 9601f5582f33 -r bbda3b4f3c99 src/HOL/Tools/Nunchaku/nunchaku_commands.ML
--- 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"),
diff -r 9601f5582f33 -r bbda3b4f3c99 src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- 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) ^ "\" " ^
diff -r 9601f5582f33 -r bbda3b4f3c99 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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 =
diff -r 9601f5582f33 -r bbda3b4f3c99 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- 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,
diff -r 9601f5582f33 -r bbda3b4f3c99 src/HOL/Tools/etc/options
--- 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