enable SMT weights and triggers, since they lead to slight improvements according to the Judgment Day suite
authorblanchet
Tue, 08 Feb 2011 16:10:06 +0100
changeset 41723 bb366da22483
parent 41722 9575694d2da5
child 41724 14d135c09bec
enable SMT weights and triggers, since they lead to slight improvements according to the Judgment Day suite
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Feb 08 08:58:24 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Feb 08 16:10:06 2011 +0100
@@ -281,8 +281,8 @@
 fun proof_banner auto =
   if auto then "Auto Sledgehammer found a proof" else "Try this command"
 
-val smt_triggers = Unsynchronized.ref false
-val smt_weights = Unsynchronized.ref false
+val smt_triggers = Unsynchronized.ref true
+val smt_weights = Unsynchronized.ref true
 val smt_weight_min_facts = Unsynchronized.ref 20
 
 (* FUDGE *)