# HG changeset patch # User blanchet # Date 1643641763 -3600 # Node ID e5750bcb8c412c7f5a4038c35128e46850378f86 # Parent 46e3a423a7871126ad0c4698f9203eae100153f8 removed experimental prover z3_tptp diff -r 46e3a423a787 -r e5750bcb8c41 src/Doc/Sledgehammer/document/root.tex --- 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 diff -r 46e3a423a787 -r e5750bcb8c41 src/HOL/TPTP/atp_problem_import.ML --- 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 diff -r 46e3a423a787 -r e5750bcb8c41 src/HOL/Tools/ATP/atp_proof.ML --- 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 ... *) -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 = diff -r 46e3a423a787 -r e5750bcb8c41 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- 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 diff -r 46e3a423a787 -r e5750bcb8c41 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- 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]