src/HOL/Tools/sat_solver.ML
changeset 14514 15abb7d42e2e
parent 14489 3676def6b8b9
child 14703 837d7180c39a
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Fri Apr 02 17:26:00 2004 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Fri Apr 02 17:28:16 2004 +0200
     1.3 @@ -283,11 +283,12 @@
     1.4  	in
     1.5  		fun dpll_solver fm =
     1.6  		let
     1.7 -			(* We could use 'PropLogic.defcnf fm' instead of 'fm', but that   *)
     1.8 -			(* sometimes introduces more boolean variables than we can handle *)
     1.9 -			(* efficiently.                                                   *)
    1.10 +			(* We could use 'PropLogic.defcnf fm' instead of 'nnf fm', but that *)
    1.11 +			(* sometimes introduces more boolean variables than we can handle   *)
    1.12 +			(* efficiently.                                                     *)
    1.13 +			val fm' = PropLogic.nnf fm
    1.14  			(* int list *)
    1.15 -			val indices = PropLogic.indices fm
    1.16 +			val indices = PropLogic.indices fm'
    1.17  			(* int list -> int -> prop_formula *)
    1.18  			fun partial_var_eval []      i = BoolVar i
    1.19  			  | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i
    1.20 @@ -351,7 +352,7 @@
    1.21  				else assignment_from_list xs i
    1.22  		in
    1.23  			(* initially, no variable is interpreted yet *)
    1.24 -			apsome assignment_from_list (dpll [] fm)
    1.25 +			apsome assignment_from_list (dpll [] fm')
    1.26  		end
    1.27  	end  (* local *)
    1.28  in