added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
--- 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 10:06:35 2012 +0100
@@ -1939,10 +1939,7 @@
AAbs ((name, ho_type_from_typ format type_enc true 0 T),
term Elsewhere tm)
else
- ATerm (("LAMBDA", "LAMBDA"), []) (*###*)
-(*###
raise Fail "unexpected lambda-abstraction"
-*)
| IApp _ => raise Fail "impossible \"IApp\""
val T = ityp_of u
in
@@ -2764,7 +2761,7 @@
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])) =
+ fun add_eq_deps (SOME true) (ATerm (s, [lhs as _, rhs])) =
if is_tptp_equal s then
case make_head_roll lhs of
(head, rest as _ :: _) =>
@@ -2772,16 +2769,20 @@
| _ => I
else
I
- | add_eq_deps _ = I
- 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
+ | add_eq_deps _ _ = I
+ fun add_deps pred (Formula (_, role, phi, _, info)) =
+ if pred (role, info) then
+ formula_fold (SOME (role <> Conjecture)) add_eq_deps phi
else
I
+ | add_deps _ _ = I
+ fun has_status status (_, info) =
+ extract_isabelle_status info = SOME status
+ fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
val graph =
- Graph.empty |> fold (fold (add_line_deps spec_eqN) o snd) problem
- |> fold (fold (add_line_deps simpN) o snd) problem
+ Graph.empty
+ |> fold (fold (add_deps (has_status spec_eqN)) o snd) problem
+ |> fold (fold (add_deps (has_status simpN orf is_conj)) o snd) problem
fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1
fun add_weights _ [] = I
| add_weights weight syms =
--- 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 10:06:35 2012 +0100
@@ -290,8 +290,8 @@
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 =
+fun e_term_order_info_arguments false false _ = ""
+ | e_term_order_info_arguments 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 "") ^
@@ -310,7 +310,7 @@
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 ^ " " ^
+ e_term_order_info_arguments 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,
--- a/src/HOL/Tools/Metis/metis_generate.ML Tue Mar 20 00:44:30 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML Tue Mar 20 10:06:35 2012 +0100
@@ -32,6 +32,7 @@
val prepare_metis_problem :
Proof.context -> type_enc -> string -> thm list -> thm list
-> int Symtab.table * (Metis_Thm.thm * isa_thm) list
+ * (unit -> (string * int) list)
* ((string * term) list * (string * term) list)
end
@@ -221,10 +222,11 @@
|> fst |> chop (length conj_clauses)
|> pairself (maps (map (zero_var_indexes o snd)))
val num_conjs = length conj_clauses
+ (* Pretend every clause is a "simp" rule, to guide the term ordering. *)
val clauses =
- map2 (fn j => pair (Int.toString j, (Local, General)))
+ map2 (fn j => pair (Int.toString j, (Local, Simp)))
(0 upto num_conjs - 1) conj_clauses @
- map2 (fn j => pair (Int.toString (num_conjs + j), (Local, General)))
+ map2 (fn j => pair (Int.toString (num_conjs + j), (Local, Simp)))
(0 upto length fact_clauses - 1) fact_clauses
val (old_skolems, props) =
fold_rev (fn (name, th) => fn (old_skolems, props) =>
@@ -241,8 +243,8 @@
*)
val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
val (atp_problem, _, _, lifted, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans
- false false false [] @{prop False} props
+ prepare_atp_problem ctxt CNF Hypothesis Hypothesis type_enc false
+ lam_trans false false false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (lines_for_atp_problem CNF atp_problem))
@@ -251,6 +253,7 @@
val axioms =
atp_problem
|> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
- in (sym_tab, axioms, (lifted, old_skolems)) end
+ fun ord_info () = atp_problem_term_order_info atp_problem
+ in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end
end;
--- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Mar 20 00:44:30 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Mar 20 10:06:35 2012 +0100
@@ -12,6 +12,7 @@
val trace : bool Config.T
val verbose : bool Config.T
val new_skolemizer : bool Config.T
+ val advisory_simp : bool Config.T
val type_has_top_sort : typ -> bool
val metis_tac :
string list -> string -> Proof.context -> thm list -> int -> tactic
@@ -30,6 +31,8 @@
val new_skolemizer =
Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
+val advisory_simp =
+ Attrib.setup_config_bool @{binding metis_advisory_simp} (K false)
(* Designed to work also with monomorphic instances of polymorphic theorems. *)
fun have_common_thm ths1 ths2 =
@@ -105,12 +108,12 @@
val eq_th' = Goal.prove_internal [] eq_ct (K (Tactic.rtac eq_th 1))
in Thm.equal_elim eq_th' th end
-val clause_params =
- {ordering = Metis_KnuthBendixOrder.default,
+fun clause_params ordering =
+ {ordering = ordering,
orderLiterals = Metis_Clause.UnsignedLiteralOrder,
orderTerms = true}
-val active_params =
- {clause = clause_params,
+fun active_params ordering =
+ {clause = clause_params ordering,
prefactor = #prefactor Metis_Active.default,
postfactor = #postfactor Metis_Active.default}
val waiting_params =
@@ -118,7 +121,18 @@
variablesWeight = 0.5,
literalsWeight = 0.1,
models = []}
-val resolution_params = {active = active_params, waiting = waiting_params}
+fun resolution_params ordering =
+ {active = active_params ordering, waiting = waiting_params}
+
+fun kbo_advisory_simp_ordering ord_info =
+ let
+ fun weight (m, _) =
+ AList.lookup (op =) ord_info (Metis_Name.toString m) |> the_default 1
+ fun precedence p =
+ case int_ord (pairself weight p) of
+ EQUAL => #precedence Metis_KnuthBendixOrder.default p
+ | ord => ord
+ in {weight = weight, precedence = precedence} end
(* Main function to start Metis proof and reconstruction *)
fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
@@ -143,7 +157,7 @@
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
val type_enc = type_enc_from_string Strict type_enc
- val (sym_tab, axioms, concealed) =
+ val (sym_tab, axioms, ord_info, concealed) =
prepare_metis_problem ctxt type_enc lam_trans cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
@@ -156,11 +170,16 @@
val _ = trace_msg ctxt (fn () => "METIS CLAUSES")
val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
+ val ordering =
+ if Config.get ctxt advisory_simp then
+ kbo_advisory_simp_ordering (ord_info ())
+ else
+ Metis_KnuthBendixOrder.default
in
case filter (fn t => prop_of t aconv @{prop False}) cls of
false_th :: _ => [false_th RS @{thm FalseE}]
| [] =>
- case Metis_Resolution.new resolution_params
+ case Metis_Resolution.new (resolution_params ordering)
{axioms = axioms |> map fst, conjecture = []}
|> Metis_Resolution.loop of
Metis_Resolution.Contradiction mth =>