# HG changeset patch
# User blanchet
# Date 1283354830 -7200
# Node ID 78ac4468cf9d4254c76384e0ba885e235adb76f9
# Parent  6905ba37376c7f5953990d8433cf44eabc0a590c
got rid of the "theory_relevant" option;
instead, have fudge factors that behave more smoothly for all provers

diff -r 6905ba37376c -r 78ac4468cf9d doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Sep 01 16:46:11 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Sep 01 17:27:10 2010 +0200
@@ -467,11 +467,11 @@
 filter. If the option is set to \textit{smart}, it is set to a value that was
 empirically found to be appropriate for the ATP. A typical value would be 300.
 
-\opsmartx{theory\_relevant}{theory\_irrelevant}
-Specifies whether the theory from which a fact comes should be taken into
-consideration by the relevance filter. If the option is set to \textit{smart},
-it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs;
-empirical results suggest that these are the best settings.
+%\opsmartx{theory\_relevant}{theory\_irrelevant}
+%Specifies whether the theory from which a fact comes should be taken into
+%consideration by the relevance filter. If the option is set to \textit{smart},
+%it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs;
+%empirical results suggest that these are the best settings.
 
 %\opfalse{defs\_relevant}{defs\_irrelevant}
 %Specifies whether the definition of constants occurring in the formula to prove
diff -r 6905ba37376c -r 78ac4468cf9d src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Sep 01 16:46:11 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Sep 01 17:27:10 2010 +0200
@@ -103,15 +103,14 @@
                            SOME rf => (rf := the (Real.fromString value); false)
                          | NONE => true)
 
-         val {relevance_thresholds, full_types, max_relevant, theory_relevant,
-              ...} = Sledgehammer_Isar.default_params thy args
+         val {relevance_thresholds, full_types, max_relevant, ...} =
+           Sledgehammer_Isar.default_params thy args
          val subgoal = 1
          val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
          val facts =
            SF.relevant_facts ctxt full_types
                relevance_thresholds
                (the_default default_max_relevant max_relevant)
-               (the_default false theory_relevant)
                {add = [], del = [], only = false} facts hyp_ts concl_t
            |> map (fst o fst)
          val (found_facts, lost_facts) =
diff -r 6905ba37376c -r 78ac4468cf9d src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 01 16:46:11 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 01 17:27:10 2010 +0200
@@ -20,7 +20,6 @@
      proof_delims: (string * string) list,
      known_failures: (failure * string) list,
      default_max_relevant: int,
-     default_theory_relevant: bool,
      explicit_forall: bool,
      use_conjecture_for_hypotheses: bool}
 
@@ -53,7 +52,6 @@
    proof_delims: (string * string) list,
    known_failures: (failure * string) list,
    default_max_relevant: int,
-   default_theory_relevant: bool,
    explicit_forall: bool,
    use_conjecture_for_hypotheses: bool}
 
@@ -160,7 +158,6 @@
       (OutOfResources, "SZS status: ResourceOut"),
       (OutOfResources, "SZS status ResourceOut")],
    default_max_relevant = 500 (* FUDGE *),
-   default_theory_relevant = false,
    explicit_forall = false,
    use_conjecture_for_hypotheses = true}
 
@@ -187,7 +184,6 @@
       (MalformedInput, "Free Variable"),
       (SpassTooOld, "tptp2dfg")],
    default_max_relevant = 350 (* FUDGE *),
-   default_theory_relevant = true,
    explicit_forall = true,
    use_conjecture_for_hypotheses = true}
 
@@ -217,7 +213,6 @@
       (Unprovable, "Termination reason: Satisfiable"),
       (VampireTooOld, "not a valid option")],
    default_max_relevant = 400 (* FUDGE *),
-   default_theory_relevant = false,
    explicit_forall = false,
    use_conjecture_for_hypotheses = true}
 
@@ -256,8 +251,8 @@
   | SOME sys => sys
 
 fun remote_config system_name system_versions proof_delims known_failures
-                  default_max_relevant default_theory_relevant
-                  use_conjecture_for_hypotheses : prover_config =
+                  default_max_relevant use_conjecture_for_hypotheses
+                  : prover_config =
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
    arguments = fn _ => fn timeout =>
@@ -269,26 +264,21 @@
      known_failures @ known_perl_failures @
      [(TimedOut, "says Timeout")],
    default_max_relevant = default_max_relevant,
