defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
authorwebertj
Mon Jul 25 21:40:43 2005 +0200 (2005-07-25)
changeset 16909acbc7a9c3864
parent 16908 d374530bfaaa
child 16910 19b4bf469fb2
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
src/HOL/Tools/prop_logic.ML
     1.1 --- a/src/HOL/Tools/prop_logic.ML	Mon Jul 25 18:54:49 2005 +0200
     1.2 +++ b/src/HOL/Tools/prop_logic.ML	Mon Jul 25 21:40:43 2005 +0200
     1.3 @@ -16,21 +16,23 @@
     1.4  		| Or of prop_formula * prop_formula
     1.5  		| And of prop_formula * prop_formula
     1.6  
     1.7 -	val SNot : prop_formula -> prop_formula
     1.8 -	val SOr  : prop_formula * prop_formula -> prop_formula
     1.9 -	val SAnd : prop_formula * prop_formula -> prop_formula
    1.10 +	val SNot     : prop_formula -> prop_formula
    1.11 +	val SOr      : prop_formula * prop_formula -> prop_formula
    1.12 +	val SAnd     : prop_formula * prop_formula -> prop_formula
    1.13 +	val simplify : prop_formula -> prop_formula  (* eliminates True/False and double-negation *)
    1.14  
    1.15  	val indices : prop_formula -> int list  (* set of all variable indices *)
    1.16  	val maxidx  : prop_formula -> int       (* maximal variable index *)
    1.17  
    1.18 -	val nnf    : prop_formula -> prop_formula  (* negation normal form *)
    1.19 -	val cnf    : prop_formula -> prop_formula  (* conjunctive normal form *)
    1.20 -	val defcnf : prop_formula -> prop_formula  (* definitional cnf *)
    1.21 -
    1.22  	val exists      : prop_formula list -> prop_formula  (* finite disjunction *)
    1.23  	val all         : prop_formula list -> prop_formula  (* finite conjunction *)
    1.24  	val dot_product : prop_formula list * prop_formula list -> prop_formula
    1.25  
    1.26 +	val nnf    : prop_formula -> prop_formula  (* negation normal form *)
    1.27 +	val cnf    : prop_formula -> prop_formula  (* conjunctive normal form *)
    1.28 +	val auxcnf : prop_formula -> prop_formula  (* cnf with auxiliary variables *)
    1.29 +	val defcnf : prop_formula -> prop_formula  (* definitional cnf *)
    1.30 +
    1.31  	val eval : (int -> bool) -> prop_formula -> bool  (* semantics *)
    1.32  end;
    1.33  
    1.34 @@ -81,18 +83,30 @@
    1.35  	  | SAnd (fm1, fm2) = And (fm1, fm2);
    1.36  
    1.37  (* ------------------------------------------------------------------------- *)
    1.38 +(* simplify: eliminates True/False below other connectives, and double-      *)
    1.39 +(*      negation                                                             *)
    1.40 +(* ------------------------------------------------------------------------- *)
    1.41 +
    1.42 +	(* prop_formula -> prop_formula *)
    1.43 +
    1.44 +	fun simplify (Not fm)         = SNot (simplify fm)
    1.45 +	  | simplify (Or (fm1, fm2))  = SOr (simplify fm1, simplify fm2)
    1.46 +	  | simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2)
    1.47 +	  | simplify fm               = fm;
    1.48 +
    1.49 +(* ------------------------------------------------------------------------- *)
    1.50  (* indices: collects all indices of Boolean variables that occur in a        *)
    1.51  (*      propositional formula 'fm'; no duplicates                            *)
    1.52  (* ------------------------------------------------------------------------- *)
    1.53  
    1.54  	(* prop_formula -> int list *)
    1.55  
    1.56 -	fun indices True            = []
    1.57 -	  | indices False           = []
    1.58 -	  | indices (BoolVar i)     = [i]
    1.59 -	  | indices (Not fm)        = indices fm
    1.60 -	  | indices (Or (fm1,fm2))  = (indices fm1) union_int (indices fm2)
    1.61 -	  | indices (And (fm1,fm2)) = (indices fm1) union_int (indices fm2);
    1.62 +	fun indices True             = []
    1.63 +	  | indices False            = []
    1.64 +	  | indices (BoolVar i)      = [i]
    1.65 +	  | indices (Not fm)         = indices fm
    1.66 +	  | indices (Or (fm1, fm2))  = (indices fm1) union_int (indices fm2)
    1.67 +	  | indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2);
    1.68  
    1.69  (* ------------------------------------------------------------------------- *)
    1.70  (* maxidx: computes the maximal variable index occuring in a formula of      *)
    1.71 @@ -101,39 +115,65 @@
    1.72  
    1.73  	(* prop_formula -> int *)
    1.74  
    1.75 -	fun maxidx True            = 0
    1.76 -	  | maxidx False           = 0
    1.77 -	  | maxidx (BoolVar i)     = i
    1.78 -	  | maxidx (Not fm)        = maxidx fm
    1.79 -	  | maxidx (Or (fm1,fm2))  = Int.max (maxidx fm1, maxidx fm2)
    1.80 -	  | maxidx (And (fm1,fm2)) = Int.max (maxidx fm1, maxidx fm2);
    1.81 +	fun maxidx True             = 0
    1.82 +	  | maxidx False            = 0
    1.83 +	  | maxidx (BoolVar i)      = i
    1.84 +	  | maxidx (Not fm)         = maxidx fm
    1.85 +	  | maxidx (Or (fm1, fm2))  = Int.max (maxidx fm1, maxidx fm2)
    1.86 +	  | maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2);
    1.87 +
    1.88 +(* ------------------------------------------------------------------------- *)
    1.89 +(* exists: computes the disjunction over a list 'xs' of propositional        *)
    1.90 +(*      formulas                                                             *)
    1.91 +(* ------------------------------------------------------------------------- *)
    1.92 +
    1.93 +	(* prop_formula list -> prop_formula *)
    1.94 +
    1.95 +	fun exists xs = Library.foldl SOr (False, xs);
    1.96 +
    1.97 +(* ------------------------------------------------------------------------- *)
    1.98 +(* all: computes the conjunction over a list 'xs' of propositional formulas  *)
    1.99 +(* ------------------------------------------------------------------------- *)
   1.100 +
   1.101 +	(* prop_formula list -> prop_formula *)
   1.102 +
   1.103 +	fun all xs = Library.foldl SAnd (True, xs);
   1.104 +
   1.105 +(* ------------------------------------------------------------------------- *)
   1.106 +(* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn                *)
   1.107 +(* ------------------------------------------------------------------------- *)
   1.108 +
   1.109 +	(* prop_formula list * prop_formula list -> prop_formula *)
   1.110 +
   1.111 +	fun dot_product (xs,ys) = exists (map SAnd (xs~~ys));
   1.112  
   1.113  (* ------------------------------------------------------------------------- *)
   1.114  (* nnf: computes the negation normal form of a formula 'fm' of propositional *)
   1.115 -(*      logic (i.e. only variables may be negated, but not subformulas)      *)
   1.116 +(*      logic (i.e. only variables may be negated, but not subformulas).     *)
   1.117 +(*      Simplification (c.f. 'simplify') is performed as well.               *)
   1.118  (* ------------------------------------------------------------------------- *)
   1.119  
   1.120  	(* prop_formula -> prop_formula *)
   1.121  
   1.122  	fun
   1.123  	(* constants *)
   1.124 -	    nnf True                  = True
   1.125 -	  | nnf False                 = False
   1.126 +	    nnf True                   = True
   1.127 +	  | nnf False                  = False
   1.128  	(* variables *)
   1.129 -	  | nnf (BoolVar i)           = (BoolVar i)
   1.130 +	  | nnf (BoolVar i)            = (BoolVar i)
   1.131  	(* 'or' and 'and' as outermost connectives are left untouched *)
   1.132 -	  | nnf (Or  (fm1,fm2))       = SOr  (nnf fm1, nnf fm2)
   1.133 -	  | nnf (And (fm1,fm2))       = SAnd (nnf fm1, nnf fm2)
   1.134 +	  | nnf (Or  (fm1, fm2))       = SOr  (nnf fm1, nnf fm2)
   1.135 +	  | nnf (And (fm1, fm2))       = SAnd (nnf fm1, nnf fm2)
   1.136  	(* 'not' + constant *)
   1.137 -	  | nnf (Not True)            = False
   1.138 -	  | nnf (Not False)           = True
   1.139 +	  | nnf (Not True)             = False
   1.140 +	  | nnf (Not False)            = True
   1.141  	(* 'not' + variable *)
   1.142 -	  | nnf (Not (BoolVar i))     = Not (BoolVar i)
   1.143 +	  | nnf (Not (BoolVar i))      = Not (BoolVar i)
   1.144  	(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
   1.145 -	  | nnf (Not (Or  (fm1,fm2))) = SAnd (nnf (SNot fm1), nnf (SNot fm2))
   1.146 -	  | nnf (Not (And (fm1,fm2))) = SOr  (nnf (SNot fm1), nnf (SNot fm2))
   1.147 +	  | nnf (Not (Or  (fm1, fm2))) = SAnd (nnf (SNot fm1), nnf (SNot fm2))
   1.148 +	  | nnf (Not (And (fm1, fm2))) = SOr  (nnf (SNot fm1), nnf (SNot fm2))
   1.149  	(* double-negation elimination *)
   1.150 -	  | nnf (Not (Not fm))        = nnf fm;
   1.151 +	  | nnf (Not (Not fm))         = nnf fm;
   1.152  
   1.153  (* ------------------------------------------------------------------------- *)
   1.154  (* cnf: computes the conjunctive normal form (i.e. a conjunction of          *)
   1.155 @@ -172,18 +212,27 @@
   1.156  	end;
   1.157  
   1.158  (* ------------------------------------------------------------------------- *)
   1.159 -(* defcnf: computes the definitional conjunctive normal form of a formula    *)
   1.160 +(* auxcnf: computes the definitional conjunctive normal form of a formula    *)
   1.161  (*      'fm' of propositional logic, introducing auxiliary variables if      *)
   1.162  (*      necessary to avoid an exponential blowup of the formula.  The result *)
   1.163  (*      formula is satisfiable if and only if 'fm' is satisfiable.           *)
   1.164  (*      Auxiliary variables are introduced as switches for OR-nodes, based   *)
   1.165 -(*      on the observation that "fm1 OR (fm21 AND fm22)" is equisatisfiable  *)
   1.166 -(*      with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR aux)".            *)
   1.167 +(*      on the observation that e.g. "fm1 OR (fm21 AND fm22)" is             *)
   1.168 +(*      equisatisfiable with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR   *)
   1.169 +(*      aux)".                                                               *)
   1.170 +(* ------------------------------------------------------------------------- *)
   1.171 +
   1.172 +(* ------------------------------------------------------------------------- *)
   1.173 +(* Note: 'auxcnf' tends to use fewer variables and fewer clauses than        *)
   1.174 +(*      'defcnf' below, but sometimes generates slightly larger SAT problems *)
   1.175 +(*      overall (hence it must sometimes generate longer clauses than        *)
   1.176 +(*      'defcnf' does).  It is currently not quite clear to me if one of the *)
   1.177 +(*      algorithms is clearly superior to the other.                         *)
   1.178  (* ------------------------------------------------------------------------- *)
   1.179  
   1.180  	(* prop_formula -> prop_formula *)
   1.181  
   1.182 -	fun defcnf fm =
   1.183 +	fun auxcnf fm =
   1.184  	let
   1.185  		(* convert formula to NNF first *)
   1.186  		val fm' = nnf fm
   1.187 @@ -195,80 +244,167 @@
   1.188  		(* prop_formula -> prop_formula *)
   1.189  		fun
   1.190  		(* constants *)
   1.191 -		    defcnf_from_nnf True  = True
   1.192 -		  | defcnf_from_nnf False = False
   1.193 +		    auxcnf_from_nnf True  = True
   1.194 +		  | auxcnf_from_nnf False = False
   1.195  		(* literals *)
   1.196 -		  | defcnf_from_nnf (BoolVar i) = BoolVar i
   1.197 -		  | defcnf_from_nnf (Not fm1)   = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
   1.198 +		  | auxcnf_from_nnf (BoolVar i) = BoolVar i
   1.199 +		  | auxcnf_from_nnf (Not fm1)   = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
   1.200  		(* pushing 'or' inside of 'and' using auxiliary variables *)
   1.201 -		  | defcnf_from_nnf (Or (fm1, fm2)) =
   1.202 +		  | auxcnf_from_nnf (Or (fm1, fm2)) =
   1.203  			let
   1.204 -				val fm1' = defcnf_from_nnf fm1
   1.205 -				val fm2' = defcnf_from_nnf fm2
   1.206 +				val fm1' = auxcnf_from_nnf fm1
   1.207 +				val fm2' = auxcnf_from_nnf fm2
   1.208  				(* prop_formula * prop_formula -> prop_formula *)
   1.209 -				fun defcnf_or (And (fm11, fm12), fm2) =
   1.210 +				fun auxcnf_or (And (fm11, fm12), fm2) =
   1.211  					(case fm2 of
   1.212  					(* do not introduce an auxiliary variable for literals *)
   1.213  					  BoolVar _ =>
   1.214 -							And (defcnf_or (fm11, fm2), defcnf_or (fm12, fm2))
   1.215 +							And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
   1.216  					| Not _ =>
   1.217 -							And (defcnf_or (fm11, fm2), defcnf_or (fm12, fm2))
   1.218 +							And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
   1.219  					| _ =>
   1.220  						let
   1.221  							val aux = BoolVar (new_idx ())
   1.222  						in
   1.223 -							And (And (defcnf_or (fm11, aux), defcnf_or (fm12, aux)), defcnf_or (fm2, Not aux))
   1.224 +							And (And (auxcnf_or (fm11, aux), auxcnf_or (fm12, aux)), auxcnf_or (fm2, Not aux))
   1.225  						end)
   1.226 -				  | defcnf_or (fm1, And (fm21, fm22)) =
   1.227 +				  | auxcnf_or (fm1, And (fm21, fm22)) =
   1.228  					(case fm1 of
   1.229  					(* do not introduce an auxiliary variable for literals *)
   1.230  					  BoolVar _ =>
   1.231 -							And (defcnf_or (fm1, fm21), defcnf_or (fm1, fm22))
   1.232 +							And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
   1.233  					| Not _ =>
   1.234 -							And (defcnf_or (fm1, fm21), defcnf_or (fm1, fm22))
   1.235 +							And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
   1.236  					| _ =>
   1.237  						let
   1.238  							val aux = BoolVar (new_idx ())
   1.239  						in
   1.240 -							And (defcnf_or (fm1, Not aux), And (defcnf_or (fm21, aux), defcnf_or (fm22, aux)))
   1.241 +							And (auxcnf_or (fm1, Not aux), And (auxcnf_or (fm21, aux), auxcnf_or (fm22, aux)))
   1.242  						end)
   1.243  				(* neither subformula contains 'and' *)
   1.244 -				  | defcnf_or (fm1, fm2) =
   1.245 +				  | auxcnf_or (fm1, fm2) =
   1.246  					Or (fm1, fm2)
   1.247  			in
   1.248 -				defcnf_or (fm1', fm2')
   1.249 +				auxcnf_or (fm1', fm2')
   1.250  			end
   1.251  		(* 'and' as outermost connective is left untouched *)
   1.252 -		  | defcnf_from_nnf (And (fm1, fm2)) =
   1.253 -				And (defcnf_from_nnf fm1, defcnf_from_nnf fm2)
   1.254 +		  | auxcnf_from_nnf (And (fm1, fm2)) =
   1.255 +				And (auxcnf_from_nnf fm1, auxcnf_from_nnf fm2)
   1.256  	in
   1.257 -		defcnf_from_nnf fm'
   1.258 +		auxcnf_from_nnf fm'
   1.259  	end;
   1.260  
   1.261  (* ------------------------------------------------------------------------- *)
   1.262 -(* exists: computes the disjunction over a list 'xs' of propositional        *)
   1.263 -(*      formulas                                                             *)
   1.264 -(* ------------------------------------------------------------------------- *)
   1.265 -
   1.266 -	(* prop_formula list -> prop_formula *)
   1.267 -
   1.268 -	fun exists xs = Library.foldl SOr (False, xs);
   1.269 -
   1.270 -(* ------------------------------------------------------------------------- *)
   1.271 -(* all: computes the conjunction over a list 'xs' of propositional formulas  *)
   1.272 +(* defcnf: computes the definitional conjunctive normal form of a formula    *)
   1.273 +(*      'fm' of propositional logic, introducing auxiliary variables to      *)
   1.274 +(*      avoid an exponential blowup of the formula.  The result formula is   *)
   1.275 +(*      satisfiable if and only if 'fm' is satisfiable.  Auxiliary variables *)
   1.276 +(*      are introduced as abbreviations for AND-, OR-, and NOT-nodes, based  *)
   1.277 +(*      on the following equisatisfiabilities (+/- indicates polarity):      *)
   1.278 +(*      LITERAL+       == LITERAL                                            *)
   1.279 +(*      LITERAL-       == NOT LITERAL                                        *)
   1.280 +(*      (NOT fm1)+     == aux AND (NOT aux OR fm1-)                          *)
   1.281 +(*      (fm1 OR fm2)+  == aux AND (NOT aux OR fm1+ OR fm2+)                  *)
   1.282 +(*      (fm1 AND fm2)+ == aux AND (NOT aux OR fm1+) AND (NOT aux OR fm2+)    *)
   1.283 +(*      (NOT fm1)-     == aux AND (NOT aux OR fm1+)                          *)
   1.284 +(*      (fm1 OR fm2)-  == aux AND (NOT aux OR fm1-) AND (NOT aux OR fm2-)    *)
   1.285 +(*      (fm1 AND fm2)- == aux AND (NOT aux OR fm1- OR fm2-)                  *)
   1.286 +(*      Example:                                                             *)
   1.287 +(*      NOT (a AND b) == aux1 AND (NOT aux1 OR aux2)                         *)
   1.288 +(*                            AND (NOT aux2 OR NOT a OR NOT b)               *)
   1.289  (* ------------------------------------------------------------------------- *)
   1.290  
   1.291 -	(* prop_formula list -> prop_formula *)
   1.292 -
   1.293 -	fun all xs = Library.foldl SAnd (True, xs);
   1.294 +	(* prop_formula -> prop_formula *)
   1.295  
   1.296 -(* ------------------------------------------------------------------------- *)
   1.297 -(* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn                *)
   1.298 -(* ------------------------------------------------------------------------- *)
   1.299 -
   1.300 -	(* prop_formula list * prop_formula list -> prop_formula *)
   1.301 -
   1.302 -	fun dot_product (xs,ys) = exists (map SAnd (xs~~ys));
   1.303 +	fun defcnf fm =
   1.304 +	let
   1.305 +		(* simplify formula first *)
   1.306 +		val fm' = simplify fm
   1.307 +		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
   1.308 +		(* int ref *)
   1.309 +		val new = ref (maxidx fm' + 1)
   1.310 +		(* unit -> int *)
   1.311 +		fun new_idx () = let val idx = !new in new := idx+1; idx end
   1.312 +		(* optimization for n-ary disjunction/conjunction *)
   1.313 +		(* prop_formula -> prop_formula list *)
   1.314 +		fun disjuncts (Or (fm1, fm2)) = (disjuncts fm1) @ (disjuncts fm2)
   1.315 +		  | disjuncts fm1             = [fm1]
   1.316 +		(* prop_formula -> prop_formula list *)
   1.317 +		fun conjuncts (And (fm1, fm2)) = (conjuncts fm1) @ (conjuncts fm2)
   1.318 +		  | conjuncts fm1              = [fm1]
   1.319 +		(* polarity -> formula -> (defining clauses, literal) *)
   1.320 +		(* bool -> prop_formula -> prop_formula * prop_formula *)
   1.321 +		fun
   1.322 +		(* constants *)
   1.323 +		    defcnf' true  True  = (True, True)
   1.324 +		  | defcnf' false True  = (*(True, False)*) error "formula is not simplified, True occurs with negative polarity"
   1.325 +		  | defcnf' true  False = (True, False)
   1.326 +		  | defcnf' false False = (*(True, True)*) error "formula is not simplified, False occurs with negative polarity"
   1.327 +		(* literals *)
   1.328 +		  | defcnf' true  (BoolVar i)       = (True, BoolVar i)
   1.329 +		  | defcnf' false (BoolVar i)       = (True, Not (BoolVar i))
   1.330 +		  | defcnf' true  (Not (BoolVar i)) = (True, Not (BoolVar i))
   1.331 +		  | defcnf' false (Not (BoolVar i)) = (True, BoolVar i)
   1.332 +		(* 'not' *)
   1.333 +		  | defcnf' polarity (Not fm1) =
   1.334 +			let
   1.335 +				val (def1, aux1) = defcnf' (not polarity) fm1
   1.336 +				val aux          = BoolVar (new_idx ())
   1.337 +				val def          = Or (Not aux, aux1)
   1.338 +			in
   1.339 +				(SAnd (def1, def), aux)
   1.340 +			end
   1.341 +		(* 'or' *)
   1.342 +		  | defcnf' polarity (Or (fm1, fm2)) =
   1.343 +			let
   1.344 +				val fms          = disjuncts (Or (fm1, fm2))
   1.345 +				val (defs, auxs) = split_list (map (defcnf' polarity) fms)
   1.346 +				val aux          = BoolVar (new_idx ())
   1.347 +				val def          = if polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
   1.348 +			in
   1.349 +				(SAnd (all defs, def), aux)
   1.350 +			end
   1.351 +		(* 'and' *)
   1.352 +		  | defcnf' polarity (And (fm1, fm2)) =
   1.353 +			let
   1.354 +				val fms          = conjuncts (And (fm1, fm2))
   1.355 +				val (defs, auxs) = split_list (map (defcnf' polarity) fms)
   1.356 +				val aux          = BoolVar (new_idx ())
   1.357 +				val def          = if not polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
   1.358 +			in
   1.359 +				(SAnd (all defs, def), aux)
   1.360 +			end
   1.361 +		(* optimization: do not introduce auxiliary variables for parts of the formula that are in CNF already *)
   1.362 +		(* prop_formula -> prop_formula * prop_formula *)
   1.363 +		fun defcnf_or (Or (fm1, fm2)) =
   1.364 +			let
   1.365 +				val (def1, aux1) = defcnf_or fm1
   1.366 +				val (def2, aux2) = defcnf_or fm2
   1.367 +			in
   1.368 +				(SAnd (def1, def2), Or (aux1, aux2))
   1.369 +			end
   1.370 +		  | defcnf_or fm =
   1.371 +			defcnf' true fm
   1.372 +		(* prop_formula -> prop_formula * prop_formula *)
   1.373 +		fun defcnf_and (And (fm1, fm2)) =
   1.374 +			let
   1.375 +				val (def1, aux1) = defcnf_and fm1
   1.376 +				val (def2, aux2) = defcnf_and fm2
   1.377 +			in
   1.378 +				(SAnd (def1, def2), And (aux1, aux2))
   1.379 +			end
   1.380 +		  | defcnf_and (Or (fm1, fm2)) =
   1.381 +			let
   1.382 +				val (def1, aux1) = defcnf_or fm1
   1.383 +				val (def2, aux2) = defcnf_or fm2
   1.384 +			in
   1.385 +				(SAnd (def1, def2), Or (aux1, aux2))
   1.386 +			end
   1.387 +		  | defcnf_and fm =
   1.388 +			defcnf' true fm
   1.389 +	in
   1.390 +		SAnd (defcnf_and fm')
   1.391 +	end;
   1.392  
   1.393  (* ------------------------------------------------------------------------- *)
   1.394  (* eval: given an assignment 'a' of Boolean values to variable indices, the  *)