--- a/src/Doc/Sledgehammer/document/root.tex Thu Oct 08 17:02:56 2020 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Oct 08 17:46:03 2020 +0200
@@ -869,10 +869,6 @@
\item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III
runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
-\item[\labelitemi] \textbf{\textit{remote\_pirate}:} Pirate is a
-highly experimental first-order resolution prover developed by Daniel Wand.
-The remote version of Pirate run on a private server he generously set up.
-
\item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a first-order
resolution prover developed by Stickel et al.\ \cite{snark}. The remote
version of SNARK runs on Geoff Sutcliffe's Miami servers.
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Oct 08 17:02:56 2020 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Oct 08 17:46:03 2020 +0200
@@ -57,7 +57,7 @@
int Symtab.table -> string atp_proof -> (term, string) atp_step list
val repair_waldmeister_endgame : (term, 'a) atp_step list -> (term, 'a) atp_step list
val infer_formulas_types : Proof.context -> term list -> term list
- val introduce_spassy_skolems : (term, string) atp_step list -> (term, string) atp_step list
+ val introduce_spass_skolems : (term, string) atp_step list -> (term, string) atp_step list
val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list ->
(term, string) atp_step list
end;
@@ -710,7 +710,7 @@
subst_vars ([], subst) t
end
-fun introduce_spassy_skolems proof =
+fun introduce_spass_skolems proof =
let
fun add_skolem (Free (s, _)) = String.isPrefix spass_skolem_prefix s ? insert (op =) s
| add_skolem _ = I
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Oct 08 17:02:56 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Oct 08 17:46:03 2020 +0200
@@ -83,8 +83,8 @@
best_max_mono_iters : int,
best_max_new_mono_instances : int}
-(* "best_slices" must be found empirically, taking a wholistic approach since
- the ATPs are run in parallel. Each slice has the format
+(* "best_slices" must be found empirically, taking a holistic approach since the
+ ATPs are run in parallel. Each slice has the format
(time_frac, ((max_facts, fact_filter), format, type_enc,
lam_trans, uncurried_aliases), extra)
@@ -581,21 +581,6 @@
val zipperposition = (zipperpositionN, fn () => zipperposition_config)
-(* Remote Pirate invocation *)
-
-val remote_pirate_config : atp_config =
- {exec = K (["ISABELLE_ATP"], ["scripts/remote_pirate"]),
- arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
- string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
- proof_delims = [("Involved clauses:", "Involved clauses:")],
- known_failures = known_szs_status_failures,
- prem_role = #prem_role spass_config,
- best_slices = K [(1.0, (((200, ""), DFG Polymorphic, "tc_native", combsN, true), ""))],
- best_max_mono_iters = default_max_mono_iters,
- best_max_new_mono_instances = default_max_new_mono_instances}
-val remote_pirate = (remote_prefix ^ pirateN, fn () => remote_pirate_config)
-
-
(* Remote ATP invocation via SystemOnTPTP *)
val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list)
@@ -725,7 +710,7 @@
let val ord = Config.get ctxt term_order in
if ord = smartN then
{is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN),
- gen_simp = String.isSuffix pirateN atp}
+ gen_simp = false}
else
let val is_lpo = String.isSubstring lpoN ord in
{is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
@@ -736,8 +721,7 @@
val atps =
[agsyhol, alt_ergo, e, e_par, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp,
zipperposition, remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2,
- remote_leo3, remote_pirate, remote_snark, remote_vampire, remote_waldmeister,
- remote_zipperposition]
+ remote_leo3, remote_snark, remote_vampire, remote_waldmeister, remote_zipperposition]
val _ = Theory.setup (fold add_atp atps)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 08 17:02:56 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 08 17:46:03 2020 +0200
@@ -50,7 +50,6 @@
val e_definition_rule = "definition"
val e_skolemize_rule = "skolemize"
val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg"
-val pirate_datatype_rule = "DT"
val satallax_skolemize_rule = "tab_ex"
val vampire_skolemisation_rule = "skolemisation"
val veriT_la_generic_rule = "la_generic"
@@ -72,7 +71,6 @@
fun is_arith_rule rule =
String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse
rule = veriT_la_generic_rule
-val is_datatype_rule = String.isPrefix pirate_datatype_rule
fun raw_label_of_num num = (num, 0)
@@ -123,8 +121,7 @@
if is_duplicate orelse
(role = Plain andalso not (is_skolemize_rule rule) andalso
not (is_ext_rule rule) andalso not (is_arith_rule rule) andalso
- not (is_datatype_rule rule) andalso not (null lines) andalso looks_boring () andalso
- not (is_before_skolemize_rule ())) then
+ not (null lines) andalso looks_boring () andalso not (is_before_skolemize_rule ())) then
add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
else
add_lines_pass2 (line :: res) lines
@@ -139,7 +136,6 @@
val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods
-val datatype_methods = [Simp_Method, Simp_Size_Method]
val systematic_methods =
basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @
[Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)]
@@ -319,7 +315,6 @@
val meths =
(if skolem then skolem_methods
else if is_arith_rule rule then arith_methods
- else if is_datatype_rule rule then datatype_methods
else systematic_methods')
|> massage_methods
@@ -388,7 +383,7 @@
fun str_of_preplay_outcome outcome =
if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
fun str_of_meth l meth =
- string_of_proof_method ctxt [] meth ^ " " ^
+ string_of_proof_method [] meth ^ " " ^
str_of_preplay_outcome
(preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
fun comment_of l = map (str_of_meth l) #> commas
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Thu Oct 08 17:02:56 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Thu Oct 08 17:46:03 2020 +0200
@@ -315,7 +315,7 @@
fun of_method ls ss meth =
let val direct = is_proof_method_direct meth in
using_facts ls (if direct then [] else ss) ^
- "by " ^ string_of_proof_method ctxt (if direct then ss else []) meth
+ "by " ^ string_of_proof_method (if direct then ss else []) meth
end
fun of_free (s, T) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Oct 08 17:02:56 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Oct 08 17:46:03 2020 +0200
@@ -16,7 +16,6 @@
SATx_Method |
Blast_Method |
Simp_Method |
- Simp_Size_Method |
Auto_Method |
Fastforce_Method |
Force_Method |
@@ -35,7 +34,7 @@
val is_proof_method_direct : proof_method -> bool
val proof_method_distinguishes_chained_and_direct : proof_method -> bool
- val string_of_proof_method : Proof.context -> string list -> proof_method -> string
+ val string_of_proof_method : string list -> proof_method -> string
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
val string_of_play_outcome : play_outcome -> string
val play_outcome_ord : play_outcome ord
@@ -56,7 +55,6 @@
SATx_Method |
Blast_Method |
Simp_Method |
- Simp_Size_Method |
Auto_Method |
Fastforce_Method |
Force_Method |
@@ -77,11 +75,9 @@
| is_proof_method_direct Meson_Method = true
| is_proof_method_direct SMT_Method = true
| is_proof_method_direct Simp_Method = true
- | is_proof_method_direct Simp_Size_Method = true
| is_proof_method_direct _ = false
fun proof_method_distinguishes_chained_and_direct Simp_Method = true
- | proof_method_distinguishes_chained_and_direct Simp_Size_Method = true
| proof_method_distinguishes_chained_and_direct _ = false
fun is_proof_method_multi_goal Auto_Method = true
@@ -89,7 +85,7 @@
fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
-fun string_of_proof_method ctxt ss meth =
+fun string_of_proof_method ss meth =
let
val meth_s =
(case meth of
@@ -101,7 +97,6 @@
| SATx_Method => "satx"
| Blast_Method => "blast"
| Simp_Method => if null ss then "simp" else "simp add:"
- | Simp_Size_Method => "simp add: " ^ short_thm_name ctxt @{thm size_ne_size_imp_ne}
| Auto_Method => "auto"
| Fastforce_Method => "fastforce"
| Force_Method => "force"
@@ -130,8 +125,6 @@
(case meth of
Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
| Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
- | Simp_Size_Method =>
- Simplifier.asm_full_simp_tac (ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts))
| _ =>
Method.insert_tac ctxt global_facts THEN'
(case meth of
@@ -174,7 +167,7 @@
(extras, [])
in
(if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^
- apply_on_subgoal i n ^ string_of_proof_method ctxt direct_ss meth ^
+ apply_on_subgoal i n ^ string_of_proof_method direct_ss meth ^
(if is_proof_method_multi_goal meth andalso n <> 1 then "[1]" else "")
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Oct 08 17:02:56 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Oct 08 17:46:03 2020 +0200
@@ -141,7 +141,6 @@
val full_proofs = isar_proofs |> the_default (mode = Minimize)
val local_name = perhaps (try (unprefix remote_prefix)) name
- val spassy = (local_name = pirateN orelse local_name = spassN)
val completish = Config.get ctxt atp_completish
val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer
@@ -378,7 +377,7 @@
val atp_proof =
atp_proof
|> termify_atp_proof ctxt name format type_enc pool lifted sym_tab
- |> spassy ? introduce_spassy_skolems
+ |> local_name = spassN ? introduce_spass_skolems
|> factify_atp_proof (map fst used_from) hyp_ts concl_t
in
(verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,