-   default_theory_relevant = default_theory_relevant,
    explicit_forall = true,
    use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
 
 fun remotify_config system_name system_versions
         ({proof_delims, known_failures, default_max_relevant,
-          default_theory_relevant, use_conjecture_for_hypotheses, ...}
-         : prover_config) : prover_config =
+          use_conjecture_for_hypotheses, ...} : prover_config) : prover_config =
   remote_config system_name system_versions proof_delims known_failures
-                default_max_relevant default_theory_relevant
-                use_conjecture_for_hypotheses
+                default_max_relevant use_conjecture_for_hypotheses
 
 val remotify_name = prefix "remote_"
 fun remote_prover name system_name system_versions proof_delims known_failures
-                  default_max_relevant default_theory_relevant
-                  use_conjecture_for_hypotheses =
+                  default_max_relevant use_conjecture_for_hypotheses =
   (remotify_name name,
    remote_config system_name system_versions proof_delims known_failures
-                 default_max_relevant default_theory_relevant
-                 use_conjecture_for_hypotheses)
+                 default_max_relevant use_conjecture_for_hypotheses)
 fun remotify_prover (name, config) system_name system_versions =
   (remotify_name name, remotify_config system_name system_versions config)
 
@@ -296,10 +286,10 @@
 val remote_vampire = remotify_prover vampire "Vampire" ["9.0", "1.0", "0.6"]
 val remote_sine_e =
   remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")]
-                1000 (* FUDGE *) false true
+                1000 (* FUDGE *) true
 val remote_snark =
   remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []
-                350 (* FUDGE *) false true
+                350 (* FUDGE *) true
 
 (* Setup *)
 
diff -r 6905ba37376c -r 78ac4468cf9d src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 16:46:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 17:27:10 2010 +0200
@@ -22,7 +22,6 @@
      explicit_apply: bool,
      relevance_thresholds: real * real,
      max_relevant: int option,
-     theory_relevant: bool option,
      isar_proof: bool,
      isar_shrink_factor: int,
      timeout: Time.time,
@@ -91,7 +90,6 @@
    explicit_apply: bool,
    relevance_thresholds: real * real,
    max_relevant: int option,
-   theory_relevant: bool option,
    isar_proof: bool,
    isar_shrink_factor: int,
    timeout: Time.time,
@@ -215,11 +213,11 @@
 
 fun prover_fun atp_name
         {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
-         known_failures, default_max_relevant, default_theory_relevant,
-         explicit_forall, use_conjecture_for_hypotheses}
+         known_failures, default_max_relevant, explicit_forall,
+         use_conjecture_for_hypotheses}
         ({debug, verbose, overlord, full_types, explicit_apply,
-          relevance_thresholds, max_relevant, theory_relevant, isar_proof,
-          isar_shrink_factor, timeout, ...} : params)
+          relevance_thresholds, max_relevant, isar_proof, isar_shrink_factor,
+          timeout, ...} : params)
         minimize_command
         ({subgoal, goal = (ctxt, (chained_ths, th)), relevance_override,
           axioms} : problem) =
