put the SMT weights back where they belong, so that they're also used by Mirabelle

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Dec 17 18:23:56 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Dec 17 21:31:19 2010 +0100
@@ -53,6 +53,12 @@
   type prover = params -> minimize_command -> prover_problem -> prover_result
 
   (* for experimentation purposes -- do not use in production code *)
+  val smt_weights : bool Unsynchronized.ref
+  val smt_weight_min_facts : int Unsynchronized.ref
+  val smt_min_weight : int Unsynchronized.ref
+  val smt_max_weight : int Unsynchronized.ref
+  val smt_max_weight_index : int Unsynchronized.ref
+  val smt_weight_curve : (int -> int) Unsynchronized.ref
   val smt_max_iters : int Unsynchronized.ref
   val smt_iter_fact_frac : real Unsynchronized.ref
   val smt_iter_time_frac : real Unsynchronized.ref
@@ -73,9 +79,13 @@
   val dest_dir : string Config.T
   val problem_prefix : string Config.T
   val measure_run_time : bool Config.T
+  val weight_smt_fact :
+    theory -> int -> ((string * locality) * thm) * int
+    -> (string * locality) * (int option * thm)
   val untranslated_fact : prover_fact -> (string * locality) * thm
   val smt_weighted_fact :
-    prover_fact -> (string * locality) * (int option * thm)
+    theory -> int -> prover_fact * int
+    -> (string * locality) * (int option * thm)
   val available_provers : Proof.context -> unit
   val kill_provers : unit -> unit
   val running_provers : unit -> unit
@@ -277,7 +287,26 @@
 fun proof_banner auto =
   if auto then "Auto Sledgehammer found a proof" else "Try this command"
 
-(* generic TPTP-based ATPs *)
+val smt_weights = Unsynchronized.ref true
+val smt_weight_min_facts = Unsynchronized.ref 20
+
+(* FUDGE *)
+val smt_min_weight = Unsynchronized.ref 0
+val smt_max_weight = Unsynchronized.ref 10
+val smt_max_weight_index = Unsynchronized.ref 200
+val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
+
+fun smt_fact_weight j num_facts =
+  if !smt_weights andalso num_facts >= !smt_weight_min_facts then
+    SOME (!smt_max_weight
+          - (!smt_max_weight - !smt_min_weight + 1)
+            * !smt_weight_curve (Int.max (0, !smt_max_weight_index - j - 1))
+            div !smt_weight_curve (!smt_max_weight_index))
+  else
+    NONE
+
+fun weight_smt_fact thy num_facts ((info, th), j) =
+  (info, (smt_fact_weight j num_facts, th |> Thm.transfer thy))
 
 fun untranslated_fact (Untranslated_Fact p) = p
   | untranslated_fact (ATP_Translated_Fact (_, p)) = p
@@ -285,8 +314,11 @@
 fun atp_translated_fact _ (ATP_Translated_Fact p) = p
   | atp_translated_fact ctxt fact =
     translate_atp_fact ctxt (untranslated_fact fact)
-fun smt_weighted_fact (SMT_Weighted_Fact p) = p
-  | smt_weighted_fact fact = untranslated_fact fact |> apsnd (pair NONE)
+fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
+  | smt_weighted_fact thy num_facts (fact, j) =
+    (untranslated_fact fact, j) |> weight_smt_fact thy num_facts
+
+(* generic TPTP-based ATPs *)
 
 fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
   | int_opt_add _ _ = NONE
@@ -602,7 +634,10 @@
          : prover_problem) =
   let
     val ctxt = Proof.context_of state
-    val facts = facts |> map smt_weighted_fact
+    val thy = Proof.theory_of state
+    val num_facts = length facts
+    val facts = facts ~~ (0 upto num_facts - 1)
+                |> map (smt_weighted_fact thy num_facts)
     val {outcome, used_facts, run_time_in_msecs} =
       smt_filter_loop name params state subgoal smt_head facts
     val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Dec 17 18:23:56 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Dec 17 21:31:19 2010 +0100
@@ -14,12 +14,6 @@
 
   (* for experimentation purposes -- do not use in production code *)
   val show_facts_in_proofs : bool Unsynchronized.ref
-  val smt_weights : bool Unsynchronized.ref
-  val smt_weight_min_facts : int Unsynchronized.ref
-  val smt_min_weight : int Unsynchronized.ref
-  val smt_max_weight : int Unsynchronized.ref
-  val smt_max_weight_index : int Unsynchronized.ref
-  val smt_weight_curve : (int -> int) Unsynchronized.ref
 
   val run_sledgehammer :
     params -> bool -> int -> relevance_override -> (string -> minimize_command)
