src/HOL/Tools/sat_solver.ML
changeset 15299 576fd0b65ed8
parent 15128 da03f05815b0
child 15313 24aee76539df
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Fri Nov 19 14:00:31 2004 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Fri Nov 19 15:05:10 2004 +0100
     1.3 @@ -484,8 +484,8 @@
     1.4  
     1.5  (* ------------------------------------------------------------------------- *)
     1.6  (* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses  *)
     1.7 -(* all installed solvers (other than "auto" itself) until one returns either *)
     1.8 -(* SATISFIABLE or UNSATISFIABLE                                              *)
     1.9 +(* the first installed solver (other than "auto" itself) that does not raise *)
    1.10 +(* 'NOT_CONFIGURED'.  (However, the solver may return 'UNKNOWN'.)            *)
    1.11  (* ------------------------------------------------------------------------- *)
    1.12  
    1.13  let
    1.14 @@ -497,18 +497,14 @@
    1.15  			if name="auto" then
    1.16  				(* do not call solver "auto" from within "auto" *)
    1.17  				loop solvers
    1.18 -			else
    1.19 -			(
    1.20 +			else (
    1.21  				(if name="dpll" orelse name="enumerate" then
    1.22  					warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
    1.23  				else
    1.24  					());
    1.25  				(* apply 'solver' to 'fm' *)
    1.26 -				(case solver fm of
    1.27 -				  SatSolver.SATISFIABLE a => SatSolver.SATISFIABLE a
    1.28 -				| SatSolver.UNSATISFIABLE => SatSolver.UNSATISFIABLE
    1.29 -				| SatSolver.UNKNOWN       => loop solvers)
    1.30 -				handle SatSolver.NOT_CONFIGURED => loop solvers
    1.31 +				solver fm
    1.32 +					handle SatSolver.NOT_CONFIGURED => loop solvers
    1.33  			)
    1.34  	in
    1.35  		loop (rev (!SatSolver.solvers))