faster defcnf conversion
authorwebertj
Sun Jun 13 17:57:35 2004 +0200 (2004-06-13)
changeset 1493929fe4a9a7cb5
parent 14938 393b75c92c07
child 14940 b9ab8babd8b3
faster defcnf conversion
src/HOL/Tools/prop_logic.ML
     1.1 --- a/src/HOL/Tools/prop_logic.ML	Sun Jun 13 15:43:55 2004 +0200
     1.2 +++ b/src/HOL/Tools/prop_logic.ML	Sun Jun 13 17:57:35 2004 +0200
     1.3 @@ -109,6 +109,14 @@
     1.4  	  | maxidx (And (fm1,fm2)) = Int.max (maxidx fm1, maxidx fm2);
     1.5  
     1.6  (* ------------------------------------------------------------------------- *)
     1.7 +(* exception SAME: raised to indicate that the return value of a function is *)
     1.8 +(*                 identical to its argument (optimization to allow sharing, *)
     1.9 +(*                 rather than copying)                                      *)
    1.10 +(* ------------------------------------------------------------------------- *)
    1.11 +
    1.12 +	exception SAME;
    1.13 +
    1.14 +(* ------------------------------------------------------------------------- *)
    1.15  (* nnf: computes the negation normal form of a formula 'fm' of propositional *)
    1.16  (*      logic (i.e. only variables may be negated, but not subformulas)      *)
    1.17  (* ------------------------------------------------------------------------- *)
    1.18 @@ -120,7 +128,7 @@
    1.19  	    nnf True                  = True
    1.20  	  | nnf False                 = False
    1.21  	(* variables *)
    1.22 -	  | nnf (BoolVar i)           = BoolVar i
    1.23 +	  | nnf (BoolVar i)           = (BoolVar i)
    1.24  	(* 'or' and 'and' as outermost connectives are left untouched *)
    1.25  	  | nnf (Or  (fm1,fm2))       = SOr  (nnf fm1, nnf fm2)
    1.26  	  | nnf (And (fm1,fm2))       = SAnd (nnf fm1, nnf fm2)
    1.27 @@ -147,29 +155,26 @@
    1.28  	let
    1.29  		fun
    1.30  		(* constants *)
    1.31 -		    cnf_from_nnf True              = True
    1.32 -		  | cnf_from_nnf False             = False
    1.33 +		    cnf_from_nnf True             = True
    1.34 +		  | cnf_from_nnf False            = False
    1.35  		(* literals *)
    1.36 -		  | cnf_from_nnf (BoolVar i)       = BoolVar i
    1.37 -		  | cnf_from_nnf (Not (BoolVar i)) = Not (BoolVar i)
    1.38 +		  | cnf_from_nnf (BoolVar i)      = BoolVar i
    1.39 +		  | cnf_from_nnf (Not fm1)        = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
    1.40  		(* pushing 'or' inside of 'and' using distributive laws *)
    1.41 -		  | cnf_from_nnf (Or (fm1,fm2)) =
    1.42 +		  | cnf_from_nnf (Or (fm1, fm2))  =
    1.43  			let
    1.44 -				val fm1' = cnf_from_nnf fm1
    1.45 -				val fm2' = cnf_from_nnf fm2
    1.46 +				fun cnf_or (And (fm11, fm12), fm2) =
    1.47 +					And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
    1.48 +				  | cnf_or (fm1, And (fm21, fm22)) =
    1.49 +					And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
    1.50 +				(* neither subformula contains 'and' *)
    1.51 +				  | cnf_or (fm1, fm2) =
    1.52 +					Or (fm1, fm2)
    1.53  			in
    1.54 -				case fm1' of
    1.55 -				  And (fm11,fm12) => cnf_from_nnf (SAnd (SOr(fm11,fm2'),SOr(fm12,fm2')))
    1.56 -				| _               =>
    1.57 -					(case fm2' of
    1.58 -					  And (fm21,fm22) => cnf_from_nnf (SAnd (SOr(fm1',fm21),SOr(fm1',fm22)))
    1.59 -					(* neither subformula contains 'and' *)
    1.60 -					| _               => Or (fm1,fm2))
    1.61 +				cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
    1.62  			end
    1.63  		(* 'and' as outermost connective is left untouched *)
    1.64 -		  | cnf_from_nnf (And (fm1,fm2))   = SAnd (cnf_from_nnf fm1, cnf_from_nnf fm2)
    1.65 -		(* 'not' + something other than a variable: formula is not in negation normal form *)
    1.66 -		  | cnf_from_nnf _                 = raise ERROR
    1.67 +		  | cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2)
    1.68  	in
    1.69  		(cnf_from_nnf o nnf) fm
    1.70  	end;
    1.71 @@ -189,49 +194,52 @@
    1.72  		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
    1.73  		fun
    1.74  		(* constants *)
    1.75 -		    defcnf_from_nnf (True,new)            = (True, new)
    1.76 -		  | defcnf_from_nnf (False,new)           = (False, new)
    1.77 +		    defcnf_from_nnf (True, new)            = (True, new)
    1.78 +		  | defcnf_from_nnf (False, new)           = (False, new)
    1.79  		(* literals *)
    1.80 -		  | defcnf_from_nnf (BoolVar i,new)       = (BoolVar i, new)
    1.81 -		  | defcnf_from_nnf (Not (BoolVar i),new) = (Not (BoolVar i), new)
    1.82 -		(* pushing 'or' inside of 'and' using distributive laws *)
    1.83 -		  | defcnf_from_nnf (Or (fm1,fm2),new)    =
    1.84 +		  | defcnf_from_nnf (BoolVar i, new)       = (BoolVar i, new)
    1.85 +		  | defcnf_from_nnf (Not fm1, new)         = (Not fm1, new)  (* 'fm1' must be a variable since the formula is in NNF *)
    1.86 +		(* pushing 'or' inside of 'and' using auxiliary variables *)
    1.87 +		  | defcnf_from_nnf (Or (fm1, fm2), new)   =
    1.88  			let
    1.89 -				val (fm1',new')  = defcnf_from_nnf (fm1, new)
    1.90 -				val (fm2',new'') = defcnf_from_nnf (fm2, new')
    1.91 -			in
    1.92 -				case fm1' of
    1.93 -				  And (fm11,fm12) =>
    1.94 +				val (fm1', new')  = defcnf_from_nnf (fm1, new)
    1.95 +				val (fm2', new'') = defcnf_from_nnf (fm2, new')
    1.96 +				(* prop_formula * prop_formula -> int -> prop_formula * int *)
    1.97 +				fun defcnf_or (And (fm11, fm12), fm2) new =
    1.98  					let
    1.99 -						val aux = BoolVar new''
   1.100 +						val aux            = BoolVar new
   1.101 +						val (fm_a, new')   = defcnf_or (fm11, aux)     (new+1)
   1.102 +						val (fm_b, new'')  = defcnf_or (fm12, aux)     new'
   1.103 +						val (fm_c, new''') = defcnf_or (fm2,  Not aux) new''
   1.104  					in
   1.105 -						(* '(fm11 AND fm12) OR fm2' is SAT-equivalent to '(fm11 OR aux) AND (fm12 OR aux) AND (fm2 OR NOT aux)' *)
   1.106 -						defcnf_from_nnf (SAnd (SAnd (SOr (fm11,aux), SOr (fm12,aux)), SOr(fm2', Not aux)), new''+1)
   1.107 +						(And (And (fm_a, fm_b), fm_c), new''')
   1.108  					end
   1.109 -				| _               =>
   1.110 -					(case fm2' of
   1.111 -					  And (fm21,fm22) =>
   1.112 -						let
   1.113 -							val aux = BoolVar new''
   1.114 -						in
   1.115 -							(* 'fm1 OR (fm21 AND fm22)' is SAT-equivalent to '(fm1 OR NOT aux) AND (fm21 OR aux) AND (fm22 OR NOT aux)' *)
   1.116 -							defcnf_from_nnf (SAnd (SOr (fm1', Not aux), SAnd (SOr (fm21,aux), SOr (fm22,aux))), new''+1)
   1.117 -						end
   1.118 -					(* neither subformula contains 'and' *)
   1.119 -					| _               => (Or (fm1,fm2),new))
   1.120 +				  | defcnf_or (fm1, And (fm21, fm22)) new =
   1.121 +					let
   1.122 +						val aux            = BoolVar new
   1.123 +						val (fm_a, new')   = defcnf_or (fm1,  Not aux) (new+1)
   1.124 +						val (fm_b, new'')  = defcnf_or (fm21, aux)     new'
   1.125 +						val (fm_c, new''') = defcnf_or (fm22, aux)     new''
   1.126 +					in
   1.127 +						(And (fm_a, And (fm_b, fm_c)), new''')
   1.128 +					end
   1.129 +				(* neither subformula contains 'and' *)
   1.130 +				  | defcnf_or (fm1, fm2) new =
   1.131 +					(Or (fm1, fm2), new)
   1.132 +			in
   1.133 +				defcnf_or (fm1', fm2') new''
   1.134  			end
   1.135  		(* 'and' as outermost connective is left untouched *)
   1.136 -		  | defcnf_from_nnf (And (fm1,fm2),new)   =
   1.137 +		  | defcnf_from_nnf (And (fm1, fm2), new)   =
   1.138  			let
   1.139 -				val (fm1',new')  = defcnf_from_nnf (fm1, new)
   1.140 -				val (fm2',new'') = defcnf_from_nnf (fm2, new')
   1.141 +				val (fm1', new')  = defcnf_from_nnf (fm1, new)
   1.142 +				val (fm2', new'') = defcnf_from_nnf (fm2, new')
   1.143  			in
   1.144 -				(SAnd (fm1', fm2'), new'')
   1.145 +				(And (fm1', fm2'), new'')
   1.146  			end
   1.147 -		(* 'not' + something other than a variable: formula is not in negation normal form *)
   1.148 -		  | defcnf_from_nnf (_,_)                 = raise ERROR
   1.149 +		val fm'    = nnf fm
   1.150  	in
   1.151 -		(fst o defcnf_from_nnf) (nnf fm, (maxidx fm)+1)
   1.152 +		(fst o defcnf_from_nnf) (fm', (maxidx fm')+1)
   1.153  	end;
   1.154  
   1.155  (* ------------------------------------------------------------------------- *)