--- a/src/Doc/Sledgehammer/document/root.tex Tue Dec 17 11:12:10 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Tue Dec 17 14:03:29 2013 +0100
@@ -960,6 +960,11 @@
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.
--- a/src/HOL/TPTP/atp_theory_export.ML Tue Dec 17 11:12:10 2013 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Tue Dec 17 14:03:29 2013 +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_polyN
+ | atp_of_format (DFG Polymorphic) = spass_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_problem.ML Tue Dec 17 11:12:10 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Dec 17 14:03:29 2013 +0100
@@ -50,8 +50,7 @@
Class_Decl of string * 'a * 'a list |
Type_Decl of string * 'a * int |
Sym_Decl of string * 'a * 'a atp_type |
- Datatype_Decl of string * ('a * 'a list) list * 'a atp_type
- * ('a, 'a atp_type) atp_term list * bool |
+ Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list |
Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a |
Formula of (string * string) * atp_formula_role
* ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula
@@ -195,8 +194,7 @@
Class_Decl of string * 'a * 'a list |
Type_Decl of string * 'a * int |
Sym_Decl of string * 'a * 'a atp_type |
- Datatype_Decl of string * ('a * 'a list) list * 'a atp_type
- * ('a, 'a atp_type) atp_term list * bool |
+ Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list |
Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a |
Formula of (string * string) * atp_formula_role
* ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula
@@ -624,9 +622,7 @@
(if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^
typ ty
fun sort_decl xs ty cl = "sort(" ^ binder_typ xs ty ^ ", " ^ cl ^ ")."
- fun datatype_decl xs ty tms exhaust =
- "datatype(" ^ commas (binder_typ xs ty :: map term tms @
- (if exhaust then [] else ["..."])) ^ ")."
+ fun datatype_decl xs ty tms = "datatype(" ^ commas (binder_typ xs ty :: map term tms) ^ ")."
fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
fun formula pred (Formula ((ident, alt), kind, phi, _, info)) =
if pred kind then
@@ -674,8 +670,7 @@
else NONE
| _ => NONE) |> flat
val datatype_decls =
- filt (try (fn Datatype_Decl (_, xs, ty, tms, exhaust) =>
- datatype_decl xs ty tms exhaust)) |> flat
+ filt (try (fn Datatype_Decl (_, xs, ty, tms) => datatype_decl xs ty tms)) |> flat
val sort_decls =
filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat
val subclass_decls =
@@ -952,9 +947,9 @@
| nice_line (Sym_Decl (ident, sym, ty)) =
nice_name sym ##>> nice_type ty
#>> (fn (sym, ty) => Sym_Decl (ident, sym, ty))
- | nice_line (Datatype_Decl (ident, xs, ty, tms, exhaust)) =
+ | nice_line (Datatype_Decl (ident, xs, ty, tms)) =
nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms
- #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms, exhaust))
+ #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms))
| nice_line (Class_Memb (ident, xs, ty, cl)) =
nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl
#>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl))
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Dec 17 11:12:10 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Dec 17 14:03:29 2013 +0100
@@ -2573,18 +2573,21 @@
end
fun datatype_of_ctrs (ctrs as (_, T1) :: _) =
let val ctrs' = map do_ctr ctrs in
- (native_ho_type_of_typ type_enc false 0 (body_type T1),
- map_filter I ctrs', forall is_some ctrs')
+ if forall is_some ctrs' then
+ SOME (native_ho_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs')
+ else
+ NONE
end
- in ctrss |> map datatype_of_ctrs |> filter_out (null o #2) end
+ in
+ map_filter datatype_of_ctrs ctrss
+ end
else
[]
| datatypes_of_sym_table _ _ _ _ _ _ = []
-fun decl_line_of_datatype (ty as AType ((_, s'), ty_args), ctrs, exhaust) =
+fun decl_line_of_datatype (ty as AType ((_, s'), ty_args), ctrs) =
let val xs = map (fn AType (name, []) => name) ty_args in
- Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty,
- ctrs, exhaust)
+ Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty, ctrs)
end
fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
@@ -2704,7 +2707,7 @@
fun do_line (Class_Decl (_, _, cls)) = fold do_class cls
| do_line (Type_Decl _) = I
| do_line (Sym_Decl (_, _, ty)) = do_type ty
- | do_line (Datatype_Decl (_, xs, ty, tms, _)) =
+ | do_line (Datatype_Decl (_, xs, ty, tms)) =
fold do_bound_tvars xs #> do_type ty #> fold (do_term false) tms
| do_line (Class_Memb (_, xs, ty, cl)) =
fold do_bound_tvars xs #> do_type ty #> do_class cl
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Dec 17 11:12:10 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Dec 17 14:03:29 2013 +0100
@@ -41,6 +41,12 @@
type 'a atp_proof =
(('a, 'a, ('a, 'a) atp_term, 'a) atp_formula, string) atp_step list
+ val agsyhol_core_rule : string
+ val satallax_core_rule : string
+ val spass_input_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
val extract_important_message : string -> string
@@ -51,9 +57,6 @@
-> string * atp_failure option
val is_same_atp_step : atp_step_name -> atp_step_name -> bool
val scan_general_id : string list -> string * string list
- val agsyhol_coreN : string
- val satallax_coreN : string
- val z3_tptp_coreN : string
val parse_formula :
string list
-> (string, 'a, (string, 'a) atp_term, string) atp_formula * string list
@@ -72,6 +75,12 @@
open ATP_Util
open ATP_Problem
+val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *)
+val satallax_core_rule = "__satallax_core" (* arbitrary *)
+val spass_input_rule = "Inp"
+val spass_skolemize_rule = "__Sko" (* arbitrary *)
+val z3_tptp_core_rule = "__z3_tptp_core" (* arbitrary *)
+
exception UNRECOGNIZED_ATP_PROOF of unit
datatype atp_failure =
@@ -103,9 +112,8 @@
" appears to be missing. You will need to install it if you want to invoke \
\remote provers."
-fun involving [] = ""
- | involving ss =
- " involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
+fun from_lemmas [] = ""
+ | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
fun string_of_atp_failure Unprovable = "The generated problem is unprovable."
| string_of_atp_failure GaveUp = "The prover gave up."
@@ -115,10 +123,10 @@
"The prover claims the conjecture is a theorem but provided an incomplete \
\(or unparsable) proof."
| string_of_atp_failure (UnsoundProof (false, ss)) =
- "The prover derived \"False\" using" ^ involving ss ^
+ "The prover derived \"False\"" ^ from_lemmas ss ^
". Specify a sound type encoding or omit the \"type_enc\" option."
| string_of_atp_failure (UnsoundProof (true, ss)) =
- "The prover derived \"False\" using" ^ involving ss ^
+ "The prover derived \"False\"" ^ from_lemmas ss ^
". This could be due to inconsistent axioms (including \"sorry\"s) or to \
\a bug in Sledgehammer. If the problem persists, please contact the \
\Isabelle developers."
@@ -152,20 +160,19 @@
("% SZS start RequiredInformation", "% SZS end RequiredInformation")
fun extract_important_message output =
- case extract_delimited tstp_important_message_delims output of
+ (case extract_delimited tstp_important_message_delims output of
"" => ""
| s => s |> space_explode "\n" |> filter_out (curry (op =) "")
|> map (perhaps (try (unprefix "%")))
|> map (perhaps (try (unprefix " ")))
- |> space_implode "\n " |> quote
+ |> space_implode "\n " |> quote)
(* Splits by the first possible of a list of delimiters. *)
fun extract_tstplike_proof delims output =
- case pairself (find_first (fn s => String.isSubstring s output))
+ (case pairself (find_first (fn s => String.isSubstring s output))
(ListPair.unzip delims) of
- (SOME begin_delim, SOME end_delim) =>
- extract_delimited (begin_delim, end_delim) output
- | _ => ""
+ (SOME begin_delim, SOME end_delim) => extract_delimited (begin_delim, end_delim) output
+ | _ => "")
fun extract_known_atp_failure known_failures output =
known_failures
@@ -174,13 +181,13 @@
fun extract_tstplike_proof_and_outcome verbose proof_delims known_failures
output =
- case (extract_tstplike_proof proof_delims output,
+ (case (extract_tstplike_proof proof_delims output,
extract_known_atp_failure known_failures output) of
(_, SOME ProofIncomplete) => ("", NONE)
| ("", SOME ProofMissing) => ("", NONE)
| ("", NONE) => ("", SOME (UnknownError (short_output verbose output)))
| res as ("", _) => res
- | (tstplike_proof, _) => (tstplike_proof, NONE)
+ | (tstplike_proof, _) => (tstplike_proof, NONE))
type atp_step_name = string * string list
@@ -191,10 +198,9 @@
fun vampire_step_name_ord p =
let val q = pairself fst p in
(* The "unprefix" part is to cope with Vampire's output. *)
- case pairself (Int.fromString
- o perhaps (try (unprefix vampire_fact_prefix))) q of
+ (case pairself (Int.fromString o perhaps (try (unprefix vampire_fact_prefix))) q of
(SOME i, SOME j) => int_ord (i, j)
- | _ => raise Fail "not Vampire"
+ | _ => raise Fail "not Vampire")
end
type ('a, 'b) atp_step =
@@ -278,8 +284,7 @@
| (u1, SOME (neg, u2)) =>
AAtom (ATerm (("equal", []), [u1, u2])) |> is_some neg ? mk_anot)) x
-(* TPTP formulas are fully parenthesized, so we don't need to worry about
- operator precedence. *)
+(* TPTP formulas are fully parenthesized, so we don't need to worry about operator precedence. *)
fun parse_literal x =
((Scan.repeat ($$ tptp_not) >> length)
-- ($$ "(" |-- parse_formula --| $$ ")"
@@ -322,7 +327,7 @@
let
fun do_term_pair _ NONE = NONE
| do_term_pair (ATerm ((s1, _), tm1), ATerm ((s2, _), tm2)) (SOME subst) =
- case pairself is_tptp_variable (s1, s2) of
+ (case pairself is_tptp_variable (s1, s2) of
(true, true) =>
(case AList.lookup (op =) subst s1 of
SOME s2' => if s2' = s2 then SOME subst else NONE
@@ -334,8 +339,10 @@
SOME subst |> fold do_term_pair (tm1 ~~ tm2)
else
NONE
- | _ => NONE
- in SOME subst |> do_term_pair (tm1, tm2) |> is_some end
+ | _ => NONE)
+ in
+ SOME subst |> do_term_pair (tm1, tm2) |> is_some
+ end
fun is_same_formula comm subst (AQuant (q1, xs1, phi1)) (AQuant (q2, xs2, phi2)) =
q1 = q2 andalso length xs1 = length xs2 andalso
@@ -370,8 +377,7 @@
| role_of_tptp_string "plain" = Plain
| role_of_tptp_string _ = Unknown
-(* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>,
- <formula> <extra_arguments>\).
+(* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>, <formula> <extra_arguments>\).
The <num> could be an identifier, but we assume integers. *)
fun parse_tstp_line problem =
((Scan.this_string tptp_cnf || Scan.this_string tptp_fof
@@ -383,17 +389,16 @@
let
val ((name, phi), rule, deps) =
(* Waldmeister isn't exactly helping. *)
- case deps of
+ (case deps of
File_Source (_, SOME s) =>
(if s = waldmeister_conjecture_name then
- case find_formula_in_problem problem (mk_anot phi) of
+ (case find_formula_in_problem problem (mk_anot phi) of
(* Waldmeister hack: Get the original orientation of the
equation to avoid confusing Isar. *)
[(s, phi')] =>
((num, [s]),
- phi |> not (is_same_formula false [] (mk_anot phi) phi')
- ? commute_eq)
- | _ => ((num, []), phi)
+ phi |> not (is_same_formula false [] (mk_anot phi) phi') ? commute_eq)
+ | _ => ((num, []), phi))
else
((num, [s |> perhaps (try (unprefix tofof_fact_prefix))]),
phi),
@@ -401,18 +406,18 @@
| File_Source _ =>
(((num, phi |> find_formula_in_problem problem |> map fst),
phi), "", [])
- | Inference_Source (rule, deps) => (((num, []), phi), rule, deps)
+ | Inference_Source (rule, deps) => (((num, []), phi), rule, deps))
fun mk_step () =
(name, role_of_tptp_string role, phi, rule, map (rpair []) deps)
in
- case role_of_tptp_string role of
+ (case role_of_tptp_string role of
Definition =>
(case phi of
AAtom (ATerm (("equal", []), _)) =>
(* Vampire's equality proxy axiom *)
(name, Definition, phi, rule, map (rpair []) deps)
| _ => mk_step ())
- | _ => mk_step ()
+ | _ => mk_step ())
end)
(**** PARSING OF SPASS OUTPUT ****)
@@ -444,38 +449,57 @@
>> (mk_horn o apfst (op @))) x
val parse_spass_debug =
- Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ","))
- --| $$ ")")
+ Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) --| $$ ")")
-(* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>.
+(* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms> .
derived from formulae <ident>* *)
fun parse_spass_line x =
- (parse_spass_debug |-- scan_general_id --| $$ "[" --|
- Scan.many1 Symbol.is_digit --| $$ ":" -- Symbol.scan_ascii_id
- -- parse_spass_annotations --| $$ "]"
- -- parse_horn_clause --| $$ "."
+ (parse_spass_debug |-- scan_general_id --| $$ "[" --| Scan.many1 Symbol.is_digit --| $$ ":"
+ -- Symbol.scan_ascii_id -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "."
-- Scan.option (Scan.this_string "derived from formulae "
|-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
>> (fn ((((num, rule), deps), u), names) =>
((num, these names), Unknown, u, rule, map (rpair []) deps))) x
-val agsyhol_coreN = "__agsyhol_core" (* arbitrary *)
-val satallax_coreN = "__satallax_core" (* arbitrary *)
-val z3_tptp_coreN = "__z3_tptp_core" (* arbitrary *)
+fun parse_spass_pirate_dependency x = (Scan.option ($$ "-") |-- scan_general_id) x
+fun parse_spass_pirate_dependencies x =
+ (parse_spass_pirate_dependency ::: Scan.repeat ($$ "," |-- parse_spass_pirate_dependency)) x
+fun parse_spass_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
+
+(* Syntax: <num> <stuff> || <atoms> -> <atoms> . origin\(<origin>\) *)
+fun parse_spass_pirate_line x =
+ (scan_general_id --| Scan.repeat (~$$ "|") -- parse_horn_clause --| $$ "."
+ --| Scan.this_string "origin" --| $$ "(" -- parse_spass_pirate_source --| $$ ")"
+ >> (fn ((((num, u), source))) =>
+ let
+ val (names, rule, deps) =
+ (case source of
+ File_Source (_, SOME s) => ([s], spass_input_rule, [])
+ | Inference_Source (rule, deps) => ([], rule, deps))
+ in
+ ((num, names), Unknown, u, rule, map (rpair []) deps)
+ end)) x
fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, [])
(* Syntax: core(<name>,[<name>,...,<name>]). *)
fun parse_z3_tptp_line x =
(scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]"
- >> (fn (name, names) => (("", name :: names), Unknown, dummy_phi, z3_tptp_coreN, []))) x
+ >> (fn (name, names) => (("", name :: names), Unknown, dummy_phi, z3_tptp_core_rule, []))) x
(* Syntax: <name> *)
fun parse_satallax_line x =
- (scan_general_id --| Scan.option ($$ " ") >> core_inference satallax_coreN) x
+ (scan_general_id --| Scan.option ($$ " ") >> core_inference satallax_core_rule) x
fun parse_line problem =
- parse_tstp_line problem || parse_spass_line || parse_z3_tptp_line
+ parse_tstp_line problem || parse_spass_line || parse_spass_pirate_line || parse_z3_tptp_line
|| parse_satallax_line
fun parse_proof problem =
strip_spaces_except_between_idents
@@ -486,20 +510,19 @@
#> fst
fun core_of_agsyhol_proof s =
- case split_lines s of
+ (case split_lines s of
"The transformed problem consists of the following conjectures:" :: conj ::
- _ :: proof_term :: _ =>
- SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term)
- | _ => NONE
+ _ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term)
+ | _ => NONE)
fun atp_proof_of_tstplike_proof _ "" = []
| atp_proof_of_tstplike_proof problem tstp =
- case core_of_agsyhol_proof tstp of
- SOME facts => facts |> map (core_inference agsyhol_coreN)
+ (case core_of_agsyhol_proof tstp of
+ SOME facts => facts |> map (core_inference agsyhol_core_rule)
| NONE =>
tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
|> parse_proof problem
- |> perhaps (try (sort (vampire_step_name_ord o pairself #1)))
+ |> perhaps (try (sort (vampire_step_name_ord o pairself #1))))
fun clean_up_dependencies _ [] = []
| clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) =
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Dec 17 11:12:10 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Dec 17 14:03:29 2013 +0100
@@ -15,7 +15,6 @@
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
type 'a atp_proof = 'a ATP_Proof.atp_proof
- val spass_skolemize_rule : string
val metisN : string
val full_typesN : string
val partial_typesN : string
@@ -60,9 +59,6 @@
open ATP_Proof
open ATP_Problem_Generate
-val spass_input_rule = "Inp"
-val spass_skolemize_rule = "__Sko" (* arbitrary *)
-
val metisN = "metis"
val full_typesN = "full_types"
@@ -414,7 +410,7 @@
dependencies in the TSTP proof. Remove the next line once this is
fixed. *)
add_non_rec_defs fact_names
- else if rule = agsyhol_coreN orelse rule = satallax_coreN then
+ else if rule = agsyhol_core_rule orelse rule = satallax_core_rule then
(fn [] =>
(* agsyHOL and Satallax don't include definitions in their
unsatisfiable cores, so we assume the worst and include them all
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Dec 17 11:12:10 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Dec 17 14:03:29 2013 +0100
@@ -62,7 +62,7 @@
val satallaxN : string
val snarkN : string
val spassN : string
- val spass_polyN : string
+ val spass_pirateN : string
val vampireN : string
val waldmeisterN : string
val z3_tptpN : string
@@ -173,7 +173,7 @@
val satallaxN = "satallax"
val snarkN = "snark"
val spassN = "spass"
-val spass_polyN = "spass_poly"
+val spass_pirateN = "spass_pirate"
val vampireN = "vampire"
val waldmeisterN = "waldmeister"
val z3_tptpN = "z3_tptp"
@@ -654,14 +654,21 @@
best_max_new_mono_instances = default_max_new_mono_instances}
val dummy_thf_format = THF (Polymorphic, THF_With_Choice)
-val dummy_thf_config =
- dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
+val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
-val spass_poly_format = DFG Polymorphic
-val spass_poly_config =
- dummy_config (#prem_role spass_config) spass_poly_format "tc_native" true
-val spass_poly = (spass_polyN, fn () => spass_poly_config)
+val spass_pirate_format = DFG Polymorphic
+val remote_spass_pirate_config =
+ {exec = K (["ISABELLE_ATP"], ["scripts/remote_spass_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_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)
(* Remote ATP invocation via SystemOnTPTP *)
@@ -693,29 +700,27 @@
|> `(`(find_remote_system name versions)))
fun the_remote_system name versions =
- case get_remote_system name versions of
+ (case get_remote_system name versions of
(SOME sys, _) => sys
- | (NONE, []) => error ("SystemOnTPTP is not available.")
+ | (NONE, []) => error "SystemOnTPTP is not available."
| (NONE, syss) =>
- case syss |> filter_out (String.isPrefix "%")
- |> filter_out (curry (op =) "") of
- [] => error ("SystemOnTPTP is currently not available.")
+ (case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of
+ [] => error "SystemOnTPTP is currently not available."
| [msg] => error ("SystemOnTPTP is currently not available: " ^ msg ^ ".")
| syss =>
- error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
- "(Available systems: " ^ commas_quote syss ^ ".)")
+ error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^
+ commas_quote syss ^ ".)")))
val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
fun remote_config system_name system_versions proof_delims known_failures
prem_role best_slice : atp_config =
{exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]),
- arguments = fn _ => fn _ => fn command => fn timeout => fn file_name =>
- fn _ =>
- (if command <> "" then "-c " ^ quote command ^ " " else "") ^
- "-s " ^ the_remote_system system_name system_versions ^ " " ^
- "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
- " " ^ file_name,
+ arguments = fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ =>
+ (if command <> "" then "-c " ^ quote command ^ " " else "") ^
+ "-s " ^ the_remote_system system_name system_versions ^ " " ^
+ "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
+ " " ^ file_name,
proof_delims = union (op =) tstp_proof_delims proof_delims,
known_failures = known_failures @ known_perl_failures @ known_says_failures,
prem_role = prem_role,
@@ -788,7 +793,7 @@
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
fun get_atp thy name =
- the (Symtab.lookup (Data.get thy) name) |> fst
+ fst (the (Symtab.lookup (Data.get thy) name))
handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
val supported_atps = Symtab.keys o Data.get
@@ -804,25 +809,20 @@
fun effective_term_order ctxt atp =
let val ord = Config.get ctxt term_order in
if ord = smartN then
- let val is_spass = (atp = spassN orelse atp = spass_polyN) in
- {is_lpo = false, gen_weights = is_spass, gen_prec = is_spass,
- gen_simp = false}
- end
+ {is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN),
+ gen_simp = String.isSuffix spass_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,
- gen_prec = String.isSubstring xprecN ord,
- gen_simp = String.isSubstring xsimpN ord}
+ {is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
+ gen_prec = String.isSubstring xprecN ord, gen_simp = String.isSubstring xsimpN ord}
end
end
val atps =
- [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax,
- spass, spass_poly, vampire, z3_tptp, dummy_thf, remote_agsyhol, remote_e,
- remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
- remote_leo2, remote_satallax, remote_vampire, remote_snark,
- remote_waldmeister]
+ [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
+ z3_tptp, dummy_thf, 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]
val setup = fold add_atp atps
--- a/src/HOL/Tools/ATP/scripts/dummy_atp Tue Dec 17 11:12:10 2013 +0100
+++ b/src/HOL/Tools/ATP/scripts/dummy_atp Tue Dec 17 14:03:29 2013 +0100
@@ -1,1 +1,2 @@
+#!/usr/bin/env bash
echo "SZS status Unknown"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/scripts/remote_spass_pirate Tue Dec 17 14:03:29 2013 +0100
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+curl -F file=@"$2" "http://91.228.53.68:8080/solve/pirate/"$1"s" \
+ | sed "s/Invovled clauses/Involved clauses/"