--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Dec 17 16:45:31 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Dec 17 16:55:27 2010 +0100
@@ -12,6 +12,14 @@
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
@@ -117,20 +125,20 @@
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