--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Sep 06 18:07:44 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Sep 06 18:13:36 2011 +0200
@@ -22,15 +22,15 @@
AFun of 'a ho_type * 'a ho_type |
ATyAbs of 'a list * 'a ho_type
- datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
- datatype tff_explicitness = TFF_Implicit | TFF_Explicit
+ datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
+ datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
datatype thf_flavor = THF_Without_Choice | THF_With_Choice
- datatype format =
+ datatype tptp_format =
CNF |
CNF_UEQ |
FOF |
- TFF of tff_polymorphism * tff_explicitness |
- THF0 of thf_flavor
+ TFF of tptp_polymorphism * tptp_explicitness |
+ THF of tptp_polymorphism * tptp_explicitness * thf_flavor
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -92,9 +92,9 @@
bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
-> 'd -> 'd
val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
- val is_format_thf : format -> bool
- val is_format_typed : format -> bool
- val tptp_lines_for_atp_problem : format -> string problem -> string list
+ val is_format_thf : tptp_format -> bool
+ val is_format_typed : tptp_format -> bool
+ val tptp_lines_for_atp_problem : tptp_format -> string problem -> string list
val ensure_cnf_problem :
(string * string) problem -> (string * string) problem
val filter_cnf_ueq_problem :
@@ -130,16 +130,16 @@
AFun of 'a ho_type * 'a ho_type |
ATyAbs of 'a list * 'a ho_type
-datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
-datatype tff_explicitness = TFF_Implicit | TFF_Explicit
+datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
+datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
datatype thf_flavor = THF_Without_Choice | THF_With_Choice
-datatype format =
+datatype tptp_format =
CNF |
CNF_UEQ |
FOF |
- TFF of tff_polymorphism * tff_explicitness |
- THF0 of thf_flavor
+ TFF of tptp_polymorphism * tptp_explicitness |
+ THF of tptp_polymorphism * tptp_explicitness * thf_flavor
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -224,10 +224,10 @@
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
| formula_map f (AAtom tm) = AAtom (f tm)
-fun is_format_thf (THF0 _) = true
+fun is_format_thf (THF _) = true
| is_format_thf _ = false
fun is_format_typed (TFF _) = true
- | is_format_typed (THF0 _) = true
+ | is_format_typed (THF _) = true
| is_format_typed _ = false
fun string_for_kind Axiom = "axiom"
@@ -266,7 +266,7 @@
ss) ^ "]: " ^ str false ty
in str true ty end
-fun string_for_type (THF0 _) ty = str_for_type ty
+fun string_for_type (THF _) ty = str_for_type ty
| string_for_type (TFF _) ty = str_for_type (flatten_type ty)
| string_for_type _ _ = raise Fail "unexpected type in untyped format"
@@ -288,6 +288,9 @@
else
"")
+fun is_format_with_choice (THF (_, _, THF_With_Choice)) = true
+ | is_format_with_choice _ = false
+
fun string_for_term _ (ATerm (s, [])) = s
| string_for_term format (ATerm (s, ts)) =
if s = tptp_empty_list then
@@ -298,7 +301,7 @@
|> is_format_thf format ? enclose "(" ")"
else
(case (s = tptp_ho_forall orelse s = tptp_ho_exists,
- s = tptp_choice andalso format = THF0 THF_With_Choice, ts) of
+ s = tptp_choice andalso is_format_with_choice format, ts) of
(true, _, [AAbs ((s', ty), tm)]) =>
(* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
possible, to work around LEO-II 1.2.8 parser limitation. *)
@@ -306,8 +309,8 @@
(AQuant (if s = tptp_ho_forall then AForall else AExists,
[(s', SOME ty)], AAtom tm))
| (_, true, [AAbs ((s', ty), tm)]) =>
- (*There is code in ATP_Translate to ensure that Eps is always applied
- to an abstraction*)
+ (* There is code in "ATP_Translate" to ensure that "Eps" is always
+ applied to an abstraction. *)
tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
string_for_term format tm ^ ""
|> enclose "(" ")"
@@ -319,7 +322,7 @@
else
s ^ "(" ^ commas ss ^ ")"
end)
- | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
+ | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
"(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
string_for_term format tm ^ ")"
| string_for_term _ _ = raise Fail "unexpected term in first-order format"
@@ -352,7 +355,7 @@
| string_for_format CNF_UEQ = tptp_cnf
| string_for_format FOF = tptp_fof
| string_for_format (TFF _) = tptp_tff
- | string_for_format (THF0 _) = tptp_thf
+ | string_for_format (THF _) = tptp_thf
fun string_for_problem_line format (Decl (ident, sym, ty)) =
string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Sep 06 18:07:44 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Sep 06 18:13:36 2011 +0200
@@ -7,7 +7,7 @@
signature ATP_SYSTEMS =
sig
- type format = ATP_Problem.format
+ type tptp_format = ATP_Problem.tptp_format
type formula_kind = ATP_Problem.formula_kind
type failure = ATP_Proof.failure
@@ -22,7 +22,8 @@
conj_sym_kind : formula_kind,
prem_kind : formula_kind,
best_slices :
- Proof.context -> (real * (bool * (int * format * string * string))) list}
+ Proof.context
+ -> (real * (bool * (int * tptp_format * string * string))) list}
val force_sos : bool Config.T
val e_smartN : string
@@ -41,6 +42,7 @@
val e_tofofN : string
val leo2N : string
val pffN : string
+ val phfN : string
val satallaxN : string
val snarkN : string
val spassN : string
@@ -51,7 +53,7 @@
val remote_atp :
string -> string -> string list -> (string * string) list
-> (failure * string) list -> formula_kind -> formula_kind
- -> (Proof.context -> int * format * string) -> string * atp_config
+ -> (Proof.context -> int * tptp_format * string) -> string * atp_config
val add_atp : string * atp_config -> theory -> theory
val get_atp : theory -> string -> atp_config
val supported_atps : theory -> string list
@@ -79,7 +81,8 @@
conj_sym_kind : formula_kind,
prem_kind : formula_kind,
best_slices :
- Proof.context -> (real * (bool * (int * format * string * string))) list}
+ Proof.context
+ -> (real * (bool * (int * tptp_format * string * string))) list}
(* "best_slices" must be found empirically, taking a wholistic approach since
the ATPs are run in parallel. The "real" components give the faction of the
@@ -105,6 +108,7 @@
val e_tofofN = "e_tofof"
val leo2N = "leo2"
val pffN = "pff"
+val phfN = "phf"
val satallaxN = "satallax"
val snarkN = "snark"
val spassN = "spass"
@@ -230,6 +234,8 @@
(* LEO-II *)
+val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice)
+
val leo2_config : atp_config =
{exec = ("LEO2_HOME", "leo"),
required_execs = [],
@@ -243,10 +249,8 @@
prem_kind = Hypothesis,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.667, (false, (150, THF0 THF_Without_Choice,
- "mono_simple_higher", sosN))),
- (0.333, (true, (50, THF0 THF_Without_Choice,
- "mono_simple_higher", no_sosN)))]
+ [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", sosN))),
+ (0.333, (true, (50, leo2_thf0, "mono_simple_higher", no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -255,6 +259,8 @@
(* Satallax *)
+val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice)
+
val satallax_config : atp_config =
{exec = ("SATALLAX_HOME", "satallax"),
required_execs = [],
@@ -266,8 +272,8 @@
conj_sym_kind = Axiom,
prem_kind = Hypothesis,
best_slices =
- K [(1.0, (true, (100, THF0 THF_With_Choice, "mono_simple_higher", "")))]
- (* FUDGE *)}
+ (* FUDGE *)
+ K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", "")))]}
val satallax = (satallaxN, satallax_config)
@@ -314,7 +320,7 @@
fun is_old_vampire_version () =
string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
-val vampire_tff = TFF (TFF_Monomorphic, TFF_Implicit)
+val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
val vampire_config : atp_config =
{exec = ("VAMPIRE_HOME", "vampire"),
@@ -347,9 +353,9 @@
(0.333, (false, (500, FOF, "mono_tags?", sosN))),
(0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
else
- [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))),
- (0.333, (false, (500, vampire_tff, "mono_simple", sosN))),
- (0.334, (true, (50, vampire_tff, "mono_simple", no_sosN)))])
+ [(0.333, (false, (150, vampire_tff0, "poly_guards", sosN))),
+ (0.333, (false, (500, vampire_tff0, "mono_simple", sosN))),
+ (0.334, (true, (50, vampire_tff0, "mono_simple", no_sosN)))])
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -358,7 +364,7 @@
(* Z3 with TPTP syntax *)
-val z3_tff = TFF (TFF_Monomorphic, TFF_Implicit)
+val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
val z3_tptp_config : atp_config =
{exec = ("Z3_HOME", "z3"),
@@ -377,18 +383,17 @@
prem_kind = Hypothesis,
best_slices =
(* FUDGE *)
- K [(0.5, (false, (250, z3_tff, "mono_simple", ""))),
- (0.25, (false, (125, z3_tff, "mono_simple", ""))),
- (0.125, (false, (62, z3_tff, "mono_simple", ""))),
- (0.125, (false, (31, z3_tff, "mono_simple", "")))]}
+ K [(0.5, (false, (250, z3_tff0, "mono_simple", ""))),
+ (0.25, (false, (125, z3_tff0, "mono_simple", ""))),
+ (0.125, (false, (62, z3_tff0, "mono_simple", ""))),
+ (0.125, (false, (31, z3_tff0, "mono_simple", "")))]}
val z3_tptp = (z3_tptpN, z3_tptp_config)
-(* Not really a prover: Experimental PFF (Polymorphic TFF) output *)
-val poly_tff = TFF (TFF_Polymorphic, TFF_Implicit)
+(* Not really a prover: Experimental Polymorphic TFF and THF output *)
-val pff_config : atp_config =
+fun dummy_config format type_enc : atp_config =
{exec = ("ISABELLE_ATP", "scripts/dummy_atp"),
required_execs = [],
arguments = K (K (K (K (K "")))),
@@ -396,10 +401,16 @@
known_failures = [(GaveUp, "SZS status Unknown")],
conj_sym_kind = Hypothesis,
prem_kind = Hypothesis,
- best_slices = K [(1.0, (false, (200, poly_tff, "poly_simple", "")))]}
+ best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
+val pff_format = TFF (TPTP_Polymorphic, TPTP_Implicit)
+val pff_config = dummy_config pff_format "poly_simple"
val pff = (pffN, pff_config)
+val phf_format = THF (TPTP_Polymorphic, TPTP_Implicit, THF_With_Choice)
+val phf_config = dummy_config phf_format "poly_simple_higher"
+val phf = (phfN, phf_config)
+
(* Remote ATP invocation via SystemOnTPTP *)
@@ -475,34 +486,33 @@
(remote_prefix ^ name,
remotify_config system_name system_versions best_slice config)
-val dumb_tff = TFF (TFF_Monomorphic, TFF_Explicit)
+val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit)
val remote_e =
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
(K (750, FOF, "mono_tags?") (* FUDGE *))
val remote_leo2 =
remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
- (K (100, THF0 THF_Without_Choice,
- "mono_simple_higher") (* FUDGE *))
+ (K (100, leo2_thf0, "mono_simple_higher") (* FUDGE *))
val remote_satallax =
remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
- (K (100, THF0 THF_With_Choice,
- "mono_simple_higher") (* FUDGE *))
+ (K (100, satallax_thf0, "mono_simple_higher") (* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["1.8"]
(K (250, FOF, "mono_guards?") (* FUDGE *))
val remote_z3_tptp =
- remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "mono_simple") (* FUDGE *))
+ remotify_atp z3_tptp "Z3" ["3.0"]
+ (K (250, z3_tff0, "mono_simple") (* FUDGE *))
val remote_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
- (K (100, dumb_tff, "mono_simple") (* FUDGE *))
+ (K (100, explicit_tff0, "mono_simple") (* FUDGE *))
val remote_e_tofof =
remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
- Hypothesis (K (150, dumb_tff, "mono_simple") (* FUDGE *))
+ Hypothesis (K (150, explicit_tff0, "mono_simple") (* FUDGE *))
val remote_waldmeister =
remote_atp waldmeisterN "Waldmeister" ["710"]
[("#START OF PROOF", "Proved Goals:")]
@@ -532,7 +542,7 @@
Synchronized.change systems (fn _ => get_systems ())
val atps =
- [e, leo2, pff, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
+ [e, leo2, pff, phf, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
remote_e_tofof, remote_waldmeister]
val setup = fold add_atp atps
--- a/src/HOL/Tools/ATP/atp_translate.ML Tue Sep 06 18:07:44 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Sep 06 18:13:36 2011 +0200
@@ -11,7 +11,7 @@
type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
type connective = ATP_Problem.connective
type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
- type format = ATP_Problem.format
+ type tptp_format = ATP_Problem.tptp_format
type formula_kind = ATP_Problem.formula_kind
type 'a problem = 'a ATP_Problem.problem
@@ -92,7 +92,7 @@
val level_of_type_enc : type_enc -> type_level
val is_type_enc_quasi_sound : type_enc -> bool
val is_type_enc_fairly_sound : type_enc -> bool
- val adjust_type_enc : format -> type_enc -> type_enc
+ val adjust_type_enc : tptp_format -> type_enc -> type_enc
val mk_aconns :
connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
val unmangled_const : string -> string * (string, 'b) ho_term list
@@ -100,7 +100,7 @@
val helper_table : ((string * bool) * thm list) list
val factsN : string
val prepare_atp_problem :
- Proof.context -> format -> formula_kind -> formula_kind -> type_enc
+ Proof.context -> tptp_format -> formula_kind -> formula_kind -> type_enc
-> bool -> string -> bool -> bool -> term list -> term
-> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
@@ -142,7 +142,7 @@
(* TFF1 is still in development, and it is still unclear whether symbols will be
allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
"dummy" type variables. *)
-val exploit_tff1_dummy_type_vars = false
+val avoid_first_order_dummy_type_vars = true
val bound_var_prefix = "B_"
val all_bound_var_prefix = "BA_"
@@ -325,8 +325,8 @@
fun default c = const_prefix ^ lookup_const c
in
fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
- | make_fixed_const (SOME (THF0 THF_With_Choice)) c =
- if c = choice_const then tptp_choice else default c
+ | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c =
+ if c = choice_const then tptp_choice else default c
| make_fixed_const _ c = default c
end
@@ -587,7 +587,9 @@
| _ => raise Same.SAME)
| ("simple_higher", (SOME poly, _, Nonuniform)) =>
(case (poly, level) of
- (_, Noninf_Nonmono_Types _) => raise Same.SAME
+ (Polymorphic, All_Types) =>
+ Simple_Types (Higher_Order, Polymorphic, All_Types)
+ | (_, Noninf_Nonmono_Types _) => raise Same.SAME
| (Mangled_Monomorphic, _) =>
Simple_Types (Higher_Order, Mangled_Monomorphic, level)
| _ => raise Same.SAME)
@@ -631,12 +633,13 @@
| is_type_level_monotonicity_based Fin_Nonmono_Types = true
| is_type_level_monotonicity_based _ = false
-fun adjust_type_enc (THF0 _) (Simple_Types (order, Polymorphic, level)) =
+fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
+ (Simple_Types (order, _, level)) =
Simple_Types (order, Mangled_Monomorphic, level)
- | adjust_type_enc (THF0 _) type_enc = type_enc
- | adjust_type_enc (TFF (TFF_Monomorphic, _)) (Simple_Types (_, _, level)) =
+ | adjust_type_enc (THF _) type_enc = type_enc
+ | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
Simple_Types (First_Order, Mangled_Monomorphic, level)
- | adjust_type_enc (TFF (_, _)) (Simple_Types (_, poly, level)) =
+ | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
Simple_Types (First_Order, poly, level)
| adjust_type_enc format (Simple_Types (_, poly, level)) =
adjust_type_enc format (Guards (poly, level, Uniform))
@@ -746,8 +749,9 @@
fun type_class_formula type_enc class arg =
AAtom (ATerm (class, arg ::
(case type_enc of
- Simple_Types (_, Polymorphic, _) =>
- if exploit_tff1_dummy_type_vars then [] else [ATerm (TYPE_name, [arg])]
+ Simple_Types (First_Order, Polymorphic, _) =>
+ if avoid_first_order_dummy_type_vars then [ATerm (TYPE_name, [arg])]
+ else []
| _ => [])))
fun formulas_for_types type_enc add_sorts_on_typ Ts =
[] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
@@ -1779,18 +1783,19 @@
(** Symbol declarations **)
-fun decl_line_for_class s =
+fun decl_line_for_class order s =
let val name as (s, _) = `make_type_class s in
Decl (sym_decl_prefix ^ s, name,
- if exploit_tff1_dummy_type_vars then
- AFun (atype_of_types, bool_atype)
+ if order = First_Order andalso avoid_first_order_dummy_type_vars then
+ ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype))
else
- ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype)))
+ AFun (atype_of_types, bool_atype))
end
fun decl_lines_for_classes type_enc classes =
case type_enc of
- Simple_Types (_, Polymorphic, _) => map decl_line_for_class classes
+ Simple_Types (order, Polymorphic, _) =>
+ map (decl_line_for_class order) classes
| _ => []
fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
@@ -2232,7 +2237,8 @@
CNF => ensure_cnf_problem
| CNF_UEQ => filter_cnf_ueq_problem
| FOF => I
- | TFF (_, TFF_Implicit) => I
+ | TFF (_, TPTP_Implicit) => I
+ | THF (_, TPTP_Implicit, _) => I
| _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
implicit_declsN)
val (problem, pool) = problem |> nice_atp_problem readable_names