@@ -143,27 +137,6 @@
        (false, state))
   end
 
-val smt_weights = Unsynchronized.ref true
-val smt_weight_min_facts = Unsynchronized.ref 20
-
-(* FUDGE *)
-val smt_min_weight = Unsynchronized.ref 0
-val smt_max_weight = Unsynchronized.ref 10
-val smt_max_weight_index = Unsynchronized.ref 200
-val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
-
-fun smt_fact_weight j num_facts =
-  if !smt_weights andalso num_facts >= !smt_weight_min_facts then
-    SOME (!smt_max_weight
-          - (!smt_max_weight - !smt_min_weight + 1)
-            * !smt_weight_curve (Int.max (0, !smt_max_weight_index - j - 1))
-            div !smt_weight_curve (!smt_max_weight_index))
-  else
-    NONE
-
-fun weight_smt_fact thy num_facts (fact, j) =
-  fact |> apsnd (pair (smt_fact_weight j num_facts) o Thm.transfer thy)
-
 fun class_of_smt_solver ctxt name =
   ctxt |> select_smt_solver name
        |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
@@ -173,6 +146,9 @@
   | smart_par_list_map f [x] = [f x]
   | smart_par_list_map f xs = Par_List.map f xs
 
+fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p
+  | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"
+
 (* FUDGE *)
 val auto_max_relevant_divisor = 2
 
@@ -200,32 +176,29 @@
               | NONE => ()
       val _ = if auto then () else Output.urgent_message "Sledgehammering..."
       val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
-      fun run_provers get_facts translate maybe_smt_head provers
-                      (res as (success, state)) =
-        if success orelse null provers then
-          res
-        else
-          let
-            val facts = get_facts ()
-            val num_facts = length facts
-            val facts = facts ~~ (0 upto num_facts - 1)
-                        |> map (translate num_facts)
-            val problem =
-              {state = state, goal = goal, subgoal = i, subgoal_count = n,
-               facts = facts,
-               smt_head = maybe_smt_head (map smt_weighted_fact facts) i}
-            val run_prover = run_prover params auto minimize_command only
-          in
-            if auto then
-              fold (fn prover => fn (true, state) => (true, state)
-                                  | (false, _) => run_prover problem prover)
-                   provers (false, state)
-            else
-              provers
-              |> (if blocking then smart_par_list_map else map)
-                     (run_prover problem)
-              |> exists fst |> rpair state
-          end
+      fun run_provers state get_facts translate maybe_smt_head provers =
+        let
+          val facts = get_facts ()
+          val num_facts = length facts
+          val facts = facts ~~ (0 upto num_facts - 1)
+                      |> map (translate num_facts)
+          val problem =
+            {state = state, goal = goal, subgoal = i, subgoal_count = n,
+             facts = facts,
+             smt_head = maybe_smt_head
+                  (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
+          val run_prover = run_prover params auto minimize_command only
+        in
+          if auto then
+            fold (fn prover => fn (true, state) => (true, state)
+                                | (false, _) => run_prover problem prover)
+                 provers (false, state)
+          else
+            provers
+            |> (if blocking then smart_par_list_map else map)
+                   (run_prover problem)
+            |> exists fst |> rpair state
+        end
       fun get_facts label no_dangerous_types relevance_fudge provers =
         let
           val max_max_relevant =
@@ -254,24 +227,27 @@
                      else
                        ())
         end
-      val run_atps =
-        run_provers
-            (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
-            (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
-            (K (K NONE)) atps
+      fun run_atps (accum as (success, _)) =
+        if success orelse null atps then
+          accum
+        else
+          run_provers state
+              (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
+              (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
+              (K (K NONE)) atps
       fun run_smts (accum as (success, _)) =
         if success orelse null smts then
           accum
         else
           let
             val facts = get_facts "SMT solver" true smt_relevance_fudge smts
-            val translate = SMT_Weighted_Fact oo weight_smt_fact thy
-            val maybe_smt_head = try o SMT_Solver.smt_filter_head state
+            val weight = SMT_Weighted_Fact oo weight_smt_fact thy
+            fun smt_head facts =
+              try (SMT_Solver.smt_filter_head state (facts ()))
           in
             smts |> map (`(class_of_smt_solver ctxt))
                  |> AList.group (op =)
-                 |> map (fn (_, smts) => run_provers (K facts) translate
-                                                     maybe_smt_head smts accum)
+                 |> map (run_provers state (K facts) weight smt_head o snd)
                  |> exists fst |> rpair state
           end
       fun run_atps_and_smt_solvers () =