src/HOL/Tools/SMT/smt_systems.ML

--- a/src/HOL/Tools/SMT/smt_systems.ML	Thu Aug 11 13:23:00 2022 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Fri Aug 12 15:35:07 2022 +0200
@@ -6,7 +6,7 @@
 
 signature SMT_SYSTEMS =
 sig
-  val cvc4_extensions: bool Config.T
+  val cvc_extensions: bool Config.T
   val z3_extensions: bool Config.T
 end;
 
@@ -59,9 +59,9 @@
   on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines)
 
 
-(* CVC4 *)
+(* CVC4 and cvc5 *)
 
-val cvc4_extensions = Attrib.setup_config_bool \<^binding>\<open>cvc4_extensions\<close> (K false)
+val cvc_extensions = Attrib.setup_config_bool \<^binding>\<open>cvc_extensions\<close> (K false)
 
 local
   fun cvc4_options ctxt =
@@ -72,12 +72,20 @@
       NONE => []
     | SOME t => ["--tlimit", string_of_int (Time.toMilliseconds t)])
 
+  fun cvc5_options ctxt =
+    ["--no-stats",
+     "--sat-random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
+     "--lang=smt2"] @
+    (case SMT_Config.get_timeout ctxt of
+      NONE => []
+    | SOME t => ["--tlimit", string_of_int (Time.toMilliseconds t)])
+
   fun select_class ctxt =
-    if Config.get ctxt cvc4_extensions then
+    if Config.get ctxt cvc_extensions then
       if Config.get ctxt SMT_Config.higher_order then
-        CVC4_Interface.hosmtlib_cvc4C
+        CVC_Interface.hosmtlib_cvcC
       else
-        CVC4_Interface.smtlib_cvc4C
+        CVC_Interface.smtlib_cvcC
     else
       if Config.get ctxt SMT_Config.higher_order then
         SMTLIB_Interface.hosmtlibC
@@ -104,7 +112,27 @@
      ((1, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
      ((1, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
-  parse_proof = SOME (K CVC4_Proof_Parse.parse_proof),
+  parse_proof = SOME (K CVC_Proof_Parse.parse_proof),
+  replay = NONE }
+
+val cvc5: SMT_Solver.solver_config = {
+  name = "cvc5",
+  class = select_class,
+  avail = make_avail "CVC5",
+  command = make_command "CVC5",
+  options = cvc5_options,
+  smt_options = [(":produce-unsat-cores", "true")],
+  good_slices =
+    (* FUDGE *)
+    [((1, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
+     ((1, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
+     ((1, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
+     ((1, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
+     ((1, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
+     ((1, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
+     ((1, 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 }
 
 end
@@ -228,6 +256,7 @@
 
 val _ = Theory.setup (
   SMT_Solver.add_solver cvc4 #>
+  SMT_Solver.add_solver cvc5 #>
   SMT_Solver.add_solver veriT #>
   SMT_Solver.add_solver z3)