satsolver=dpll
authorwebertj
Fri Mar 26 19:58:43 2004 +0100 (2004-03-26)
changeset 144893676def6b8b9
parent 14488 863258b0cdca
child 14490 7b37aa726d2d
satsolver=dpll
src/HOL/Main.thy
src/HOL/Tools/sat_solver.ML
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/src/HOL/Main.thy	Fri Mar 26 14:53:17 2004 +0100
     1.2 +++ b/src/HOL/Main.thy	Fri Mar 26 19:58:43 2004 +0100
     1.3 @@ -101,6 +101,6 @@
     1.4  refute_params [minsize=1,
     1.5                 maxsize=8,
     1.6                 maxvars=100,
     1.7 -               satsolver="auto"]
     1.8 +               satsolver="dpll"]
     1.9  
    1.10  end
     2.1 --- a/src/HOL/Tools/sat_solver.ML	Fri Mar 26 14:53:17 2004 +0100
     2.2 +++ b/src/HOL/Tools/sat_solver.ML	Fri Mar 26 19:58:43 2004 +0100
     2.3 @@ -283,10 +283,11 @@
     2.4  	in
     2.5  		fun dpll_solver fm =
     2.6  		let
     2.7 -			(* prop_formula *)
     2.8 -			val defcnf = PropLogic.defcnf fm
     2.9 +			(* We could use 'PropLogic.defcnf fm' instead of 'fm', but that   *)
    2.10 +			(* sometimes introduces more boolean variables than we can handle *)
    2.11 +			(* efficiently.                                                   *)
    2.12  			(* int list *)
    2.13 -			val indices = PropLogic.indices defcnf
    2.14 +			val indices = PropLogic.indices fm
    2.15  			(* int list -> int -> prop_formula *)
    2.16  			fun partial_var_eval []      i = BoolVar i
    2.17  			  | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i
    2.18 @@ -297,6 +298,7 @@
    2.19  			  | partial_eval xs (Not fm)         = SNot (partial_eval xs fm)
    2.20  			  | partial_eval xs (Or (fm1, fm2))  = SOr (partial_eval xs fm1, partial_eval xs fm2)
    2.21  			  | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2)
    2.22 +			  | partial_eval xs _                = raise ERROR  (* formula is not in negation normal form *)
    2.23  			(* prop_formula -> int list *)
    2.24  			fun forced_vars True              = []
    2.25  			  | forced_vars False             = []
    2.26 @@ -349,7 +351,7 @@
    2.27  				else assignment_from_list xs i
    2.28  		in
    2.29  			(* initially, no variable is interpreted yet *)
    2.30 -			apsome assignment_from_list (dpll [] defcnf)
    2.31 +			apsome assignment_from_list (dpll [] fm)
    2.32  		end
    2.33  	end  (* local *)
    2.34  in
     3.1 --- a/src/HOL/ex/Refute_Examples.thy	Fri Mar 26 14:53:17 2004 +0100
     3.2 +++ b/src/HOL/ex/Refute_Examples.thy	Fri Mar 26 19:58:43 2004 +0100
     3.3 @@ -26,7 +26,7 @@
     3.4    refute [satsolver="dpll"] 2  -- {* ... and specify a subgoal at the same time *}
     3.5  oops
     3.6  
     3.7 -refute_params
     3.8 +refute_params [satsolver="dpll"]
     3.9  
    3.10  section {* Examples and Test Cases *}
    3.11  
    3.12 @@ -155,7 +155,7 @@
    3.13  text {* A true statement (also testing names of free and bound variables being identical) *}
    3.14  
    3.15  lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
    3.16 -  refute [maxsize=2]  (* [maxsize=5] works well with ZChaff *)
    3.17 +  refute
    3.18    apply fast
    3.19  done
    3.20  
    3.21 @@ -172,13 +172,13 @@
    3.22  text {* "Every reflexive and symmetric relation is transitive." *}
    3.23  
    3.24  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"
    3.25 -  (* refute -- works well with ZChaff, but the internal solver is too slow *)
    3.26 +  refute
    3.27  oops
    3.28  
    3.29  text {* The "Drinker's theorem" ... *}
    3.30  
    3.31  lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
    3.32 -  refute [maxsize=4]  (* [maxsize=6] works well with ZChaff *)
    3.33 +  refute
    3.34    apply (auto simp add: ext)
    3.35  done
    3.36  
    3.37 @@ -262,7 +262,7 @@
    3.38          \<longrightarrow> trans_closure TP P
    3.39          \<longrightarrow> trans_closure TR R
    3.40          \<longrightarrow> (T x y = (TP x y | TR x y))"
    3.41 -  (* refute -- works well with ZChaff, but the internal solver is too slow *)
    3.42 +  refute
    3.43  oops
    3.44  
    3.45  text {* "Every surjective function is invertible." *}
    3.46 @@ -280,7 +280,7 @@
    3.47  text {* Every point is a fixed point of some function. *}
    3.48  
    3.49  lemma "\<exists>f. f x = x"
    3.50 -  refute [maxsize=4]
    3.51 +  refute [maxsize=5]
    3.52    apply (rule_tac x="\<lambda>x. x" in exI)
    3.53    apply simp
    3.54  done
    3.55 @@ -294,12 +294,12 @@
    3.56  text {* ... and now two correct ones *}
    3.57  
    3.58  lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
    3.59 -  refute [maxsize=5]
    3.60 +  refute
    3.61    apply (simp add: choice)
    3.62  done
    3.63  
    3.64  lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
    3.65 -  refute [maxsize=3]  (* [maxsize=4] works well with ZChaff *)
    3.66 +  refute
    3.67    apply auto
    3.68      apply (simp add: ex1_implies_ex choice)
    3.69    apply (fast intro: ext)
    3.70 @@ -361,7 +361,7 @@
    3.71  oops
    3.72  
    3.73  lemma "{x. P x} = {y. P y}"
    3.74 -  refute [maxsize=2]  (* [maxsize=8] works well with ZChaff *)
    3.75 +  refute
    3.76    apply simp
    3.77  done
    3.78  
    3.79 @@ -430,7 +430,7 @@
    3.80  oops
    3.81  
    3.82  lemma "Ex P \<longrightarrow> P (The P)"
    3.83 -  (* refute -- works well with ZChaff, but the internal solver is too slow *)
    3.84 +  refute
    3.85  oops
    3.86  
    3.87  subsection {* Eps *}
    3.88 @@ -452,7 +452,7 @@
    3.89  oops
    3.90  
    3.91  lemma "Ex P \<longrightarrow> P (Eps P)"
    3.92 -  refute [maxsize=2]  (* [maxsize=3] works well with ZChaff *)
    3.93 +  refute [maxsize=3]
    3.94    apply (auto simp add: someI)
    3.95  done
    3.96