# HG changeset patch # User blanchet # Date 1425397065 -3600 # Node ID 012c6165bbd2f19c16d9f6772a0e38b85ce634b9 # Parent 913c4afb03887a77ed69753aef8791591d0d4a0b SPASS-Pirate is now called Pirate diff -r 913c4afb0388 -r 012c6165bbd2 src/Doc/Sledgehammer/document/root.tex --- 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}. diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/TPTP/atp_theory_export.ML --- 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 diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/Tools/ATP/atp_proof.ML --- 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: || -> . 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 diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- 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 diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/Tools/ATP/atp_systems.ML --- 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) diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/Tools/ATP/scripts/remote_pirate --- /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" diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/Tools/ATP/scripts/remote_spass_pirate --- 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" diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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) diff -r 913c4afb0388 -r 012c6165bbd2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- 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