author webertj Mon Jul 25 15:51:30 2005 +0200 (2005-07-25) changeset 16907 2187e3f94761 parent 16906 74eddde1de2f child 16908 d374530bfaaa
defcnf modified to internally use a reference
```     1.1 --- a/src/HOL/Tools/prop_logic.ML	Fri Jul 22 17:43:49 2005 +0200
1.2 +++ b/src/HOL/Tools/prop_logic.ML	Mon Jul 25 15:51:30 2005 +0200
1.3 @@ -1,7 +1,7 @@
1.4  (*  Title:      HOL/Tools/prop_logic.ML
1.5      ID:         \$Id\$
1.6      Author:     Tjark Weber
1.9
1.10  Formulas of propositional logic.
1.11  *)
1.12 @@ -176,96 +176,73 @@
1.13  (*      'fm' of propositional logic, introducing auxiliary variables if      *)
1.14  (*      necessary to avoid an exponential blowup of the formula.  The result *)
1.15  (*      formula is satisfiable if and only if 'fm' is satisfiable.           *)
1.16 +(*      Auxiliary variables are introduced as switches for OR-nodes, based   *)
1.17 +(*      on the observation that "fm1 OR (fm21 AND fm22)" is equisatisfiable  *)
1.18 +(*      with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR aux)".            *)
1.19  (* ------------------------------------------------------------------------- *)
1.20
1.21  	(* prop_formula -> prop_formula *)
1.22
1.23  	fun defcnf fm =
1.24  	let
1.25 -		(* prop_formula * int -> prop_formula * int *)
1.26 +		(* convert formula to NNF first *)
1.27 +		val fm' = nnf fm
1.28  		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
1.29 +		(* int ref *)
1.30 +		val new = ref (maxidx fm' + 1)
1.31 +		(* unit -> int *)
1.32 +		fun new_idx () = let val idx = !new in new := idx+1; idx end
1.33 +		(* prop_formula -> prop_formula *)
1.34  		fun
1.35  		(* constants *)
1.36 -		    defcnf_from_nnf (True, new)            = (True, new)
1.37 -		  | defcnf_from_nnf (False, new)           = (False, new)
1.38 +		    defcnf_from_nnf True  = True
1.39 +		  | defcnf_from_nnf False = False
1.40  		(* literals *)
1.41 -		  | defcnf_from_nnf (BoolVar i, new)       = (BoolVar i, new)
1.42 -		  | defcnf_from_nnf (Not fm1, new)         = (Not fm1, new)  (* 'fm1' must be a variable since the formula is in NNF *)
1.43 +		  | defcnf_from_nnf (BoolVar i) = BoolVar i
1.44 +		  | defcnf_from_nnf (Not fm1)   = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
1.45  		(* pushing 'or' inside of 'and' using auxiliary variables *)
1.46 -		  | defcnf_from_nnf (Or (fm1, fm2), new)   =
1.47 +		  | defcnf_from_nnf (Or (fm1, fm2)) =
1.48  			let
1.49 -				val (fm1', new')  = defcnf_from_nnf (fm1, new)
1.50 -				val (fm2', new'') = defcnf_from_nnf (fm2, new')
1.51 -				(* prop_formula * prop_formula -> int -> prop_formula * int *)
1.52 -				fun defcnf_or (And (fm11, fm12), fm2) new =
1.53 +				val fm1' = defcnf_from_nnf fm1
1.54 +				val fm2' = defcnf_from_nnf fm2
1.55 +				(* prop_formula * prop_formula -> prop_formula *)
1.56 +				fun defcnf_or (And (fm11, fm12), fm2) =
1.57  					(case fm2 of
1.58  					(* do not introduce an auxiliary variable for literals *)
1.59  					  BoolVar _ =>
1.60 -						let
1.61 -							val (fm_a, new')  = defcnf_or (fm11, fm2) new
1.62 -							val (fm_b, new'') = defcnf_or (fm12, fm2) new'
1.63 -						in
1.64 -							(And (fm_a, fm_b), new'')
1.65 -						end
1.66 +							And (defcnf_or (fm11, fm2), defcnf_or (fm12, fm2))
1.67  					| Not _ =>
1.68 -						let
1.69 -							val (fm_a, new')  = defcnf_or (fm11, fm2) new
1.70 -							val (fm_b, new'') = defcnf_or (fm12, fm2) new'
1.71 -						in
1.72 -							(And (fm_a, fm_b), new'')
1.73 -						end
1.74 +							And (defcnf_or (fm11, fm2), defcnf_or (fm12, fm2))
1.75  					| _ =>
1.76  						let
1.77 -							val aux            = BoolVar new
1.78 -							val (fm_a, new')   = defcnf_or (fm11, aux)     (new+1)
1.79 -							val (fm_b, new'')  = defcnf_or (fm12, aux)     new'
1.80 -							val (fm_c, new''') = defcnf_or (fm2,  Not aux) new''
1.81 +							val aux = BoolVar (new_idx ())
1.82  						in
1.83 -							(And (And (fm_a, fm_b), fm_c), new''')
1.84 +							And (And (defcnf_or (fm11, aux), defcnf_or (fm12, aux)), defcnf_or (fm2, Not aux))
1.85  						end)
1.86 -				  | defcnf_or (fm1, And (fm21, fm22)) new =
1.87 +				  | defcnf_or (fm1, And (fm21, fm22)) =
1.88  					(case fm1 of
1.89  					(* do not introduce an auxiliary variable for literals *)
1.90  					  BoolVar _ =>
1.91 -						let
1.92 -							val (fm_a, new')  = defcnf_or (fm1, fm21) new
1.93 -							val (fm_b, new'') = defcnf_or (fm1, fm22) new'
1.94 -						in
1.95 -							(And (fm_a, fm_b), new'')
1.96 -						end
1.97 +							And (defcnf_or (fm1, fm21), defcnf_or (fm1, fm22))
1.98  					| Not _ =>
1.99 -						let
1.100 -							val (fm_a, new')  = defcnf_or (fm1, fm21) new
1.101 -							val (fm_b, new'') = defcnf_or (fm1, fm22) new'
1.102 -						in
1.103 -							(And (fm_a, fm_b), new'')
1.104 -						end
1.105 +							And (defcnf_or (fm1, fm21), defcnf_or (fm1, fm22))
1.106  					| _ =>
1.107  						let
1.108 -							val aux            = BoolVar new
1.109 -							val (fm_a, new')   = defcnf_or (fm1,  Not aux) (new+1)
1.110 -							val (fm_b, new'')  = defcnf_or (fm21, aux)     new'
1.111 -							val (fm_c, new''') = defcnf_or (fm22, aux)     new''
1.112 +							val aux = BoolVar (new_idx ())
1.113  						in
1.114 -							(And (fm_a, And (fm_b, fm_c)), new''')
1.115 +							And (defcnf_or (fm1, Not aux), And (defcnf_or (fm21, aux), defcnf_or (fm22, aux)))
1.116  						end)
1.117  				(* neither subformula contains 'and' *)
1.118 -				  | defcnf_or (fm1, fm2) new =
1.119 -					(Or (fm1, fm2), new)
1.120 +				  | defcnf_or (fm1, fm2) =
1.121 +					Or (fm1, fm2)
1.122  			in
1.123 -				defcnf_or (fm1', fm2') new''
1.124 +				defcnf_or (fm1', fm2')
1.125  			end
1.126  		(* 'and' as outermost connective is left untouched *)
1.127 -		  | defcnf_from_nnf (And (fm1, fm2), new)   =
1.128 -			let
1.129 -				val (fm1', new')  = defcnf_from_nnf (fm1, new)
1.130 -				val (fm2', new'') = defcnf_from_nnf (fm2, new')
1.131 -			in
1.132 -				(And (fm1', fm2'), new'')
1.133 -			end
1.134 -		val fm' = nnf fm
1.135 +		  | defcnf_from_nnf (And (fm1, fm2)) =
1.136 +				And (defcnf_from_nnf fm1, defcnf_from_nnf fm2)
1.137  	in
1.138 -		(fst o defcnf_from_nnf) (fm', (maxidx fm')+1)
1.139 +		defcnf_from_nnf fm'
1.140  	end;
1.141
1.142  (* ------------------------------------------------------------------------- *)
```