src/HOL/Tools/sat_solver.ML
changeset 14514 15abb7d42e2e
parent 14489 3676def6b8b9
child 14703 837d7180c39a
--- a/src/HOL/Tools/sat_solver.ML	Fri Apr 02 17:26:00 2004 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Fri Apr 02 17:28:16 2004 +0200
@@ -283,11 +283,12 @@
 	in
 		fun dpll_solver fm =
 		let
-			(* We could use 'PropLogic.defcnf fm' instead of 'fm', but that   *)
-			(* sometimes introduces more boolean variables than we can handle *)
-			(* efficiently.                                                   *)
+			(* We could use 'PropLogic.defcnf fm' instead of 'nnf fm', but that *)
+			(* sometimes introduces more boolean variables than we can handle   *)
+			(* efficiently.                                                     *)
+			val fm' = PropLogic.nnf fm
 			(* int list *)
-			val indices = PropLogic.indices fm
+			val indices = PropLogic.indices fm'
 			(* int list -> int -> prop_formula *)
 			fun partial_var_eval []      i = BoolVar i
 			  | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i
@@ -351,7 +352,7 @@
 				else assignment_from_list xs i
 		in
 			(* initially, no variable is interpreted yet *)
-			apsome assignment_from_list (dpll [] fm)
+			apsome assignment_from_list (dpll [] fm')
 		end
 	end  (* local *)
 in