slightly different SAT solver interface
authorwebertj
Fri Mar 26 14:53:17 2004 +0100 (2004-03-26)
changeset 14488863258b0cdca
parent 14487 157d0ea7b2da
child 14489 3676def6b8b9
slightly different SAT solver interface
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Mar 26 12:21:50 2004 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Mar 26 14:53:17 2004 +0100
     1.3 @@ -466,9 +466,12 @@
     1.4  						std_output " invoking SAT solver...";
     1.5  						case SatSolver.invoke_solver satsolver fm of
     1.6  						  None =>
     1.7 +							(std_output (" error: SAT solver " ^ quote satsolver ^ " not configured.\n");
     1.8 +							true)
     1.9 +						| Some None =>
    1.10  							(std_output " no model found.\n";
    1.11  							false)
    1.12 -						| Some assignment =>
    1.13 +						| Some (Some assignment) =>
    1.14  							(writeln ("\nModel found:\n" ^ print_model thy model assignment);
    1.15  							true)
    1.16  					)