src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML

   type mode = Sledgehammer_Prover.mode
   type prover = Sledgehammer_Prover.prover
 
   val smt2_builtins : bool Config.T
   val smt2_triggers : bool Config.T
-  val smt2_weights : bool Config.T
-  val smt2_weight_min_facts : int Config.T
-  val smt2_min_weight : int Config.T
-  val smt2_max_weight : int Config.T
-  val smt2_max_weight_index : int Config.T
-  val smt2_weight_curve : (int -> int) Unsynchronized.ref
   val smt2_max_slices : int Config.T
   val smt2_slice_fact_frac : real Config.T
   val smt2_slice_time_frac : real Config.T
   val smt2_slice_min_secs : int Config.T
 

 open Sledgehammer_Isar
 open Sledgehammer_Prover
 
 val smt2_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt2_builtins} (K true)
 val smt2_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt2_triggers} (K true)
-val smt2_weights = Attrib.setup_config_bool @{binding sledgehammer_smt2_weights} (K true)
-val smt2_weight_min_facts =
-  Attrib.setup_config_int @{binding sledgehammer_smt2_weight_min_facts} (K 20)
 
 val is_smt2_prover = member (op =) o SMT2_Config.available_solvers_of
-
-(* FUDGE *)
-val smt2_min_weight = Attrib.setup_config_int @{binding sledgehammer_smt2_min_weight} (K 0)
-val smt2_max_weight = Attrib.setup_config_int @{binding sledgehammer_smt2_max_weight} (K 10)
-val smt2_max_weight_index =
-  Attrib.setup_config_int @{binding sledgehammer_smt2_max_weight_index} (K 200)
-val smt2_weight_curve = Unsynchronized.ref (fn x : int => x * x)
-
-fun smt2_fact_weight ctxt j num_facts =
-  if Config.get ctxt smt2_weights andalso num_facts >= Config.get ctxt smt2_weight_min_facts then
-    let
-      val min = Config.get ctxt smt2_min_weight
-      val max = Config.get ctxt smt2_max_weight
-      val max_index = Config.get ctxt smt2_max_weight_index
-      val curve = !smt2_weight_curve
-    in
-      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1)) div curve max_index)
-    end
-  else
-    NONE
-
-fun weight_smt2_fact ctxt num_facts ((info, th), j) =
-  (info, (smt2_fact_weight ctxt j num_facts, th))
 
 (* "SMT2_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
    properly in the SMT module, we must interpret these here. *)
 val z3_failures =
   [(101, OutOfResources),

 
     val state = Proof.map_context (repair_context) state
     val ctxt = Proof.context_of state
     val max_slices = if slice then Config.get ctxt smt2_max_slices else 1
 
-    fun do_slice timeout slice outcome0 time_so_far
-        (weighted_factss as (fact_filter, weighted_facts) :: _) =
+    fun do_slice timeout slice outcome0 time_so_far (factss as (fact_filter, facts) :: _) =
       let
         val timer = Timer.startRealTimer ()
         val slice_timeout =
           if slice < max_slices then
             let val ms = Time.toMilliseconds timeout in

                 Real.ceil (Config.get ctxt smt2_slice_time_frac * Real.fromInt ms)))
               |> Time.fromMilliseconds
             end
           else
             timeout
-        val num_facts = length weighted_facts
+        val num_facts = length facts
         val _ =
           if debug then
             quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
             " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
             |> Output.urgent_message
           else
             ()
         val birth = Timer.checkRealTimer timer
 
         val filter_result as {outcome, ...} =
-          SMT2_Solver.smt2_filter ctxt goal weighted_facts i slice_timeout
+          SMT2_Solver.smt2_filter ctxt goal facts i slice_timeout
           handle exn =>
             if Exn.is_interrupt exn orelse debug then
               reraise exn
             else
               {outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)),

         if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
            Time.> (timeout, Time.zeroTime) then
           let
             val new_num_facts =
               Real.ceil (Config.get ctxt smt2_slice_fact_frac * Real.fromInt num_facts)
-            val weighted_factss as (new_fact_filter, _) :: _ =
-              weighted_factss
+            val factss as (new_fact_filter, _) :: _ =
+              factss
               |> (fn (x :: xs) => xs @ [x])
               |> app_hd (apsnd (take new_num_facts))
             val show_filter = fact_filter <> new_fact_filter
 
             fun num_of_facts fact_filter num_facts =

                 "..."
                 |> Output.urgent_message
               else
                 ()
           in
-            do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
+            do_slice timeout (slice + 1) outcome0 time_so_far factss
           end
         else
           {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result,
-           used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
+           used_from = facts, run_time = time_so_far}
       end
   in
     do_slice timeout 1 NONE Time.zeroTime
   end
 

     minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
 
-    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
-
-    fun weight_facts facts =
-      let val num_facts = length facts in
-        map (weight_smt2_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
-      end
-
-    val weighted_factss = map (apsnd weight_facts) factss
     val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
-      smt2_filter_loop name params state goal subgoal weighted_factss
+      smt2_filter_loop name params state goal subgoal factss
     val used_named_facts = map snd fact_ids
     val used_facts = map fst used_named_facts
     val outcome = Option.map failure_of_smt2_failure outcome
 
     val (preplay, message, message_tail) =