src/HOL/Tools/sat_solver.ML
changeset 18678 dd0c569fa43d
parent 17621 afffade1697e
child 19190 7c311c513bae
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Fri Jan 13 17:39:41 2006 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Sat Jan 14 17:14:06 2006 +0100
     1.3 @@ -307,7 +307,7 @@
     1.4  				  []      => [xs1]
     1.5  				| (0::[]) => [xs1]
     1.6  				| (0::tl) => xs1 :: clauses tl
     1.7 -				| _       => raise ERROR  (* this cannot happen *)
     1.8 +				| _       => sys_error "this cannot happen"
     1.9  			end
    1.10  		(* int -> PropLogic.prop_formula *)
    1.11  		fun literal_from_int i =
    1.12 @@ -457,7 +457,7 @@
    1.13  			  | forced_vars (And (fm1, fm2))  = (forced_vars fm1) union_int (forced_vars fm2)
    1.14  			  (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
    1.15  			  (* precedence, and the next partial evaluation of the formula returns 'False'. *)
    1.16 -			  | forced_vars _                 = raise ERROR  (* formula is not in negation normal form *)
    1.17 +			  | forced_vars _                 = error "formula is not in negation normal form"
    1.18  			(* int list -> prop_formula -> (int list * prop_formula) *)
    1.19  			fun eval_and_force xs fm =
    1.20  			let
    1.21 @@ -528,7 +528,7 @@
    1.22  				(if name="dpll" orelse name="enumerate" then
    1.23  					warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
    1.24  				else
    1.25 -					debug ("Using SAT solver " ^ quote name ^ "."));
    1.26 +					Output.debug ("Using SAT solver " ^ quote name ^ "."));
    1.27  				(* apply 'solver' to 'fm' *)
    1.28  				solver fm
    1.29  					handle SatSolver.NOT_CONFIGURED => loop solvers