--- a/src/Doc/Sledgehammer/document/root.tex Mon Jan 31 16:09:23 2022 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Jan 31 16:09:23 2022 +0100
@@ -734,12 +734,6 @@
\texttt{Z3\_SOLVER} to the complete path of the executable, including the
file name.
-\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to
-be an ATP, exploiting Z3's support for the TPTP typed first-order format (TF0).
-It is included for experimental purposes. To use it, set the environment
-variable \texttt{Z3\_TPTP\_HOME} to the directory that contains the
-\texttt{z3\_tptp} executable.
-
\item[\labelitemi] \textbf{\textit{zipperposition}:} Zipperposition
\cite{cruanes-2014} is a higher-order superposition prover developed by Simon
Cruanes, Petar Vukmirovi\'c, and colleagues. To use Zipperposition, set the
--- a/src/HOL/TPTP/atp_problem_import.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Mon Jan 31 16:09:23 2022 +0100
@@ -214,7 +214,6 @@
slice 2 0 ATP_Proof.spassN
ORELSE slice 2 0 ATP_Proof.vampireN
ORELSE slice 2 0 ATP_Proof.eN
- ORELSE slice 2 0 ATP_Proof.z3_tptpN
ORELSE slice 1 1 ATP_Proof.spassN
ORELSE slice 1 2 ATP_Proof.eN
ORELSE slice 1 1 ATP_Proof.vampireN
--- a/src/HOL/Tools/ATP/atp_proof.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Jan 31 16:09:23 2022 +0100
@@ -54,7 +54,6 @@
val veritN : string
val waldmeisterN : string
val z3N : string
- val z3_tptpN : string
val zipperpositionN : string
val remote_prefix : string
val dummy_fofN : string
@@ -65,7 +64,6 @@
val spass_input_rule : string
val spass_pre_skolemize_rule : string
val spass_skolemize_rule : string
- val z3_tptp_core_rule : string
val short_output : bool -> string -> string
val string_of_atp_failure : atp_failure -> string
@@ -121,7 +119,6 @@
val veritN = "verit"
val waldmeisterN = "waldmeister"
val z3N = "z3"
-val z3_tptpN = "z3_tptp"
val zipperpositionN = "zipperposition"
val remote_prefix = "remote_"
@@ -133,7 +130,6 @@
val spass_input_rule = "Inp"
val spass_pre_skolemize_rule = "__Sko0" (* arbitrary *)
val spass_skolemize_rule = "__Sko" (* arbitrary *)
-val z3_tptp_core_rule = "__z3_tptp_core" (* arbitrary *)
exception UNRECOGNIZED_ATP_PROOF of unit
@@ -262,7 +258,7 @@
(**** PARSING OF TSTP FORMAT ****)
(* Strings enclosed in single quotes (e.g., file names), identifiers possibly starting
- with "$" and possibly with "!" in them (for "z3_tptp"). *)
+ with "$" and possibly with "!" in them. *)
val scan_general_id =
$$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
|| (Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode))
@@ -645,15 +641,9 @@
fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, [])
-(* Syntax: SZS core <name> ... <name> *)
-fun parse_z3_tptp_core_line x =
- (Scan.this_string "SZS core" |-- Scan.repeat ($$ " " |-- scan_general_id)
- >> map (core_inference z3_tptp_core_rule)) x
-
fun parse_line local_name problem =
(* Satallax is handled separately, in "atp_satallax.ML". *)
if local_name = spassN then parse_spass_line
- else if local_name = z3_tptpN then parse_z3_tptp_core_line
else parse_tstp_line problem
fun core_of_agsyhol_proof s =
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
@@ -379,10 +379,9 @@
(override_params prover type_enc (my_timeout time_slice)) fact_override []
in
if meth = "sledgehammer_tac" then
- sledge_tac 0.2 ATP_Proof.vampireN "mono_native"
- ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??"
- ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native"
- ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??"
+ sledge_tac 0.25 ATP_Proof.vampireN "mono_native"
+ ORELSE' sledge_tac 0.25 ATP_Proof.eN "poly_guards??"
+ ORELSE' sledge_tac 0.25 ATP_Proof.spassN "mono_native"
ORELSE' SMT_Solver.smt_tac ctxt thms
else if meth = "smt" then
SMT_Solver.smt_tac ctxt thms
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Jan 31 16:09:23 2022 +0100
@@ -498,27 +498,6 @@
val vampire = (vampireN, fn () => vampire_config)
-(* Z3 with TPTP syntax (half experimental, half legacy) *)
-
-val z3_tptp_config : atp_config =
- {exec = (["Z3_TPTP_HOME"], ["z3_tptp"]),
- arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
- ["-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ File.bash_path problem],
- proof_delims = [("SZS status Theorem", "")],
- known_failures = known_szs_status_failures,
- prem_role = Hypothesis,
- good_slices =
- (* FUDGE *)
- K [((250, meshN), (TF0, "mono_native", combsN, false, "")),
- ((125, mepoN), (TF0, "mono_native", combsN, false, "")),
- ((62, mashN), (TF0, "mono_native", combsN, false, "")),
- ((31, meshN), (TF0, "mono_native", combsN, false, ""))],
- good_max_mono_iters = default_max_mono_iters,
- good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
-
-val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
-
-
(* Zipperposition *)
val zipperposition_config : atp_config =
@@ -704,7 +683,7 @@
end
val local_atps =
- [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition]
+ [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, zipperposition]
val remote_atps =
[remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
remote_waldmeister, remote_zipperposition, dummy_fof, dummy_tfx, dummy_thf, dummy_thf_reduced]