@@ -236,7 +234,6 @@
       | NONE =>
         (relevant_facts ctxt full_types relevance_thresholds
                         (the_default default_max_relevant max_relevant)
-                        (the_default default_theory_relevant theory_relevant)
                         relevance_override chained_ths hyp_ts concl_t
          |> tap ((fn n => print_v (fn () =>
                           "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
diff -r 6905ba37376c -r 78ac4468cf9d src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 01 16:46:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 01 17:27:10 2010 +0200
@@ -34,7 +34,7 @@
     Proof.context -> unit Symtab.table -> thm list
     -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
   val relevant_facts :
-    Proof.context -> bool -> real * real -> int -> bool -> relevance_override
+    Proof.context -> bool -> real * real -> int -> relevance_override
     -> thm list -> term list -> term -> ((string * locality) * thm) list
 end;
 
@@ -46,10 +46,28 @@
 val trace = Unsynchronized.ref false
 fun trace_msg msg = if !trace then tracing (msg ()) else ()
 
-(* experimental feature *)
+(* experimental features *)
 val term_patterns = false
+val respect_no_atp = true
 
-val respect_no_atp = true
+(* FUDGE *)
+val worse_irrel_freq = Unsynchronized.ref 100.0
+val higher_order_irrel_weight = Unsynchronized.ref 1.05
+val abs_rel_weight = Unsynchronized.ref 0.5
+val abs_irrel_weight = Unsynchronized.ref 2.0
+val skolem_irrel_weight = Unsynchronized.ref 0.75
+val theory_const_rel_weight = Unsynchronized.ref 0.5
+val theory_const_irrel_weight = Unsynchronized.ref 0.25
+val intro_bonus = Unsynchronized.ref 0.15
+val elim_bonus = Unsynchronized.ref 0.15
+val simp_bonus = Unsynchronized.ref 0.15
+val local_bonus = Unsynchronized.ref 0.55
+val assum_bonus = Unsynchronized.ref 1.05
+val chained_bonus = Unsynchronized.ref 1.5
+val max_imperfect = Unsynchronized.ref 11.5
+val max_imperfect_exp = Unsynchronized.ref 1.0
+val threshold_divisor = Unsynchronized.ref 2.0
+val ridiculous_threshold = Unsynchronized.ref 0.1
 
 datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
 
@@ -235,8 +253,9 @@
 
 (*Inserts a dummy "constant" referring to the theory name, so that relevance
   takes the given theory into account.*)
-fun theory_const_prop_of theory_relevant th =
-  if theory_relevant then
+fun theory_const_prop_of th =
+  if exists (curry (op <) 0.0) [!theory_const_rel_weight,
+                                !theory_const_irrel_weight] then
     let
       val name = Context.theory_name (theory_of_thm th)
       val t = Const (name ^ theory_const_suffix, @{typ bool})
@@ -262,7 +281,7 @@
 
 structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
 
-fun count_axiom_consts theory_relevant thy =
+fun count_axiom_consts thy =
   let
     fun do_const const (s, T) ts =
       (* Two-dimensional table update. Constant maps to types maps to count. *)
@@ -275,7 +294,7 @@
       | (Free x, ts) => do_const false x ts
       | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
       | (_, ts) => fold do_term ts
-  in do_term o theory_const_prop_of theory_relevant o snd end
+  in do_term o theory_const_prop_of o snd end
 
 
 (**** Actual Filtering Code ****)
@@ -298,10 +317,6 @@
    rare ones. *)
 fun rel_weight_for order freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
 
-(* FUDGE *)
-val worse_irrel_freq = Unsynchronized.ref 100.0
-val higher_order_irrel_weight = Unsynchronized.ref 1.05
-
 (* Irrelevant constants are treated differently. We associate lower penalties to
    very rare constants and very common ones -- the former because they can't
    lead to the inclusion of too many new facts, and the latter because they are
@@ -313,13 +328,6 @@
     * pow_int (!higher_order_irrel_weight) (order - 1)
   end
 
-(* FUDGE *)
-val abs_rel_weight = Unsynchronized.ref 0.5
-val abs_irrel_weight = Unsynchronized.ref 2.0
-val skolem_irrel_weight = Unsynchronized.ref 0.75
-val theory_const_rel_weight = Unsynchronized.ref 0.5
-val theory_const_irrel_weight = Unsynchronized.ref 0.25
-
 (* Computes a constant's weight, as determined by its frequency. *)
 fun generic_pconst_weight abs_weight skolem_weight theory_const_weight
                           weight_for f const_tab (c as (s, PType (m, _))) =
@@ -335,14 +343,6 @@
   generic_pconst_weight (!abs_irrel_weight) (!skolem_irrel_weight)
                     (!theory_const_irrel_weight) irrel_weight_for swap const_tab
 
-(* FUDGE *)
-val intro_bonus = Unsynchronized.ref 0.15
-val elim_bonus = Unsynchronized.ref 0.15
-val simp_bonus = Unsynchronized.ref 0.15
-val local_bonus = Unsynchronized.ref 0.55
-val assum_bonus = Unsynchronized.ref 1.05
-val chained_bonus = Unsynchronized.ref 1.5
-
 fun locality_bonus General = 0.0
   | locality_bonus Intro = !intro_bonus
   | locality_bonus Elim = !elim_bonus
@@ -388,19 +388,14 @@
 fun pconsts_in_axiom thy t =
   Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
               (pconsts_in_terms thy true (SOME true) [t]) []
-fun pair_consts_axiom theory_relevant thy axiom =
-  case axiom |> snd |> theory_const_prop_of theory_relevant
-             |> pconsts_in_axiom thy of
+fun pair_consts_axiom thy axiom =
+  case axiom |> snd |> theory_const_prop_of |> pconsts_in_axiom thy of
     [] => NONE
   | consts => SOME ((axiom, consts), NONE)
 
 type annotated_thm =
   (((unit -> string) * locality) * thm) * (string * ptype) list
 
-(* FUDGE *)
-val max_imperfect = Unsynchronized.ref 11.5
-val max_imperfect_exp = Unsynchronized.ref 1.0
-
 fun take_most_relevant max_relevant remaining_max
                        (candidates : (annotated_thm * real) list) =
   let
@@ -431,16 +426,11 @@
   else
     tab
 
-(* FUDGE *)
-val threshold_divisor = Unsynchronized.ref 2.0
-val ridiculous_threshold = Unsynchronized.ref 0.1
-
-fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant
+fun relevance_filter ctxt threshold0 decay max_relevant
                      ({add, del, ...} : relevance_override) axioms goal_ts =
   let
     val thy = ProofContext.theory_of ctxt
-    val const_tab =
-      fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty
+    val const_tab = fold (count_axiom_consts thy) axioms Symtab.empty
     val goal_const_tab =
       pconsts_in_terms thy false (SOME false) goal_ts
       |> fold (if_empty_replace_with_locality thy axioms)
@@ -533,7 +523,7 @@
         end
   in
     axioms |> filter_out (member Thm.eq_thm del_thms o snd)
-           |> map_filter (pair_consts_axiom theory_relevant thy)
+           |> map_filter (pair_consts_axiom thy)
            |> iter 0 max_relevant threshold0 goal_const_tab []
            |> tap (fn res => trace_msg (fn () =>
                                 "Total relevant: " ^ Int.toString (length res)))
@@ -791,8 +781,8 @@
 (***************************************************************)
 
 fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant
-                   theory_relevant (relevance_override as {add, del, only})
-                   chained_ths hyp_ts concl_t =
+                   (relevance_override as {add, del, only}) chained_ths hyp_ts
+                   concl_t =
   let
     val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
                           1.0 / Real.fromInt (max_relevant + 1))
@@ -814,8 +804,8 @@
      else if threshold0 < 0.0 then
        axioms
      else
-       relevance_filter ctxt threshold0 decay max_relevant theory_relevant
-                        relevance_override axioms (concl_t :: hyp_ts))
+       relevance_filter ctxt threshold0 decay max_relevant relevance_override
+                        axioms (concl_t :: hyp_ts))
     |> map (apfst (apfst (fn f => f ())))
   end
 
diff -r 6905ba37376c -r 78ac4468cf9d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 01 16:46:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 01 17:27:10 2010 +0200
@@ -70,7 +70,6 @@
    ("explicit_apply", "false"),
    ("relevance_thresholds", "45 85"),
    ("max_relevant", "smart"),
-   ("theory_relevant", "smart"),
    ("isar_proof", "false"),
    ("isar_shrink_factor", "1")]
 
@@ -83,7 +82,6 @@
    ("no_overlord", "overlord"),
    ("partial_types", "full_types"),
    ("implicit_apply", "explicit_apply"),
-   ("theory_irrelevant", "theory_relevant"),
    ("no_isar_proof", "isar_proof")]
 
 val params_for_minimize =
