# HG changeset patch
# User webertj
# Date 1080919696 -7200
# Node ID 15abb7d42e2ee6c98e78eaecb6b7f0a10aa1030b
# Parent  81d32b739a2b9e4010f169e49c4bc1c0e15996e0
fixed dpll solver (now uses NNF)

diff -r 81d32b739a2b -r 15abb7d42e2e src/HOL/Tools/sat_solver.ML
--- 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