--- 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
--- 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 ^ "_"
--- 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
--- 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)
--- 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)) =