# HG changeset patch
# User desharna
# Date 1759081774 0
# Node ID 4f15c5c3781f6a0ad99e45c3f96c85918418c051
# Parent  06a05e0983476e58ce94c27e5477f67b5de03bd4
added a dummy SMT solver to more efficiently generate SMT-LIB problem files with Mirabelle

diff -r 06a05e098347 -r 4f15c5c3781f src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Sep 25 22:26:31 2025 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Sun Sep 28 17:49:34 2025 +0000
@@ -222,6 +222,7 @@
           SOME pp => pp outer_ctxt replay_data xfacts prems concl lines
         | NONE => {outcome = NONE, fact_ids = NONE, atp_proof = K []})
     | (Time_Out, _) => raise SMT_Failure.SMT (SMT_Failure.Time_Out)
+    | (Unknown, _) => raise SMT_Failure.SMT (SMT_Failure.Other_Failure "Unknown")
     | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
 
   fun replay outcome replay0 oracle outer_ctxt
@@ -236,6 +237,7 @@
           | NONE => error "No proof reconstruction for solver -- \
             \declare [[smt_oracle]] to allow oracle")
     | (Time_Out, _) => raise SMT_Failure.SMT (SMT_Failure.Time_Out)
+    | (Unknown, _) => raise SMT_Failure.SMT (SMT_Failure.Other_Failure "Unknown")
     | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
 
   val cfalse = Thm.cterm_of \<^context> \<^prop>\<open>False\<close>
diff -r 06a05e098347 -r 4f15c5c3781f src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Thu Sep 25 22:26:31 2025 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Sun Sep 28 17:49:34 2025 +0000
@@ -287,6 +287,22 @@
 
 end
 
+
+(* Dummy SMT solvers *)
+
+val dummy_smtlib: SMT_Solver.solver_config =
+  {
+    name = "dummy_smtlib",
+    class = K SMTLIB_Interface.smtlibC,
+    avail = make_avail "DUMMY_SMTLIB",
+    command = make_command "DUMMY_SMTLIB",
+    options = K [],
+    smt_options = [],
+    good_slices = [((2, false, false, 1024, meshN), [])],
+    outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
+    parse_proof = NONE,
+    replay = NONE }
+
 (* smt tactic *)
 val parse_smt_options =
   Scan.optional
@@ -330,6 +346,7 @@
   SMT_Solver.add_solver vampire_smt_dt #>
   SMT_Solver.add_solver vampire_smt_nodt #>
   SMT_Solver.add_solver veriT #>
-  SMT_Solver.add_solver z3)
+  SMT_Solver.add_solver z3 #>
+  SMT_Solver.add_solver dummy_smtlib)
 
 end;
diff -r 06a05e098347 -r 4f15c5c3781f src/HOL/Tools/etc/settings
--- a/src/HOL/Tools/etc/settings	Thu Sep 25 22:26:31 2025 +0200
+++ b/src/HOL/Tools/etc/settings	Sun Sep 28 17:49:34 2025 +0000
@@ -1,3 +1,4 @@
 # -*- shell-script -*- :mode=shellscript:
 
 ISABELLE_ATP="$COMPONENT/ATP"
+DUMMY_SMTLIB_SOLVER="$COMPONENT/SMT/scripts/dummy_smtlib_solver"