# HG changeset patch # User desharna # Date 1606832994 -3600 # Node ID e732c98b02e63da6c0185792ecaa570234e5e848 # Parent 402afc68f2f9ac645b9f556218d1f0a0f109cd1e tuned proof preplay to explicitly refer to Z3 backend diff -r 402afc68f2f9 -r e732c98b02e6 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r 402afc68f2f9 -r e732c98b02e6 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- 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 diff -r 402afc68f2f9 -r e732c98b02e6 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- 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 diff -r 402afc68f2f9 -r e732c98b02e6 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- 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;