# HG changeset patch
# User blanchet
# Date 1275324572 -7200
# Node ID 3625d37a0079e8f7852613901db75f5727c85f8b
# Parent  e01c1fe245cda419a25d8e3e703493eefc13de62
move SAT solver warning from every invocation of SAT solver to the tool, Refute, that uses it;
"size_change" rarely needs anything beyond "dpll", so this warning is annoying at best, and when "size_change" is called from Nitpick the warning confuses users, who then think that Nitpick is using "dpll" when it's really using MiniSat or some other fast solver

diff -r e01c1fe245cd -r 3625d37a0079 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Mon May 31 18:00:28 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Mon May 31 18:49:32 2010 +0200
@@ -1165,6 +1165,13 @@
         val fm_u  = (if negate then toFalse else toTrue) (hd intrs)
         val fm_ax = PropLogic.all (map toTrue (tl intrs))
         val fm    = PropLogic.all [#wellformed args, fm_ax, fm_u]
+        val _ =
+          (if satsolver = "dpll" orelse satsolver = "enumerate" then
+            warning ("Using SAT solver " ^ quote satsolver ^
+                     "; for better performance, consider installing an \
+                     \external solver.")
+          else
+            ());
         val solver =
           SatSolver.invoke_solver satsolver
           handle Option.Option =>
diff -r e01c1fe245cd -r 3625d37a0079 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Mon May 31 18:00:28 2010 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Mon May 31 18:49:32 2010 +0200
@@ -543,10 +543,6 @@
         (* do not call solver "auto" from within "auto" *)
         loop solvers
       else (
-        (if name="dpll" orelse name="enumerate" then
-          warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
-        else
-          ());
         (* apply 'solver' to 'fm' *)
         solver fm
           handle SatSolver.NOT_CONFIGURED => loop solvers