Context Navigation

source: vis_dev/glu-2.1/src/cuBdd/cuddPriority.c @ 8

Last change on this file since 8 was 8, checked in by cecile, 13 years ago
src glu
File size: 44.0 KB

Line
1	/CFile*********************************************************************
2
3	FileName [cuddPriority.c]
4
5	PackageName [cudd]
6
7	Synopsis [Priority functions.]
8
9	Description [External procedures included in this file:
10	<ul>
11	<li> Cudd_PrioritySelect()
12	<li> Cudd_Xgty()
13	<li> Cudd_Xeqy()
14	<li> Cudd_addXeqy()
15	<li> Cudd_Dxygtdxz()
16	<li> Cudd_Dxygtdyz()
17	<li> Cudd_CProjection()
18	<li> Cudd_addHamming()
19	<li> Cudd_MinHammingDist()
20	<li> Cudd_bddClosestCube()
21	</ul>
22	Internal procedures included in this module:
23	<ul>
24	<li> cuddCProjectionRecur()
25	<li> cuddBddClosestCube()
26	</ul>
27	Static procedures included in this module:
28	<ul>
29	<li> cuddMinHammingDistRecur()
30	<li> separateCube()
31	<li> createResult()
32	</ul>
33	]
34
35	SeeAlso []
36
37	Author [Fabio Somenzi]
38
39	Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
40
41	All rights reserved.
42
43	Redistribution and use in source and binary forms, with or without
44	modification, are permitted provided that the following conditions
45	are met:
46
47	Redistributions of source code must retain the above copyright
48	notice, this list of conditions and the following disclaimer.
49
50	Redistributions in binary form must reproduce the above copyright
51	notice, this list of conditions and the following disclaimer in the
52	documentation and/or other materials provided with the distribution.
53
54	Neither the name of the University of Colorado nor the names of its
55	contributors may be used to endorse or promote products derived from
56	this software without specific prior written permission.
57
58	THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
59	"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
60	LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
61	FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
62	COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
63	INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
64	BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
65	LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
66	CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
67	LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
68	ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
69	POSSIBILITY OF SUCH DAMAGE.]
70
71	******************************************************************************/
72
73	#include "util.h"
74	#include "cuddInt.h"
75
76
77	/---------------------------------------------------------------------------/
78	/* Constant declarations */
79	/---------------------------------------------------------------------------/
80
81	#define DD_DEBUG 1
82
83	/---------------------------------------------------------------------------/
84	/* Stucture declarations */
85	/---------------------------------------------------------------------------/
86
87
88	/---------------------------------------------------------------------------/
89	/* Type declarations */
90	/---------------------------------------------------------------------------/
91
92
93	/---------------------------------------------------------------------------/
94	/* Variable declarations */
95	/---------------------------------------------------------------------------/
96
97	#ifndef lint
98	static char rcsid[] DD_UNUSED = "$Id: cuddPriority.c,v 1.26 2004/08/13 18:04:50 fabio Exp $";
99	#endif
100
101	/---------------------------------------------------------------------------/
102	/* Macro declarations */
103	/---------------------------------------------------------------------------/
104
105
106	/AutomaticStart***********************************************************/
107
108	/---------------------------------------------------------------------------/
109	/* Static function prototypes */
110	/---------------------------------------------------------------------------/
111	static int cuddMinHammingDistRecur (DdNode * f, int minterm, DdHashTable table, int upperBound);
112	static DdNode * separateCube (DdManager dd, DdNode f, CUDD_VALUE_TYPE *distance);
113	static DdNode * createResult (DdManager dd, unsigned int index, unsigned int phase, DdNode cube, CUDD_VALUE_TYPE distance);
114
115	/AutomaticEnd*************************************************************/
116
117
118	/---------------------------------------------------------------------------/
119	/* Definition of exported functions */
120	/---------------------------------------------------------------------------/
121
122
123	/Function******************************************************************
124
125	Synopsis [Selects pairs from R using a priority function.]
126
127	Description [Selects pairs from a relation R(x,y) (given as a BDD)
128	in such a way that a given x appears in one pair only. Uses a
129	priority function to determine which y should be paired to a given x.
130	Cudd_PrioritySelect returns a pointer to
131	the selected function if successful; NULL otherwise.
132	Three of the arguments--x, y, and z--are vectors of BDD variables.
133	The first two are the variables on which R depends. The third vectore
134	is a vector of auxiliary variables, used during the computation. This
135	vector is optional. If a NULL value is passed instead,
136	Cudd_PrioritySelect will create the working variables on the fly.
137	The sizes of x and y (and z if it is not NULL) should equal n.
138	The priority function Pi can be passed as a BDD, or can be built by
139	Cudd_PrioritySelect. If NULL is passed instead of a DdNode *,
140	parameter Pifunc is used by Cudd_PrioritySelect to build a BDD for the
141	priority function. (Pifunc is a pointer to a C function.) If Pi is not
142	NULL, then Pifunc is ignored. Pifunc should have the same interface as
143	the standard priority functions (e.g., Cudd_Dxygtdxz).
144	Cudd_PrioritySelect and Cudd_CProjection can sometimes be used
145	interchangeably. Specifically, calling Cudd_PrioritySelect with
146	Cudd_Xgty as Pifunc produces the same result as calling
147	Cudd_CProjection with the all-zero minterm as reference minterm.
148	However, depending on the application, one or the other may be
149	preferable:
150	<ul>
151	<li> When extracting representatives from an equivalence relation,
152	Cudd_CProjection has the advantage of nor requiring the auxiliary
153	variables.
154	<li> When computing matchings in general bipartite graphs,
155	Cudd_PrioritySelect normally obtains better results because it can use
156	more powerful matching schemes (e.g., Cudd_Dxygtdxz).
157	</ul>
158	]
159
160	SideEffects [If called with z == NULL, will create new variables in
161	the manager.]
162
163	SeeAlso [Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_Xgty
164	Cudd_bddAdjPermuteX Cudd_CProjection]
165
166	******************************************************************************/
167	DdNode *
168	Cudd_PrioritySelect(
169	DdManager * dd /* manager */,
170	DdNode * R /* BDD of the relation */,
171	DdNode ** x /* array of x variables */,
172	DdNode ** y /* array of y variables */,
173	DdNode ** z /* array of z variables (optional: may be NULL) */,
174	DdNode * Pi /* BDD of the priority function (optional: may be NULL) */,
175	int n /* size of x, y, and z */,
176	DD_PRFP Pifunc /* function used to build Pi if it is NULL */)
177	{
178	DdNode *res = NULL;
179	DdNode *zcube = NULL;
180	DdNode Rxz, Q;
181	int createdZ = 0;
182	int createdPi = 0;
183	int i;
184
185	/* Create z variables if needed. */
186	if (z == NULL) {
187	if (Pi != NULL) return(NULL);
188	z = ALLOC(DdNode *,n);
189	if (z == NULL) {
190	dd->errorCode = CUDD_MEMORY_OUT;
191	return(NULL);
192	}
193	createdZ = 1;
194	for (i = 0; i < n; i++) {
195	if (dd->size >= (int) CUDD_MAXINDEX - 1) goto endgame;
196	z[i] = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one));
197	if (z[i] == NULL) goto endgame;
198	}
199	}
200
201	/* Create priority function BDD if needed. */
202	if (Pi == NULL) {
203	Pi = Pifunc(dd,n,x,y,z);
204	if (Pi == NULL) goto endgame;
205	createdPi = 1;
206	cuddRef(Pi);
207	}
208
209	/* Initialize abstraction cube. */
210	zcube = DD_ONE(dd);
211	cuddRef(zcube);
212	for (i = n - 1; i >= 0; i--) {
213	DdNode *tmpp;
214	tmpp = Cudd_bddAnd(dd,z[i],zcube);
215	if (tmpp == NULL) goto endgame;
216	cuddRef(tmpp);
217	Cudd_RecursiveDeref(dd,zcube);
218	zcube = tmpp;
219	}
220
221	/* Compute subset of (x,y) pairs. */
222	Rxz = Cudd_bddSwapVariables(dd,R,y,z,n);
223	if (Rxz == NULL) goto endgame;
224	cuddRef(Rxz);
225	Q = Cudd_bddAndAbstract(dd,Rxz,Pi,zcube);
226	if (Q == NULL) {
227	Cudd_RecursiveDeref(dd,Rxz);
228	goto endgame;
229	}
230	cuddRef(Q);
231	Cudd_RecursiveDeref(dd,Rxz);
232	res = Cudd_bddAnd(dd,R,Cudd_Not(Q));
233	if (res == NULL) {
234	Cudd_RecursiveDeref(dd,Q);
235	goto endgame;
236	}
237	cuddRef(res);
238	Cudd_RecursiveDeref(dd,Q);
239
240	endgame:
241	if (zcube != NULL) Cudd_RecursiveDeref(dd,zcube);
242	if (createdZ) {
243	FREE(z);
244	}
245	if (createdPi) {
246	Cudd_RecursiveDeref(dd,Pi);
247	}
248	if (res != NULL) cuddDeref(res);
249	return(res);
250
251	} /* Cudd_PrioritySelect */
252
253
254	/Function******************************************************************
255
256	Synopsis [Generates a BDD for the function x > y.]
257
258	Description [This function generates a BDD for the function x > y.
259	Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
260	y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit.
261	The BDD is built bottom-up.
262	It has 3*N-1 internal nodes, if the variables are ordered as follows:
263	x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].
264	Argument z is not used by Cudd_Xgty: it is included to make it
265	call-compatible to Cudd_Dxygtdxz and Cudd_Dxygtdyz.]
266
267	SideEffects [None]
268
269	SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Dxygtdyz]
270
271	******************************************************************************/
272	DdNode *
273	Cudd_Xgty(
274	DdManager * dd /* DD manager */,
275	int N /* number of x and y variables */,
276	DdNode ** z /* array of z variables: unused */,
277	DdNode ** x /* array of x variables */,
278	DdNode ** y /* array of y variables */)
279	{
280	DdNode u, v, *w;
281	int i;
282
283	/* Build bottom part of BDD outside loop. */
284	u = Cudd_bddAnd(dd, x[N-1], Cudd_Not(y[N-1]));
285	if (u == NULL) return(NULL);
286	cuddRef(u);
287
288	/* Loop to build the rest of the BDD. */
289	for (i = N-2; i >= 0; i--) {
290	v = Cudd_bddAnd(dd, y[i], Cudd_Not(u));
291	if (v == NULL) {
292	Cudd_RecursiveDeref(dd, u);
293	return(NULL);
294	}
295	cuddRef(v);
296	w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
297	if (w == NULL) {
298	Cudd_RecursiveDeref(dd, u);
299	Cudd_RecursiveDeref(dd, v);
300	return(NULL);
301	}
302	cuddRef(w);
303	Cudd_RecursiveDeref(dd, u);
304	u = Cudd_bddIte(dd, x[i], Cudd_Not(v), w);
305	if (u == NULL) {
306	Cudd_RecursiveDeref(dd, v);
307	Cudd_RecursiveDeref(dd, w);
308	return(NULL);
309	}
310	cuddRef(u);
311	Cudd_RecursiveDeref(dd, v);
312	Cudd_RecursiveDeref(dd, w);
313
314	}
315	cuddDeref(u);
316	return(u);
317
318	} /* end of Cudd_Xgty */
319
320
321	/Function******************************************************************
322
323	Synopsis [Generates a BDD for the function x==y.]
324
325	Description [This function generates a BDD for the function x==y.
326	Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
327	y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit.
328	The BDD is built bottom-up.
329	It has 3*N-1 internal nodes, if the variables are ordered as follows:
330	x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. ]
331
332	SideEffects [None]
333
334	SeeAlso [Cudd_addXeqy]
335
336	******************************************************************************/
337	DdNode *
338	Cudd_Xeqy(
339	DdManager * dd /* DD manager */,
340	int N /* number of x and y variables */,
341	DdNode ** x /* array of x variables */,
342	DdNode ** y /* array of y variables */)
343	{
344	DdNode u, v, *w;
345	int i;
346
347	/* Build bottom part of BDD outside loop. */
348	u = Cudd_bddIte(dd, x[N-1], y[N-1], Cudd_Not(y[N-1]));
349	if (u == NULL) return(NULL);
350	cuddRef(u);
351
352	/* Loop to build the rest of the BDD. */
353	for (i = N-2; i >= 0; i--) {
354	v = Cudd_bddAnd(dd, y[i], u);
355	if (v == NULL) {
356	Cudd_RecursiveDeref(dd, u);
357	return(NULL);
358	}
359	cuddRef(v);
360	w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
361	if (w == NULL) {
362	Cudd_RecursiveDeref(dd, u);
363	Cudd_RecursiveDeref(dd, v);
364	return(NULL);
365	}
366	cuddRef(w);
367	Cudd_RecursiveDeref(dd, u);
368	u = Cudd_bddIte(dd, x[i], v, w);
369	if (u == NULL) {
370	Cudd_RecursiveDeref(dd, v);
371	Cudd_RecursiveDeref(dd, w);
372	return(NULL);
373	}
374	cuddRef(u);
375	Cudd_RecursiveDeref(dd, v);
376	Cudd_RecursiveDeref(dd, w);
377	}
378	cuddDeref(u);
379	return(u);
380
381	} /* end of Cudd_Xeqy */
382
383
384	/Function******************************************************************
385
386	Synopsis [Generates an ADD for the function x==y.]
387
388	Description [This function generates an ADD for the function x==y.
389	Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
390	y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit.
391	The ADD is built bottom-up.
392	It has 3*N-1 internal nodes, if the variables are ordered as follows:
393	x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. ]
394
395	SideEffects [None]
396
397	SeeAlso [Cudd_Xeqy]
398
399	******************************************************************************/
400	DdNode *
401	Cudd_addXeqy(
402	DdManager * dd /* DD manager */,
403	int N /* number of x and y variables */,
404	DdNode ** x /* array of x variables */,
405	DdNode ** y /* array of y variables */)
406	{
407	DdNode one, zero;
408	DdNode u, v, *w;
409	int i;
410
411	one = DD_ONE(dd);
412	zero = DD_ZERO(dd);
413
414	/* Build bottom part of ADD outside loop. */
415	v = Cudd_addIte(dd, y[N-1], one, zero);
416	if (v == NULL) return(NULL);
417	cuddRef(v);
418	w = Cudd_addIte(dd, y[N-1], zero, one);
419	if (w == NULL) {
420	Cudd_RecursiveDeref(dd, v);
421	return(NULL);
422	}
423	cuddRef(w);
424	u = Cudd_addIte(dd, x[N-1], v, w);
425	if (w == NULL) {
426	Cudd_RecursiveDeref(dd, v);
427	Cudd_RecursiveDeref(dd, w);
428	return(NULL);
429	}
430	cuddRef(u);
431	Cudd_RecursiveDeref(dd, v);
432	Cudd_RecursiveDeref(dd, w);
433
434	/* Loop to build the rest of the ADD. */
435	for (i = N-2; i >= 0; i--) {
436	v = Cudd_addIte(dd, y[i], u, zero);
437	if (v == NULL) {
438	Cudd_RecursiveDeref(dd, u);
439	return(NULL);
440	}
441	cuddRef(v);
442	w = Cudd_addIte(dd, y[i], zero, u);
443	if (w == NULL) {
444	Cudd_RecursiveDeref(dd, u);
445	Cudd_RecursiveDeref(dd, v);
446	return(NULL);
447	}
448	cuddRef(w);
449	Cudd_RecursiveDeref(dd, u);
450	u = Cudd_addIte(dd, x[i], v, w);
451	if (w == NULL) {
452	Cudd_RecursiveDeref(dd, v);
453	Cudd_RecursiveDeref(dd, w);
454	return(NULL);
455	}
456	cuddRef(u);
457	Cudd_RecursiveDeref(dd, v);
458	Cudd_RecursiveDeref(dd, w);
459	}
460	cuddDeref(u);
461	return(u);
462
463	} /* end of Cudd_addXeqy */
464
465
466	/Function******************************************************************
467
468	Synopsis [Generates a BDD for the function d(x,y) > d(x,z).]
469
470	Description [This function generates a BDD for the function d(x,y)
471	> d(x,z);
472	x, y, and z are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\],
473	y\[0\] y\[1\] ... y\[N-1\], and z\[0\] z\[1\] ... z\[N-1\],
474	with 0 the most significant bit.
475	The distance d(x,y) is defined as:
476	\sum_{i=0}^{N-1}(\|x_i - y_i\| \cdot 2^{N-i-1}).
477	The BDD is built bottom-up.
478	It has 7*N-3 internal nodes, if the variables are ordered as follows:
479	x\[0\] y\[0\] z\[0\] x\[1\] y\[1\] z\[1\] ... x\[N-1\] y\[N-1\] z\[N-1\]. ]
480
481	SideEffects [None]
482
483	SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdyz Cudd_Xgty Cudd_bddAdjPermuteX]
484
485	******************************************************************************/
486	DdNode *
487	Cudd_Dxygtdxz(
488	DdManager * dd /* DD manager */,
489	int N /* number of x, y, and z variables */,
490	DdNode ** x /* array of x variables */,
491	DdNode ** y /* array of y variables */,
492	DdNode ** z /* array of z variables */)
493	{
494	DdNode one, zero;
495	DdNode z1, z2, z3, z4, y1_, y2, *x1;
496	int i;
497
498	one = DD_ONE(dd);
499	zero = Cudd_Not(one);
500
501	/* Build bottom part of BDD outside loop. */
502	y1_ = Cudd_bddIte(dd, y[N-1], one, Cudd_Not(z[N-1]));
503	if (y1_ == NULL) return(NULL);
504	cuddRef(y1_);
505	y2 = Cudd_bddIte(dd, y[N-1], z[N-1], one);
506	if (y2 == NULL) {
507	Cudd_RecursiveDeref(dd, y1_);
508	return(NULL);
509	}
510	cuddRef(y2);
511	x1 = Cudd_bddIte(dd, x[N-1], y1_, y2);
512	if (x1 == NULL) {
513	Cudd_RecursiveDeref(dd, y1_);
514	Cudd_RecursiveDeref(dd, y2);
515	return(NULL);
516	}
517	cuddRef(x1);
518	Cudd_RecursiveDeref(dd, y1_);
519	Cudd_RecursiveDeref(dd, y2);
520
521	/* Loop to build the rest of the BDD. */
522	for (i = N-2; i >= 0; i--) {
523	z1 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1));
524	if (z1 == NULL) {
525	Cudd_RecursiveDeref(dd, x1);
526	return(NULL);
527	}
528	cuddRef(z1);
529	z2 = Cudd_bddIte(dd, z[i], x1, one);
530	if (z2 == NULL) {
531	Cudd_RecursiveDeref(dd, x1);
532	Cudd_RecursiveDeref(dd, z1);
533	return(NULL);
534	}
535	cuddRef(z2);
536	z3 = Cudd_bddIte(dd, z[i], one, x1);
537	if (z3 == NULL) {
538	Cudd_RecursiveDeref(dd, x1);
539	Cudd_RecursiveDeref(dd, z1);
540	Cudd_RecursiveDeref(dd, z2);
541	return(NULL);
542	}
543	cuddRef(z3);
544	z4 = Cudd_bddIte(dd, z[i], x1, zero);
545	if (z4 == NULL) {
546	Cudd_RecursiveDeref(dd, x1);
547	Cudd_RecursiveDeref(dd, z1);
548	Cudd_RecursiveDeref(dd, z2);
549	Cudd_RecursiveDeref(dd, z3);
550	return(NULL);
551	}
552	cuddRef(z4);
553	Cudd_RecursiveDeref(dd, x1);
554	y1_ = Cudd_bddIte(dd, y[i], z2, Cudd_Not(z1));
555	if (y1_ == NULL) {
556	Cudd_RecursiveDeref(dd, z1);
557	Cudd_RecursiveDeref(dd, z2);
558	Cudd_RecursiveDeref(dd, z3);
559	Cudd_RecursiveDeref(dd, z4);
560	return(NULL);
561	}
562	cuddRef(y1_);
563	y2 = Cudd_bddIte(dd, y[i], z4, z3);
564	if (y2 == NULL) {
565	Cudd_RecursiveDeref(dd, z1);
566	Cudd_RecursiveDeref(dd, z2);
567	Cudd_RecursiveDeref(dd, z3);
568	Cudd_RecursiveDeref(dd, z4);
569	Cudd_RecursiveDeref(dd, y1_);
570	return(NULL);
571	}
572	cuddRef(y2);
573	Cudd_RecursiveDeref(dd, z1);
574	Cudd_RecursiveDeref(dd, z2);
575	Cudd_RecursiveDeref(dd, z3);
576	Cudd_RecursiveDeref(dd, z4);
577	x1 = Cudd_bddIte(dd, x[i], y1_, y2);
578	if (x1 == NULL) {
579	Cudd_RecursiveDeref(dd, y1_);
580	Cudd_RecursiveDeref(dd, y2);
581	return(NULL);
582	}
583	cuddRef(x1);
584	Cudd_RecursiveDeref(dd, y1_);
585	Cudd_RecursiveDeref(dd, y2);
586	}
587	cuddDeref(x1);
588	return(Cudd_Not(x1));
589
590	} /* end of Cudd_Dxygtdxz */
591
592
593	/Function******************************************************************
594
595	Synopsis [Generates a BDD for the function d(x,y) > d(y,z).]
596
597	Description [This function generates a BDD for the function d(x,y)
598	> d(y,z);
599	x, y, and z are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\],
600	y\[0\] y\[1\] ... y\[N-1\], and z\[0\] z\[1\] ... z\[N-1\],
601	with 0 the most significant bit.
602	The distance d(x,y) is defined as:
603	\sum_{i=0}^{N-1}(\|x_i - y_i\| \cdot 2^{N-i-1}).
604	The BDD is built bottom-up.
605	It has 7*N-3 internal nodes, if the variables are ordered as follows:
606	x\[0\] y\[0\] z\[0\] x\[1\] y\[1\] z\[1\] ... x\[N-1\] y\[N-1\] z\[N-1\]. ]
607
608	SideEffects [None]
609
610	SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Xgty Cudd_bddAdjPermuteX]
611
612	******************************************************************************/
613	DdNode *
614	Cudd_Dxygtdyz(
615	DdManager * dd /* DD manager */,
616	int N /* number of x, y, and z variables */,
617	DdNode ** x /* array of x variables */,
618	DdNode ** y /* array of y variables */,
619	DdNode ** z /* array of z variables */)
620	{
621	DdNode one, zero;
622	DdNode z1, z2, z3, z4, y1_, y2, *x1;
623	int i;
624
625	one = DD_ONE(dd);
626	zero = Cudd_Not(one);
627
628	/* Build bottom part of BDD outside loop. */
629	y1_ = Cudd_bddIte(dd, y[N-1], one, z[N-1]);
630	if (y1_ == NULL) return(NULL);
631	cuddRef(y1_);
632	y2 = Cudd_bddIte(dd, y[N-1], z[N-1], zero);
633	if (y2 == NULL) {
634	Cudd_RecursiveDeref(dd, y1_);
635	return(NULL);
636	}
637	cuddRef(y2);
638	x1 = Cudd_bddIte(dd, x[N-1], y1_, Cudd_Not(y2));
639	if (x1 == NULL) {
640	Cudd_RecursiveDeref(dd, y1_);
641	Cudd_RecursiveDeref(dd, y2);
642	return(NULL);
643	}
644	cuddRef(x1);
645	Cudd_RecursiveDeref(dd, y1_);
646	Cudd_RecursiveDeref(dd, y2);
647
648	/* Loop to build the rest of the BDD. */
649	for (i = N-2; i >= 0; i--) {
650	z1 = Cudd_bddIte(dd, z[i], x1, zero);
651	if (z1 == NULL) {
652	Cudd_RecursiveDeref(dd, x1);
653	return(NULL);
654	}
655	cuddRef(z1);
656	z2 = Cudd_bddIte(dd, z[i], x1, one);
657	if (z2 == NULL) {
658	Cudd_RecursiveDeref(dd, x1);
659	Cudd_RecursiveDeref(dd, z1);
660	return(NULL);
661	}
662	cuddRef(z2);
663	z3 = Cudd_bddIte(dd, z[i], one, x1);
664	if (z3 == NULL) {
665	Cudd_RecursiveDeref(dd, x1);
666	Cudd_RecursiveDeref(dd, z1);
667	Cudd_RecursiveDeref(dd, z2);
668	return(NULL);
669	}
670	cuddRef(z3);
671	z4 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1));
672	if (z4 == NULL) {
673	Cudd_RecursiveDeref(dd, x1);
674	Cudd_RecursiveDeref(dd, z1);
675	Cudd_RecursiveDeref(dd, z2);
676	Cudd_RecursiveDeref(dd, z3);
677	return(NULL);
678	}
679	cuddRef(z4);
680	Cudd_RecursiveDeref(dd, x1);
681	y1_ = Cudd_bddIte(dd, y[i], z2, z1);
682	if (y1_ == NULL) {
683	Cudd_RecursiveDeref(dd, z1);
684	Cudd_RecursiveDeref(dd, z2);
685	Cudd_RecursiveDeref(dd, z3);
686	Cudd_RecursiveDeref(dd, z4);
687	return(NULL);
688	}
689	cuddRef(y1_);
690	y2 = Cudd_bddIte(dd, y[i], z4, Cudd_Not(z3));
691	if (y2 == NULL) {
692	Cudd_RecursiveDeref(dd, z1);
693	Cudd_RecursiveDeref(dd, z2);
694	Cudd_RecursiveDeref(dd, z3);
695	Cudd_RecursiveDeref(dd, z4);
696	Cudd_RecursiveDeref(dd, y1_);
697	return(NULL);
698	}
699	cuddRef(y2);
700	Cudd_RecursiveDeref(dd, z1);
701	Cudd_RecursiveDeref(dd, z2);
702	Cudd_RecursiveDeref(dd, z3);
703	Cudd_RecursiveDeref(dd, z4);
704	x1 = Cudd_bddIte(dd, x[i], y1_, Cudd_Not(y2));
705	if (x1 == NULL) {
706	Cudd_RecursiveDeref(dd, y1_);
707	Cudd_RecursiveDeref(dd, y2);
708	return(NULL);
709	}
710	cuddRef(x1);
711	Cudd_RecursiveDeref(dd, y1_);
712	Cudd_RecursiveDeref(dd, y2);
713	}
714	cuddDeref(x1);
715	return(Cudd_Not(x1));
716
717	} /* end of Cudd_Dxygtdyz */
718
719
720	/Function******************************************************************
721
722	Synopsis [Computes the compatible projection of R w.r.t. cube Y.]
723
724	Description [Computes the compatible projection of relation R with
725	respect to cube Y. Returns a pointer to the c-projection if
726	successful; NULL otherwise. For a comparison between Cudd_CProjection
727	and Cudd_PrioritySelect, see the documentation of the latter.]
728
729	SideEffects [None]
730
731	SeeAlso [Cudd_PrioritySelect]
732
733	******************************************************************************/
734	DdNode *
735	Cudd_CProjection(
736	DdManager * dd,
737	DdNode * R,
738	DdNode * Y)
739	{
740	DdNode *res;
741	DdNode *support;
742
743	if (cuddCheckCube(dd,Y) == 0) {
744	(void) fprintf(dd->err,
745	"Error: The third argument of Cudd_CProjection should be a cube\n");
746	dd->errorCode = CUDD_INVALID_ARG;
747	return(NULL);
748	}
749
750	/* Compute the support of Y, which is used by the abstraction step
751	** in cuddCProjectionRecur.
752	*/
753	support = Cudd_Support(dd,Y);
754	if (support == NULL) return(NULL);
755	cuddRef(support);
756
757	do {
758	dd->reordered = 0;
759	res = cuddCProjectionRecur(dd,R,Y,support);
760	} while (dd->reordered == 1);
761
762	if (res == NULL) {
763	Cudd_RecursiveDeref(dd,support);
764	return(NULL);
765	}
766	cuddRef(res);
767	Cudd_RecursiveDeref(dd,support);
768	cuddDeref(res);
769
770	return(res);
771
772	} /* end of Cudd_CProjection */
773
774
775	/Function******************************************************************
776
777	Synopsis [Computes the Hamming distance ADD.]
778
779	Description [Computes the Hamming distance ADD. Returns an ADD that
780	gives the Hamming distance between its two arguments if successful;
781	NULL otherwise. The two vectors xVars and yVars identify the variables
782	that form the two arguments.]
783
784	SideEffects [None]
785
786	SeeAlso []
787
788	******************************************************************************/
789	DdNode *
790	Cudd_addHamming(
791	DdManager * dd,
792	DdNode ** xVars,
793	DdNode ** yVars,
794	int nVars)
795	{
796	DdNode result,tempBdd;
797	DdNode tempAdd,temp;
798	int i;
799
800	result = DD_ZERO(dd);
801	cuddRef(result);
802
803	for (i = 0; i < nVars; i++) {
804	tempBdd = Cudd_bddIte(dd,xVars[i],Cudd_Not(yVars[i]),yVars[i]);
805	if (tempBdd == NULL) {
806	Cudd_RecursiveDeref(dd,result);
807	return(NULL);
808	}
809	cuddRef(tempBdd);
810	tempAdd = Cudd_BddToAdd(dd,tempBdd);
811	if (tempAdd == NULL) {
812	Cudd_RecursiveDeref(dd,tempBdd);
813	Cudd_RecursiveDeref(dd,result);
814	return(NULL);
815	}
816	cuddRef(tempAdd);
817	Cudd_RecursiveDeref(dd,tempBdd);
818	temp = Cudd_addApply(dd,Cudd_addPlus,tempAdd,result);
819	if (temp == NULL) {
820	Cudd_RecursiveDeref(dd,tempAdd);
821	Cudd_RecursiveDeref(dd,result);
822	return(NULL);
823	}
824	cuddRef(temp);
825	Cudd_RecursiveDeref(dd,tempAdd);
826	Cudd_RecursiveDeref(dd,result);
827	result = temp;
828	}
829
830	cuddDeref(result);
831	return(result);
832
833	} /* end of Cudd_addHamming */
834
835
836	/Function******************************************************************
837
838	Synopsis [Returns the minimum Hamming distance between f and minterm.]
839
840	Description [Returns the minimum Hamming distance between the
841	minterms of a function f and a reference minterm. The function is
842	given as a BDD; the minterm is given as an array of integers, one
843	for each variable in the manager. Returns the minimum distance if
844	it is less than the upper bound; the upper bound if the minimum
845	distance is at least as large; CUDD_OUT_OF_MEM in case of failure.]
846
847	SideEffects [None]
848
849	SeeAlso [Cudd_addHamming Cudd_bddClosestCube]
850
851	******************************************************************************/
852	int
853	Cudd_MinHammingDist(
854	DdManager dd / DD manager */,
855	DdNode f / function to examine */,
856	int minterm / reference minterm */,
857	int upperBound /* distance above which an approximate answer is OK */)
858	{
859	DdHashTable *table;
860	CUDD_VALUE_TYPE epsilon;
861	int res;
862
863	table = cuddHashTableInit(dd,1,2);
864	if (table == NULL) {
865	return(CUDD_OUT_OF_MEM);
866	}
867	epsilon = Cudd_ReadEpsilon(dd);
868	Cudd_SetEpsilon(dd,(CUDD_VALUE_TYPE)0.0);
869	res = cuddMinHammingDistRecur(f,minterm,table,upperBound);
870	cuddHashTableQuit(table);
871	Cudd_SetEpsilon(dd,epsilon);
872
873	return(res);
874
875	} /* end of Cudd_MinHammingDist */
876
877
878	/Function******************************************************************
879
880	Synopsis [Finds a cube of f at minimum Hamming distance from g.]
881
882	Description [Finds a cube of f at minimum Hamming distance from the
883	minterms of g. All the minterms of the cube are at the minimum
884	distance. If the distance is 0, the cube belongs to the
885	intersection of f and g. Returns the cube if successful; NULL
886	otherwise.]
887
888	SideEffects [The distance is returned as a side effect.]
889
890	SeeAlso [Cudd_MinHammingDist]
891
892	******************************************************************************/
893	DdNode *
894	Cudd_bddClosestCube(
895	DdManager *dd,
896	DdNode * f,
897	DdNode *g,
898	int *distance)
899	{
900	DdNode res, acube;
901	CUDD_VALUE_TYPE rdist;
902
903	/* Compute the cube and distance as a single ADD. */
904	do {
905	dd->reordered = 0;
906	res = cuddBddClosestCube(dd,f,g,CUDD_CONST_INDEX + 1.0);
907	} while (dd->reordered == 1);
908	if (res == NULL) return(NULL);
909	cuddRef(res);
910
911	/* Unpack distance and cube. */
912	do {
913	dd->reordered = 0;
914	acube = separateCube(dd, res, &rdist);
915	} while (dd->reordered == 1);
916	if (acube == NULL) {
917	Cudd_RecursiveDeref(dd, res);
918	return(NULL);
919	}
920	cuddRef(acube);
921	Cudd_RecursiveDeref(dd, res);
922
923	/* Convert cube from ADD to BDD. */
924	do {
925	dd->reordered = 0;
926	res = cuddAddBddDoPattern(dd, acube);
927	} while (dd->reordered == 1);
928	if (res == NULL) {
929	Cudd_RecursiveDeref(dd, acube);
930	return(NULL);
931	}
932	cuddRef(res);
933	Cudd_RecursiveDeref(dd, acube);
934
935	*distance = (int) rdist;
936	cuddDeref(res);
937	return(res);
938
939	} /* end of Cudd_bddClosestCube */
940
941
942	/---------------------------------------------------------------------------/
943	/* Definition of internal functions */
944	/---------------------------------------------------------------------------/
945
946
947	/Function******************************************************************
948
949	Synopsis [Performs the recursive step of Cudd_CProjection.]
950
951	Description [Performs the recursive step of Cudd_CProjection. Returns
952	the projection if successful; NULL otherwise.]
953
954	SideEffects [None]
955
956	SeeAlso [Cudd_CProjection]
957
958	******************************************************************************/
959	DdNode *
960	cuddCProjectionRecur(
961	DdManager * dd,
962	DdNode * R,
963	DdNode * Y,
964	DdNode * Ysupp)
965	{
966	DdNode res, res1, res2, resA;
967	DdNode r, y, RT, RE, YT, YE, Yrest, Ra, Ran, Gamma, *Alpha;
968	unsigned int topR, topY, top, index;
969	DdNode *one = DD_ONE(dd);
970
971	statLine(dd);
972	if (Y == one) return(R);
973
974	#ifdef DD_DEBUG
975	assert(!Cudd_IsConstant(Y));
976	#endif
977
978	if (R == Cudd_Not(one)) return(R);
979
980	res = cuddCacheLookup2(dd, Cudd_CProjection, R, Y);
981	if (res != NULL) return(res);
982
983	r = Cudd_Regular(R);
984	topR = cuddI(dd,r->index);
985	y = Cudd_Regular(Y);
986	topY = cuddI(dd,y->index);
987
988	top = ddMin(topR, topY);
989
990	/* Compute the cofactors of R */
991	if (topR == top) {
992	index = r->index;
993	RT = cuddT(r);
994	RE = cuddE(r);
995	if (r != R) {
996	RT = Cudd_Not(RT); RE = Cudd_Not(RE);
997	}
998	} else {
999	RT = RE = R;
1000	}
1001
1002	if (topY > top) {
1003	/* Y does not depend on the current top variable.
1004	** We just need to compute the results on the two cofactors of R
1005	** and make them the children of a node labeled r->index.
1006	*/
1007	res1 = cuddCProjectionRecur(dd,RT,Y,Ysupp);
1008	if (res1 == NULL) return(NULL);
1009	cuddRef(res1);
1010	res2 = cuddCProjectionRecur(dd,RE,Y,Ysupp);
1011	if (res2 == NULL) {
1012	Cudd_RecursiveDeref(dd,res1);
1013	return(NULL);
1014	}
1015	cuddRef(res2);
1016	res = cuddBddIteRecur(dd, dd->vars[index], res1, res2);
1017	if (res == NULL) {
1018	Cudd_RecursiveDeref(dd,res1);
1019	Cudd_RecursiveDeref(dd,res2);
1020	return(NULL);
1021	}
1022	/* If we have reached this point, res1 and res2 are now
1023	** incorporated in res. cuddDeref is therefore sufficient.
1024	*/
1025	cuddDeref(res1);
1026	cuddDeref(res2);
1027	} else {
1028	/* Compute the cofactors of Y */
1029	index = y->index;
1030	YT = cuddT(y);
1031	YE = cuddE(y);
1032	if (y != Y) {
1033	YT = Cudd_Not(YT); YE = Cudd_Not(YE);
1034	}
1035	if (YT == Cudd_Not(one)) {
1036	Alpha = Cudd_Not(dd->vars[index]);
1037	Yrest = YE;
1038	Ra = RE;
1039	Ran = RT;
1040	} else {
1041	Alpha = dd->vars[index];
1042	Yrest = YT;
1043	Ra = RT;
1044	Ran = RE;
1045	}
1046	Gamma = cuddBddExistAbstractRecur(dd,Ra,cuddT(Ysupp));
1047	if (Gamma == NULL) return(NULL);
1048	if (Gamma == one) {
1049	res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp));
1050	if (res1 == NULL) return(NULL);
1051	cuddRef(res1);
1052	res = cuddBddAndRecur(dd, Alpha, res1);
1053	if (res == NULL) {
1054	Cudd_RecursiveDeref(dd,res1);
1055	return(NULL);
1056	}
1057	cuddDeref(res1);
1058	} else if (Gamma == Cudd_Not(one)) {
1059	res1 = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp));
1060	if (res1 == NULL) return(NULL);
1061	cuddRef(res1);
1062	res = cuddBddAndRecur(dd, Cudd_Not(Alpha), res1);
1063	if (res == NULL) {
1064	Cudd_RecursiveDeref(dd,res1);
1065	return(NULL);
1066	}
1067	cuddDeref(res1);
1068	} else {
1069	cuddRef(Gamma);
1070	resA = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp));
1071	if (resA == NULL) {
1072	Cudd_RecursiveDeref(dd,Gamma);
1073	return(NULL);
1074	}
1075	cuddRef(resA);
1076	res2 = cuddBddAndRecur(dd, Cudd_Not(Gamma), resA);
1077	if (res2 == NULL) {
1078	Cudd_RecursiveDeref(dd,Gamma);
1079	Cudd_RecursiveDeref(dd,resA);
1080	return(NULL);
1081	}
1082	cuddRef(res2);
1083	Cudd_RecursiveDeref(dd,Gamma);
1084	Cudd_RecursiveDeref(dd,resA);
1085	res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp));
1086	if (res1 == NULL) {
1087	Cudd_RecursiveDeref(dd,res2);
1088	return(NULL);
1089	}
1090	cuddRef(res1);
1091	res = cuddBddIteRecur(dd, Alpha, res1, res2);
1092	if (res == NULL) {
1093	Cudd_RecursiveDeref(dd,res1);
1094	Cudd_RecursiveDeref(dd,res2);
1095	return(NULL);
1096	}
1097	cuddDeref(res1);
1098	cuddDeref(res2);
1099	}
1100	}
1101
1102	cuddCacheInsert2(dd,Cudd_CProjection,R,Y,res);
1103
1104	return(res);
1105
1106	} /* end of cuddCProjectionRecur */
1107
1108
1109	/Function******************************************************************
1110
1111	Synopsis [Performs the recursive step of Cudd_bddClosestCube.]
1112
1113	Description [Performs the recursive step of Cudd_bddClosestCube.
1114	Returns the cube if succesful; NULL otherwise. The procedure uses a
1115	four-way recursion to examine all four combinations of cofactors of
1116	<code>f</code> and <code>g</code> according to the following formula.
1117	<pre>
1118	H(f,g) = min(H(ft,gt), H(fe,ge), H(ft,ge)+1, H(fe,gt)+1)
1119	</pre>
1120	Bounding is based on the following observations.
1121	<ul>
1122	<li> If we already found two points at distance 0, there is no point in
1123	continuing. Furthermore,
1124	<li> If F == not(G) then the best we can hope for is a minimum distance
1125	of 1. If we have already found two points at distance 1, there is
1126	no point in continuing. (Indeed, H(F,G) == 1 in this case. We
1127	have to continue, though, to find the cube.)
1128	</ul>
1129	The variable <code>bound</code> is set at the largest value of the distance
1130	that we are still interested in. Therefore, we desist when
1131	<pre>
1132	(bound == -1) and (F != not(G)) or (bound == 0) and (F == not(G)).
1133	</pre>
1134	If we were maximally aggressive in using the bound, we would always
1135	set the bound to the minimum distance seen thus far minus one. That
1136	is, we would maintain the invariant
1137	<pre>
1138	bound < minD,
1139	</pre>
1140	except at the very beginning, when we have no value for
1141	<code>minD</code>.<p>
1142
1143	However, we do not use <code>bound < minD</code> when examining the
1144	two negative cofactors, because we try to find a large cube at
1145	minimum distance. To do so, we try to find a cube in the negative
1146	cofactors at the same or smaller distance from the cube found in the
1147	positive cofactors.<p>
1148
1149	When we compute <code>H(ft,ge)</code> and <code>H(fe,gt)</code> we
1150	know that we are going to add 1 to the result of the recursive call
1151	to account for the difference in the splitting variable. Therefore,
1152	we decrease the bound correspondingly.<p>
1153
1154	Another important observation concerns the need of examining all
1155	four pairs of cofators only when both <code>f</code> and
1156	<code>g</code> depend on the top variable.<p>
1157
1158	Suppose <code>gt == ge == g</code>. (That is, <code>g</code> does
1159	not depend on the top variable.) Then
1160	<pre>
1161	H(f,g) = min(H(ft,g), H(fe,g), H(ft,g)+1, H(fe,g)+1)
1162	= min(H(ft,g), H(fe,g)) .
1163	</pre>
1164	Therefore, under these circumstances, we skip the two "cross" cases.<p>
1165
1166	An interesting feature of this function is the scheme used for
1167	caching the results in the global computed table. Since we have a
1168	cube and a distance, we combine them to form an ADD. The
1169	combination replaces the zero child of the top node of the cube with
1170	the negative of the distance. (The use of the negative is to avoid
1171	ambiguity with 1.) The degenerate cases (zero and one) are treated
1172	specially because the distance is known (0 for one, and infinity for
1173	zero).]
1174
1175	SideEffects [None]
1176
1177	SeeAlso [Cudd_bddClosestCube]
1178
1179	******************************************************************************/
1180	DdNode *
1181	cuddBddClosestCube(
1182	DdManager *dd,
1183	DdNode *f,
1184	DdNode *g,
1185	CUDD_VALUE_TYPE bound)
1186	{
1187	DdNode res, F, G, ft, fe, gt, ge, tt, *ee;
1188	DdNode ctt, cee, cte, cet;
1189	CUDD_VALUE_TYPE minD, dtt, dee, dte, det;
1190	DdNode *one = DD_ONE(dd);
1191	DdNode *lzero = Cudd_Not(one);
1192	DdNode *azero = DD_ZERO(dd);
1193	unsigned int topf, topg, index;
1194
1195	statLine(dd);
1196	if (bound < (f == Cudd_Not(g))) return(azero);
1197	/* Terminal cases. */
1198	if (g == lzero \|\| f == lzero) return(azero);
1199	if (f == one && g == one) return(one);
1200
1201	/* Check cache. */
1202	F = Cudd_Regular(f);
1203	G = Cudd_Regular(g);
1204	if (F->ref != 1 \|\| G->ref != 1) {
1205	res = cuddCacheLookup2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g);
1206	if (res != NULL) return(res);
1207	}
1208
1209	topf = cuddI(dd,F->index);
1210	topg = cuddI(dd,G->index);
1211
1212	/* Compute cofactors. */
1213	if (topf <= topg) {
1214	index = F->index;
1215	ft = cuddT(F);
1216	fe = cuddE(F);
1217	if (Cudd_IsComplement(f)) {
1218	ft = Cudd_Not(ft);
1219	fe = Cudd_Not(fe);
1220	}
1221	} else {
1222	index = G->index;
1223	ft = fe = f;
1224	}
1225
1226	if (topg <= topf) {
1227	gt = cuddT(G);
1228	ge = cuddE(G);
1229	if (Cudd_IsComplement(g)) {
1230	gt = Cudd_Not(gt);
1231	ge = Cudd_Not(ge);
1232	}
1233	} else {
1234	gt = ge = g;
1235	}
1236
1237	tt = cuddBddClosestCube(dd,ft,gt,bound);
1238	if (tt == NULL) return(NULL);
1239	cuddRef(tt);
1240	ctt = separateCube(dd,tt,&dtt);
1241	if (ctt == NULL) {
1242	Cudd_RecursiveDeref(dd, tt);
1243	return(NULL);
1244	}
1245	cuddRef(ctt);
1246	Cudd_RecursiveDeref(dd, tt);
1247	minD = dtt;
1248	bound = ddMin(bound,minD);
1249
1250	ee = cuddBddClosestCube(dd,fe,ge,bound);
1251	if (ee == NULL) {
1252	Cudd_RecursiveDeref(dd, ctt);
1253	return(NULL);
1254	}
1255	cuddRef(ee);
1256	cee = separateCube(dd,ee,&dee);
1257	if (cee == NULL) {
1258	Cudd_RecursiveDeref(dd, ctt);
1259	Cudd_RecursiveDeref(dd, ee);
1260	return(NULL);
1261	}
1262	cuddRef(cee);
1263	Cudd_RecursiveDeref(dd, ee);
1264	minD = ddMin(dtt, dee);
1265	if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1);
1266
1267	if (minD > 0 && topf == topg) {
1268	DdNode *te = cuddBddClosestCube(dd,ft,ge,bound-1);
1269	if (te == NULL) {
1270	Cudd_RecursiveDeref(dd, ctt);
1271	Cudd_RecursiveDeref(dd, cee);
1272	return(NULL);
1273	}
1274	cuddRef(te);
1275	cte = separateCube(dd,te,&dte);
1276	if (cte == NULL) {
1277	Cudd_RecursiveDeref(dd, ctt);
1278	Cudd_RecursiveDeref(dd, cee);
1279	Cudd_RecursiveDeref(dd, te);
1280	return(NULL);
1281	}
1282	cuddRef(cte);
1283	Cudd_RecursiveDeref(dd, te);
1284	dte += 1.0;
1285	minD = ddMin(minD, dte);
1286	} else {
1287	cte = azero;
1288	cuddRef(cte);
1289	dte = CUDD_CONST_INDEX + 1.0;
1290	}
1291	if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1);
1292
1293	if (minD > 0 && topf == topg) {
1294	DdNode *et = cuddBddClosestCube(dd,fe,gt,bound-1);
1295	if (et == NULL) {
1296	Cudd_RecursiveDeref(dd, ctt);
1297	Cudd_RecursiveDeref(dd, cee);
1298	Cudd_RecursiveDeref(dd, cte);
1299	return(NULL);
1300	}
1301	cuddRef(et);
1302	cet = separateCube(dd,et,&det);
1303	if (cet == NULL) {
1304	Cudd_RecursiveDeref(dd, ctt);
1305	Cudd_RecursiveDeref(dd, cee);
1306	Cudd_RecursiveDeref(dd, cte);
1307	Cudd_RecursiveDeref(dd, et);
1308	return(NULL);
1309	}
1310	cuddRef(cet);
1311	Cudd_RecursiveDeref(dd, et);
1312	det += 1.0;
1313	minD = ddMin(minD, det);
1314	} else {
1315	cet = azero;
1316	cuddRef(cet);
1317	det = CUDD_CONST_INDEX + 1.0;
1318	}
1319
1320	if (minD == dtt) {
1321	if (dtt == dee && ctt == cee) {
1322	res = createResult(dd,CUDD_CONST_INDEX,1,ctt,dtt);
1323	} else {
1324	res = createResult(dd,index,1,ctt,dtt);
1325	}
1326	} else if (minD == dee) {
1327	res = createResult(dd,index,0,cee,dee);
1328	} else if (minD == dte) {
1329	#ifdef DD_DEBUG
1330	assert(topf == topg);
1331	#endif
1332	res = createResult(dd,index,1,cte,dte);
1333	} else {
1334	#ifdef DD_DEBUG
1335	assert(topf == topg);
1336	#endif
1337	res = createResult(dd,index,0,cet,det);
1338	}
1339	if (res == NULL) {
1340	Cudd_RecursiveDeref(dd, ctt);
1341	Cudd_RecursiveDeref(dd, cee);
1342	Cudd_RecursiveDeref(dd, cte);
1343	Cudd_RecursiveDeref(dd, cet);
1344	return(NULL);
1345	}
1346	cuddRef(res);
1347	Cudd_RecursiveDeref(dd, ctt);
1348	Cudd_RecursiveDeref(dd, cee);
1349	Cudd_RecursiveDeref(dd, cte);
1350	Cudd_RecursiveDeref(dd, cet);
1351
1352	/* Only cache results that are different from azero to avoid
1353	** storing results that depend on the value of the bound. */
1354	if ((F->ref != 1 \|\| G->ref != 1) && res != azero)
1355	cuddCacheInsert2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g, res);
1356
1357	cuddDeref(res);
1358	return(res);
1359
1360	} /* end of cuddBddClosestCube */
1361
1362
1363	/---------------------------------------------------------------------------/
1364	/* Definition of static functions */
1365	/---------------------------------------------------------------------------/
1366
1367
1368	/Function******************************************************************
1369
1370	Synopsis [Performs the recursive step of Cudd_MinHammingDist.]
1371
1372	Description [Performs the recursive step of Cudd_MinHammingDist.
1373	It is based on the following identity. Let H(f) be the
1374	minimum Hamming distance of the minterms of f from the reference
1375	minterm. Then:
1376	<xmp>
1377	H(f) = min(H(f0)+h0,H(f1)+h1)
1378	</xmp>
1379	where f0 and f1 are the two cofactors of f with respect to its top
1380	variable; h0 is 1 if the minterm assigns 1 to the top variable of f;
1381	h1 is 1 if the minterm assigns 0 to the top variable of f.
1382	The upper bound on the distance is used to bound the depth of the
1383	recursion.
1384	Returns the minimum distance unless it exceeds the upper bound or
1385	computation fails.]
1386
1387	SideEffects [None]
1388
1389	SeeAlso [Cudd_MinHammingDist]
1390
1391	******************************************************************************/
1392	static int
1393	cuddMinHammingDistRecur(
1394	DdNode * f,
1395	int *minterm,
1396	DdHashTable * table,
1397	int upperBound)
1398	{
1399	DdNode F, Ft, *Fe;
1400	double h, hT, hE;
1401	DdNode zero, res;
1402	DdManager *dd = table->manager;
1403
1404	statLine(dd);
1405	if (upperBound == 0) return(0);
1406
1407	F = Cudd_Regular(f);
1408
1409	if (cuddIsConstant(F)) {
1410	zero = Cudd_Not(DD_ONE(dd));
1411	if (f == dd->background \|\| f == zero) {
1412	return(upperBound);
1413	} else {
1414	return(0);
1415	}
1416	}
1417	if ((res = cuddHashTableLookup1(table,f)) != NULL) {
1418	h = cuddV(res);
1419	if (res->ref == 0) {
1420	dd->dead++;
1421	dd->constants.dead++;
1422	}
1423	return((int) h);
1424	}
1425
1426	Ft = cuddT(F); Fe = cuddE(F);
1427	if (Cudd_IsComplement(f)) {
1428	Ft = Cudd_Not(Ft); Fe = Cudd_Not(Fe);
1429	}
1430	if (minterm[F->index] == 0) {
1431	DdNode *temp = Ft;
1432	Ft = Fe; Fe = temp;
1433	}
1434
1435	hT = cuddMinHammingDistRecur(Ft,minterm,table,upperBound);
1436	if (hT == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
1437	if (hT == 0) {
1438	hE = upperBound;
1439	} else {
1440	hE = cuddMinHammingDistRecur(Fe,minterm,table,upperBound - 1);
1441	if (hE == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
1442	}
1443	h = ddMin(hT, hE + 1);
1444
1445	if (F->ref != 1) {
1446	ptrint fanout = (ptrint) F->ref;
1447	cuddSatDec(fanout);
1448	res = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) h);
1449	if (!cuddHashTableInsert1(table,f,res,fanout)) {
1450	cuddRef(res); Cudd_RecursiveDeref(dd, res);
1451	return(CUDD_OUT_OF_MEM);
1452	}
1453	}
1454
1455	return((int) h);
1456
1457	} /* end of cuddMinHammingDistRecur */
1458
1459
1460	/Function******************************************************************
1461
1462	Synopsis [Separates cube from distance.]
1463
1464	Description [Separates cube from distance. Returns the cube if
1465	successful; NULL otherwise.]
1466
1467	SideEffects [The distance is returned as a side effect.]
1468
1469	SeeAlso [cuddBddClosestCube createResult]
1470
1471	******************************************************************************/
1472	static DdNode *
1473	separateCube(
1474	DdManager *dd,
1475	DdNode *f,
1476	CUDD_VALUE_TYPE *distance)
1477	{
1478	DdNode cube, t;
1479
1480	/* One and zero are special cases because the distance is implied. */
1481	if (Cudd_IsConstant(f)) {
1482	*distance = (f == DD_ONE(dd)) ? 0.0 :
1483	(1.0 + (CUDD_VALUE_TYPE) CUDD_CONST_INDEX);
1484	return(f);
1485	}
1486
1487	/* Find out which branch points to the distance and replace the top
1488	** node with one pointing to zero instead. */
1489	t = cuddT(f);
1490	if (Cudd_IsConstant(t) && cuddV(t) <= 0) {
1491	#ifdef DD_DEBUG
1492	assert(!Cudd_IsConstant(cuddE(f)) \|\| cuddE(f) == DD_ONE(dd));
1493	#endif
1494	*distance = -cuddV(t);
1495	cube = cuddUniqueInter(dd, f->index, DD_ZERO(dd), cuddE(f));
1496	} else {
1497	#ifdef DD_DEBUG
1498	assert(!Cudd_IsConstant(t) \|\| t == DD_ONE(dd));
1499	#endif
1500	*distance = -cuddV(cuddE(f));
1501	cube = cuddUniqueInter(dd, f->index, t, DD_ZERO(dd));
1502	}
1503
1504	return(cube);
1505
1506	} /* end of separateCube */
1507
1508
1509	/Function******************************************************************
1510
1511	Synopsis [Builds a result for cache storage.]
1512
1513	Description [Builds a result for cache storage. Returns a pointer
1514	to the resulting ADD if successful; NULL otherwise.]
1515
1516	SideEffects [None]
1517
1518	SeeAlso [cuddBddClosestCube separateCube]
1519
1520	******************************************************************************/
1521	static DdNode *
1522	createResult(
1523	DdManager *dd,
1524	unsigned int index,
1525	unsigned int phase,
1526	DdNode *cube,
1527	CUDD_VALUE_TYPE distance)
1528	{
1529	DdNode res, constant;
1530
1531	/* Special case. The cube is either one or zero, and we do not
1532	** add any variables. Hence, the result is also one or zero,
1533	** and the distance remains implied by the value of the constant. */
1534	if (index == CUDD_CONST_INDEX && Cudd_IsConstant(cube)) return(cube);
1535
1536	constant = cuddUniqueConst(dd,-distance);
1537	if (constant == NULL) return(NULL);
1538	cuddRef(constant);
1539
1540	if (index == CUDD_CONST_INDEX) {
1541	/* Replace the top node. */
1542	if (cuddT(cube) == DD_ZERO(dd)) {
1543	res = cuddUniqueInter(dd,cube->index,constant,cuddE(cube));
1544	} else {
1545	res = cuddUniqueInter(dd,cube->index,cuddT(cube),constant);
1546	}
1547	} else {
1548	/* Add a new top node. */
1549	#ifdef DD_DEBUG
1550	assert(cuddI(dd,index) < cuddI(dd,cube->index));
1551	#endif
1552	if (phase) {
1553	res = cuddUniqueInter(dd,index,cube,constant);
1554	} else {
1555	res = cuddUniqueInter(dd,index,constant,cube);
1556	}
1557	}
1558	if (res == NULL) {
1559	Cudd_RecursiveDeref(dd, constant);
1560	return(NULL);
1561	}
1562	cuddDeref(constant); /* safe because constant is part of res */
1563
1564	return(res);
1565
1566	} /* end of createResult */

Note: See TracBrowser for help on using the repository browser.

Download in other formats: