--- 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