--- a/src/Doc/Sledgehammer/document/root.tex Tue Mar 03 16:37:45 2015 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Tue Mar 03 16:37:45 2015 +0100
@@ -920,6 +920,10 @@
\item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
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\_satallax}:} The remote version of
Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
@@ -928,11 +932,6 @@
TPTP typed first-order format (TFF0). The remote version of SNARK runs on
Geoff Sutcliffe's Miami servers.
-\item[\labelitemi] \textbf{\textit{remote\_spass\_pirate}:} SPASS-Pirate is a
-highly experimental first-order resolution prover developed by Daniel Wand.
-The remote version of SPASS-Pirate run on a private server set up by Daniel
-Wand.
-
\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
Vampire runs on Geoff Sutcliffe's Miami servers.
@@ -944,9 +943,9 @@
\end{enum}
By default, Sledgehammer runs a subset of CVC4, E, E-SInE, SPASS, Vampire,
-veriT, and Z3 in parallel---either locally or remotely, depending on the number
-of processor cores available and on which provers are actually installed.
-It is generally a good idea to run several provers in parallel.
+veriT, and Z3 in parallel, either locally or remotely---depending on the number
+of processor cores available and on which provers are actually installed. It is
+generally a good idea to run several provers in parallel.
\opnodefault{prover}{string}
Alias for \textit{provers}.
--- a/src/HOL/TPTP/atp_theory_export.ML Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Tue Mar 03 16:37:45 2015 +0100
@@ -36,7 +36,7 @@
fun atp_of_format (THF (Polymorphic, _)) = dummy_thfN
| atp_of_format (THF (Monomorphic, _)) = satallaxN
- | atp_of_format (DFG Polymorphic) = spass_pirateN
+ | atp_of_format (DFG Polymorphic) = pirateN
| atp_of_format (DFG Monomorphic) = spassN
| atp_of_format (TFF Polymorphic) = alt_ergoN
| atp_of_format (TFF Monomorphic) = vampireN
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Mar 03 16:37:45 2015 +0100
@@ -57,10 +57,10 @@
val iproverN : string
val iprover_eqN : string
val leo2N : string
+ val pirateN : string
val satallaxN : string
val snarkN : string
val spassN : string
- val spass_pirateN : string
val vampireN : string
val waldmeisterN : string
val waldmeister_newN : string
@@ -126,10 +126,10 @@
val iproverN = "iprover"
val iprover_eqN = "iprover_eq"
val leo2N = "leo2"
+val pirateN = "pirate"
val satallaxN = "satallax"
val snarkN = "snark"
val spassN = "spass"
-val spass_pirateN = "spass_pirate"
val vampireN = "vampire"
val waldmeisterN = "waldmeister"
val waldmeister_newN = "waldmeister_new"
@@ -654,22 +654,22 @@
>> (fn ((((num, rule), deps), u), names) =>
[((num, these names), Unknown, u, rule, map (rpair []) deps)])) x
-fun parse_spass_pirate_dependency x = (Scan.option ($$ "-") |-- scan_general_id) x
-fun parse_spass_pirate_dependencies x =
- Scan.repeat (parse_spass_pirate_dependency --| Scan.option ($$ "," || $$ " ")) x
-fun parse_spass_pirate_file_source x =
+fun parse_pirate_dependency x = (Scan.option ($$ "-") |-- scan_general_id) x
+fun parse_pirate_dependencies x =
+ Scan.repeat (parse_pirate_dependency --| Scan.option ($$ "," || $$ " ")) x
+fun parse_pirate_file_source x =
((Scan.this_string "Input" || Scan.this_string "Conj") |-- $$ "(" |-- scan_general_id
--| $$ ")") x
-fun parse_spass_pirate_inference_source x =
- (scan_general_id -- ($$ "(" |-- parse_spass_pirate_dependencies --| $$ ")")) x
-fun parse_spass_pirate_source x =
- (parse_spass_pirate_file_source >> (fn s => File_Source ("", SOME s))
- || parse_spass_pirate_inference_source >> Inference_Source) x
+fun parse_pirate_inference_source x =
+ (scan_general_id -- ($$ "(" |-- parse_pirate_dependencies --| $$ ")")) x
+fun parse_pirate_source x =
+ (parse_pirate_file_source >> (fn s => File_Source ("", SOME s))
+ || parse_pirate_inference_source >> Inference_Source) x
(* Syntax: <num> <stuff> || <atoms> -> <atoms> . origin\(<origin>\) *)
-fun parse_spass_pirate_line x =
+fun parse_pirate_line x =
(scan_general_id --| Scan.repeat (~$$ "|") -- parse_horn_clause --| $$ "."
- --| Scan.this_string "origin" --| $$ "(" -- parse_spass_pirate_source --| $$ ")"
+ --| Scan.this_string "origin" --| $$ "(" -- parse_pirate_source --| $$ ")"
>> (fn ((((num, u), source))) =>
let
val (names, rule, deps) =
@@ -690,7 +690,7 @@
fun parse_line local_name problem =
if local_name = leo2N then parse_tstp_thf0_line problem
else if local_name = spassN then parse_spass_line
- else if local_name = spass_pirateN then parse_spass_pirate_line
+ else if local_name = pirateN then parse_pirate_line
else if local_name = z3_tptpN then parse_z3_tptp_core_line
else parse_tstp_line problem
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Mar 03 16:37:45 2015 +0100
@@ -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_spass_skolems : (term, string) atp_step list -> (term, string) atp_step list
+ val introduce_spassy_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_spass_skolems proof =
+fun introduce_spassy_skolems proof =
let
fun add_skolem (Free (s, _)) = String.isPrefix spass_skolem_prefix s ? insert (op =) s
| add_skolem _ = I
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Mar 03 16:37:45 2015 +0100
@@ -614,18 +614,18 @@
val dummy_thf_ml_config = dummy_config Hypothesis dummy_thf_format "ml_poly_native_higher" false
val dummy_thf_ml = (dummy_thf_mlN, fn () => dummy_thf_ml_config)
-val spass_pirate_format = DFG Polymorphic
-val remote_spass_pirate_config : atp_config =
- {exec = K (["ISABELLE_ATP"], ["scripts/remote_spass_pirate"]),
+val pirate_format = DFG Polymorphic
+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, ""), spass_pirate_format, "tc_native", combsN, true), ""))],
+ best_slices = K [(1.0, (((200, ""), pirate_format, "tc_native", combsN, true), ""))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
-val remote_spass_pirate = (remote_prefix ^ spass_pirateN, fn () => remote_spass_pirate_config)
+val remote_pirate = (remote_prefix ^ pirateN, fn () => remote_pirate_config)
(* Remote ATP invocation via SystemOnTPTP *)
@@ -764,7 +764,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 spass_pirateN atp}
+ gen_simp = String.isSuffix pirateN atp}
else
let val is_lpo = String.isSubstring lpoN ord in
{is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
@@ -776,7 +776,7 @@
[agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine,
remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire,
- remote_snark, remote_spass_pirate, remote_waldmeister, remote_waldmeister_new]
+ remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new]
val _ = Theory.setup (fold add_atp atps)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/scripts/remote_pirate Tue Mar 03 16:37:45 2015 +0100
@@ -0,0 +1,2 @@
+#!/usr/bin/env bash
+curl -s -F file=@"$2" "http://91.228.53.68:51642/solve/pirate/"$1"s"
--- a/src/HOL/Tools/ATP/scripts/remote_spass_pirate Tue Mar 03 16:37:45 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-#!/usr/bin/env bash
-curl -s -F file=@"$2" "http://91.228.53.68:51642/solve/pirate/"$1"s"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Mar 03 16:37:45 2015 +0100
@@ -50,8 +50,8 @@
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 spass_pirate_datatype_rule = "DT"
val vampire_skolemisation_rule = "skolemisation"
val veriT_la_generic_rule = "la_generic"
val veriT_simp_arith_rule = "simp_arith"
@@ -73,7 +73,7 @@
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 spass_pirate_datatype_rule
+val is_datatype_rule = String.isPrefix pirate_datatype_rule
fun raw_label_of_num num = (num, 0)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Mar 03 16:37:45 2015 +0100
@@ -144,7 +144,7 @@
val full_proofs = isar_proofs |> the_default (mode = Minimize)
val local_name = perhaps (try (unprefix remote_prefix)) name
val waldmeister_new = (local_name = waldmeister_newN)
- val spass = (local_name = spassN orelse local_name = spass_pirateN)
+ val spassy = (local_name = pirateN orelse local_name = spassN)
val atp_mode = if Config.get ctxt atp_completish then Sledgehammer_Completish else Sledgehammer
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
@@ -381,7 +381,7 @@
atp_proof
|> (if waldmeister_new then termify_waldmeister_proof ctxt pool
else termify_atp_proof ctxt name format type_enc pool lifted sym_tab)
- |> spass ? introduce_spass_skolems
+ |> spassy ? introduce_spassy_skolems
|> (if waldmeister_new then introduce_waldmeister_skolems (the wm_info) else I)
|> factify_atp_proof (map fst used_from) hyp_ts concl_t
in