src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

 signature SLEDGEHAMMER_RUN =
 sig
   type relevance_override = Sledgehammer_Filter.relevance_override
   type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
   type params = Sledgehammer_Provers.params
+
+  (* 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 run_sledgehammer :
     params -> bool -> int -> relevance_override -> (string -> minimize_command)
     -> Proof.state -> bool * Proof.state
 end;

       (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
        (false, state))
   end
 
 val smt_weights = Unsynchronized.ref true
-val smt_weight_min_facts = 20
+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_index = Unsynchronized.ref 200
+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
+  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_index - j - 1))
-            div !smt_weight_curve (!smt_max_index))
+            * !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)