author blanchet Tue, 20 Mar 2012 10:06:35 +0100 changeset 47039 1b36a05a070d parent 47038 2409b484e1cc child 47040 78e88d26f19d
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
 src/HOL/Tools/ATP/atp_problem_generate.ML file | annotate | diff | comparison | revisions src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | comparison | revisions src/HOL/Tools/Metis/metis_generate.ML file | annotate | diff | comparison | revisions src/HOL/Tools/Metis/metis_tactic.ML file | annotate | diff | comparison | revisions
```--- 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 @@
-    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
(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
```--- 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)
+  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}
+
+  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