# HG changeset patch # User blanchet # Date 1338229538 -7200 # Node ID 989a34fa72b3dda1c224b8a10b70ad3c6b4638a0 # Parent 1d11af40b106fe5dde11c29112a17d8926635cbb don't generate definitions for LEO-II -- this cuases more harm than good diff -r 1d11af40b106 -r 989a34fa72b3 src/HOL/Tools/ATP/atp_problem.ML --- 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. *) diff -r 1d11af40b106 -r 989a34fa72b3 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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) = diff -r 1d11af40b106 -r 989a34fa72b3 src/HOL/Tools/ATP/atp_systems.ML --- 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)