solver "auto" now issues a warning when it uses solver "enumerate"
authorwebertj
Wed May 26 17:42:46 2004 +0200 (2004-05-26)
changeset 14805eff7b9df27e9
parent 14804 8de39d3e8eb6
child 14806 b42ad431cbae
solver "auto" now issues a warning when it uses solver "enumerate"
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Wed May 26 14:57:06 2004 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Wed May 26 17:42:46 2004 +0200
     1.3 @@ -369,8 +369,8 @@
     1.4  			if name="auto" then
     1.5  				None
     1.6  			else
     1.7 -				((if name="dpll" then
     1.8 -					warning ("Using SAT solver \"dpll\"; for better performance, consider using an external solver.")
     1.9 +				((if name="dpll" orelse name="enumerate" then
    1.10 +					warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
    1.11  				else
    1.12  					());
    1.13  				solver fm)) (rev (!SatSolver.solvers))