# HG changeset patch
# User webertj
# Date 1100873110 -3600
# Node ID 576fd0b65ed859befa04552146724cccaea4d929
# Parent  a5bea99352d6716a793374353d730a1197ecc8a5
solver auto now returns the result of the first solver that does not raise NOT_CONFIGURED (which may be UNKNOWN)

diff -r a5bea99352d6 -r 576fd0b65ed8 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Fri Nov 19 14:00:31 2004 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Fri Nov 19 15:05:10 2004 +0100
@@ -484,8 +484,8 @@
 
 (* ------------------------------------------------------------------------- *)
 (* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses  *)
-(* all installed solvers (other than "auto" itself) until one returns either *)
-(* SATISFIABLE or UNSATISFIABLE                                              *)
+(* the first installed solver (other than "auto" itself) that does not raise *)
+(* 'NOT_CONFIGURED'.  (However, the solver may return 'UNKNOWN'.)            *)
 (* ------------------------------------------------------------------------- *)
 
 let
@@ -497,18 +497,14 @@
 			if name="auto" then
 				(* do not call solver "auto" from within "auto" *)
 				loop solvers
-			else
-			(
+			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' *)
-				(case solver fm of
-				  SatSolver.SATISFIABLE a => SatSolver.SATISFIABLE a
-				| SatSolver.UNSATISFIABLE => SatSolver.UNSATISFIABLE
-				| SatSolver.UNKNOWN       => loop solvers)
-				handle SatSolver.NOT_CONFIGURED => loop solvers
+				solver fm
+					handle SatSolver.NOT_CONFIGURED => loop solvers
 			)
 	in
 		loop (rev (!SatSolver.solvers))