author blanchet Tue, 22 Jun 2010 17:07:39 +0200 changeset 37503 c2dfa26b9da6 parent 37502 a8f7b25d5478 child 37504 4308d2bbbca8
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 16:50:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 17:07:39 2010 +0200
@@ -50,19 +50,6 @@
fun strip_Trueprop (@{const Trueprop} \$ t) = t
| strip_Trueprop t = t;

-(*A surprising number of theorems contain only a few significant constants.
-  These include all induction rules, and other general theorems. Filtering
-  theorems in clause form reveals these complexities in the form of Skolem
-  functions. If we were instead to filter theorems in their natural form,
-  some other method of measuring theorem complexity would become necessary.*)
-
-fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0);
-
-(*The default seems best in practice. A constant function of one ignores
-  the constant frequencies.*)
-val weight_fn = log_weight2;
-
-
(*** constants with types ***)

(*An abstraction of Isabelle types*)
@@ -158,20 +145,22 @@

structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);

-fun count_axiom_consts theory_relevant thy ((thm,_), tab) =
-  let fun count_const (a, T, tab) =
-        let val (c, cts) = const_with_typ thy (a,T)
-        in  (*Two-dimensional table update. Constant maps to types maps to count.*)
-            Symtab.map_default (c, CTtab.empty)
-                               (CTtab.map_default (cts,0) (fn n => n+1)) tab
-        end
-      fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
-        | count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
-        | count_term_consts (t \$ u, tab) =
-            count_term_consts (t, count_term_consts (u, tab))
-        | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
-        | count_term_consts (_, tab) = tab
-  in  count_term_consts (const_prop_of theory_relevant thm, tab)  end;
+fun count_axiom_consts theory_relevant thy (thm, _) =
+  let
+    fun do_const (a, T) =
+      let val (c, cts) = const_with_typ thy (a,T) in
+        (* Two-dimensional table update. Constant maps to types maps to
+           count. *)
+        CTtab.map_default (cts, 0) (Integer.add 1)
+        |> Symtab.map_default (c, CTtab.empty)
+      end
+    fun do_term (Const x) = do_const x
+      | do_term (Free x) = do_const x
+      | do_term (Const (@{const_name skolem_id}, _) \$ _) = I
+      | do_term (t \$ u) = do_term t #> do_term u
+      | do_term (Abs (_, _, t)) = do_term t
+      | do_term _ = I
+  in do_term (const_prop_of theory_relevant thm) end

(**** Actual Filtering Code ****)
@@ -181,16 +170,25 @@
CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m)
(the (Symtab.lookup ctab c)) 0

-(*Add in a constant's weight, as determined by its frequency.*)
-fun add_ct_weight ctab ((c,T), w) =
-  w + weight_fn (real (const_frequency ctab (c,T)));
+(*A surprising number of theorems contain only a few significant constants.
+  These include all induction rules, and other general theorems. Filtering
+  theorems in clause form reveals these complexities in the form of Skolem
+  functions. If we were instead to filter theorems in their natural form,
+  some other method of measuring theorem complexity would become necessary.*)
+
+(* "log" seems best in practice. A constant function of one ignores the constant
+   frequencies. *)
+fun log_weight2 (x:real) = 1.0 + 2.0 / Math.ln (x + 1.0)
+
+(* Computes a constant's weight, as determined by its frequency. *)
+val ct_weight = log_weight2 o real oo const_frequency

(*Relevant constants are weighted according to frequency,
but irrelevant constants are simply counted. Otherwise, Skolem functions,
which are rare, would harm a clause's chances of being picked.*)
fun clause_weight ctab gctyps consts_typs =
let val rel = filter (uni_mem gctyps) consts_typs
-        val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel
+        val rel_weight = fold (curry Real.+ o ct_weight ctab) rel 0.0
in
rel_weight / (rel_weight + real (length consts_typs - length rel))
end;
@@ -276,7 +274,7 @@
(more_rejects @ rejects)
end
| relevant (newrels, rejects)
-                     ((ax as (clsthm as (thm, ((name, n), orig_th)),
+                     ((ax as (clsthm as (_, ((name, n), orig_th)),
consts_typs)) :: axs) =
let
val weight = if member Thm.eq_thm add_thms orig_th then 1.0
@@ -303,8 +301,8 @@
thy (axioms : cnf_thm list) goals =
if relevance_threshold > 0.0 then
let
-      val const_tab = List.foldl (count_axiom_consts theory_relevant thy)
-                                 Symtab.empty axioms
+      val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
+                           Symtab.empty
val goal_const_tab = get_goal_consts_typs thy goals
val _ =
trace_msg (fn () => "Initial constants: " ^```