# HG changeset patch
# User blanchet
# Date 1708071885 -3600
# Node ID e905fb37467ff5318918f07a43d8b3b7cf162b59
# Parent  e413c94b192a399bb1b477221b9bb29d0244c3aa
Distinguish two versions of cvc5 -- one used for Sledgehammer, one for proof reconstruction in SMT. provided by Mathias Fleury

diff -r e413c94b192a -r e905fb37467f src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Thu Feb 15 13:00:56 2024 +0100
+++ b/src/HOL/SMT.thy	Fri Feb 16 09:24:45 2024 +0100
@@ -720,7 +720,8 @@
 \<close>
 
 declare [[cvc4_options = ""]]
-declare [[cvc5_options = "--proof-format-mode=alethe --proof-granularity=dsl-rewrite"]]
+declare [[cvc5_options = ""]]
+declare [[cvc5_proof_options = "--proof-format-mode=alethe --proof-granularity=dsl-rewrite"]]
 declare [[verit_options = ""]]
 declare [[z3_options = ""]]
 
diff -r e413c94b192a -r e905fb37467f src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Thu Feb 15 13:00:56 2024 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Fri Feb 16 09:24:45 2024 +0100
@@ -121,6 +121,30 @@
   avail = make_avail "CVC5",
   command = make_command "CVC5",
   options = cvc5_options,
+  smt_options = [(":produce-unsat-cores", "true")],
+  good_slices =
+    (* FUDGE *)
+    [((2, false, false, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
+     ((2, false, false, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
+     ((2, false, true, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
+     ((2, false, false, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
+     ((2, false, false, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
+     ((2, false, false, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
+     ((2, false, false, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
+  outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
+  parse_proof = SOME (K CVC_Proof_Parse.parse_proof),
+  replay = NONE }
+
+(*
+We need different options for alethe proof production by cvc5 and the smt_options
+cannot be changed, so different configuration.
+*)
+val cvc5_proof: SMT_Solver.solver_config = {
+  name = "cvc5_proof",
+  class = select_class,
+  avail = make_avail "CVC5",
+  command = make_command "CVC5",
+  options = cvc5_options,
   smt_options = [(":produce-proofs", "true")],
   good_slices =
     (* FUDGE *)
@@ -231,7 +255,11 @@
 fun smt_method ((solver, stgy), thms) ctxt facts =
   let
     val default_solver = SMT_Config.solver_of ctxt
-    val solver = the_default default_solver solver
+    val solver =
+      (case solver of
+        NONE => default_solver
+      | SOME "cvc5" => "cvc5_proof"
+      | SOME a => a)
     val _ = 
       if solver = "z3" andalso stgy <> NONE
       then warning ("No strategy is available for z3. Ignoring " ^ quote (the stgy)) 
@@ -257,6 +285,7 @@
 val _ = Theory.setup (
   SMT_Solver.add_solver cvc4 #>
   SMT_Solver.add_solver cvc5 #>
+  SMT_Solver.add_solver cvc5_proof #>
   SMT_Solver.add_solver veriT #>
   SMT_Solver.add_solver z3)