satsolver=dpll

--- a/src/HOL/Main.thy	Fri Mar 26 14:53:17 2004 +0100
+++ b/src/HOL/Main.thy	Fri Mar 26 19:58:43 2004 +0100
@@ -101,6 +101,6 @@
 refute_params [minsize=1,
                maxsize=8,
                maxvars=100,
-               satsolver="auto"]
+               satsolver="dpll"]
 
 end

--- a/src/HOL/Tools/sat_solver.ML	Fri Mar 26 14:53:17 2004 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Fri Mar 26 19:58:43 2004 +0100
@@ -283,10 +283,11 @@
 	in
 		fun dpll_solver fm =
 		let
-			(* prop_formula *)
-			val defcnf = PropLogic.defcnf fm
+			(* We could use 'PropLogic.defcnf fm' instead of 'fm', but that   *)
+			(* sometimes introduces more boolean variables than we can handle *)
+			(* efficiently.                                                   *)
 			(* int list *)
-			val indices = PropLogic.indices defcnf
+			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
@@ -297,6 +298,7 @@
 			  | partial_eval xs (Not fm)         = SNot (partial_eval xs fm)
 			  | partial_eval xs (Or (fm1, fm2))  = SOr (partial_eval xs fm1, partial_eval xs fm2)
 			  | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2)
+			  | partial_eval xs _                = raise ERROR  (* formula is not in negation normal form *)
 			(* prop_formula -> int list *)
 			fun forced_vars True              = []
 			  | forced_vars False             = []
@@ -349,7 +351,7 @@
 				else assignment_from_list xs i
 		in
 			(* initially, no variable is interpreted yet *)
-			apsome assignment_from_list (dpll [] defcnf)
+			apsome assignment_from_list (dpll [] fm)
 		end
 	end  (* local *)
 in

--- a/src/HOL/ex/Refute_Examples.thy	Fri Mar 26 14:53:17 2004 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Fri Mar 26 19:58:43 2004 +0100
@@ -26,7 +26,7 @@
   refute [satsolver="dpll"] 2  -- {* ... and specify a subgoal at the same time *}
 oops
 
-refute_params
+refute_params [satsolver="dpll"]
 
 section {* Examples and Test Cases *}
 
@@ -155,7 +155,7 @@
 text {* A true statement (also testing names of free and bound variables being identical) *}
 
 lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
-  refute [maxsize=2]  (* [maxsize=5] works well with ZChaff *)
+  refute
   apply fast
 done
 
@@ -172,13 +172,13 @@
 text {* "Every reflexive and symmetric relation is transitive." *}
 
 lemma "\<lbrakk> \<forall>x. P x x; \<forall>x y. P x y \<longrightarrow> P y x \<rbrakk> \<Longrightarrow> P x y \<longrightarrow> P y z \<longrightarrow> P x z"
-  (* refute -- works well with ZChaff, but the internal solver is too slow *)
+  refute
 oops
 
 text {* The "Drinker's theorem" ... *}
 
 lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
-  refute [maxsize=4]  (* [maxsize=6] works well with ZChaff *)
+  refute
   apply (auto simp add: ext)
 done
 
@@ -262,7 +262,7 @@
         \<longrightarrow> trans_closure TP P
         \<longrightarrow> trans_closure TR R
         \<longrightarrow> (T x y = (TP x y | TR x y))"
-  (* refute -- works well with ZChaff, but the internal solver is too slow *)
+  refute
 oops
 
 text {* "Every surjective function is invertible." *}
@@ -280,7 +280,7 @@
 text {* Every point is a fixed point of some function. *}
 
 lemma "\<exists>f. f x = x"
-  refute [maxsize=4]
+  refute [maxsize=5]
   apply (rule_tac x="\<lambda>x. x" in exI)
   apply simp
 done
@@ -294,12 +294,12 @@
 text {* ... and now two correct ones *}
 
 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
-  refute [maxsize=5]
+  refute
   apply (simp add: choice)
 done
 
 lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
-  refute [maxsize=3]  (* [maxsize=4] works well with ZChaff *)
+  refute
   apply auto
     apply (simp add: ex1_implies_ex choice)
   apply (fast intro: ext)
@@ -361,7 +361,7 @@
 oops
 
 lemma "{x. P x} = {y. P y}"
-  refute [maxsize=2]  (* [maxsize=8] works well with ZChaff *)
+  refute
   apply simp
 done
 
@@ -430,7 +430,7 @@
 oops
 
 lemma "Ex P \<longrightarrow> P (The P)"
-  (* refute -- works well with ZChaff, but the internal solver is too slow *)
+  refute
 oops
 
 subsection {* Eps *}
@@ -452,7 +452,7 @@
 oops
 
 lemma "Ex P \<longrightarrow> P (Eps P)"
-  refute [maxsize=2]  (* [maxsize=3] works well with ZChaff *)
+  refute [maxsize=3]
   apply (auto simp add: someI)
 done