@@ -180,7 +178,6 @@
       lookup_int_pair "relevance_thresholds"
       |> pairself (fn n => 0.01 * Real.fromInt n)
     val max_relevant = lookup_int_option "max_relevant"
-    val theory_relevant = lookup_bool_option "theory_relevant"
     val isar_proof = lookup_bool "isar_proof"
     val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
     val timeout = lookup_time "timeout"
@@ -189,9 +186,8 @@
     {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
      atps = atps, full_types = full_types, explicit_apply = explicit_apply,
      relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
-     theory_relevant = theory_relevant, isar_proof = isar_proof,
-     isar_shrink_factor = isar_shrink_factor, timeout = timeout,
-     expect = expect}
+     isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
+     timeout = timeout, expect = expect}
   end
 
 fun get_params thy = extract_params (default_raw_params thy)
diff -r 6905ba37376c -r 78ac4468cf9d src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Sep 01 16:46:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Sep 01 17:27:10 2010 +0200
@@ -53,8 +53,8 @@
       {blocking = true, debug = debug, verbose = verbose, overlord = overlord,
        atps = atps, full_types = full_types, explicit_apply = explicit_apply,
        relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
-       theory_relevant = NONE, isar_proof = isar_proof,
-       isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
+       isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
+       timeout = timeout, expect = ""}
     val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
     val {context = ctxt, facts, goal} = Proof.goal state
     val problem =