--- a/src/HOL/Tools/ATP/atp_problem.ML Mon May 28 13:38:07 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Mon May 28 20:25:38 2012 +0200
@@ -30,7 +30,8 @@
datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
- datatype thf_flavor = THF_Without_Choice | THF_With_Choice
+ datatype thf_choice = THF_Without_Choice | THF_With_Choice
+ datatype thf_defs = THF_Without_Defs | THF_With_Defs
datatype dfg_flavor = DFG_Unsorted | DFG_Sorted
datatype atp_format =
@@ -38,7 +39,7 @@
CNF_UEQ |
FOF |
TFF of tptp_polymorphism * tptp_explicitness |
- THF of tptp_polymorphism * tptp_explicitness * thf_flavor |
+ THF of tptp_polymorphism * tptp_explicitness * thf_choice * thf_defs |
DFG of dfg_flavor
datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
@@ -162,7 +163,8 @@
datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
-datatype thf_flavor = THF_Without_Choice | THF_With_Choice
+datatype thf_choice = THF_Without_Choice | THF_With_Choice
+datatype thf_defs = THF_Without_Defs | THF_With_Defs
datatype dfg_flavor = DFG_Unsorted | DFG_Sorted
datatype atp_format =
@@ -170,7 +172,7 @@
CNF_UEQ |
FOF |
TFF of tptp_polymorphism * tptp_explicitness |
- THF of tptp_polymorphism * tptp_explicitness * thf_flavor |
+ THF of tptp_polymorphism * tptp_explicitness * thf_choice * thf_defs |
DFG of dfg_flavor
datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
@@ -380,9 +382,6 @@
else
"")
-fun is_format_with_choice (THF (_, _, THF_With_Choice)) = true
- | is_format_with_choice _ = false
-
fun tptp_string_for_term _ (ATerm (s, [])) = s
| tptp_string_for_term format (ATerm (s, ts)) =
(if s = tptp_empty_list then
@@ -392,8 +391,8 @@
space_implode (" " ^ tptp_equal ^ " ")
(map (tptp_string_for_term format) ts)
|> is_format_higher_order format ? enclose "(" ")"
- else case (s = tptp_ho_forall orelse s = tptp_ho_exists,
- s = tptp_choice andalso is_format_with_choice format, ts) of
+ else case (s = tptp_ho_forall orelse s = tptp_ho_exists, s = tptp_choice,
+ 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. *)
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon May 28 13:38:07 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon May 28 20:25:38 2012 +0200
@@ -127,7 +127,7 @@
datatype order =
First_Order |
- Higher_Order of thf_flavor
+ Higher_Order of thf_choice
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype strictness = Strict | Non_Strict
datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
@@ -686,12 +686,12 @@
Higher_Order THF_Without_Choice
| adjust_order _ type_enc = type_enc
-fun adjust_type_enc (THF (TPTP_Polymorphic, _, flavor))
+fun adjust_type_enc (THF (TPTP_Polymorphic, _, choice, _))
(Native (order, poly, level)) =
- Native (adjust_order flavor order, poly, level)
- | adjust_type_enc (THF (TPTP_Monomorphic, _, flavor))
+ Native (adjust_order choice order, poly, level)
+ | adjust_type_enc (THF (TPTP_Monomorphic, _, choice, _))
(Native (order, _, level)) =
- Native (adjust_order flavor order, Mangled_Monomorphic, level)
+ Native (adjust_order choice order, Mangled_Monomorphic, level)
| adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Native (_, _, level)) =
Native (First_Order, Mangled_Monomorphic, level)
| adjust_type_enc (DFG DFG_Sorted) (Native (_, _, level)) =
@@ -1282,11 +1282,14 @@
atomic_types = atomic_Ts}
end
+fun is_format_with_defs (THF (_, _, _, THF_With_Defs)) = true
+ | is_format_with_defs _ = false
+
fun make_fact ctxt format type_enc iff_for_eq
((name, stature as (_, status)), t) =
let
val role =
- if is_type_enc_higher_order type_enc andalso status = Def andalso
+ if is_format_with_defs format andalso status = Def andalso
is_legitimate_tptp_def t then
Definition
else
@@ -1309,7 +1312,7 @@
map (fn ((name, stature), (role, t)) =>
let
val role =
- if is_type_enc_higher_order type_enc andalso
+ if is_format_with_defs format andalso
role <> Conjecture andalso is_legitimate_tptp_def t then
Definition
else
@@ -2777,7 +2780,7 @@
| CNF_UEQ => filter_cnf_ueq_problem
| FOF => I
| TFF (_, TPTP_Implicit) => I
- | THF (_, TPTP_Implicit, _) => I
+ | THF (_, TPTP_Implicit, _, _) => I
| _ => declare_undeclared_syms_in_atp_problem type_enc)
val (problem, pool) = problem |> nice_atp_problem readable_names format
fun add_sym_ary (s, {min_ary, ...} : sym_info) =
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon May 28 13:38:07 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon May 28 20:25:38 2012 +0200
@@ -327,7 +327,10 @@
(* LEO-II *)
-val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice)
+(* LEO-II supports definitions, but it performs significantly better on our
+ benchmarks when they are not used. *)
+val leo2_thf0 =
+ THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
val leo2_config : atp_config =
{exec = (["LEO2_HOME"], "leo"),
@@ -352,7 +355,8 @@
(* Satallax *)
-val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice)
+val satallax_thf0 =
+ THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
val satallax_config : atp_config =
{exec = (["SATALLAX_HOME"], "satallax"),
@@ -532,7 +536,8 @@
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
-val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
+val dummy_thf_format =
+ THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)