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
1.1 --- a/src/HOL/Tools/refute.ML Mon May 31 18:00:28 2010 +0200
1.2 +++ b/src/HOL/Tools/refute.ML Mon May 31 18:49:32 2010 +0200
1.3 @@ -1165,6 +1165,13 @@
1.4 val fm_u = (if negate then toFalse else toTrue) (hd intrs)
1.5 val fm_ax = PropLogic.all (map toTrue (tl intrs))
1.6 val fm = PropLogic.all [#wellformed args, fm_ax, fm_u]
1.7 + val _ =
1.8 + (if satsolver = "dpll" orelse satsolver = "enumerate" then
1.9 + warning ("Using SAT solver " ^ quote satsolver ^
1.10 + "; for better performance, consider installing an \
1.11 + \external solver.")
1.12 + else
1.13 + ());
1.14 val solver =
1.15 SatSolver.invoke_solver satsolver
1.16 handle Option.Option =>
2.1 --- a/src/HOL/Tools/sat_solver.ML Mon May 31 18:00:28 2010 +0200
2.2 +++ b/src/HOL/Tools/sat_solver.ML Mon May 31 18:49:32 2010 +0200
2.3 @@ -543,10 +543,6 @@
2.4 (* do not call solver "auto" from within "auto" *)
2.5 loop solvers
2.6 else (
2.7 - (if name="dpll" orelse name="enumerate" then
2.8 - warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
2.9 - else
2.10 - ());
2.11 (* apply 'solver' to 'fm' *)
2.12 solver fm
2.13 handle SatSolver.NOT_CONFIGURED => loop solvers