# HG changeset patch # User blanchet # Date 1332200670 -3600 # Node ID 2409b484e1ccf66dcc86804234e2a80a666bd20f # Parent ea6695d58aad8b32a28d690f473989f2ffa5eac1 continued implementation of term ordering attributes diff -r ea6695d58aad -r 2409b484e1cc src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Tue Mar 20 00:44:30 2012 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Tue Mar 20 00:44:30 2012 +0100 @@ -118,19 +118,19 @@ let val thy = Proof_Context.theory_of ctxt val prob_file = File.tmp_path (Path.explode "prob.tptp") - val {exec, arguments, proof_delims, known_failures, ...} = - get_atp thy (case format of DFG _ => spassN | _ => eN) - val _ = problem |> lines_for_atp_problem format (K []) + val atp = case format of DFG _ => spass_newN | _ => eN + val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp + val ord = effective_term_order ctxt atp + val _ = problem |> lines_for_atp_problem format ord (K []) |> File.write_list prob_file val command = File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^ - " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^ + " " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^ File.shell_path prob_file in TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command |> fst - |> extract_tstplike_proof_and_outcome false true proof_delims - known_failures + |> extract_tstplike_proof_and_outcome false true proof_delims known_failures |> snd end handle TimeLimit.TimeOut => SOME TimedOut @@ -214,7 +214,8 @@ atp_problem |> (case format of DFG _ => I | _ => add_inferences_to_problem infers) |> order_problem_facts name_ord - val ss = lines_for_atp_problem format (K []) atp_problem + val ord = effective_term_order ctxt eN (* dummy *) + val ss = lines_for_atp_problem format ord (K []) atp_problem val _ = app (File.append path) ss in () end diff -r ea6695d58aad -r 2409b484e1cc src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Mar 20 00:44:30 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Mar 20 00:44:30 2012 +0100 @@ -22,6 +22,12 @@ AFun of 'a ho_type * 'a ho_type | ATyAbs of 'a list * 'a ho_type + type term_order = + {is_lpo : bool, + gen_weights : bool, + gen_prec : bool, + gen_simp : bool} + datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit datatype thf_flavor = THF_Without_Choice | THF_With_Choice @@ -75,7 +81,7 @@ val tptp_true : string val tptp_empty_list : string val isabelle_info_prefix : string - val isabelle_info : atp_format -> string -> int -> (string, 'a) ho_term list + val isabelle_info : string -> int -> (string, 'a) ho_term list val extract_isabelle_status : (string, 'a) ho_term list -> string option val extract_isabelle_rank : (string, 'a) ho_term list -> int val introN : string @@ -112,7 +118,8 @@ val is_format_higher_order : atp_format -> bool val is_format_typed : atp_format -> bool val lines_for_atp_problem : - atp_format -> (unit -> (string * int) list) -> string problem -> string list + atp_format -> term_order -> (unit -> (string * int) list) -> string problem + -> string list val ensure_cnf_problem : (string * string) problem -> (string * string) problem val filter_cnf_ueq_problem : @@ -147,6 +154,12 @@ AFun of 'a ho_type * 'a ho_type | ATyAbs of 'a list * 'a ho_type +type term_order = + {is_lpo : bool, + gen_weights : bool, + gen_prec : bool, + gen_simp : bool} + datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit datatype thf_flavor = THF_Without_Choice | THF_With_Choice @@ -215,12 +228,11 @@ (* Currently, only newer versions of SPASS, with sorted DFG format support, can process Isabelle metainformation. *) -fun isabelle_info (DFG DFG_Sorted) status rank = - [] |> rank <> default_rank - ? cons (ATerm (isabelle_info_prefix ^ rankN, - [ATerm (string_of_int rank, [])])) - |> status <> "" ? cons (ATerm (isabelle_info_prefix ^ status, [])) - | isabelle_info _ _ _ = [] +fun isabelle_info status rank = + [] |> rank <> default_rank + ? cons (ATerm (isabelle_info_prefix ^ rankN, + [ATerm (string_of_int rank, [])])) + |> status <> "" ? cons (ATerm (isabelle_info_prefix ^ status, [])) fun extract_isabelle_status (ATerm (s, []) :: _) = try (unprefix isabelle_info_prefix) s @@ -420,11 +432,6 @@ |> enclose "(" ")" | tptp_string_for_formula format (AAtom tm) = tptp_string_for_term format tm -fun the_source (SOME source) = source - | the_source NONE = - ATerm ("inference", - ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", []))) - fun tptp_string_for_format CNF = tptp_cnf | tptp_string_for_format CNF_UEQ = tptp_cnf | tptp_string_for_format FOF = tptp_fof @@ -436,17 +443,13 @@ tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^ string_for_type format ty ^ ").\n" | tptp_string_for_problem_line format - (Formula (ident, kind, phi, source, info)) = + (Formula (ident, kind, phi, source, _)) = tptp_string_for_format format ^ "(" ^ ident ^ ", " ^ tptp_string_for_kind kind ^ ",\n (" ^ tptp_string_for_formula format phi ^ ")" ^ - (case (source, info) of - (NONE, []) => "" - | (SOME tm, []) => ", " ^ tptp_string_for_term format tm - | (_, tms) => - ", " ^ tptp_string_for_term format (the_source source) ^ - ", " ^ tptp_string_for_term format (ATerm (tptp_empty_list, tms))) ^ - ").\n" + (case source of + SOME tm => ", " ^ tptp_string_for_term format tm + | NONE => "") ^ ").\n" fun tptp_lines format = maps (fn (_, []) => [] @@ -460,13 +463,13 @@ fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2 | binder_atypes _ = [] -fun dfg_string_for_formula flavor info = +fun dfg_string_for_formula gen_simp flavor info = let fun suffix_tag top_level s = if top_level then case extract_isabelle_status info of - SOME s' => if s' = simpN then s ^ ":lr" - else if s' = spec_eqN then s ^ ":lt" + SOME s' => if s' = spec_eqN then s ^ ":lt" + else if s' = simpN andalso gen_simp then s ^ ":lr" else s | NONE => s else @@ -496,7 +499,11 @@ | str_for_formula top_level (AAtom tm) = str_for_term top_level tm in str_for_formula true end -fun dfg_lines flavor ord_weights problem = +fun maybe_enclose bef aft "" = "% " ^ bef ^ aft + | maybe_enclose bef aft s = bef ^ s ^ aft + +fun dfg_lines flavor {is_lpo, gen_weights, gen_prec, gen_simp} ord_info + problem = let val sorted = (flavor = DFG_Sorted) val format = DFG flavor @@ -510,7 +517,8 @@ fun formula pred (Formula (ident, kind, phi, _, info)) = if pred kind then let val rank = extract_isabelle_rank info in - "formula(" ^ dfg_string_for_formula flavor info phi ^ ", " ^ ident ^ + "formula(" ^ dfg_string_for_formula gen_simp flavor info phi ^ + ", " ^ ident ^ (if rank = default_rank then "" else ", " ^ string_of_int rank) ^ ")." |> SOME end @@ -522,19 +530,22 @@ filt (fn Decl (_, sym, ty) => if is_function_type ty then SOME (ary sym ty) else NONE | _ => NONE) - |> flat |> commas |> enclose "functions [" "]." + |> flat |> commas |> maybe_enclose "functions [" "]." val pred_aries = filt (fn Decl (_, sym, ty) => if is_predicate_type ty then SOME (ary sym ty) else NONE | _ => NONE) - |> flat |> commas |> enclose "predicates [" "]." + |> flat |> commas |> maybe_enclose "predicates [" "]." fun sorts () = filt (fn Decl (_, sym, AType (s, [])) => if s = tptp_type_of_types then SOME sym else NONE | _ => NONE) @ [[dfg_individual_type]] - |> flat |> commas |> enclose "sorts [" "]." + |> flat |> commas |> maybe_enclose "sorts [" "]." + val ord_info = + if sorted andalso (gen_weights orelse gen_prec) then ord_info () else [] fun do_term_order_weights () = - ord_weights () |> map spair |> commas |> enclose "weights [" "]." + (if gen_weights then ord_info else []) + |> map spair |> commas |> maybe_enclose "weights [" "]." val syms = [func_aries] @ (if sorted then [do_term_order_weights ()] else []) @ [pred_aries] @ (if sorted then [sorts ()] else []) @@ -554,27 +565,37 @@ filt (formula (curry (op <>) Conjecture)) |> separate [""] |> flat val conjs = filt (formula (curry (op =) Conjecture)) |> separate [""] |> flat - fun list_of _ [] = [] - | list_of heading ss = - "list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @ - ["end_of_list.\n\n"] + (* The second layer of ")." is a temporary workaround for a quirk in SPASS's + parser. *) + val settings = + (if is_lpo then ["set_flag(Ordering, 1).)."] else []) @ + (if gen_prec then + [ord_info |> map fst |> rev |> commas + |> maybe_enclose "set_precedence(" ")."] + else + []) + fun list_of _ _ _ [] = [] + | list_of heading bef aft ss = + "list_of_" ^ heading ^ ".\n" :: bef :: map (suffix "\n") ss @ + [aft, "end_of_list.\n\n"] in "\nbegin_problem(isabelle).\n\n" :: - list_of "descriptions" + list_of "descriptions" "" "" ["name({**}).", "author({**}).", "status(unknown).", "description({**})."] @ - list_of "symbols" syms @ - list_of "declarations" decls @ - list_of "formulae(axioms)" axioms @ - list_of "formulae(conjectures)" conjs @ + list_of "symbols" "" "" syms @ + list_of "declarations" "" "" decls @ + list_of "formulae(axioms)" "" "" axioms @ + list_of "formulae(conjectures)" "" "" conjs @ + list_of "settings(SPASS)" "{*\n" "*}\n" settings @ ["end_problem.\n"] end -fun lines_for_atp_problem format ord_weights problem = +fun lines_for_atp_problem format ord ord_info problem = "% This file was generated by Isabelle (most likely Sledgehammer)\n\ \% " ^ timestamp () ^ "\n" :: (case format of - DFG flavor => dfg_lines flavor ord_weights + DFG flavor => dfg_lines flavor ord ord_info | _ => tptp_lines format) problem @@ -739,7 +760,7 @@ fun add j = let val nice_name = - nice_prefix ^ (if j = 0 then "" else string_of_int j) + nice_prefix ^ (if j = 1 then "" else string_of_int j) in case Symtab.lookup (snd the_pool) nice_name of SOME full_name' => @@ -750,7 +771,7 @@ (Symtab.update_new (full_name, nice_name) (fst the_pool), Symtab.update_new (nice_name, full_name) (snd the_pool))) end - in add 0 |> apsnd SOME end + in add 1 |> apsnd SOME end fun avoid_clash_with_alt_ergo_type_vars s = if is_tptp_variable s then s else s ^ "_" diff -r ea6695d58aad -r 2409b484e1cc src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Mar 20 00:44:30 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Mar 20 00:44:30 2012 +0100 @@ -108,7 +108,7 @@ -> string problem * string Symtab.table * (string * stature) list vector * (string * term) list * int Symtab.table val atp_problem_selection_weights : string problem -> (string * real) list - val atp_problem_term_order_weights : string problem -> (string * int) list + val atp_problem_term_order_info : string problem -> (string * int) list end; structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE = @@ -1671,7 +1671,7 @@ val type_tag = `(make_fixed_const NONE) type_tag_name -fun type_tag_idempotence_fact format type_enc = +fun type_tag_idempotence_fact type_enc = let fun var s = ATerm (`I s, []) fun tag tm = ATerm (type_tag, [var "A", tm]) @@ -1679,7 +1679,7 @@ in Formula (type_tag_idempotence_helper_name, Axiom, eq_formula type_enc [] [] false (tag tagged_var) tagged_var, - NONE, isabelle_info format spec_eqN helper_rank) + NONE, isabelle_info spec_eqN helper_rank) end fun should_specialize_helper type_enc t = @@ -2006,15 +2006,15 @@ NONE, let val rank = rank j in case snd stature of - Intro => isabelle_info format introN rank - | Elim => isabelle_info format elimN rank - | Simp => isabelle_info format simpN rank - | Spec_Eq => isabelle_info format spec_eqN rank - | _ => isabelle_info format "" rank + Intro => isabelle_info introN rank + | Elim => isabelle_info elimN rank + | Simp => isabelle_info simpN rank + | Spec_Eq => isabelle_info spec_eqN rank + | _ => isabelle_info "" rank end) |> Formula -fun formula_line_for_class_rel_clause format type_enc +fun formula_line_for_class_rel_clause type_enc ({name, subclass, superclass, ...} : class_rel_clause) = let val ty_arg = ATerm (tvar_a_name, []) in Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, @@ -2023,21 +2023,21 @@ type_class_formula type_enc superclass ty_arg]) |> mk_aquant AForall [(tvar_a_name, atype_of_type_vars type_enc)], - NONE, isabelle_info format introN helper_rank) + NONE, isabelle_info introN helper_rank) end fun formula_from_arity_atom type_enc (class, t, args) = ATerm (t, map (fn arg => ATerm (arg, [])) args) |> type_class_formula type_enc class -fun formula_line_for_arity_clause format type_enc +fun formula_line_for_arity_clause type_enc ({name, prem_atoms, concl_atom} : arity_clause) = Formula (arity_clause_prefix ^ name, Axiom, mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms) (formula_from_arity_atom type_enc concl_atom) |> mk_aquant AForall (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)), - NONE, isabelle_info format introN helper_rank) + NONE, isabelle_info introN helper_rank) fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc ({name, kind, iformula, atomic_types, ...} : translated_formula) = @@ -2246,7 +2246,7 @@ always_guard_var_in_formula (SOME true) |> close_formula_universally |> bound_tvars type_enc true (atomic_types_of T), - NONE, isabelle_info format introN helper_rank) + NONE, isabelle_info introN helper_rank) fun formula_line_for_tags_mono_type ctxt format mono type_enc T = let val x_var = ATerm (`make_bound_var "X", []) in @@ -2255,7 +2255,7 @@ Axiom, eq_formula type_enc (atomic_types_of T) [] false (tag_with_type ctxt format mono type_enc NONE T x_var) x_var, - NONE, isabelle_info format spec_eqN helper_rank) + NONE, isabelle_info spec_eqN helper_rank) end fun problem_lines_for_mono_types ctxt format mono type_enc Ts = @@ -2326,7 +2326,7 @@ |> close_formula_universally |> bound_tvars type_enc (n > 1) (atomic_types_of T) |> maybe_negate, - NONE, isabelle_info format introN helper_rank) + NONE, isabelle_info introN helper_rank) end fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s @@ -2360,7 +2360,7 @@ in cons (Formula (ident_base ^ "_res", kind, eq (tag_with res_T (cst bounds)) (cst tagged_bounds), - NONE, isabelle_info format spec_eqN helper_rank)) + NONE, isabelle_info spec_eqN helper_rank)) end else I @@ -2372,7 +2372,7 @@ cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind, eq (cst (bounds1 @ tag_with arg_T bound :: bounds2)) (cst bounds), - NONE, isabelle_info format spec_eqN helper_rank)) + NONE, isabelle_info spec_eqN helper_rank)) | _ => raise Fail "expected nonempty tail" else I @@ -2480,7 +2480,7 @@ in ([tm1, tm2], [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate, - NONE, isabelle_info format spec_eqN helper_rank)]) + NONE, isabelle_info spec_eqN helper_rank)]) |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I else pair_append (do_alias (ary - 1))) end @@ -2663,7 +2663,7 @@ |> map (formula_line_for_fact ctxt polym_constrs format helper_prefix I false true mono type_enc (K default_rank)) |> (if needs_type_tag_idempotence ctxt type_enc then - cons (type_tag_idempotence_fact format type_enc) + cons (type_tag_idempotence_fact type_enc) else I) (* Reordering these might confuse the proof reconstruction code or the SPASS @@ -2673,10 +2673,8 @@ (uncurried_alias_eqsN, uncurried_alias_eq_lines), (factsN, fact_lines), (class_relsN, - map (formula_line_for_class_rel_clause format type_enc) - class_rel_clauses), - (aritiesN, - map (formula_line_for_arity_clause format type_enc) arity_clauses), + map (formula_line_for_class_rel_clause type_enc) class_rel_clauses), + (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses), (helpersN, helper_lines), (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs)), (conjsN, @@ -2756,22 +2754,26 @@ val max_term_order_weight = 2147483647 -fun atp_problem_term_order_weights problem = +fun atp_problem_term_order_info problem = let + fun add_edge s s' = + Graph.default_node (s, ()) + #> Graph.default_node (s', ()) + #> Graph.add_edge_acyclic (s, s') fun add_term_deps head (ATerm (s, args)) = - is_tptp_user_symbol s ? perhaps (try (Graph.add_edge_acyclic (s, head))) + is_tptp_user_symbol s ? perhaps (try (add_edge s head)) #> fold (add_term_deps head) args | add_term_deps head (AAbs (_, tm)) = add_term_deps head tm fun add_eq_deps (ATerm (s, [lhs as _, rhs])) = if is_tptp_equal s then - let val (head, rest) = make_head_roll lhs in - fold (add_term_deps head) (rhs :: rest) - end + case make_head_roll lhs of + (head, rest as _ :: _) => + is_tptp_user_symbol head ? fold (add_term_deps head) (rhs :: rest) + | _ => I else I | add_eq_deps _ = I - fun add_line_deps _ (Decl (_, s, ty)) = - is_function_type ty ? Graph.default_node (s, ()) + fun add_line_deps _ (Decl _) = I | add_line_deps status (Formula (_, _, phi, _, info)) = if extract_isabelle_status info = SOME status then formula_fold NONE (K add_eq_deps) phi @@ -2787,6 +2789,8 @@ #> add_weights (next_weight weight) (fold (union (op =) o Graph.immediate_succs graph) syms []) in + (* Sorting is not just for aesthetics: It specifies the precedence order + for the term ordering (KBO or LPO), from smaller to larger values. *) [] |> add_weights 1 (Graph.minimals graph) |> sort (int_ord o pairself snd) end diff -r ea6695d58aad -r 2409b484e1cc src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Mar 20 00:44:30 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Mar 20 00:44:30 2012 +0100 @@ -7,22 +7,19 @@ signature ATP_SYSTEMS = sig + type term_order = ATP_Problem.term_order type atp_format = ATP_Problem.atp_format type formula_kind = ATP_Problem.formula_kind type failure = ATP_Proof.failure - type term_order = - {is_lpo : bool, - generate_weights : bool, - generate_prec : bool, - generate_simp : bool} type slice_spec = int * atp_format * string * string * bool type atp_config = {exec : string * string, required_execs : (string * string) list, arguments : Proof.context -> bool -> string -> Time.time - -> (unit -> (string * real) list) -> string, + -> term_order * (unit -> (string * int) list) + * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, known_failures : (failure * string) list, conj_sym_kind : formula_kind, @@ -88,7 +85,8 @@ required_execs : (string * string) list, arguments : Proof.context -> bool -> string -> Time.time - -> (unit -> (string * real) list) -> string, + -> term_order * (unit -> (string * int) list) + * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, known_failures : (failure * string) list, conj_sym_kind : formula_kind, @@ -175,29 +173,26 @@ val xprecN = "_prec" val xsimpN = "_simp" (* SPASS-specific *) +(* Possible values for "atp_term_order": + "smart", "(kbo(_weights)?|lpo)(_prec|_simp)?" *) val term_order = Attrib.setup_config_string @{binding atp_term_order} (K smartN) -type term_order = - {is_lpo : bool, - generate_weights : bool, - generate_prec : bool, - generate_simp : bool} - fun effective_term_order ctxt atp = let val ord = Config.get ctxt term_order in if ord = smartN then if atp = spass_newN then - {is_lpo = false, generate_weights = true, generate_prec = false, - generate_simp = true} + {is_lpo = false, gen_weights = true, gen_prec = false, gen_simp = true} else - {is_lpo = false, generate_weights = false, generate_prec = false, - generate_simp = false} + {is_lpo = false, gen_weights = false, gen_prec = false, + gen_simp = false} else - {is_lpo = String.isSubstring lpoN ord, - generate_weights = String.isSubstring xweightsN ord, - generate_prec = String.isSubstring xprecN ord, - generate_simp = String.isSubstring xsimpN ord} + 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} + end end (* Alt-Ergo *) @@ -254,41 +249,56 @@ val e_sym_offs_weight_span = Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0) -fun e_selection_heuristic_case method fw sow = - if method = e_fun_weightN then fw - else if method = e_sym_offset_weightN then sow - else raise Fail ("unexpected " ^ quote method) +fun e_selection_heuristic_case heuristic fw sow = + if heuristic = e_fun_weightN then fw + else if heuristic = e_sym_offset_weightN then sow + else raise Fail ("unexpected " ^ quote heuristic) -fun scaled_e_selection_weight ctxt method w = - w * Config.get ctxt (e_selection_heuristic_case method +fun scaled_e_selection_weight ctxt heuristic w = + w * Config.get ctxt (e_selection_heuristic_case heuristic e_fun_weight_span e_sym_offs_weight_span) - + Config.get ctxt (e_selection_heuristic_case method + + Config.get ctxt (e_selection_heuristic_case heuristic e_fun_weight_base e_sym_offs_weight_base) |> Real.ceil |> signed_string_of_int -fun e_selection_weight_arguments ctxt method sel_weights = - if method = e_autoN then - "-xAutoDev" +fun e_selection_weight_arguments ctxt heuristic sel_weights = + if heuristic = e_autoN then + "-xAuto" else (* supplied by Stephan Schulz *) "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ \--destructive-er-aggressive --destructive-er --presat-simplify \ \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \ - \-H'(4*" ^ e_selection_heuristic_case method "FunWeight" "SymOffsetWeight" ^ + \-H'(4*" ^ + e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^ "(SimulateSOS, " ^ - (e_selection_heuristic_case method + (e_selection_heuristic_case heuristic e_default_fun_weight e_default_sym_offs_weight |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^ ",20,1.5,1.5,1" ^ (sel_weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ - scaled_e_selection_weight ctxt method w) + scaled_e_selection_weight ctxt heuristic w) |> implode) ^ "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\ \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ \FIFOWeight(PreferProcessed))'" +val e_ord_weights = + map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode "," +fun e_ord_precedence [_] = "" + | e_ord_precedence info = info |> map fst |> space_implode "<" + +fun e_term_order_info_arguments _ false false _ = "" + | e_term_order_info_arguments ctxt gen_weights gen_prec ord_info = + let val ord_info = ord_info () in + (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " + else "") ^ + (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " + else "") + end + fun effective_e_selection_heuristic ctxt = if is_old_e_version () then e_autoN else Config.get ctxt e_selection_heuristic @@ -296,10 +306,13 @@ {exec = ("E_HOME", "eproof"), required_execs = [], arguments = - fn ctxt => fn _ => fn method => fn timeout => fn sel_weights => - "--tstp-in --tstp-out -l5 " ^ - e_selection_weight_arguments ctxt method sel_weights ^ - " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs 2 timeout), + fn ctxt => fn _ => fn heuristic => fn timeout => + fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => + "--tstp-in --tstp-out --output-level=5 --silent " ^ + e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^ + e_term_order_info_arguments ctxt gen_weights gen_prec ord_info ^ " " ^ + "--term-ordering=" ^ (if is_lpo then "LPO4" else "Auto") ^ " " ^ + "--cpu-limit=" ^ string_of_int (to_secs 2 timeout), proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures @ @@ -309,14 +322,14 @@ conj_sym_kind = Hypothesis, prem_kind = Conjecture, best_slices = fn ctxt => - let val method = effective_e_selection_heuristic ctxt in + let val heuristic = effective_e_selection_heuristic ctxt in (* FUDGE *) - if method = e_smartN then + if heuristic = e_smartN then [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN))), (0.334, (true, ((50, FOF, "mono_guards??", combsN, false), e_fun_weightN))), (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false), e_sym_offset_weightN)))] else - [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), method)))] + [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), heuristic)))] end} val e = (eN, e_config) diff -r ea6695d58aad -r 2409b484e1cc src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Mar 20 00:44:30 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Mar 20 00:44:30 2012 +0100 @@ -651,7 +651,8 @@ Monomorph.monomorph atp_schematic_consts_of rths ctxt |> fst |> tl |> curry ListPair.zip (map fst facts) - |> maps (fn (name, rths) => map (pair name o snd) rths) + |> maps (fn (name, rths) => + map (pair name o zero_var_indexes o snd) rths) end fun run_slice time_left (cache_key, cache_value) (slice, (time_frac, (complete, @@ -710,20 +711,18 @@ type_enc false lam_trans uncurried_aliases readable_names true hyp_ts concl_t fun sel_weights () = atp_problem_selection_weights atp_problem - fun ord_weights () = - if #generate_weights (effective_term_order ctxt name) then - atp_problem_term_order_weights atp_problem - else - [] + fun ord_info () = atp_problem_term_order_info atp_problem + val ord = effective_term_order ctxt name val full_proof = debug orelse isar_proof + val args = arguments ctxt full_proof extra slice_timeout + (ord, ord_info, sel_weights) val command = - File.shell_path command ^ " " ^ - arguments ctxt full_proof extra slice_timeout sel_weights ^ - " " ^ File.shell_path prob_file + File.shell_path command ^ " " ^ args ^ " " ^ + File.shell_path prob_file |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1" val _ = atp_problem - |> lines_for_atp_problem format ord_weights + |> lines_for_atp_problem format ord ord_info |> cons ("% " ^ command ^ "\n") |> File.write_list prob_file val ((output, run_time), (atp_proof, outcome)) =