--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Nov 30 22:00:23 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Dec 01 15:29:54 2020 +0100
@@ -160,7 +160,7 @@
fun massage_methods (meths as meth :: _) =
if not try0 then [meth]
- else if smt_proofs then SMT_Method SMT_Default :: meths
+ else if smt_proofs then SMT_Method SMT_Z3 :: meths
else meths
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Nov 30 22:00:23 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Dec 01 15:29:54 2020 +0100
@@ -10,7 +10,7 @@
type stature = ATP_Problem_Generate.stature
datatype SMT_backend =
- SMT_Default |
+ SMT_Z3 |
SMT_Verit of string
datatype proof_method =
@@ -53,7 +53,7 @@
open ATP_Proof_Reconstruct
datatype SMT_backend =
- SMT_Default |
+ SMT_Z3 |
SMT_Verit of string
datatype proof_method =
@@ -101,7 +101,7 @@
| Metis_Method (type_enc_opt, lam_trans_opt) =>
"metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
| Meson_Method => "meson"
- | SMT_Method SMT_Default => "smt"
+ | SMT_Method SMT_Z3 => "smt (z3)"
| SMT_Method (SMT_Verit strategy) =>
"smt (" ^ commas ("verit" :: (if strategy = "default" then [] else [strategy])) ^ ")"
| SATx_Method => "satx"
@@ -130,7 +130,7 @@
global_facts) ctxt local_facts)
end
- fun tac_of_smt SMT_Default = SMT_Solver.smt_tac
+ fun tac_of_smt SMT_Z3 = SMT_Solver.smt_tac
| tac_of_smt (SMT_Verit strategy) = Verit_Proof.verit_tac_stgy strategy
in
(case meth of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Nov 30 22:00:23 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Tue Dec 01 15:29:54 2020 +0100
@@ -177,7 +177,7 @@
val smt_methodss =
if smt_proofs then
- [SMT_Method SMT_Default ::
+ [SMT_Method SMT_Z3 ::
map (fn strategy => SMT_Method (SMT_Verit strategy))
(Verit_Proof.all_veriT_stgies (Context.Proof ctxt))]
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Nov 30 22:00:23 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Tue Dec 01 15:29:54 2020 +0100
@@ -202,7 +202,7 @@
val _ = found_proof ();
val preferred =
if smt_proofs then
- SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Default)
+ SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Z3)
else
Metis_Method (NONE, NONE);
val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN;