Context Navigation

← Previous Revision
Latest Revision
Next Revision →
Blame
Revision Log

cuddUtil.c @ 104

Last change on this file since 104 was 13, checked in by cecile, 13 years ago
library glu 2.3
File size: 103.6 KB

Line
1	/CFile*********************************************************************
2
3	FileName [cuddUtil.c]
4
5	PackageName [cudd]
6
7	Synopsis [Utility functions.]
8
9	Description [External procedures included in this module:
10	<ul>
11	<li> Cudd_PrintMinterm()
12	<li> Cudd_bddPrintCover()
13	<li> Cudd_PrintDebug()
14	<li> Cudd_DagSize()
15	<li> Cudd_EstimateCofactor()
16	<li> Cudd_EstimateCofactorSimple()
17	<li> Cudd_SharingSize()
18	<li> Cudd_CountMinterm()
19	<li> Cudd_EpdCountMinterm()
20	<li> Cudd_CountPath()
21	<li> Cudd_CountPathsToNonZero()
22	<li> Cudd_Support()
23	<li> Cudd_SupportIndex()
24	<li> Cudd_SupportSize()
25	<li> Cudd_VectorSupport()
26	<li> Cudd_VectorSupportIndex()
27	<li> Cudd_VectorSupportSize()
28	<li> Cudd_ClassifySupport()
29	<li> Cudd_CountLeaves()
30	<li> Cudd_bddPickOneCube()
31	<li> Cudd_bddPickOneMinterm()
32	<li> Cudd_bddPickArbitraryMinterms()
33	<li> Cudd_SubsetWithMaskVars()
34	<li> Cudd_FirstCube()
35	<li> Cudd_NextCube()
36	<li> Cudd_bddComputeCube()
37	<li> Cudd_addComputeCube()
38	<li> Cudd_FirstNode()
39	<li> Cudd_NextNode()
40	<li> Cudd_GenFree()
41	<li> Cudd_IsGenEmpty()
42	<li> Cudd_IndicesToCube()
43	<li> Cudd_PrintVersion()
44	<li> Cudd_AverageDistance()
45	<li> Cudd_Random()
46	<li> Cudd_Srandom()
47	<li> Cudd_Density()
48	</ul>
49	Internal procedures included in this module:
50	<ul>
51	<li> cuddP()
52	<li> cuddStCountfree()
53	<li> cuddCollectNodes()
54	<li> cuddNodeArray()
55	</ul>
56	Static procedures included in this module:
57	<ul>
58	<li> dp2()
59	<li> ddPrintMintermAux()
60	<li> ddDagInt()
61	<li> ddCountMintermAux()
62	<li> ddEpdCountMintermAux()
63	<li> ddCountPathAux()
64	<li> ddSupportStep()
65	<li> ddClearFlag()
66	<li> ddLeavesInt()
67	<li> ddPickArbitraryMinterms()
68	<li> ddPickRepresentativeCube()
69	<li> ddEpdFree()
70	</ul>]
71
72	Author [Fabio Somenzi]
73
74	Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
75
76	All rights reserved.
77
78	Redistribution and use in source and binary forms, with or without
79	modification, are permitted provided that the following conditions
80	are met:
81
82	Redistributions of source code must retain the above copyright
83	notice, this list of conditions and the following disclaimer.
84
85	Redistributions in binary form must reproduce the above copyright
86	notice, this list of conditions and the following disclaimer in the
87	documentation and/or other materials provided with the distribution.
88
89	Neither the name of the University of Colorado nor the names of its
90	contributors may be used to endorse or promote products derived from
91	this software without specific prior written permission.
92
93	THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
94	"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
95	LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
96	FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
97	COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
98	INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
99	BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
100	LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
101	CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
102	LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
103	ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
104	POSSIBILITY OF SUCH DAMAGE.]
105
106	******************************************************************************/
107
108	#include "util.h"
109	#include "cuddInt.h"
110
111	/---------------------------------------------------------------------------/
112	/* Constant declarations */
113	/---------------------------------------------------------------------------/
114
115	/* Random generator constants. */
116	#define MODULUS1 2147483563
117	#define LEQA1 40014
118	#define LEQQ1 53668
119	#define LEQR1 12211
120	#define MODULUS2 2147483399
121	#define LEQA2 40692
122	#define LEQQ2 52774
123	#define LEQR2 3791
124	#define STAB_SIZE 64
125	#define STAB_DIV (1 + (MODULUS1 - 1) / STAB_SIZE)
126
127	/---------------------------------------------------------------------------/
128	/* Stucture declarations */
129	/---------------------------------------------------------------------------/
130
131	/---------------------------------------------------------------------------/
132	/* Type declarations */
133	/---------------------------------------------------------------------------/
134
135
136	/---------------------------------------------------------------------------/
137	/* Variable declarations */
138	/---------------------------------------------------------------------------/
139
140	#ifndef lint
141	static char rcsid[] DD_UNUSED = "$Id: cuddUtil.c,v 1.81 2009/03/08 02:49:02 fabio Exp $";
142	#endif
143
144	static DdNode background, zero;
145
146	static long cuddRand = 0;
147	static long cuddRand2;
148	static long shuffleSelect;
149	static long shuffleTable[STAB_SIZE];
150
151	/---------------------------------------------------------------------------/
152	/* Macro declarations */
153	/---------------------------------------------------------------------------/
154
155	#define bang(f) ((Cudd_IsComplement(f)) ? '!' : ' ')
156
157	#ifdef __cplusplus
158	extern "C" {
159	#endif
160
161	/AutomaticStart***********************************************************/
162
163	/---------------------------------------------------------------------------/
164	/* Static function prototypes */
165	/---------------------------------------------------------------------------/
166
167	static int dp2 (DdManager dd, DdNode f, st_table *t);
168	static void ddPrintMintermAux (DdManager dd, DdNode node, int *list);
169	static int ddDagInt (DdNode *n);
170	static int cuddNodeArrayRecur (DdNode f, DdNodePtr table, int index);
171	static int cuddEstimateCofactor (DdManager dd, st_table table, DdNode * node, int i, int phase, DdNode ** ptr);
172	static DdNode * cuddUniqueLookup (DdManager * unique, int index, DdNode * T, DdNode * E);
173	static int cuddEstimateCofactorSimple (DdNode * node, int i);
174	static double ddCountMintermAux (DdNode node, double max, DdHashTable table);
175	static int ddEpdCountMintermAux (DdNode node, EpDouble max, EpDouble epd, st_table table);
176	static double ddCountPathAux (DdNode node, st_table table);
177	static double ddCountPathsToNonZero (DdNode * N, st_table * table);
178	static void ddSupportStep (DdNode f, int support);
179	static void ddClearFlag (DdNode *f);
180	static int ddLeavesInt (DdNode *n);
181	static int ddPickArbitraryMinterms (DdManager dd, DdNode node, int nvars, int nminterms, char **string);
182	static int ddPickRepresentativeCube (DdManager dd, DdNode node, double weight, char string);
183	static enum st_retval ddEpdFree (char * key, char * value, char * arg);
184
185	/AutomaticEnd*************************************************************/
186
187	#ifdef __cplusplus
188	}
189	#endif
190
191	/---------------------------------------------------------------------------/
192	/* Definition of exported functions */
193	/---------------------------------------------------------------------------/
194
195
196	/Function******************************************************************
197
198	Synopsis [Prints a disjoint sum of products.]
199
200	Description [Prints a disjoint sum of product cover for the function
201	rooted at node. Each product corresponds to a path from node to a
202	leaf node different from the logical zero, and different from the
203	background value. Uses the package default output file. Returns 1
204	if successful; 0 otherwise.]
205
206	SideEffects [None]
207
208	SeeAlso [Cudd_PrintDebug Cudd_bddPrintCover]
209
210	******************************************************************************/
211	int
212	Cudd_PrintMinterm(
213	DdManager * manager,
214	DdNode * node)
215	{
216	int i, *list;
217
218	background = manager->background;
219	zero = Cudd_Not(manager->one);
220	list = ALLOC(int,manager->size);
221	if (list == NULL) {
222	manager->errorCode = CUDD_MEMORY_OUT;
223	return(0);
224	}
225	for (i = 0; i < manager->size; i++) list[i] = 2;
226	ddPrintMintermAux(manager,node,list);
227	FREE(list);
228	return(1);
229
230	} /* end of Cudd_PrintMinterm */
231
232
233	/Function******************************************************************
234
235	Synopsis [Prints a sum of prime implicants of a BDD.]
236
237	Description [Prints a sum of product cover for an incompletely
238	specified function given by a lower bound and an upper bound. Each
239	product is a prime implicant obtained by expanding the product
240	corresponding to a path from node to the constant one. Uses the
241	package default output file. Returns 1 if successful; 0 otherwise.]
242
243	SideEffects [None]
244
245	SeeAlso [Cudd_PrintMinterm]
246
247	******************************************************************************/
248	int
249	Cudd_bddPrintCover(
250	DdManager *dd,
251	DdNode *l,
252	DdNode *u)
253	{
254	int *array;
255	int q, result;
256	DdNode *lb;
257	#ifdef DD_DEBUG
258	DdNode *cover;
259	#endif
260
261	array = ALLOC(int, Cudd_ReadSize(dd));
262	if (array == NULL) return(0);
263	lb = l;
264	cuddRef(lb);
265	#ifdef DD_DEBUG
266	cover = Cudd_ReadLogicZero(dd);
267	cuddRef(cover);
268	#endif
269	while (lb != Cudd_ReadLogicZero(dd)) {
270	DdNode implicant, prime, *tmp;
271	int length;
272	implicant = Cudd_LargestCube(dd,lb,&length);
273	if (implicant == NULL) {
274	Cudd_RecursiveDeref(dd,lb);
275	FREE(array);
276	return(0);
277	}
278	cuddRef(implicant);
279	prime = Cudd_bddMakePrime(dd,implicant,u);
280	if (prime == NULL) {
281	Cudd_RecursiveDeref(dd,lb);
282	Cudd_RecursiveDeref(dd,implicant);
283	FREE(array);
284	return(0);
285	}
286	cuddRef(prime);
287	Cudd_RecursiveDeref(dd,implicant);
288	tmp = Cudd_bddAnd(dd,lb,Cudd_Not(prime));
289	if (tmp == NULL) {
290	Cudd_RecursiveDeref(dd,lb);
291	Cudd_RecursiveDeref(dd,prime);
292	FREE(array);
293	return(0);
294	}
295	cuddRef(tmp);
296	Cudd_RecursiveDeref(dd,lb);
297	lb = tmp;
298	result = Cudd_BddToCubeArray(dd,prime,array);
299	if (result == 0) {
300	Cudd_RecursiveDeref(dd,lb);
301	Cudd_RecursiveDeref(dd,prime);
302	FREE(array);
303	return(0);
304	}
305	for (q = 0; q < dd->size; q++) {
306	switch (array[q]) {
307	case 0:
308	(void) fprintf(dd->out, "0");
309	break;
310	case 1:
311	(void) fprintf(dd->out, "1");
312	break;
313	case 2:
314	(void) fprintf(dd->out, "-");
315	break;
316	default:
317	(void) fprintf(dd->out, "?");
318	}
319	}
320	(void) fprintf(dd->out, " 1\n");
321	#ifdef DD_DEBUG
322	tmp = Cudd_bddOr(dd,prime,cover);
323	if (tmp == NULL) {
324	Cudd_RecursiveDeref(dd,cover);
325	Cudd_RecursiveDeref(dd,lb);
326	Cudd_RecursiveDeref(dd,prime);
327	FREE(array);
328	return(0);
329	}
330	cuddRef(tmp);
331	Cudd_RecursiveDeref(dd,cover);
332	cover = tmp;
333	#endif
334	Cudd_RecursiveDeref(dd,prime);
335	}
336	(void) fprintf(dd->out, "\n");
337	Cudd_RecursiveDeref(dd,lb);
338	FREE(array);
339	#ifdef DD_DEBUG
340	if (!Cudd_bddLeq(dd,cover,u) \|\| !Cudd_bddLeq(dd,l,cover)) {
341	Cudd_RecursiveDeref(dd,cover);
342	return(0);
343	}
344	Cudd_RecursiveDeref(dd,cover);
345	#endif
346	return(1);
347
348	} /* end of Cudd_bddPrintCover */
349
350
351	/Function******************************************************************
352
353	Synopsis [Prints to the standard output a DD and its statistics.]
354
355	Description [Prints to the standard output a DD and its statistics.
356	The statistics include the number of nodes, the number of leaves, and
357	the number of minterms. (The number of minterms is the number of
358	assignments to the variables that cause the function to be different
359	from the logical zero (for BDDs) and from the background value (for
360	ADDs.) The statistics are printed if pr > 0. Specifically:
361	<ul>
362	<li> pr = 0 : prints nothing
363	<li> pr = 1 : prints counts of nodes and minterms
364	<li> pr = 2 : prints counts + disjoint sum of product
365	<li> pr = 3 : prints counts + list of nodes
366	<li> pr > 3 : prints counts + disjoint sum of product + list of nodes
367	</ul>
368	For the purpose of counting the number of minterms, the function is
369	supposed to depend on n variables. Returns 1 if successful; 0 otherwise.]
370
371	SideEffects [None]
372
373	SeeAlso [Cudd_DagSize Cudd_CountLeaves Cudd_CountMinterm
374	Cudd_PrintMinterm]
375
376	******************************************************************************/
377	int
378	Cudd_PrintDebug(
379	DdManager * dd,
380	DdNode * f,
381	int n,
382	int pr)
383	{
384	DdNode azero, bzero;
385	int nodes;
386	int leaves;
387	double minterms;
388	int retval = 1;
389
390	if (f == NULL) {
391	(void) fprintf(dd->out,": is the NULL DD\n");
392	(void) fflush(dd->out);
393	return(0);
394	}
395	azero = DD_ZERO(dd);
396	bzero = Cudd_Not(DD_ONE(dd));
397	if ((f == azero \|\| f == bzero) && pr > 0){
398	(void) fprintf(dd->out,": is the zero DD\n");
399	(void) fflush(dd->out);
400	return(1);
401	}
402	if (pr > 0) {
403	nodes = Cudd_DagSize(f);
404	if (nodes == CUDD_OUT_OF_MEM) retval = 0;
405	leaves = Cudd_CountLeaves(f);
406	if (leaves == CUDD_OUT_OF_MEM) retval = 0;
407	minterms = Cudd_CountMinterm(dd, f, n);
408	if (minterms == (double)CUDD_OUT_OF_MEM) retval = 0;
409	(void) fprintf(dd->out,": %d nodes %d leaves %g minterms\n",
410	nodes, leaves, minterms);
411	if (pr > 2) {
412	if (!cuddP(dd, f)) retval = 0;
413	}
414	if (pr == 2 \|\| pr > 3) {
415	if (!Cudd_PrintMinterm(dd,f)) retval = 0;
416	(void) fprintf(dd->out,"\n");
417	}
418	(void) fflush(dd->out);
419	}
420	return(retval);
421
422	} /* end of Cudd_PrintDebug */
423
424
425	/Function******************************************************************
426
427	Synopsis [Counts the number of nodes in a DD.]
428
429	Description [Counts the number of nodes in a DD. Returns the number
430	of nodes in the graph rooted at node.]
431
432	SideEffects [None]
433
434	SeeAlso [Cudd_SharingSize Cudd_PrintDebug]
435
436	******************************************************************************/
437	int
438	Cudd_DagSize(
439	DdNode * node)
440	{
441	int i;
442
443	i = ddDagInt(Cudd_Regular(node));
444	ddClearFlag(Cudd_Regular(node));
445
446	return(i);
447
448	} /* end of Cudd_DagSize */
449
450
451	/Function******************************************************************
452
453	Synopsis [Estimates the number of nodes in a cofactor of a DD.]
454
455	Description [Estimates the number of nodes in a cofactor of a DD.
456	Returns an estimate of the number of nodes in a cofactor of
457	the graph rooted at node with respect to the variable whose index is i.
458	In case of failure, returns CUDD_OUT_OF_MEM.
459	This function uses a refinement of the algorithm of Cabodi et al.
460	(ICCAD96). The refinement allows the procedure to account for part
461	of the recombination that may occur in the part of the cofactor above
462	the cofactoring variable. This procedure does no create any new node.
463	It does keep a small table of results; therefore it may run out of memory.
464	If this is a concern, one should use Cudd_EstimateCofactorSimple, which
465	is faster, does not allocate any memory, but is less accurate.]
466
467	SideEffects [None]
468
469	SeeAlso [Cudd_DagSize Cudd_EstimateCofactorSimple]
470
471	******************************************************************************/
472	int
473	Cudd_EstimateCofactor(
474	DdManager dd / manager */,
475	DdNode * f /* function */,
476	int i /* index of variable */,
477	int phase /* 1: positive; 0: negative */
478	)
479	{
480	int val;
481	DdNode *ptr;
482	st_table *table;
483
484	table = st_init_table(st_ptrcmp,st_ptrhash);
485	if (table == NULL) return(CUDD_OUT_OF_MEM);
486	val = cuddEstimateCofactor(dd,table,Cudd_Regular(f),i,phase,&ptr);
487	ddClearFlag(Cudd_Regular(f));
488	st_free_table(table);
489
490	return(val);
491
492	} /* end of Cudd_EstimateCofactor */
493
494
495	/Function******************************************************************
496
497	Synopsis [Estimates the number of nodes in a cofactor of a DD.]
498
499	Description [Estimates the number of nodes in a cofactor of a DD.
500	Returns an estimate of the number of nodes in the positive cofactor of
501	the graph rooted at node with respect to the variable whose index is i.
502	This procedure implements with minor changes the algorithm of Cabodi et al.
503	(ICCAD96). It does not allocate any memory, it does not change the
504	state of the manager, and it is fast. However, it has been observed to
505	overestimate the size of the cofactor by as much as a factor of 2.]
506
507	SideEffects [None]
508
509	SeeAlso [Cudd_DagSize]
510
511	******************************************************************************/
512	int
513	Cudd_EstimateCofactorSimple(
514	DdNode * node,
515	int i)
516	{
517	int val;
518
519	val = cuddEstimateCofactorSimple(Cudd_Regular(node),i);
520	ddClearFlag(Cudd_Regular(node));
521
522	return(val);
523
524	} /* end of Cudd_EstimateCofactorSimple */
525
526
527	/Function******************************************************************
528
529	Synopsis [Counts the number of nodes in an array of DDs.]
530
531	Description [Counts the number of nodes in an array of DDs. Shared
532	nodes are counted only once. Returns the total number of nodes.]
533
534	SideEffects [None]
535
536	SeeAlso [Cudd_DagSize]
537
538	******************************************************************************/
539	int
540	Cudd_SharingSize(
541	DdNode ** nodeArray,
542	int n)
543	{
544	int i,j;
545
546	i = 0;
547	for (j = 0; j < n; j++) {
548	i += ddDagInt(Cudd_Regular(nodeArray[j]));
549	}
550	for (j = 0; j < n; j++) {
551	ddClearFlag(Cudd_Regular(nodeArray[j]));
552	}
553	return(i);
554
555	} /* end of Cudd_SharingSize */
556
557
558	/Function******************************************************************
559
560	Synopsis [Counts the number of minterms of a DD.]
561
562	Description [Counts the number of minterms of a DD. The function is
563	assumed to depend on nvars variables. The minterm count is
564	represented as a double, to allow for a larger number of variables.
565	Returns the number of minterms of the function rooted at node if
566	successful; (double) CUDD_OUT_OF_MEM otherwise.]
567
568	SideEffects [None]
569
570	SeeAlso [Cudd_PrintDebug Cudd_CountPath]
571
572	******************************************************************************/
573	double
574	Cudd_CountMinterm(
575	DdManager * manager,
576	DdNode * node,
577	int nvars)
578	{
579	double max;
580	DdHashTable *table;
581	double res;
582	CUDD_VALUE_TYPE epsilon;
583
584	background = manager->background;
585	zero = Cudd_Not(manager->one);
586
587	max = pow(2.0,(double)nvars);
588	table = cuddHashTableInit(manager,1,2);
589	if (table == NULL) {
590	return((double)CUDD_OUT_OF_MEM);
591	}
592	epsilon = Cudd_ReadEpsilon(manager);
593	Cudd_SetEpsilon(manager,(CUDD_VALUE_TYPE)0.0);
594	res = ddCountMintermAux(node,max,table);
595	cuddHashTableQuit(table);
596	Cudd_SetEpsilon(manager,epsilon);
597
598	return(res);
599
600	} /* end of Cudd_CountMinterm */
601
602
603	/Function******************************************************************
604
605	Synopsis [Counts the number of paths of a DD.]
606
607	Description [Counts the number of paths of a DD. Paths to all
608	terminal nodes are counted. The path count is represented as a
609	double, to allow for a larger number of variables. Returns the
610	number of paths of the function rooted at node if successful;
611	(double) CUDD_OUT_OF_MEM otherwise.]
612
613	SideEffects [None]
614
615	SeeAlso [Cudd_CountMinterm]
616
617	******************************************************************************/
618	double
619	Cudd_CountPath(
620	DdNode * node)
621	{
622
623	st_table *table;
624	double i;
625
626	table = st_init_table(st_ptrcmp,st_ptrhash);
627	if (table == NULL) {
628	return((double)CUDD_OUT_OF_MEM);
629	}
630	i = ddCountPathAux(Cudd_Regular(node),table);
631	st_foreach(table, cuddStCountfree, NULL);
632	st_free_table(table);
633	return(i);
634
635	} /* end of Cudd_CountPath */
636
637
638	/Function******************************************************************
639
640	Synopsis [Counts the number of minterms of a DD with extended precision.]
641
642	Description [Counts the number of minterms of a DD with extended precision.
643	The function is assumed to depend on nvars variables. The minterm count is
644	represented as an EpDouble, to allow any number of variables.
645	Returns 0 if successful; CUDD_OUT_OF_MEM otherwise.]
646
647	SideEffects [None]
648
649	SeeAlso [Cudd_PrintDebug Cudd_CountPath]
650
651	******************************************************************************/
652	int
653	Cudd_EpdCountMinterm(
654	DdManager * manager,
655	DdNode * node,
656	int nvars,
657	EpDouble * epd)
658	{
659	EpDouble max, tmp;
660	st_table *table;
661	int status;
662
663	background = manager->background;
664	zero = Cudd_Not(manager->one);
665
666	EpdPow2(nvars, &max);
667	table = st_init_table(EpdCmp, st_ptrhash);
668	if (table == NULL) {
669	EpdMakeZero(epd, 0);
670	return(CUDD_OUT_OF_MEM);
671	}
672	status = ddEpdCountMintermAux(Cudd_Regular(node),&max,epd,table);
673	st_foreach(table, ddEpdFree, NULL);
674	st_free_table(table);
675	if (status == CUDD_OUT_OF_MEM) {
676	EpdMakeZero(epd, 0);
677	return(CUDD_OUT_OF_MEM);
678	}
679	if (Cudd_IsComplement(node)) {
680	EpdSubtract3(&max, epd, &tmp);
681	EpdCopy(&tmp, epd);
682	}
683	return(0);
684
685	} /* end of Cudd_EpdCountMinterm */
686
687
688	/Function******************************************************************
689
690	Synopsis [Counts the number of paths to a non-zero terminal of a DD.]
691
692	Description [Counts the number of paths to a non-zero terminal of a
693	DD. The path count is
694	represented as a double, to allow for a larger number of variables.
695	Returns the number of paths of the function rooted at node.]
696
697	SideEffects [None]
698
699	SeeAlso [Cudd_CountMinterm Cudd_CountPath]
700
701	******************************************************************************/
702	double
703	Cudd_CountPathsToNonZero(
704	DdNode * node)
705	{
706
707	st_table *table;
708	double i;
709
710	table = st_init_table(st_ptrcmp,st_ptrhash);
711	if (table == NULL) {
712	return((double)CUDD_OUT_OF_MEM);
713	}
714	i = ddCountPathsToNonZero(node,table);
715	st_foreach(table, cuddStCountfree, NULL);
716	st_free_table(table);
717	return(i);
718
719	} /* end of Cudd_CountPathsToNonZero */
720
721
722	/Function******************************************************************
723
724	Synopsis [Finds the variables on which a DD depends.]
725
726	Description [Finds the variables on which a DD depends.
727	Returns a BDD consisting of the product of the variables if
728	successful; NULL otherwise.]
729
730	SideEffects [None]
731
732	SeeAlso [Cudd_VectorSupport Cudd_ClassifySupport]
733
734	******************************************************************************/
735	DdNode *
736	Cudd_Support(
737	DdManager * dd /* manager */,
738	DdNode * f /* DD whose support is sought */)
739	{
740	int *support;
741	DdNode res, tmp, *var;
742	int i,j;
743	int size;
744
745	/* Allocate and initialize support array for ddSupportStep. */
746	size = ddMax(dd->size, dd->sizeZ);
747	support = ALLOC(int,size);
748	if (support == NULL) {
749	dd->errorCode = CUDD_MEMORY_OUT;
750	return(NULL);
751	}
752	for (i = 0; i < size; i++) {
753	support[i] = 0;
754	}
755
756	/* Compute support and clean up markers. */
757	ddSupportStep(Cudd_Regular(f),support);
758	ddClearFlag(Cudd_Regular(f));
759
760	/* Transform support from array to cube. */
761	do {
762	dd->reordered = 0;
763	res = DD_ONE(dd);
764	cuddRef(res);
765	for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
766	i = (j >= dd->size) ? j : dd->invperm[j];
767	if (support[i] == 1) {
768	/* The following call to cuddUniqueInter is guaranteed
769	** not to trigger reordering because the node we look up
770	** already exists. */
771	var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
772	cuddRef(var);
773	tmp = cuddBddAndRecur(dd,res,var);
774	if (tmp == NULL) {
775	Cudd_RecursiveDeref(dd,res);
776	Cudd_RecursiveDeref(dd,var);
777	res = NULL;
778	break;
779	}
780	cuddRef(tmp);
781	Cudd_RecursiveDeref(dd,res);
782	Cudd_RecursiveDeref(dd,var);
783	res = tmp;
784	}
785	}
786	} while (dd->reordered == 1);
787
788	FREE(support);
789	if (res != NULL) cuddDeref(res);
790	return(res);
791
792	} /* end of Cudd_Support */
793
794
795	/Function******************************************************************
796
797	Synopsis [Finds the variables on which a DD depends.]
798
799	Description [Finds the variables on which a DD depends. Returns an
800	index array of the variables if successful; NULL otherwise. The
801	size of the array equals the number of variables in the manager.
802	Each entry of the array is 1 if the corresponding variable is in the
803	support of the DD and 0 otherwise.]
804
805	SideEffects [None]
806
807	SeeAlso [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport]
808
809	******************************************************************************/
810	int *
811	Cudd_SupportIndex(
812	DdManager * dd /* manager */,
813	DdNode * f /* DD whose support is sought */)
814	{
815	int *support;
816	int i;
817	int size;
818
819	/* Allocate and initialize support array for ddSupportStep. */
820	size = ddMax(dd->size, dd->sizeZ);
821	support = ALLOC(int,size);
822	if (support == NULL) {
823	dd->errorCode = CUDD_MEMORY_OUT;
824	return(NULL);
825	}
826	for (i = 0; i < size; i++) {
827	support[i] = 0;
828	}
829
830	/* Compute support and clean up markers. */
831	ddSupportStep(Cudd_Regular(f),support);
832	ddClearFlag(Cudd_Regular(f));
833
834	return(support);
835
836	} /* end of Cudd_SupportIndex */
837
838
839	/Function******************************************************************
840
841	Synopsis [Counts the variables on which a DD depends.]
842
843	Description [Counts the variables on which a DD depends.
844	Returns the number of the variables if successful; CUDD_OUT_OF_MEM
845	otherwise.]
846
847	SideEffects [None]
848
849	SeeAlso [Cudd_Support]
850
851	******************************************************************************/
852	int
853	Cudd_SupportSize(
854	DdManager * dd /* manager */,
855	DdNode * f /* DD whose support size is sought */)
856	{
857	int *support;
858	int i;
859	int size;
860	int count;
861
862	/* Allocate and initialize support array for ddSupportStep. */
863	size = ddMax(dd->size, dd->sizeZ);
864	support = ALLOC(int,size);
865	if (support == NULL) {
866	dd->errorCode = CUDD_MEMORY_OUT;
867	return(CUDD_OUT_OF_MEM);
868	}
869	for (i = 0; i < size; i++) {
870	support[i] = 0;
871	}
872
873	/* Compute support and clean up markers. */
874	ddSupportStep(Cudd_Regular(f),support);
875	ddClearFlag(Cudd_Regular(f));
876
877	/* Count support variables. */
878	count = 0;
879	for (i = 0; i < size; i++) {
880	if (support[i] == 1) count++;
881	}
882
883	FREE(support);
884	return(count);
885
886	} /* end of Cudd_SupportSize */
887
888
889	/Function******************************************************************
890
891	Synopsis [Finds the variables on which a set of DDs depends.]
892
893	Description [Finds the variables on which a set of DDs depends.
894	The set must contain either BDDs and ADDs, or ZDDs.
895	Returns a BDD consisting of the product of the variables if
896	successful; NULL otherwise.]
897
898	SideEffects [None]
899
900	SeeAlso [Cudd_Support Cudd_ClassifySupport]
901
902	******************************************************************************/
903	DdNode *
904	Cudd_VectorSupport(
905	DdManager * dd /* manager */,
906	DdNode ** F /* array of DDs whose support is sought */,
907	int n /* size of the array */)
908	{
909	int *support;
910	DdNode res, tmp, *var;
911	int i,j;
912	int size;
913
914	/* Allocate and initialize support array for ddSupportStep. */
915	size = ddMax(dd->size, dd->sizeZ);
916	support = ALLOC(int,size);
917	if (support == NULL) {
918	dd->errorCode = CUDD_MEMORY_OUT;
919	return(NULL);
920	}
921	for (i = 0; i < size; i++) {
922	support[i] = 0;
923	}
924
925	/* Compute support and clean up markers. */
926	for (i = 0; i < n; i++) {
927	ddSupportStep(Cudd_Regular(F[i]),support);
928	}
929	for (i = 0; i < n; i++) {
930	ddClearFlag(Cudd_Regular(F[i]));
931	}
932
933	/* Transform support from array to cube. */
934	res = DD_ONE(dd);
935	cuddRef(res);
936	for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
937	i = (j >= dd->size) ? j : dd->invperm[j];
938	if (support[i] == 1) {
939	var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
940	cuddRef(var);
941	tmp = Cudd_bddAnd(dd,res,var);
942	if (tmp == NULL) {
943	Cudd_RecursiveDeref(dd,res);
944	Cudd_RecursiveDeref(dd,var);
945	FREE(support);
946	return(NULL);
947	}
948	cuddRef(tmp);
949	Cudd_RecursiveDeref(dd,res);
950	Cudd_RecursiveDeref(dd,var);
951	res = tmp;
952	}
953	}
954
955	FREE(support);
956	cuddDeref(res);
957	return(res);
958
959	} /* end of Cudd_VectorSupport */
960
961
962	/Function******************************************************************
963
964	Synopsis [Finds the variables on which a set of DDs depends.]
965
966	Description [Finds the variables on which a set of DDs depends.
967	The set must contain either BDDs and ADDs, or ZDDs.
968	Returns an index array of the variables if successful; NULL otherwise.]
969
970	SideEffects [None]
971
972	SeeAlso [Cudd_SupportIndex Cudd_VectorSupport Cudd_ClassifySupport]
973
974	******************************************************************************/
975	int *
976	Cudd_VectorSupportIndex(
977	DdManager * dd /* manager */,
978	DdNode ** F /* array of DDs whose support is sought */,
979	int n /* size of the array */)
980	{
981	int *support;
982	int i;
983	int size;
984
985	/* Allocate and initialize support array for ddSupportStep. */
986	size = ddMax(dd->size, dd->sizeZ);
987	support = ALLOC(int,size);
988	if (support == NULL) {
989	dd->errorCode = CUDD_MEMORY_OUT;
990	return(NULL);
991	}
992	for (i = 0; i < size; i++) {
993	support[i] = 0;
994	}
995
996	/* Compute support and clean up markers. */
997	for (i = 0; i < n; i++) {
998	ddSupportStep(Cudd_Regular(F[i]),support);
999	}
1000	for (i = 0; i < n; i++) {
1001	ddClearFlag(Cudd_Regular(F[i]));
1002	}
1003
1004	return(support);
1005
1006	} /* end of Cudd_VectorSupportIndex */
1007
1008
1009	/Function******************************************************************
1010
1011	Synopsis [Counts the variables on which a set of DDs depends.]
1012
1013	Description [Counts the variables on which a set of DDs depends.
1014	The set must contain either BDDs and ADDs, or ZDDs.
1015	Returns the number of the variables if successful; CUDD_OUT_OF_MEM
1016	otherwise.]
1017
1018	SideEffects [None]
1019
1020	SeeAlso [Cudd_VectorSupport Cudd_SupportSize]
1021
1022	******************************************************************************/
1023	int
1024	Cudd_VectorSupportSize(
1025	DdManager * dd /* manager */,
1026	DdNode ** F /* array of DDs whose support is sought */,
1027	int n /* size of the array */)
1028	{
1029	int *support;
1030	int i;
1031	int size;
1032	int count;
1033
1034	/* Allocate and initialize support array for ddSupportStep. */
1035	size = ddMax(dd->size, dd->sizeZ);
1036	support = ALLOC(int,size);
1037	if (support == NULL) {
1038	dd->errorCode = CUDD_MEMORY_OUT;
1039	return(CUDD_OUT_OF_MEM);
1040	}
1041	for (i = 0; i < size; i++) {
1042	support[i] = 0;
1043	}
1044
1045	/* Compute support and clean up markers. */
1046	for (i = 0; i < n; i++) {
1047	ddSupportStep(Cudd_Regular(F[i]),support);
1048	}
1049	for (i = 0; i < n; i++) {
1050	ddClearFlag(Cudd_Regular(F[i]));
1051	}
1052
1053	/* Count vriables in support. */
1054	count = 0;
1055	for (i = 0; i < size; i++) {
1056	if (support[i] == 1) count++;
1057	}
1058
1059	FREE(support);
1060	return(count);
1061
1062	} /* end of Cudd_VectorSupportSize */
1063
1064
1065	/Function******************************************************************
1066
1067	Synopsis [Classifies the variables in the support of two DDs.]
1068
1069	Description [Classifies the variables in the support of two DDs
1070	<code>f</code> and <code>g</code>, depending on whther they appear
1071	in both DDs, only in <code>f</code>, or only in <code>g</code>.
1072	Returns 1 if successful; 0 otherwise.]
1073
1074	SideEffects [The cubes of the three classes of variables are
1075	returned as side effects.]
1076
1077	SeeAlso [Cudd_Support Cudd_VectorSupport]
1078
1079	******************************************************************************/
1080	int
1081	Cudd_ClassifySupport(
1082	DdManager * dd /* manager */,
1083	DdNode * f /* first DD */,
1084	DdNode * g /* second DD */,
1085	DdNode ** common /* cube of shared variables */,
1086	DdNode ** onlyF /* cube of variables only in f */,
1087	DdNode ** onlyG /* cube of variables only in g */)
1088	{
1089	int supportF, supportG;
1090	DdNode tmp, var;
1091	int i,j;
1092	int size;
1093
1094	/* Allocate and initialize support arrays for ddSupportStep. */
1095	size = ddMax(dd->size, dd->sizeZ);
1096	supportF = ALLOC(int,size);
1097	if (supportF == NULL) {
1098	dd->errorCode = CUDD_MEMORY_OUT;
1099	return(0);
1100	}
1101	supportG = ALLOC(int,size);
1102	if (supportG == NULL) {
1103	dd->errorCode = CUDD_MEMORY_OUT;
1104	FREE(supportF);
1105	return(0);
1106	}
1107	for (i = 0; i < size; i++) {
1108	supportF[i] = 0;
1109	supportG[i] = 0;
1110	}
1111
1112	/* Compute supports and clean up markers. */
1113	ddSupportStep(Cudd_Regular(f),supportF);
1114	ddClearFlag(Cudd_Regular(f));
1115	ddSupportStep(Cudd_Regular(g),supportG);
1116	ddClearFlag(Cudd_Regular(g));
1117
1118	/* Classify variables and create cubes. */
1119	common = onlyF = *onlyG = DD_ONE(dd);
1120	cuddRef(common); cuddRef(onlyF); cuddRef(*onlyG);
1121	for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
1122	i = (j >= dd->size) ? j : dd->invperm[j];
1123	if (supportF[i] == 0 && supportG[i] == 0) continue;
1124	var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
1125	cuddRef(var);
1126	if (supportG[i] == 0) {
1127	tmp = Cudd_bddAnd(dd,*onlyF,var);
1128	if (tmp == NULL) {
1129	Cudd_RecursiveDeref(dd,*common);
1130	Cudd_RecursiveDeref(dd,*onlyF);
1131	Cudd_RecursiveDeref(dd,*onlyG);
1132	Cudd_RecursiveDeref(dd,var);
1133	FREE(supportF); FREE(supportG);
1134	return(0);
1135	}
1136	cuddRef(tmp);
1137	Cudd_RecursiveDeref(dd,*onlyF);
1138	*onlyF = tmp;
1139	} else if (supportF[i] == 0) {
1140	tmp = Cudd_bddAnd(dd,*onlyG,var);
1141	if (tmp == NULL) {
1142	Cudd_RecursiveDeref(dd,*common);
1143	Cudd_RecursiveDeref(dd,*onlyF);
1144	Cudd_RecursiveDeref(dd,*onlyG);
1145	Cudd_RecursiveDeref(dd,var);
1146	FREE(supportF); FREE(supportG);
1147	return(0);
1148	}
1149	cuddRef(tmp);
1150	Cudd_RecursiveDeref(dd,*onlyG);
1151	*onlyG = tmp;
1152	} else {
1153	tmp = Cudd_bddAnd(dd,*common,var);
1154	if (tmp == NULL) {
1155	Cudd_RecursiveDeref(dd,*common);
1156	Cudd_RecursiveDeref(dd,*onlyF);
1157	Cudd_RecursiveDeref(dd,*onlyG);
1158	Cudd_RecursiveDeref(dd,var);
1159	FREE(supportF); FREE(supportG);
1160	return(0);
1161	}
1162	cuddRef(tmp);
1163	Cudd_RecursiveDeref(dd,*common);
1164	*common = tmp;
1165	}
1166	Cudd_RecursiveDeref(dd,var);
1167	}
1168
1169	FREE(supportF); FREE(supportG);
1170	cuddDeref(common); cuddDeref(onlyF); cuddDeref(*onlyG);
1171	return(1);
1172
1173	} /* end of Cudd_ClassifySupport */
1174
1175
1176	/Function******************************************************************
1177
1178	Synopsis [Counts the number of leaves in a DD.]
1179
1180	Description [Counts the number of leaves in a DD. Returns the number
1181	of leaves in the DD rooted at node if successful; CUDD_OUT_OF_MEM
1182	otherwise.]
1183
1184	SideEffects [None]
1185
1186	SeeAlso [Cudd_PrintDebug]
1187
1188	******************************************************************************/
1189	int
1190	Cudd_CountLeaves(
1191	DdNode * node)
1192	{
1193	int i;
1194
1195	i = ddLeavesInt(Cudd_Regular(node));
1196	ddClearFlag(Cudd_Regular(node));
1197	return(i);
1198
1199	} /* end of Cudd_CountLeaves */
1200
1201
1202	/Function******************************************************************
1203
1204	Synopsis [Picks one on-set cube randomly from the given DD.]
1205
1206	Description [Picks one on-set cube randomly from the given DD. The
1207	cube is written into an array of characters. The array must have at
1208	least as many entries as there are variables. Returns 1 if
1209	successful; 0 otherwise.]
1210
1211	SideEffects [None]
1212
1213	SeeAlso [Cudd_bddPickOneMinterm]
1214
1215	******************************************************************************/
1216	int
1217	Cudd_bddPickOneCube(
1218	DdManager * ddm,
1219	DdNode * node,
1220	char * string)
1221	{
1222	DdNode N, T, *E;
1223	DdNode one, bzero;
1224	char dir;
1225	int i;
1226
1227	if (string == NULL \|\| node == NULL) return(0);
1228
1229	/* The constant 0 function has no on-set cubes. */
1230	one = DD_ONE(ddm);
1231	bzero = Cudd_Not(one);
1232	if (node == bzero) return(0);
1233
1234	for (i = 0; i < ddm->size; i++) string[i] = 2;
1235
1236	for (;;) {
1237
1238	if (node == one) break;
1239
1240	N = Cudd_Regular(node);
1241
1242	T = cuddT(N); E = cuddE(N);
1243	if (Cudd_IsComplement(node)) {
1244	T = Cudd_Not(T); E = Cudd_Not(E);
1245	}
1246	if (T == bzero) {
1247	string[N->index] = 0;
1248	node = E;
1249	} else if (E == bzero) {
1250	string[N->index] = 1;
1251	node = T;
1252	} else {
1253	dir = (char) ((Cudd_Random() & 0x2000) >> 13);
1254	string[N->index] = dir;
1255	node = dir ? T : E;
1256	}
1257	}
1258	return(1);
1259
1260	} /* end of Cudd_bddPickOneCube */
1261
1262
1263	/Function******************************************************************
1264
1265	Synopsis [Picks one on-set minterm randomly from the given DD.]
1266
1267	Description [Picks one on-set minterm randomly from the given
1268	DD. The minterm is in terms of <code>vars</code>. The array
1269	<code>vars</code> should contain at least all variables in the
1270	support of <code>f</code>; if this condition is not met the minterm
1271	built by this procedure may not be contained in
1272	<code>f</code>. Builds a BDD for the minterm and returns a pointer
1273	to it if successful; NULL otherwise. There are three reasons why the
1274	procedure may fail:
1275	<ul>
1276	<li> It may run out of memory;
1277	<li> the function <code>f</code> may be the constant 0;
1278	<li> the minterm may not be contained in <code>f</code>.
1279	</ul>]
1280
1281	SideEffects [None]
1282
1283	SeeAlso [Cudd_bddPickOneCube]
1284
1285	******************************************************************************/
1286	DdNode *
1287	Cudd_bddPickOneMinterm(
1288	DdManager * dd /* manager */,
1289	DdNode * f /* function from which to pick one minterm */,
1290	DdNode ** vars /* array of variables */,
1291	int n /* size of <code>vars</code> */)
1292	{
1293	char *string;
1294	int i, size;
1295	int *indices;
1296	int result;
1297	DdNode old, neW;
1298
1299	size = dd->size;
1300	string = ALLOC(char, size);
1301	if (string == NULL) {
1302	dd->errorCode = CUDD_MEMORY_OUT;
1303	return(NULL);
1304	}
1305	indices = ALLOC(int,n);
1306	if (indices == NULL) {
1307	dd->errorCode = CUDD_MEMORY_OUT;
1308	FREE(string);
1309	return(NULL);
1310	}
1311
1312	for (i = 0; i < n; i++) {
1313	indices[i] = vars[i]->index;
1314	}
1315
1316	result = Cudd_bddPickOneCube(dd,f,string);
1317	if (result == 0) {
1318	FREE(string);
1319	FREE(indices);
1320	return(NULL);
1321	}
1322
1323	/* Randomize choice for don't cares. */
1324	for (i = 0; i < n; i++) {
1325	if (string[indices[i]] == 2)
1326	string[indices[i]] = (char) ((Cudd_Random() & 0x20) >> 5);
1327	}
1328
1329	/* Build result BDD. */
1330	old = Cudd_ReadOne(dd);
1331	cuddRef(old);
1332
1333	for (i = n-1; i >= 0; i--) {
1334	neW = Cudd_bddAnd(dd,old,Cudd_NotCond(vars[i],string[indices[i]]==0));
1335	if (neW == NULL) {
1336	FREE(string);
1337	FREE(indices);
1338	Cudd_RecursiveDeref(dd,old);
1339	return(NULL);
1340	}
1341	cuddRef(neW);
1342	Cudd_RecursiveDeref(dd,old);
1343	old = neW;
1344	}
1345
1346	#ifdef DD_DEBUG
1347	/* Test. */
1348	if (Cudd_bddLeq(dd,old,f)) {
1349	cuddDeref(old);
1350	} else {
1351	Cudd_RecursiveDeref(dd,old);
1352	old = NULL;
1353	}
1354	#else
1355	cuddDeref(old);
1356	#endif
1357
1358	FREE(string);
1359	FREE(indices);
1360	return(old);
1361
1362	} /* end of Cudd_bddPickOneMinterm */
1363
1364
1365	/Function******************************************************************
1366
1367	Synopsis [Picks k on-set minterms evenly distributed from given DD.]
1368
1369	Description [Picks k on-set minterms evenly distributed from given DD.
1370	The minterms are in terms of <code>vars</code>. The array
1371	<code>vars</code> should contain at least all variables in the
1372	support of <code>f</code>; if this condition is not met the minterms
1373	built by this procedure may not be contained in
1374	<code>f</code>. Builds an array of BDDs for the minterms and returns a
1375	pointer to it if successful; NULL otherwise. There are three reasons
1376	why the procedure may fail:
1377	<ul>
1378	<li> It may run out of memory;
1379	<li> the function <code>f</code> may be the constant 0;
1380	<li> the minterms may not be contained in <code>f</code>.
1381	</ul>]
1382
1383	SideEffects [None]
1384
1385	SeeAlso [Cudd_bddPickOneMinterm Cudd_bddPickOneCube]
1386
1387	******************************************************************************/
1388	DdNode **
1389	Cudd_bddPickArbitraryMinterms(
1390	DdManager * dd /* manager */,
1391	DdNode * f /* function from which to pick k minterms */,
1392	DdNode ** vars /* array of variables */,
1393	int n /* size of <code>vars</code> */,
1394	int k /* number of minterms to find */)
1395	{
1396	char **string;
1397	int i, j, l, size;
1398	int *indices;
1399	int result;
1400	DdNode *old, neW;
1401	double minterms;
1402	char *saveString;
1403	int saveFlag, savePoint, isSame;
1404
1405	minterms = Cudd_CountMinterm(dd,f,n);
1406	if ((double)k > minterms) {
1407	return(NULL);
1408	}
1409
1410	size = dd->size;
1411	string = ALLOC(char *, k);
1412	if (string == NULL) {
1413	dd->errorCode = CUDD_MEMORY_OUT;
1414	return(NULL);
1415	}
1416	for (i = 0; i < k; i++) {
1417	string[i] = ALLOC(char, size + 1);
1418	if (string[i] == NULL) {
1419	for (j = 0; j < i; j++)
1420	FREE(string[i]);
1421	FREE(string);
1422	dd->errorCode = CUDD_MEMORY_OUT;
1423	return(NULL);
1424	}
1425	for (j = 0; j < size; j++) string[i][j] = '2';
1426	string[i][size] = '\0';
1427	}
1428	indices = ALLOC(int,n);
1429	if (indices == NULL) {
1430	dd->errorCode = CUDD_MEMORY_OUT;
1431	for (i = 0; i < k; i++)
1432	FREE(string[i]);
1433	FREE(string);
1434	return(NULL);
1435	}
1436
1437	for (i = 0; i < n; i++) {
1438	indices[i] = vars[i]->index;
1439	}
1440
1441	result = ddPickArbitraryMinterms(dd,f,n,k,string);
1442	if (result == 0) {
1443	for (i = 0; i < k; i++)
1444	FREE(string[i]);
1445	FREE(string);
1446	FREE(indices);
1447	return(NULL);
1448	}
1449
1450	old = ALLOC(DdNode *, k);
1451	if (old == NULL) {
1452	dd->errorCode = CUDD_MEMORY_OUT;
1453	for (i = 0; i < k; i++)
1454	FREE(string[i]);
1455	FREE(string);
1456	FREE(indices);
1457	return(NULL);
1458	}
1459	saveString = ALLOC(char, size + 1);
1460	if (saveString == NULL) {
1461	dd->errorCode = CUDD_MEMORY_OUT;
1462	for (i = 0; i < k; i++)
1463	FREE(string[i]);
1464	FREE(string);
1465	FREE(indices);
1466	FREE(old);
1467	return(NULL);
1468	}
1469	saveFlag = 0;
1470
1471	/* Build result BDD array. */
1472	for (i = 0; i < k; i++) {
1473	isSame = 0;
1474	if (!saveFlag) {
1475	for (j = i + 1; j < k; j++) {
1476	if (strcmp(string[i], string[j]) == 0) {
1477	savePoint = i;
1478	strcpy(saveString, string[i]);
1479	saveFlag = 1;
1480	break;
1481	}
1482	}
1483	} else {
1484	if (strcmp(string[i], saveString) == 0) {
1485	isSame = 1;
1486	} else {
1487	saveFlag = 0;
1488	for (j = i + 1; j < k; j++) {
1489	if (strcmp(string[i], string[j]) == 0) {
1490	savePoint = i;
1491	strcpy(saveString, string[i]);
1492	saveFlag = 1;
1493	break;
1494	}
1495	}
1496	}
1497	}
1498	/* Randomize choice for don't cares. */
1499	for (j = 0; j < n; j++) {
1500	if (string[i][indices[j]] == '2')
1501	string[i][indices[j]] =
1502	(char) ((Cudd_Random() & 0x20) ? '1' : '0');
1503	}
1504
1505	while (isSame) {
1506	isSame = 0;
1507	for (j = savePoint; j < i; j++) {
1508	if (strcmp(string[i], string[j]) == 0) {
1509	isSame = 1;
1510	break;
1511	}
1512	}
1513	if (isSame) {
1514	strcpy(string[i], saveString);
1515	/* Randomize choice for don't cares. */
1516	for (j = 0; j < n; j++) {
1517	if (string[i][indices[j]] == '2')
1518	string[i][indices[j]] =
1519	(char) ((Cudd_Random() & 0x20) ? '1' : '0');
1520	}
1521	}
1522	}
1523
1524	old[i] = Cudd_ReadOne(dd);
1525	cuddRef(old[i]);
1526
1527	for (j = 0; j < n; j++) {
1528	if (string[i][indices[j]] == '0') {
1529	neW = Cudd_bddAnd(dd,old[i],Cudd_Not(vars[j]));
1530	} else {
1531	neW = Cudd_bddAnd(dd,old[i],vars[j]);
1532	}
1533	if (neW == NULL) {
1534	FREE(saveString);
1535	for (l = 0; l < k; l++)
1536	FREE(string[l]);
1537	FREE(string);
1538	FREE(indices);
1539	for (l = 0; l <= i; l++)
1540	Cudd_RecursiveDeref(dd,old[l]);
1541	FREE(old);
1542	return(NULL);
1543	}
1544	cuddRef(neW);
1545	Cudd_RecursiveDeref(dd,old[i]);
1546	old[i] = neW;
1547	}
1548
1549	/* Test. */
1550	if (!Cudd_bddLeq(dd,old[i],f)) {
1551	FREE(saveString);
1552	for (l = 0; l < k; l++)
1553	FREE(string[l]);
1554	FREE(string);
1555	FREE(indices);
1556	for (l = 0; l <= i; l++)
1557	Cudd_RecursiveDeref(dd,old[l]);
1558	FREE(old);
1559	return(NULL);
1560	}
1561	}
1562
1563	FREE(saveString);
1564	for (i = 0; i < k; i++) {
1565	cuddDeref(old[i]);
1566	FREE(string[i]);
1567	}
1568	FREE(string);
1569	FREE(indices);
1570	return(old);
1571
1572	} /* end of Cudd_bddPickArbitraryMinterms */
1573
1574
1575	/Function******************************************************************
1576
1577	Synopsis [Extracts a subset from a BDD.]
1578
1579	Description [Extracts a subset from a BDD in the following procedure.
1580	1. Compute the weight for each mask variable by counting the number of
1581	minterms for both positive and negative cofactors of the BDD with
1582	respect to each mask variable. (weight = #positive - #negative)
1583	2. Find a representative cube of the BDD by using the weight. From the
1584	top variable of the BDD, for each variable, if the weight is greater
1585	than 0.0, choose THEN branch, othereise ELSE branch, until meeting
1586	the constant 1.
1587	3. Quantify out the variables not in maskVars from the representative
1588	cube and if a variable in maskVars is don't care, replace the
1589	variable with a constant(1 or 0) depending on the weight.
1590	4. Make a subset of the BDD by multiplying with the modified cube.]
1591
1592	SideEffects [None]
1593
1594	SeeAlso []
1595
1596	******************************************************************************/
1597	DdNode *
1598	Cudd_SubsetWithMaskVars(
1599	DdManager * dd /* manager */,
1600	DdNode * f /* function from which to pick a cube */,
1601	DdNode ** vars /* array of variables */,
1602	int nvars /* size of <code>vars</code> */,
1603	DdNode ** maskVars /* array of variables */,
1604	int mvars /* size of <code>maskVars</code> */)
1605	{
1606	double *weight;
1607	char *string;
1608	int i, size;
1609	int indices, mask;
1610	int result;
1611	DdNode zero, cube, newCube, subset;
1612	DdNode *cof;
1613
1614	DdNode *support;
1615	support = Cudd_Support(dd,f);
1616	cuddRef(support);
1617	Cudd_RecursiveDeref(dd,support);
1618
1619	zero = Cudd_Not(dd->one);
1620	size = dd->size;
1621
1622	weight = ALLOC(double,size);
1623	if (weight == NULL) {
1624	dd->errorCode = CUDD_MEMORY_OUT;
1625	return(NULL);
1626	}
1627	for (i = 0; i < size; i++) {
1628	weight[i] = 0.0;
1629	}
1630	for (i = 0; i < mvars; i++) {
1631	cof = Cudd_Cofactor(dd, f, maskVars[i]);
1632	cuddRef(cof);
1633	weight[i] = Cudd_CountMinterm(dd, cof, nvars);
1634	Cudd_RecursiveDeref(dd,cof);
1635
1636	cof = Cudd_Cofactor(dd, f, Cudd_Not(maskVars[i]));
1637	cuddRef(cof);
1638	weight[i] -= Cudd_CountMinterm(dd, cof, nvars);
1639	Cudd_RecursiveDeref(dd,cof);
1640	}
1641
1642	string = ALLOC(char, size + 1);
1643	if (string == NULL) {
1644	dd->errorCode = CUDD_MEMORY_OUT;
1645	FREE(weight);
1646	return(NULL);
1647	}
1648	mask = ALLOC(int, size);
1649	if (mask == NULL) {
1650	dd->errorCode = CUDD_MEMORY_OUT;
1651	FREE(weight);
1652	FREE(string);
1653	return(NULL);
1654	}
1655	for (i = 0; i < size; i++) {
1656	string[i] = '2';
1657	mask[i] = 0;
1658	}
1659	string[size] = '\0';
1660	indices = ALLOC(int,nvars);
1661	if (indices == NULL) {
1662	dd->errorCode = CUDD_MEMORY_OUT;
1663	FREE(weight);
1664	FREE(string);
1665	FREE(mask);
1666	return(NULL);
1667	}
1668	for (i = 0; i < nvars; i++) {
1669	indices[i] = vars[i]->index;
1670	}
1671
1672	result = ddPickRepresentativeCube(dd,f,weight,string);
1673	if (result == 0) {
1674	FREE(weight);
1675	FREE(string);
1676	FREE(mask);
1677	FREE(indices);
1678	return(NULL);
1679	}
1680
1681	cube = Cudd_ReadOne(dd);
1682	cuddRef(cube);
1683	zero = Cudd_Not(Cudd_ReadOne(dd));
1684	for (i = 0; i < nvars; i++) {
1685	if (string[indices[i]] == '0') {
1686	newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
1687	} else if (string[indices[i]] == '1') {
1688	newCube = Cudd_bddIte(dd,cube,vars[i],zero);
1689	} else
1690	continue;
1691	if (newCube == NULL) {
1692	FREE(weight);
1693	FREE(string);
1694	FREE(mask);
1695	FREE(indices);
1696	Cudd_RecursiveDeref(dd,cube);
1697	return(NULL);
1698	}
1699	cuddRef(newCube);
1700	Cudd_RecursiveDeref(dd,cube);
1701	cube = newCube;
1702	}
1703	Cudd_RecursiveDeref(dd,cube);
1704
1705	for (i = 0; i < mvars; i++) {
1706	mask[maskVars[i]->index] = 1;
1707	}
1708	for (i = 0; i < nvars; i++) {
1709	if (mask[indices[i]]) {
1710	if (string[indices[i]] == '2') {
1711	if (weight[indices[i]] >= 0.0)
1712	string[indices[i]] = '1';
1713	else
1714	string[indices[i]] = '0';
1715	}
1716	} else {
1717	string[indices[i]] = '2';
1718	}
1719	}
1720
1721	cube = Cudd_ReadOne(dd);
1722	cuddRef(cube);
1723	zero = Cudd_Not(Cudd_ReadOne(dd));
1724
1725	/* Build result BDD. */
1726	for (i = 0; i < nvars; i++) {
1727	if (string[indices[i]] == '0') {
1728	newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
1729	} else if (string[indices[i]] == '1') {
1730	newCube = Cudd_bddIte(dd,cube,vars[i],zero);
1731	} else
1732	continue;
1733	if (newCube == NULL) {
1734	FREE(weight);
1735	FREE(string);
1736	FREE(mask);
1737	FREE(indices);
1738	Cudd_RecursiveDeref(dd,cube);
1739	return(NULL);
1740	}
1741	cuddRef(newCube);
1742	Cudd_RecursiveDeref(dd,cube);
1743	cube = newCube;
1744	}
1745
1746	subset = Cudd_bddAnd(dd,f,cube);
1747	cuddRef(subset);
1748	Cudd_RecursiveDeref(dd,cube);
1749
1750	/* Test. */
1751	if (Cudd_bddLeq(dd,subset,f)) {
1752	cuddDeref(subset);
1753	} else {
1754	Cudd_RecursiveDeref(dd,subset);
1755	subset = NULL;
1756	}
1757
1758	FREE(weight);
1759	FREE(string);
1760	FREE(mask);
1761	FREE(indices);
1762	return(subset);
1763
1764	} /* end of Cudd_SubsetWithMaskVars */
1765
1766
1767	/Function******************************************************************
1768
1769	Synopsis [Finds the first cube of a decision diagram.]
1770
1771	Description [Defines an iterator on the onset of a decision diagram
1772	and finds its first cube. Returns a generator that contains the
1773	information necessary to continue the enumeration if successful; NULL
1774	otherwise.<p>
1775	A cube is represented as an array of literals, which are integers in
1776	{0, 1, 2}; 0 represents a complemented literal, 1 represents an
1777	uncomplemented literal, and 2 stands for don't care. The enumeration
1778	produces a disjoint cover of the function associated with the diagram.
1779	The size of the array equals the number of variables in the manager at
1780	the time Cudd_FirstCube is called.<p>
1781	For each cube, a value is also returned. This value is always 1 for a
1782	BDD, while it may be different from 1 for an ADD.
1783	For BDDs, the offset is the set of cubes whose value is the logical zero.
1784	For ADDs, the offset is the set of cubes whose value is the
1785	background value. The cubes of the offset are not enumerated.]
1786
1787	SideEffects [The first cube and its value are returned as side effects.]
1788
1789	SeeAlso [Cudd_ForeachCube Cudd_NextCube Cudd_GenFree Cudd_IsGenEmpty
1790	Cudd_FirstNode]
1791
1792	******************************************************************************/
1793	DdGen *
1794	Cudd_FirstCube(
1795	DdManager * dd,
1796	DdNode * f,
1797	int ** cube,
1798	CUDD_VALUE_TYPE * value)
1799	{
1800	DdGen *gen;
1801	DdNode top, treg, next, nreg, prev, preg;
1802	int i;
1803	int nvars;
1804
1805	/* Sanity Check. */
1806	if (dd == NULL \|\| f == NULL) return(NULL);
1807
1808	/* Allocate generator an initialize it. */
1809	gen = ALLOC(DdGen,1);
1810	if (gen == NULL) {
1811	dd->errorCode = CUDD_MEMORY_OUT;
1812	return(NULL);
1813	}
1814
1815	gen->manager = dd;
1816	gen->type = CUDD_GEN_CUBES;
1817	gen->status = CUDD_GEN_EMPTY;
1818	gen->gen.cubes.cube = NULL;
1819	gen->gen.cubes.value = DD_ZERO_VAL;
1820	gen->stack.sp = 0;
1821	gen->stack.stack = NULL;
1822	gen->node = NULL;
1823
1824	nvars = dd->size;
1825	gen->gen.cubes.cube = ALLOC(int,nvars);
1826	if (gen->gen.cubes.cube == NULL) {
1827	dd->errorCode = CUDD_MEMORY_OUT;
1828	FREE(gen);
1829	return(NULL);
1830	}
1831	for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;
1832
1833	/* The maximum stack depth is one plus the number of variables.
1834	** because a path may have nodes at all levels, including the
1835	** constant level.
1836	*/
1837	gen->stack.stack = ALLOC(DdNodePtr, nvars+1);
1838	if (gen->stack.stack == NULL) {
1839	dd->errorCode = CUDD_MEMORY_OUT;
1840	FREE(gen->gen.cubes.cube);
1841	FREE(gen);
1842	return(NULL);
1843	}
1844	for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;
1845
1846	/* Find the first cube of the onset. */
1847	gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++;
1848
1849	while (1) {
1850	top = gen->stack.stack[gen->stack.sp-1];
1851	treg = Cudd_Regular(top);
1852	if (!cuddIsConstant(treg)) {
1853	/* Take the else branch first. */
1854	gen->gen.cubes.cube[treg->index] = 0;
1855	next = cuddE(treg);
1856	if (top != treg) next = Cudd_Not(next);
1857	gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
1858	} else if (top == Cudd_Not(DD_ONE(dd)) \|\| top == dd->background) {
1859	/* Backtrack */
1860	while (1) {
1861	if (gen->stack.sp == 1) {
1862	/* The current node has no predecessor. */
1863	gen->status = CUDD_GEN_EMPTY;
1864	gen->stack.sp--;
1865	goto done;
1866	}
1867	prev = gen->stack.stack[gen->stack.sp-2];
1868	preg = Cudd_Regular(prev);
1869	nreg = cuddT(preg);
1870	if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
1871	if (next != top) { /* follow the then branch next */
1872	gen->gen.cubes.cube[preg->index] = 1;
1873	gen->stack.stack[gen->stack.sp-1] = next;
1874	break;
1875	}
1876	/* Pop the stack and try again. */
1877	gen->gen.cubes.cube[preg->index] = 2;
1878	gen->stack.sp--;
1879	top = gen->stack.stack[gen->stack.sp-1];
1880	treg = Cudd_Regular(top);
1881	}
1882	} else {
1883	gen->status = CUDD_GEN_NONEMPTY;
1884	gen->gen.cubes.value = cuddV(top);
1885	goto done;
1886	}
1887	}
1888
1889	done:
1890	*cube = gen->gen.cubes.cube;
1891	*value = gen->gen.cubes.value;
1892	return(gen);
1893
1894	} /* end of Cudd_FirstCube */
1895
1896
1897	/Function******************************************************************
1898
1899	Synopsis [Generates the next cube of a decision diagram onset.]
1900
1901	Description [Generates the next cube of a decision diagram onset,
1902	using generator gen. Returns 0 if the enumeration is completed; 1
1903	otherwise.]
1904
1905	SideEffects [The cube and its value are returned as side effects. The
1906	generator is modified.]
1907
1908	SeeAlso [Cudd_ForeachCube Cudd_FirstCube Cudd_GenFree Cudd_IsGenEmpty
1909	Cudd_NextNode]
1910
1911	******************************************************************************/
1912	int
1913	Cudd_NextCube(
1914	DdGen * gen,
1915	int ** cube,
1916	CUDD_VALUE_TYPE * value)
1917	{
1918	DdNode top, treg, next, nreg, prev, preg;
1919	DdManager *dd = gen->manager;
1920
1921	/* Backtrack from previously reached terminal node. */
1922	while (1) {
1923	if (gen->stack.sp == 1) {
1924	/* The current node has no predecessor. */
1925	gen->status = CUDD_GEN_EMPTY;
1926	gen->stack.sp--;
1927	goto done;
1928	}
1929	top = gen->stack.stack[gen->stack.sp-1];
1930	treg = Cudd_Regular(top);
1931	prev = gen->stack.stack[gen->stack.sp-2];
1932	preg = Cudd_Regular(prev);
1933	nreg = cuddT(preg);
1934	if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
1935	if (next != top) { /* follow the then branch next */
1936	gen->gen.cubes.cube[preg->index] = 1;
1937	gen->stack.stack[gen->stack.sp-1] = next;
1938	break;
1939	}
1940	/* Pop the stack and try again. */
1941	gen->gen.cubes.cube[preg->index] = 2;
1942	gen->stack.sp--;
1943	}
1944
1945	while (1) {
1946	top = gen->stack.stack[gen->stack.sp-1];
1947	treg = Cudd_Regular(top);
1948	if (!cuddIsConstant(treg)) {
1949	/* Take the else branch first. */
1950	gen->gen.cubes.cube[treg->index] = 0;
1951	next = cuddE(treg);
1952	if (top != treg) next = Cudd_Not(next);
1953	gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
1954	} else if (top == Cudd_Not(DD_ONE(dd)) \|\| top == dd->background) {
1955	/* Backtrack */
1956	while (1) {
1957	if (gen->stack.sp == 1) {
1958	/* The current node has no predecessor. */
1959	gen->status = CUDD_GEN_EMPTY;
1960	gen->stack.sp--;
1961	goto done;
1962	}
1963	prev = gen->stack.stack[gen->stack.sp-2];
1964	preg = Cudd_Regular(prev);
1965	nreg = cuddT(preg);
1966	if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
1967	if (next != top) { /* follow the then branch next */
1968	gen->gen.cubes.cube[preg->index] = 1;
1969	gen->stack.stack[gen->stack.sp-1] = next;
1970	break;
1971	}
1972	/* Pop the stack and try again. */
1973	gen->gen.cubes.cube[preg->index] = 2;
1974	gen->stack.sp--;
1975	top = gen->stack.stack[gen->stack.sp-1];
1976	treg = Cudd_Regular(top);
1977	}
1978	} else {
1979	gen->status = CUDD_GEN_NONEMPTY;
1980	gen->gen.cubes.value = cuddV(top);
1981	goto done;
1982	}
1983	}
1984
1985	done:
1986	if (gen->status == CUDD_GEN_EMPTY) return(0);
1987	*cube = gen->gen.cubes.cube;
1988	*value = gen->gen.cubes.value;
1989	return(1);
1990
1991	} /* end of Cudd_NextCube */
1992
1993
1994	/Function******************************************************************
1995
1996	Synopsis [Finds the first prime of a Boolean function.]
1997
1998	Description [Defines an iterator on a pair of BDDs describing a
1999	(possibly incompletely specified) Boolean functions and finds the
2000	first cube of a cover of the function. Returns a generator
2001	that contains the information necessary to continue the enumeration
2002	if successful; NULL otherwise.<p>
2003
2004	The two argument BDDs are the lower and upper bounds of an interval.
2005	It is a mistake to call this function with a lower bound that is not
2006	less than or equal to the upper bound.<p>
2007
2008	A cube is represented as an array of literals, which are integers in
2009	{0, 1, 2}; 0 represents a complemented literal, 1 represents an
2010	uncomplemented literal, and 2 stands for don't care. The enumeration
2011	produces a prime and irredundant cover of the function associated
2012	with the two BDDs. The size of the array equals the number of
2013	variables in the manager at the time Cudd_FirstCube is called.<p>
2014
2015	This iterator can only be used on BDDs.]
2016
2017	SideEffects [The first cube is returned as side effect.]
2018
2019	SeeAlso [Cudd_ForeachPrime Cudd_NextPrime Cudd_GenFree Cudd_IsGenEmpty
2020	Cudd_FirstCube Cudd_FirstNode]
2021
2022	******************************************************************************/
2023	DdGen *
2024	Cudd_FirstPrime(
2025	DdManager *dd,
2026	DdNode *l,
2027	DdNode *u,
2028	int **cube)
2029	{
2030	DdGen *gen;
2031	DdNode implicant, prime, *tmp;
2032	int length, result;
2033
2034	/* Sanity Check. */
2035	if (dd == NULL \|\| l == NULL \|\| u == NULL) return(NULL);
2036
2037	/* Allocate generator an initialize it. */
2038	gen = ALLOC(DdGen,1);
2039	if (gen == NULL) {
2040	dd->errorCode = CUDD_MEMORY_OUT;
2041	return(NULL);
2042	}
2043
2044	gen->manager = dd;
2045	gen->type = CUDD_GEN_PRIMES;
2046	gen->status = CUDD_GEN_EMPTY;
2047	gen->gen.primes.cube = NULL;
2048	gen->gen.primes.ub = u;
2049	gen->stack.sp = 0;
2050	gen->stack.stack = NULL;
2051	gen->node = l;
2052	cuddRef(l);
2053
2054	gen->gen.primes.cube = ALLOC(int,dd->size);
2055	if (gen->gen.primes.cube == NULL) {
2056	dd->errorCode = CUDD_MEMORY_OUT;
2057	FREE(gen);
2058	return(NULL);
2059	}
2060
2061	if (gen->node == Cudd_ReadLogicZero(dd)) {
2062	gen->status = CUDD_GEN_EMPTY;
2063	} else {
2064	implicant = Cudd_LargestCube(dd,gen->node,&length);
2065	if (implicant == NULL) {
2066	Cudd_RecursiveDeref(dd,gen->node);
2067	FREE(gen->gen.primes.cube);
2068	FREE(gen);
2069	return(NULL);
2070	}
2071	cuddRef(implicant);
2072	prime = Cudd_bddMakePrime(dd,implicant,gen->gen.primes.ub);
2073	if (prime == NULL) {
2074	Cudd_RecursiveDeref(dd,gen->node);
2075	Cudd_RecursiveDeref(dd,implicant);
2076	FREE(gen->gen.primes.cube);
2077	FREE(gen);
2078	return(NULL);
2079	}
2080	cuddRef(prime);
2081	Cudd_RecursiveDeref(dd,implicant);
2082	tmp = Cudd_bddAnd(dd,gen->node,Cudd_Not(prime));
2083	if (tmp == NULL) {
2084	Cudd_RecursiveDeref(dd,gen->node);
2085	Cudd_RecursiveDeref(dd,prime);
2086	FREE(gen->gen.primes.cube);
2087	FREE(gen);
2088	return(NULL);
2089	}
2090	cuddRef(tmp);
2091	Cudd_RecursiveDeref(dd,gen->node);
2092	gen->node = tmp;
2093	result = Cudd_BddToCubeArray(dd,prime,gen->gen.primes.cube);
2094	if (result == 0) {
2095	Cudd_RecursiveDeref(dd,gen->node);
2096	Cudd_RecursiveDeref(dd,prime);
2097	FREE(gen->gen.primes.cube);
2098	FREE(gen);
2099	return(NULL);
2100	}
2101	Cudd_RecursiveDeref(dd,prime);
2102	gen->status = CUDD_GEN_NONEMPTY;
2103	}
2104	*cube = gen->gen.primes.cube;
2105	return(gen);
2106
2107	} /* end of Cudd_FirstPrime */
2108
2109
2110	/Function******************************************************************
2111
2112	Synopsis [Generates the next prime of a Boolean function.]
2113
2114	Description [Generates the next cube of a Boolean function,
2115	using generator gen. Returns 0 if the enumeration is completed; 1
2116	otherwise.]
2117
2118	SideEffects [The cube and is returned as side effects. The
2119	generator is modified.]
2120
2121	SeeAlso [Cudd_ForeachPrime Cudd_FirstPrime Cudd_GenFree Cudd_IsGenEmpty
2122	Cudd_NextCube Cudd_NextNode]
2123
2124	******************************************************************************/
2125	int
2126	Cudd_NextPrime(
2127	DdGen *gen,
2128	int **cube)
2129	{
2130	DdNode implicant, prime, *tmp;
2131	DdManager *dd = gen->manager;
2132	int length, result;
2133
2134	if (gen->node == Cudd_ReadLogicZero(dd)) {
2135	gen->status = CUDD_GEN_EMPTY;
2136	} else {
2137	implicant = Cudd_LargestCube(dd,gen->node,&length);
2138	if (implicant == NULL) {
2139	gen->status = CUDD_GEN_EMPTY;
2140	return(0);
2141	}
2142	cuddRef(implicant);
2143	prime = Cudd_bddMakePrime(dd,implicant,gen->gen.primes.ub);
2144	if (prime == NULL) {
2145	Cudd_RecursiveDeref(dd,implicant);
2146	gen->status = CUDD_GEN_EMPTY;
2147	return(0);
2148	}
2149	cuddRef(prime);
2150	Cudd_RecursiveDeref(dd,implicant);
2151	tmp = Cudd_bddAnd(dd,gen->node,Cudd_Not(prime));
2152	if (tmp == NULL) {
2153	Cudd_RecursiveDeref(dd,prime);
2154	gen->status = CUDD_GEN_EMPTY;
2155	return(0);
2156	}
2157	cuddRef(tmp);
2158	Cudd_RecursiveDeref(dd,gen->node);
2159	gen->node = tmp;
2160	result = Cudd_BddToCubeArray(dd,prime,gen->gen.primes.cube);
2161	if (result == 0) {
2162	Cudd_RecursiveDeref(dd,prime);
2163	gen->status = CUDD_GEN_EMPTY;
2164	return(0);
2165	}
2166	Cudd_RecursiveDeref(dd,prime);
2167	gen->status = CUDD_GEN_NONEMPTY;
2168	}
2169	if (gen->status == CUDD_GEN_EMPTY) return(0);
2170	*cube = gen->gen.primes.cube;
2171	return(1);
2172
2173	} /* end of Cudd_NextPrime */
2174
2175
2176	/Function******************************************************************
2177
2178	Synopsis [Computes the cube of an array of BDD variables.]
2179
2180	Description [Computes the cube of an array of BDD variables. If
2181	non-null, the phase argument indicates which literal of each
2182	variable should appear in the cube. If phase\[i\] is nonzero, then the
2183	positive literal is used. If phase is NULL, the cube is positive unate.
2184	Returns a pointer to the result if successful; NULL otherwise.]
2185
2186	SideEffects [None]
2187
2188	SeeAlso [Cudd_addComputeCube Cudd_IndicesToCube Cudd_CubeArrayToBdd]
2189
2190	******************************************************************************/
2191	DdNode *
2192	Cudd_bddComputeCube(
2193	DdManager * dd,
2194	DdNode ** vars,
2195	int * phase,
2196	int n)
2197	{
2198	DdNode *cube;
2199	DdNode *fn;
2200	int i;
2201
2202	cube = DD_ONE(dd);
2203	cuddRef(cube);
2204
2205	for (i = n - 1; i >= 0; i--) {
2206	if (phase == NULL \|\| phase[i] != 0) {
2207	fn = Cudd_bddAnd(dd,vars[i],cube);
2208	} else {
2209	fn = Cudd_bddAnd(dd,Cudd_Not(vars[i]),cube);
2210	}
2211	if (fn == NULL) {
2212	Cudd_RecursiveDeref(dd,cube);
2213	return(NULL);
2214	}
2215	cuddRef(fn);
2216	Cudd_RecursiveDeref(dd,cube);
2217	cube = fn;
2218	}
2219	cuddDeref(cube);
2220
2221	return(cube);
2222
2223	} /* end of Cudd_bddComputeCube */
2224
2225
2226	/Function******************************************************************
2227
2228	Synopsis [Computes the cube of an array of ADD variables.]
2229
2230	Description [Computes the cube of an array of ADD variables. If
2231	non-null, the phase argument indicates which literal of each
2232	variable should appear in the cube. If phase\[i\] is nonzero, then the
2233	positive literal is used. If phase is NULL, the cube is positive unate.
2234	Returns a pointer to the result if successful; NULL otherwise.]
2235
2236	SideEffects [none]
2237
2238	SeeAlso [Cudd_bddComputeCube]
2239
2240	******************************************************************************/
2241	DdNode *
2242	Cudd_addComputeCube(
2243	DdManager * dd,
2244	DdNode ** vars,
2245	int * phase,
2246	int n)
2247	{
2248	DdNode cube, zero;
2249	DdNode *fn;
2250	int i;
2251
2252	cube = DD_ONE(dd);
2253	cuddRef(cube);
2254	zero = DD_ZERO(dd);
2255
2256	for (i = n - 1; i >= 0; i--) {
2257	if (phase == NULL \|\| phase[i] != 0) {
2258	fn = Cudd_addIte(dd,vars[i],cube,zero);
2259	} else {
2260	fn = Cudd_addIte(dd,vars[i],zero,cube);
2261	}
2262	if (fn == NULL) {
2263	Cudd_RecursiveDeref(dd,cube);
2264	return(NULL);
2265	}
2266	cuddRef(fn);
2267	Cudd_RecursiveDeref(dd,cube);
2268	cube = fn;
2269	}
2270	cuddDeref(cube);
2271
2272	return(cube);
2273
2274	} /* end of Cudd_addComputeCube */
2275
2276
2277	/Function******************************************************************
2278
2279	Synopsis [Builds the BDD of a cube from a positional array.]
2280
2281	Description [Builds a cube from a positional array. The array must
2282	have one integer entry for each BDD variable. If the i-th entry is
2283	1, the variable of index i appears in true form in the cube; If the
2284	i-th entry is 0, the variable of index i appears complemented in the
2285	cube; otherwise the variable does not appear in the cube. Returns a
2286	pointer to the BDD for the cube if successful; NULL otherwise.]
2287
2288	SideEffects [None]
2289
2290	SeeAlso [Cudd_bddComputeCube Cudd_IndicesToCube Cudd_BddToCubeArray]
2291
2292	******************************************************************************/
2293	DdNode *
2294	Cudd_CubeArrayToBdd(
2295	DdManager *dd,
2296	int *array)
2297	{
2298	DdNode cube, var, *tmp;
2299	int i;
2300	int size = Cudd_ReadSize(dd);
2301
2302	cube = DD_ONE(dd);
2303	cuddRef(cube);
2304	for (i = size - 1; i >= 0; i--) {
2305	if ((array[i] & ~1) == 0) {
2306	var = Cudd_bddIthVar(dd,i);
2307	tmp = Cudd_bddAnd(dd,cube,Cudd_NotCond(var,array[i]==0));
2308	if (tmp == NULL) {
2309	Cudd_RecursiveDeref(dd,cube);
2310	return(NULL);
2311	}
2312	cuddRef(tmp);
2313	Cudd_RecursiveDeref(dd,cube);
2314	cube = tmp;
2315	}
2316	}
2317	cuddDeref(cube);
2318	return(cube);
2319
2320	} /* end of Cudd_CubeArrayToBdd */
2321
2322
2323	/Function******************************************************************
2324
2325	Synopsis [Builds a positional array from the BDD of a cube.]
2326
2327	Description [Builds a positional array from the BDD of a cube.
2328	Array must have one entry for each BDD variable. The positional
2329	array has 1 in i-th position if the variable of index i appears in
2330	true form in the cube; it has 0 in i-th position if the variable of
2331	index i appears in complemented form in the cube; finally, it has 2
2332	in i-th position if the variable of index i does not appear in the
2333	cube. Returns 1 if successful (the BDD is indeed a cube); 0
2334	otherwise.]
2335
2336	SideEffects [The result is in the array passed by reference.]
2337
2338	SeeAlso [Cudd_CubeArrayToBdd]
2339
2340	******************************************************************************/
2341	int
2342	Cudd_BddToCubeArray(
2343	DdManager *dd,
2344	DdNode *cube,
2345	int *array)
2346	{
2347	DdNode scan, t, *e;
2348	int i;
2349	int size = Cudd_ReadSize(dd);
2350	DdNode *zero = Cudd_Not(DD_ONE(dd));
2351
2352	for (i = size-1; i >= 0; i--) {
2353	array[i] = 2;
2354	}
2355	scan = cube;
2356	while (!Cudd_IsConstant(scan)) {
2357	int index = Cudd_Regular(scan)->index;
2358	cuddGetBranches(scan,&t,&e);
2359	if (t == zero) {
2360	array[index] = 0;
2361	scan = e;
2362	} else if (e == zero) {
2363	array[index] = 1;
2364	scan = t;
2365	} else {
2366	return(0); /* cube is not a cube */
2367	}
2368	}
2369	if (scan == zero) {
2370	return(0);
2371	} else {
2372	return(1);
2373	}
2374
2375	} /* end of Cudd_BddToCubeArray */
2376
2377
2378	/Function******************************************************************
2379
2380	Synopsis [Finds the first node of a decision diagram.]
2381
2382	Description [Defines an iterator on the nodes of a decision diagram
2383	and finds its first node. Returns a generator that contains the
2384	information necessary to continue the enumeration if successful;
2385	NULL otherwise. The nodes are enumerated in a reverse topological
2386	order, so that a node is always preceded in the enumeration by its
2387	descendants.]
2388
2389	SideEffects [The first node is returned as a side effect.]
2390
2391	SeeAlso [Cudd_ForeachNode Cudd_NextNode Cudd_GenFree Cudd_IsGenEmpty
2392	Cudd_FirstCube]
2393
2394	******************************************************************************/
2395	DdGen *
2396	Cudd_FirstNode(
2397	DdManager * dd,
2398	DdNode * f,
2399	DdNode ** node)
2400	{
2401	DdGen *gen;
2402	int size;
2403
2404	/* Sanity Check. */
2405	if (dd == NULL \|\| f == NULL) return(NULL);
2406
2407	/* Allocate generator an initialize it. */
2408	gen = ALLOC(DdGen,1);
2409	if (gen == NULL) {
2410	dd->errorCode = CUDD_MEMORY_OUT;
2411	return(NULL);
2412	}
2413
2414	gen->manager = dd;
2415	gen->type = CUDD_GEN_NODES;
2416	gen->status = CUDD_GEN_EMPTY;
2417	gen->stack.sp = 0;
2418	gen->node = NULL;
2419
2420	/* Collect all the nodes on the generator stack for later perusal. */
2421	gen->stack.stack = cuddNodeArray(Cudd_Regular(f), &size);
2422	if (gen->stack.stack == NULL) {
2423	FREE(gen);
2424	dd->errorCode = CUDD_MEMORY_OUT;
2425	return(NULL);
2426	}
2427	gen->gen.nodes.size = size;
2428
2429	/* Find the first node. */
2430	if (gen->stack.sp < gen->gen.nodes.size) {
2431	gen->status = CUDD_GEN_NONEMPTY;
2432	gen->node = gen->stack.stack[gen->stack.sp];
2433	*node = gen->node;
2434	}
2435
2436	return(gen);
2437
2438	} /* end of Cudd_FirstNode */
2439
2440
2441	/Function******************************************************************
2442
2443	Synopsis [Finds the next node of a decision diagram.]
2444
2445	Description [Finds the node of a decision diagram, using generator
2446	gen. Returns 0 if the enumeration is completed; 1 otherwise.]
2447
2448	SideEffects [The next node is returned as a side effect.]
2449
2450	SeeAlso [Cudd_ForeachNode Cudd_FirstNode Cudd_GenFree Cudd_IsGenEmpty
2451	Cudd_NextCube]
2452
2453	******************************************************************************/
2454	int
2455	Cudd_NextNode(
2456	DdGen * gen,
2457	DdNode ** node)
2458	{
2459	/* Find the next node. */
2460	gen->stack.sp++;
2461	if (gen->stack.sp < gen->gen.nodes.size) {
2462	gen->node = gen->stack.stack[gen->stack.sp];
2463	*node = gen->node;
2464	return(1);
2465	} else {
2466	gen->status = CUDD_GEN_EMPTY;
2467	return(0);
2468	}
2469
2470	} /* end of Cudd_NextNode */
2471
2472
2473	/Function******************************************************************
2474
2475	Synopsis [Frees a CUDD generator.]
2476
2477	Description [Frees a CUDD generator. Always returns 0, so that it can
2478	be used in mis-like foreach constructs.]
2479
2480	SideEffects [None]
2481
2482	SeeAlso [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube
2483	Cudd_FirstNode Cudd_NextNode Cudd_IsGenEmpty]
2484
2485	******************************************************************************/
2486	int
2487	Cudd_GenFree(
2488	DdGen * gen)
2489	{
2490	if (gen == NULL) return(0);
2491	switch (gen->type) {
2492	case CUDD_GEN_CUBES:
2493	case CUDD_GEN_ZDD_PATHS:
2494	FREE(gen->gen.cubes.cube);
2495	FREE(gen->stack.stack);
2496	break;
2497	case CUDD_GEN_PRIMES:
2498	FREE(gen->gen.primes.cube);
2499	Cudd_RecursiveDeref(gen->manager,gen->node);
2500	break;
2501	case CUDD_GEN_NODES:
2502	FREE(gen->stack.stack);
2503	break;
2504	default:
2505	return(0);
2506	}
2507	FREE(gen);
2508	return(0);
2509
2510	} /* end of Cudd_GenFree */
2511
2512
2513	/Function******************************************************************
2514
2515	Synopsis [Queries the status of a generator.]
2516
2517	Description [Queries the status of a generator. Returns 1 if the
2518	generator is empty or NULL; 0 otherswise.]
2519
2520	SideEffects [None]
2521
2522	SeeAlso [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube
2523	Cudd_FirstNode Cudd_NextNode Cudd_GenFree]
2524
2525	******************************************************************************/
2526	int
2527	Cudd_IsGenEmpty(
2528	DdGen * gen)
2529	{
2530	if (gen == NULL) return(1);
2531	return(gen->status == CUDD_GEN_EMPTY);
2532
2533	} /* end of Cudd_IsGenEmpty */
2534
2535
2536	/Function******************************************************************
2537
2538	Synopsis [Builds a cube of BDD variables from an array of indices.]
2539
2540	Description [Builds a cube of BDD variables from an array of indices.
2541	Returns a pointer to the result if successful; NULL otherwise.]
2542
2543	SideEffects [None]
2544
2545	SeeAlso [Cudd_bddComputeCube Cudd_CubeArrayToBdd]
2546
2547	******************************************************************************/
2548	DdNode *
2549	Cudd_IndicesToCube(
2550	DdManager * dd,
2551	int * array,
2552	int n)
2553	{
2554	DdNode cube, tmp;
2555	int i;
2556
2557	cube = DD_ONE(dd);
2558	cuddRef(cube);
2559	for (i = n - 1; i >= 0; i--) {
2560	tmp = Cudd_bddAnd(dd,Cudd_bddIthVar(dd,array[i]),cube);
2561	if (tmp == NULL) {
2562	Cudd_RecursiveDeref(dd,cube);
2563	return(NULL);
2564	}
2565	cuddRef(tmp);
2566	Cudd_RecursiveDeref(dd,cube);
2567	cube = tmp;
2568	}
2569
2570	cuddDeref(cube);
2571	return(cube);
2572
2573	} /* end of Cudd_IndicesToCube */
2574
2575
2576	/Function******************************************************************
2577
2578	Synopsis [Prints the package version number.]
2579
2580	Description []
2581
2582	SideEffects [None]
2583
2584	SeeAlso []
2585
2586	******************************************************************************/
2587	void
2588	Cudd_PrintVersion(
2589	FILE * fp)
2590	{
2591	(void) fprintf(fp, "%s\n", CUDD_VERSION);
2592
2593	} /* end of Cudd_PrintVersion */
2594
2595
2596	/Function******************************************************************
2597
2598	Synopsis [Computes the average distance between adjacent nodes.]
2599
2600	Description [Computes the average distance between adjacent nodes in
2601	the manager. Adjacent nodes are node pairs such that the second node
2602	is the then child, else child, or next node in the collision list.]
2603
2604	SideEffects [None]
2605
2606	SeeAlso []
2607
2608	******************************************************************************/
2609	double
2610	Cudd_AverageDistance(
2611	DdManager * dd)
2612	{
2613	double tetotal, nexttotal;
2614	double tesubtotal, nextsubtotal;
2615	double temeasured, nextmeasured;
2616	int i, j;
2617	int slots, nvars;
2618	long diff;
2619	DdNode *scan;
2620	DdNodePtr *nodelist;
2621	DdNode *sentinel = &(dd->sentinel);
2622
2623	nvars = dd->size;
2624	if (nvars == 0) return(0.0);
2625
2626	/* Initialize totals. */
2627	tetotal = 0.0;
2628	nexttotal = 0.0;
2629	temeasured = 0.0;
2630	nextmeasured = 0.0;
2631
2632	/* Scan the variable subtables. */
2633	for (i = 0; i < nvars; i++) {
2634	nodelist = dd->subtables[i].nodelist;
2635	tesubtotal = 0.0;
2636	nextsubtotal = 0.0;
2637	slots = dd->subtables[i].slots;
2638	for (j = 0; j < slots; j++) {
2639	scan = nodelist[j];
2640	while (scan != sentinel) {
2641	diff = (long) scan - (long) cuddT(scan);
2642	tesubtotal += (double) ddAbs(diff);
2643	diff = (long) scan - (long) Cudd_Regular(cuddE(scan));
2644	tesubtotal += (double) ddAbs(diff);
2645	temeasured += 2.0;
2646	if (scan->next != sentinel) {
2647	diff = (long) scan - (long) scan->next;
2648	nextsubtotal += (double) ddAbs(diff);
2649	nextmeasured += 1.0;
2650	}
2651	scan = scan->next;
2652	}
2653	}
2654	tetotal += tesubtotal;
2655	nexttotal += nextsubtotal;
2656	}
2657
2658	/* Scan the constant table. */
2659	nodelist = dd->constants.nodelist;
2660	nextsubtotal = 0.0;
2661	slots = dd->constants.slots;
2662	for (j = 0; j < slots; j++) {
2663	scan = nodelist[j];
2664	while (scan != NULL) {
2665	if (scan->next != NULL) {
2666	diff = (long) scan - (long) scan->next;
2667	nextsubtotal += (double) ddAbs(diff);
2668	nextmeasured += 1.0;
2669	}
2670	scan = scan->next;
2671	}
2672	}
2673	nexttotal += nextsubtotal;
2674
2675	return((tetotal + nexttotal) / (temeasured + nextmeasured));
2676
2677	} /* end of Cudd_AverageDistance */
2678
2679
2680	/Function******************************************************************
2681
2682	Synopsis [Portable random number generator.]
2683
2684	Description [Portable number generator based on ran2 from "Numerical
2685	Recipes in C." It is a long period (> 2 * 10^18) random number generator
2686	of L'Ecuyer with Bays-Durham shuffle. Returns a long integer uniformly
2687	distributed between 0 and 2147483561 (inclusive of the endpoint values).
2688	The random generator can be explicitly initialized by calling
2689	Cudd_Srandom. If no explicit initialization is performed, then the
2690	seed 1 is assumed.]
2691
2692	SideEffects [None]
2693
2694	SeeAlso [Cudd_Srandom]
2695
2696	******************************************************************************/
2697	long
2698	Cudd_Random(void)
2699	{
2700	int i; /* index in the shuffle table */
2701	long int w; /* work variable */
2702
2703	/* cuddRand == 0 if the geneartor has not been initialized yet. */
2704	if (cuddRand == 0) Cudd_Srandom(1);
2705
2706	/* Compute cuddRand = (cuddRand * LEQA1) % MODULUS1 avoiding
2707	** overflows by Schrage's method.
2708	*/
2709	w = cuddRand / LEQQ1;
2710	cuddRand = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1;
2711	cuddRand += (cuddRand < 0) * MODULUS1;
2712
2713	/* Compute cuddRand2 = (cuddRand2 * LEQA2) % MODULUS2 avoiding
2714	** overflows by Schrage's method.
2715	*/
2716	w = cuddRand2 / LEQQ2;
2717	cuddRand2 = LEQA2 * (cuddRand2 - w * LEQQ2) - w * LEQR2;
2718	cuddRand2 += (cuddRand2 < 0) * MODULUS2;
2719
2720	/* cuddRand is shuffled with the Bays-Durham algorithm.
2721	** shuffleSelect and cuddRand2 are combined to generate the output.
2722	*/
2723
2724	/* Pick one element from the shuffle table; "i" will be in the range
2725	** from 0 to STAB_SIZE-1.
2726	*/
2727	i = (int) (shuffleSelect / STAB_DIV);
2728	/* Mix the element of the shuffle table with the current iterate of
2729	** the second sub-generator, and replace the chosen element of the
2730	** shuffle table with the current iterate of the first sub-generator.
2731	*/
2732	shuffleSelect = shuffleTable[i] - cuddRand2;
2733	shuffleTable[i] = cuddRand;
2734	shuffleSelect += (shuffleSelect < 1) * (MODULUS1 - 1);
2735	/* Since shuffleSelect != 0, and we want to be able to return 0,
2736	** here we subtract 1 before returning.
2737	*/
2738	return(shuffleSelect - 1);
2739
2740	} /* end of Cudd_Random */
2741
2742
2743	/Function******************************************************************
2744
2745	Synopsis [Initializer for the portable random number generator.]
2746
2747	Description [Initializer for the portable number generator based on
2748	ran2 in "Numerical Recipes in C." The input is the seed for the
2749	generator. If it is negative, its absolute value is taken as seed.
2750	If it is 0, then 1 is taken as seed. The initialized sets up the two
2751	recurrences used to generate a long-period stream, and sets up the
2752	shuffle table.]
2753
2754	SideEffects [None]
2755
2756	SeeAlso [Cudd_Random]
2757
2758	******************************************************************************/
2759	void
2760	Cudd_Srandom(
2761	long seed)
2762	{
2763	int i;
2764
2765	if (seed < 0) cuddRand = -seed;
2766	else if (seed == 0) cuddRand = 1;
2767	else cuddRand = seed;
2768	cuddRand2 = cuddRand;
2769	/* Load the shuffle table (after 11 warm-ups). */
2770	for (i = 0; i < STAB_SIZE + 11; i++) {
2771	long int w;
2772	w = cuddRand / LEQQ1;
2773	cuddRand = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1;
2774	cuddRand += (cuddRand < 0) * MODULUS1;
2775	shuffleTable[i % STAB_SIZE] = cuddRand;
2776	}
2777	shuffleSelect = shuffleTable[1 % STAB_SIZE];
2778
2779	} /* end of Cudd_Srandom */
2780
2781
2782	/Function******************************************************************
2783
2784	Synopsis [Computes the density of a BDD or ADD.]
2785
2786	Description [Computes the density of a BDD or ADD. The density is
2787	the ratio of the number of minterms to the number of nodes. If 0 is
2788	passed as number of variables, the number of variables existing in
2789	the manager is used. Returns the density if successful; (double)
2790	CUDD_OUT_OF_MEM otherwise.]
2791
2792	SideEffects [None]
2793
2794	SeeAlso [Cudd_CountMinterm Cudd_DagSize]
2795
2796	******************************************************************************/
2797	double
2798	Cudd_Density(
2799	DdManager * dd /* manager */,
2800	DdNode * f /* function whose density is sought */,
2801	int nvars /* size of the support of f */)
2802	{
2803	double minterms;
2804	int nodes;
2805	double density;
2806
2807	if (nvars == 0) nvars = dd->size;
2808	minterms = Cudd_CountMinterm(dd,f,nvars);
2809	if (minterms == (double) CUDD_OUT_OF_MEM) return(minterms);
2810	nodes = Cudd_DagSize(f);
2811	density = minterms / (double) nodes;
2812	return(density);
2813
2814	} /* end of Cudd_Density */
2815
2816
2817	/Function******************************************************************
2818
2819	Synopsis [Warns that a memory allocation failed.]
2820
2821	Description [Warns that a memory allocation failed.
2822	This function can be used as replacement of MMout_of_memory to prevent
2823	the safe_mem functions of the util package from exiting when malloc
2824	returns NULL. One possible use is in case of discretionary allocations;
2825	for instance, the allocation of memory to enlarge the computed table.]
2826
2827	SideEffects [None]
2828
2829	SeeAlso []
2830
2831	******************************************************************************/
2832	void
2833	Cudd_OutOfMem(
2834	long size /* size of the allocation that failed */)
2835	{
2836	(void) fflush(stdout);
2837	(void) fprintf(stderr, "\nunable to allocate %ld bytes\n", size);
2838	return;
2839
2840	} /* end of Cudd_OutOfMem */
2841
2842
2843	/---------------------------------------------------------------------------/
2844	/* Definition of internal functions */
2845	/---------------------------------------------------------------------------/
2846
2847
2848	/Function******************************************************************
2849
2850	Synopsis [Prints a DD to the standard output. One line per node is
2851	printed.]
2852
2853	Description [Prints a DD to the standard output. One line per node is
2854	printed. Returns 1 if successful; 0 otherwise.]
2855
2856	SideEffects [None]
2857
2858	SeeAlso [Cudd_PrintDebug]
2859
2860	******************************************************************************/
2861	int
2862	cuddP(
2863	DdManager * dd,
2864	DdNode * f)
2865	{
2866	int retval;
2867	st_table *table = st_init_table(st_ptrcmp,st_ptrhash);
2868
2869	if (table == NULL) return(0);
2870
2871	retval = dp2(dd,f,table);
2872	st_free_table(table);
2873	(void) fputc('\n',dd->out);
2874	return(retval);
2875
2876	} /* end of cuddP */
2877
2878
2879	/Function******************************************************************
2880
2881	Synopsis [Frees the memory used to store the minterm counts recorded
2882	in the visited table.]
2883
2884	Description [Frees the memory used to store the minterm counts
2885	recorded in the visited table. Returns ST_CONTINUE.]
2886
2887	SideEffects [None]
2888
2889	******************************************************************************/
2890	enum st_retval
2891	cuddStCountfree(
2892	char * key,
2893	char * value,
2894	char * arg)
2895	{
2896	double *d;
2897
2898	d = (double *)value;
2899	FREE(d);
2900	return(ST_CONTINUE);
2901
2902	} /* end of cuddStCountfree */
2903
2904
2905	/Function******************************************************************
2906
2907	Synopsis [Recursively collects all the nodes of a DD in a symbol
2908	table.]
2909
2910	Description [Traverses the DD f and collects all its nodes in a
2911	symbol table. f is assumed to be a regular pointer and
2912	cuddCollectNodes guarantees this assumption in the recursive calls.
2913	Returns 1 in case of success; 0 otherwise.]
2914
2915	SideEffects [None]
2916
2917	SeeAlso []
2918
2919	******************************************************************************/
2920	int
2921	cuddCollectNodes(
2922	DdNode * f,
2923	st_table * visited)
2924	{
2925	DdNode T, E;
2926	int retval;
2927
2928	#ifdef DD_DEBUG
2929	assert(!Cudd_IsComplement(f));
2930	#endif
2931
2932	/* If already visited, nothing to do. */
2933	if (st_is_member(visited, (char *) f) == 1)
2934	return(1);
2935
2936	/* Check for abnormal condition that should never happen. */
2937	if (f == NULL)
2938	return(0);
2939
2940	/* Mark node as visited. */
2941	if (st_add_direct(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
2942	return(0);
2943
2944	/* Check terminal case. */
2945	if (cuddIsConstant(f))
2946	return(1);
2947
2948	/* Recursive calls. */
2949	T = cuddT(f);
2950	retval = cuddCollectNodes(T,visited);
2951	if (retval != 1) return(retval);
2952	E = Cudd_Regular(cuddE(f));
2953	retval = cuddCollectNodes(E,visited);
2954	return(retval);
2955
2956	} /* end of cuddCollectNodes */
2957
2958
2959	/Function******************************************************************
2960
2961	Synopsis [Recursively collects all the nodes of a DD in an array.]
2962
2963	Description [Traverses the DD f and collects all its nodes in an array.
2964	The caller should free the array returned by cuddNodeArray.
2965	Returns a pointer to the array of nodes in case of success; NULL
2966	otherwise. The nodes are collected in reverse topological order, so
2967	that a node is always preceded in the array by all its descendants.]
2968
2969	SideEffects [The number of nodes is returned as a side effect.]
2970
2971	SeeAlso [Cudd_FirstNode]
2972
2973	******************************************************************************/
2974	DdNodePtr *
2975	cuddNodeArray(
2976	DdNode *f,
2977	int *n)
2978	{
2979	DdNodePtr *table;
2980	int size, retval;
2981
2982	size = ddDagInt(Cudd_Regular(f));
2983	table = ALLOC(DdNodePtr, size);
2984	if (table == NULL) {
2985	ddClearFlag(Cudd_Regular(f));
2986	return(NULL);
2987	}
2988
2989	retval = cuddNodeArrayRecur(f, table, 0);
2990	assert(retval == size);
2991
2992	*n = size;
2993	return(table);
2994
2995	} /* cuddNodeArray */
2996
2997
2998	/---------------------------------------------------------------------------/
2999	/* Definition of static functions */
3000	/---------------------------------------------------------------------------/
3001
3002
3003	/Function******************************************************************
3004
3005	Synopsis [Performs the recursive step of cuddP.]
3006
3007	Description [Performs the recursive step of cuddP. Returns 1 in case
3008	of success; 0 otherwise.]
3009
3010	SideEffects [None]
3011
3012	******************************************************************************/
3013	static int
3014	dp2(
3015	DdManager *dd,
3016	DdNode * f,
3017	st_table * t)
3018	{
3019	DdNode g, n, *N;
3020	int T,E;
3021
3022	if (f == NULL) {
3023	return(0);
3024	}
3025	g = Cudd_Regular(f);
3026	if (cuddIsConstant(g)) {
3027	#if SIZEOF_VOID_P == 8
3028	(void) fprintf(dd->out,"ID = %c0x%lx\tvalue = %-9g\n", bang(f),
3029	(ptruint) g / (ptruint) sizeof(DdNode),cuddV(g));
3030	#else
3031	(void) fprintf(dd->out,"ID = %c0x%x\tvalue = %-9g\n", bang(f),
3032	(ptruint) g / (ptruint) sizeof(DdNode),cuddV(g));
3033	#endif
3034	return(1);
3035	}
3036	if (st_is_member(t,(char *) g) == 1) {
3037	return(1);
3038	}
3039	if (st_add_direct(t,(char *) g,NULL) == ST_OUT_OF_MEM)
3040	return(0);
3041	#ifdef DD_STATS
3042	#if SIZEOF_VOID_P == 8
3043	(void) fprintf(dd->out,"ID = %c0x%lx\tindex = %d\tr = %d\t", bang(f),
3044	(ptruint) g / (ptruint) sizeof(DdNode), g->index, g->ref);
3045	#else
3046	(void) fprintf(dd->out,"ID = %c0x%x\tindex = %d\tr = %d\t", bang(f),
3047	(ptruint) g / (ptruint) sizeof(DdNode),g->index,g->ref);
3048	#endif
3049	#else
3050	#if SIZEOF_VOID_P == 8
3051	(void) fprintf(dd->out,"ID = %c0x%lx\tindex = %u\t", bang(f),
3052	(ptruint) g / (ptruint) sizeof(DdNode),g->index);
3053	#else
3054	(void) fprintf(dd->out,"ID = %c0x%x\tindex = %hu\t", bang(f),
3055	(ptruint) g / (ptruint) sizeof(DdNode),g->index);
3056	#endif
3057	#endif
3058	n = cuddT(g);
3059	if (cuddIsConstant(n)) {
3060	(void) fprintf(dd->out,"T = %-9g\t",cuddV(n));
3061	T = 1;
3062	} else {
3063	#if SIZEOF_VOID_P == 8
3064	(void) fprintf(dd->out,"T = 0x%lx\t",(ptruint) n / (ptruint) sizeof(DdNode));
3065	#else
3066	(void) fprintf(dd->out,"T = 0x%x\t",(ptruint) n / (ptruint) sizeof(DdNode));
3067	#endif
3068	T = 0;
3069	}
3070
3071	n = cuddE(g);
3072	N = Cudd_Regular(n);
3073	if (cuddIsConstant(N)) {
3074	(void) fprintf(dd->out,"E = %c%-9g\n",bang(n),cuddV(N));
3075	E = 1;
3076	} else {
3077	#if SIZEOF_VOID_P == 8
3078	(void) fprintf(dd->out,"E = %c0x%lx\n", bang(n), (ptruint) N/(ptruint) sizeof(DdNode));
3079	#else
3080	(void) fprintf(dd->out,"E = %c0x%x\n", bang(n), (ptruint) N/(ptruint) sizeof(DdNode));
3081	#endif
3082	E = 0;
3083	}
3084	if (E == 0) {
3085	if (dp2(dd,N,t) == 0)
3086	return(0);
3087	}
3088	if (T == 0) {
3089	if (dp2(dd,cuddT(g),t) == 0)
3090	return(0);
3091	}
3092	return(1);
3093
3094	} /* end of dp2 */
3095
3096
3097	/Function******************************************************************
3098
3099	Synopsis [Performs the recursive step of Cudd_PrintMinterm.]
3100
3101	Description []
3102
3103	SideEffects [None]
3104
3105	******************************************************************************/
3106	static void
3107	ddPrintMintermAux(
3108	DdManager * dd /* manager */,
3109	DdNode * node /* current node */,
3110	int * list /* current recursion path */)
3111	{
3112	DdNode N,Nv,*Nnv;
3113	int i,v,index;
3114
3115	N = Cudd_Regular(node);
3116
3117	if (cuddIsConstant(N)) {
3118	/* Terminal case: Print one cube based on the current recursion
3119	** path, unless we have reached the background value (ADDs) or
3120	** the logical zero (BDDs).
3121	*/
3122	if (node != background && node != zero) {
3123	for (i = 0; i < dd->size; i++) {
3124	v = list[i];
3125	if (v == 0) (void) fprintf(dd->out,"0");
3126	else if (v == 1) (void) fprintf(dd->out,"1");
3127	else (void) fprintf(dd->out,"-");
3128	}
3129	(void) fprintf(dd->out," % g\n", cuddV(node));
3130	}
3131	} else {
3132	Nv = cuddT(N);
3133	Nnv = cuddE(N);
3134	if (Cudd_IsComplement(node)) {
3135	Nv = Cudd_Not(Nv);
3136	Nnv = Cudd_Not(Nnv);
3137	}
3138	index = N->index;
3139	list[index] = 0;
3140	ddPrintMintermAux(dd,Nnv,list);
3141	list[index] = 1;
3142	ddPrintMintermAux(dd,Nv,list);
3143	list[index] = 2;
3144	}
3145	return;
3146
3147	} /* end of ddPrintMintermAux */
3148
3149
3150	/Function******************************************************************
3151
3152	Synopsis [Performs the recursive step of Cudd_DagSize.]
3153
3154	Description [Performs the recursive step of Cudd_DagSize. Returns the
3155	number of nodes in the graph rooted at n.]
3156
3157	SideEffects [None]
3158
3159	******************************************************************************/
3160	static int
3161	ddDagInt(
3162	DdNode * n)
3163	{
3164	int tval, eval;
3165
3166	if (Cudd_IsComplement(n->next)) {
3167	return(0);
3168	}
3169	n->next = Cudd_Not(n->next);
3170	if (cuddIsConstant(n)) {
3171	return(1);
3172	}
3173	tval = ddDagInt(cuddT(n));
3174	eval = ddDagInt(Cudd_Regular(cuddE(n)));
3175	return(1 + tval + eval);
3176
3177	} /* end of ddDagInt */
3178
3179
3180	/Function******************************************************************
3181
3182	Synopsis [Performs the recursive step of cuddNodeArray.]
3183
3184	Description [Performs the recursive step of cuddNodeArray. Returns
3185	an the number of nodes in the DD. Clear the least significant bit
3186	of the next field that was used as visited flag by
3187	cuddNodeArrayRecur when counting the nodes. node is supposed to be
3188	regular; the invariant is maintained by this procedure.]
3189
3190	SideEffects [None]
3191
3192	SeeAlso []
3193
3194	******************************************************************************/
3195	static int
3196	cuddNodeArrayRecur(
3197	DdNode *f,
3198	DdNodePtr *table,
3199	int index)
3200	{
3201	int tindex, eindex;
3202
3203	if (!Cudd_IsComplement(f->next)) {
3204	return(index);
3205	}
3206	/* Clear visited flag. */
3207	f->next = Cudd_Regular(f->next);
3208	if (cuddIsConstant(f)) {
3209	table[index] = f;
3210	return(index + 1);
3211	}
3212	tindex = cuddNodeArrayRecur(cuddT(f), table, index);
3213	eindex = cuddNodeArrayRecur(Cudd_Regular(cuddE(f)), table, tindex);
3214	table[eindex] = f;
3215	return(eindex + 1);
3216
3217	} /* end of cuddNodeArrayRecur */
3218
3219
3220	/Function******************************************************************
3221
3222	Synopsis [Performs the recursive step of Cudd_CofactorEstimate.]
3223
3224	Description [Performs the recursive step of Cudd_CofactorEstimate.
3225	Returns an estimate of the number of nodes in the DD of a
3226	cofactor of node. Uses the least significant bit of the next field as
3227	visited flag. node is supposed to be regular; the invariant is maintained
3228	by this procedure.]
3229
3230	SideEffects [None]
3231
3232	SeeAlso []
3233
3234	******************************************************************************/
3235	static int
3236	cuddEstimateCofactor(
3237	DdManager *dd,
3238	st_table *table,
3239	DdNode * node,
3240	int i,
3241	int phase,
3242	DdNode ** ptr)
3243	{
3244	int tval, eval, val;
3245	DdNode ptrT, ptrE;
3246
3247	if (Cudd_IsComplement(node->next)) {
3248	if (!st_lookup(table,(char )node,(char *)ptr)) {
3249	if (st_add_direct(table,(char )node,(char )node) ==
3250	ST_OUT_OF_MEM)
3251	return(CUDD_OUT_OF_MEM);
3252	*ptr = node;
3253	}
3254	return(0);
3255	}
3256	node->next = Cudd_Not(node->next);
3257	if (cuddIsConstant(node)) {
3258	*ptr = node;
3259	if (st_add_direct(table,(char )node,(char )node) == ST_OUT_OF_MEM)
3260	return(CUDD_OUT_OF_MEM);
3261	return(1);
3262	}
3263	if ((int) node->index == i) {
3264	if (phase == 1) {
3265	*ptr = cuddT(node);
3266	val = ddDagInt(cuddT(node));
3267	} else {
3268	*ptr = cuddE(node);
3269	val = ddDagInt(Cudd_Regular(cuddE(node)));
3270	}
3271	if (node->ref > 1) {
3272	if (st_add_direct(table,(char )node,(char )*ptr) ==
3273	ST_OUT_OF_MEM)
3274	return(CUDD_OUT_OF_MEM);
3275	}
3276	return(val);
3277	}
3278	if (dd->perm[node->index] > dd->perm[i]) {
3279	*ptr = node;
3280	tval = ddDagInt(cuddT(node));
3281	eval = ddDagInt(Cudd_Regular(cuddE(node)));
3282	if (node->ref > 1) {
3283	if (st_add_direct(table,(char )node,(char )node) ==
3284	ST_OUT_OF_MEM)
3285	return(CUDD_OUT_OF_MEM);
3286	}
3287	val = 1 + tval + eval;
3288	return(val);
3289	}
3290	tval = cuddEstimateCofactor(dd,table,cuddT(node),i,phase,&ptrT);
3291	eval = cuddEstimateCofactor(dd,table,Cudd_Regular(cuddE(node)),i,
3292	phase,&ptrE);
3293	ptrE = Cudd_NotCond(ptrE,Cudd_IsComplement(cuddE(node)));
3294	if (ptrT == ptrE) { /* recombination */
3295	*ptr = ptrT;
3296	val = tval;
3297	if (node->ref > 1) {
3298	if (st_add_direct(table,(char )node,(char )*ptr) ==
3299	ST_OUT_OF_MEM)
3300	return(CUDD_OUT_OF_MEM);
3301	}
3302	} else if ((ptrT != cuddT(node) \|\| ptrE != cuddE(node)) &&
3303	(*ptr = cuddUniqueLookup(dd,node->index,ptrT,ptrE)) != NULL) {
3304	if (Cudd_IsComplement((*ptr)->next)) {
3305	val = 0;
3306	} else {
3307	val = 1 + tval + eval;
3308	}
3309	if (node->ref > 1) {
3310	if (st_add_direct(table,(char )node,(char )*ptr) ==
3311	ST_OUT_OF_MEM)
3312	return(CUDD_OUT_OF_MEM);
3313	}
3314	} else {
3315	*ptr = node;
3316	val = 1 + tval + eval;
3317	}
3318	return(val);
3319
3320	} /* end of cuddEstimateCofactor */
3321
3322
3323	/Function******************************************************************
3324
3325	Synopsis [Checks the unique table for the existence of an internal node.]
3326
3327	Description [Checks the unique table for the existence of an internal
3328	node. Returns a pointer to the node if it is in the table; NULL otherwise.]
3329
3330	SideEffects [None]
3331
3332	SeeAlso [cuddUniqueInter]
3333
3334	******************************************************************************/
3335	static DdNode *
3336	cuddUniqueLookup(
3337	DdManager * unique,
3338	int index,
3339	DdNode * T,
3340	DdNode * E)
3341	{
3342	int posn;
3343	unsigned int level;
3344	DdNodePtr *nodelist;
3345	DdNode *looking;
3346	DdSubtable *subtable;
3347
3348	if (index >= unique->size) {
3349	return(NULL);
3350	}
3351
3352	level = unique->perm[index];
3353	subtable = &(unique->subtables[level]);
3354
3355	#ifdef DD_DEBUG
3356	assert(level < (unsigned) cuddI(unique,T->index));
3357	assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index));
3358	#endif
3359
3360	posn = ddHash(T, E, subtable->shift);
3361	nodelist = subtable->nodelist;
3362	looking = nodelist[posn];
3363
3364	while (T < cuddT(looking)) {
3365	looking = Cudd_Regular(looking->next);
3366	}
3367	while (T == cuddT(looking) && E < cuddE(looking)) {
3368	looking = Cudd_Regular(looking->next);
3369	}
3370	if (cuddT(looking) == T && cuddE(looking) == E) {
3371	return(looking);
3372	}
3373
3374	return(NULL);
3375
3376	} /* end of cuddUniqueLookup */
3377
3378
3379	/Function******************************************************************
3380
3381	Synopsis [Performs the recursive step of Cudd_CofactorEstimateSimple.]
3382
3383	Description [Performs the recursive step of Cudd_CofactorEstimateSimple.
3384	Returns an estimate of the number of nodes in the DD of the positive
3385	cofactor of node. Uses the least significant bit of the next field as
3386	visited flag. node is supposed to be regular; the invariant is maintained
3387	by this procedure.]
3388
3389	SideEffects [None]
3390
3391	SeeAlso []
3392
3393	******************************************************************************/
3394	static int
3395	cuddEstimateCofactorSimple(
3396	DdNode * node,
3397	int i)
3398	{
3399	int tval, eval;
3400
3401	if (Cudd_IsComplement(node->next)) {
3402	return(0);
3403	}
3404	node->next = Cudd_Not(node->next);
3405	if (cuddIsConstant(node)) {
3406	return(1);
3407	}
3408	tval = cuddEstimateCofactorSimple(cuddT(node),i);
3409	if ((int) node->index == i) return(tval);
3410	eval = cuddEstimateCofactorSimple(Cudd_Regular(cuddE(node)),i);
3411	return(1 + tval + eval);
3412
3413	} /* end of cuddEstimateCofactorSimple */
3414
3415
3416	/Function******************************************************************
3417
3418	Synopsis [Performs the recursive step of Cudd_CountMinterm.]
3419
3420	Description [Performs the recursive step of Cudd_CountMinterm.
3421	It is based on the following identity. Let \|f\| be the
3422	number of minterms of f. Then:
3423	<xmp>
3424	\|f\| = (\|f0\|+\|f1\|)/2
3425	</xmp>
3426	where f0 and f1 are the two cofactors of f. Does not use the
3427	identity \|f'\| = max - \|f\|, to minimize loss of accuracy due to
3428	roundoff. Returns the number of minterms of the function rooted at
3429	node.]
3430
3431	SideEffects [None]
3432
3433	******************************************************************************/
3434	static double
3435	ddCountMintermAux(
3436	DdNode * node,
3437	double max,
3438	DdHashTable * table)
3439	{
3440	DdNode N, Nt, *Ne;
3441	double min, minT, minE;
3442	DdNode *res;
3443
3444	N = Cudd_Regular(node);
3445
3446	if (cuddIsConstant(N)) {
3447	if (node == background \|\| node == zero) {
3448	return(0.0);
3449	} else {
3450	return(max);
3451	}
3452	}
3453	if (N->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
3454	min = cuddV(res);
3455	if (res->ref == 0) {
3456	table->manager->dead++;
3457	table->manager->constants.dead++;
3458	}
3459	return(min);
3460	}
3461
3462	Nt = cuddT(N); Ne = cuddE(N);
3463	if (Cudd_IsComplement(node)) {
3464	Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
3465	}
3466
3467	minT = ddCountMintermAux(Nt,max,table);
3468	if (minT == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3469	minT *= 0.5;
3470	minE = ddCountMintermAux(Ne,max,table);
3471	if (minE == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3472	minE *= 0.5;
3473	min = minT + minE;
3474
3475	if (N->ref != 1) {
3476	ptrint fanout = (ptrint) N->ref;
3477	cuddSatDec(fanout);
3478	res = cuddUniqueConst(table->manager,min);
3479	if (!cuddHashTableInsert1(table,node,res,fanout)) {
3480	cuddRef(res); Cudd_RecursiveDeref(table->manager, res);
3481	return((double)CUDD_OUT_OF_MEM);
3482	}
3483	}
3484
3485	return(min);
3486
3487	} /* end of ddCountMintermAux */
3488
3489
3490	/Function******************************************************************
3491
3492	Synopsis [Performs the recursive step of Cudd_CountPath.]
3493
3494	Description [Performs the recursive step of Cudd_CountPath.
3495	It is based on the following identity. Let \|f\| be the
3496	number of paths of f. Then:
3497	<xmp>
3498	\|f\| = \|f0\|+\|f1\|
3499	</xmp>
3500	where f0 and f1 are the two cofactors of f. Uses the
3501	identity \|f'\| = \|f\|, to improve the utilization of the (local) cache.
3502	Returns the number of paths of the function rooted at node.]
3503
3504	SideEffects [None]
3505
3506	******************************************************************************/
3507	static double
3508	ddCountPathAux(
3509	DdNode * node,
3510	st_table * table)
3511	{
3512
3513	DdNode Nv, Nnv;
3514	double paths, *ppaths, paths1, paths2;
3515	double *dummy;
3516
3517
3518	if (cuddIsConstant(node)) {
3519	return(1.0);
3520	}
3521	if (st_lookup(table, node, &dummy)) {
3522	paths = *dummy;
3523	return(paths);
3524	}
3525
3526	Nv = cuddT(node); Nnv = cuddE(node);
3527
3528	paths1 = ddCountPathAux(Nv,table);
3529	if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3530	paths2 = ddCountPathAux(Cudd_Regular(Nnv),table);
3531	if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3532	paths = paths1 + paths2;
3533
3534	ppaths = ALLOC(double,1);
3535	if (ppaths == NULL) {
3536	return((double)CUDD_OUT_OF_MEM);
3537	}
3538
3539	*ppaths = paths;
3540
3541	if (st_add_direct(table,(char )node, (char )ppaths) == ST_OUT_OF_MEM) {
3542	FREE(ppaths);
3543	return((double)CUDD_OUT_OF_MEM);
3544	}
3545	return(paths);
3546
3547	} /* end of ddCountPathAux */
3548
3549
3550	/Function******************************************************************
3551
3552	Synopsis [Performs the recursive step of Cudd_EpdCountMinterm.]
3553
3554	Description [Performs the recursive step of Cudd_EpdCountMinterm.
3555	It is based on the following identity. Let \|f\| be the
3556	number of minterms of f. Then:
3557	<xmp>
3558	\|f\| = (\|f0\|+\|f1\|)/2
3559	</xmp>
3560	where f0 and f1 are the two cofactors of f. Does not use the
3561	identity \|f'\| = max - \|f\|, to minimize loss of accuracy due to
3562	roundoff. Returns the number of minterms of the function rooted at
3563	node.]
3564
3565	SideEffects [None]
3566
3567	******************************************************************************/
3568	static int
3569	ddEpdCountMintermAux(
3570	DdNode * node,
3571	EpDouble * max,
3572	EpDouble * epd,
3573	st_table * table)
3574	{
3575	DdNode Nt, Ne;
3576	EpDouble *min, minT, minE;
3577	EpDouble *res;
3578	int status;
3579
3580	/* node is assumed to be regular */
3581	if (cuddIsConstant(node)) {
3582	if (node == background \|\| node == zero) {
3583	EpdMakeZero(epd, 0);
3584	} else {
3585	EpdCopy(max, epd);
3586	}
3587	return(0);
3588	}
3589	if (node->ref != 1 && st_lookup(table, node, &res)) {
3590	EpdCopy(res, epd);
3591	return(0);
3592	}
3593
3594	Nt = cuddT(node); Ne = cuddE(node);
3595
3596	status = ddEpdCountMintermAux(Nt,max,&minT,table);
3597	if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
3598	EpdMultiply(&minT, (double)0.5);
3599	status = ddEpdCountMintermAux(Cudd_Regular(Ne),max,&minE,table);
3600	if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
3601	if (Cudd_IsComplement(Ne)) {
3602	EpdSubtract3(max, &minE, epd);
3603	EpdCopy(epd, &minE);
3604	}
3605	EpdMultiply(&minE, (double)0.5);
3606	EpdAdd3(&minT, &minE, epd);
3607
3608	if (node->ref > 1) {
3609	min = EpdAlloc();
3610	if (!min)
3611	return(CUDD_OUT_OF_MEM);
3612	EpdCopy(epd, min);
3613	if (st_insert(table, (char )node, (char )min) == ST_OUT_OF_MEM) {
3614	EpdFree(min);
3615	return(CUDD_OUT_OF_MEM);
3616	}
3617	}
3618
3619	return(0);
3620
3621	} /* end of ddEpdCountMintermAux */
3622
3623
3624	/Function******************************************************************
3625
3626	Synopsis [Performs the recursive step of Cudd_CountPathsToNonZero.]
3627
3628	Description [Performs the recursive step of Cudd_CountPathsToNonZero.
3629	It is based on the following identity. Let \|f\| be the
3630	number of paths of f. Then:
3631	<xmp>
3632	\|f\| = \|f0\|+\|f1\|
3633	</xmp>
3634	where f0 and f1 are the two cofactors of f. Returns the number of
3635	paths of the function rooted at node.]
3636
3637	SideEffects [None]
3638
3639	******************************************************************************/
3640	static double
3641	ddCountPathsToNonZero(
3642	DdNode * N,
3643	st_table * table)
3644	{
3645
3646	DdNode node, Nt, *Ne;
3647	double paths, *ppaths, paths1, paths2;
3648	double *dummy;
3649
3650	node = Cudd_Regular(N);
3651	if (cuddIsConstant(node)) {
3652	return((double) !(Cudd_IsComplement(N) \|\| cuddV(node)==DD_ZERO_VAL));
3653	}
3654	if (st_lookup(table, N, &dummy)) {
3655	paths = *dummy;
3656	return(paths);
3657	}
3658
3659	Nt = cuddT(node); Ne = cuddE(node);
3660	if (node != N) {
3661	Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
3662	}
3663
3664	paths1 = ddCountPathsToNonZero(Nt,table);
3665	if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3666	paths2 = ddCountPathsToNonZero(Ne,table);
3667	if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
3668	paths = paths1 + paths2;
3669
3670	ppaths = ALLOC(double,1);
3671	if (ppaths == NULL) {
3672	return((double)CUDD_OUT_OF_MEM);
3673	}
3674
3675	*ppaths = paths;
3676
3677	if (st_add_direct(table,(char )N, (char )ppaths) == ST_OUT_OF_MEM) {
3678	FREE(ppaths);
3679	return((double)CUDD_OUT_OF_MEM);
3680	}
3681	return(paths);
3682
3683	} /* end of ddCountPathsToNonZero */
3684
3685
3686	/Function******************************************************************
3687
3688	Synopsis [Performs the recursive step of Cudd_Support.]
3689
3690	Description [Performs the recursive step of Cudd_Support. Performs a
3691	DFS from f. The support is accumulated in supp as a side effect. Uses
3692	the LSB of the then pointer as visited flag.]
3693
3694	SideEffects [None]
3695
3696	SeeAlso [ddClearFlag]
3697
3698	******************************************************************************/
3699	static void
3700	ddSupportStep(
3701	DdNode * f,
3702	int * support)
3703	{
3704	if (cuddIsConstant(f) \|\| Cudd_IsComplement(f->next)) {
3705	return;
3706	}
3707
3708	support[f->index] = 1;
3709	ddSupportStep(cuddT(f),support);
3710	ddSupportStep(Cudd_Regular(cuddE(f)),support);
3711	/* Mark as visited. */
3712	f->next = Cudd_Not(f->next);
3713	return;
3714
3715	} /* end of ddSupportStep */
3716
3717
3718	/Function******************************************************************
3719
3720	Synopsis [Performs a DFS from f, clearing the LSB of the next
3721	pointers.]
3722
3723	Description []
3724
3725	SideEffects [None]
3726
3727	SeeAlso [ddSupportStep ddDagInt]
3728
3729	******************************************************************************/
3730	static void
3731	ddClearFlag(
3732	DdNode * f)
3733	{
3734	if (!Cudd_IsComplement(f->next)) {
3735	return;
3736	}
3737	/* Clear visited flag. */
3738	f->next = Cudd_Regular(f->next);
3739	if (cuddIsConstant(f)) {
3740	return;
3741	}
3742	ddClearFlag(cuddT(f));
3743	ddClearFlag(Cudd_Regular(cuddE(f)));
3744	return;
3745
3746	} /* end of ddClearFlag */
3747
3748
3749	/Function******************************************************************
3750
3751	Synopsis [Performs the recursive step of Cudd_CountLeaves.]
3752
3753	Description [Performs the recursive step of Cudd_CountLeaves. Returns
3754	the number of leaves in the DD rooted at n.]
3755
3756	SideEffects [None]
3757
3758	SeeAlso [Cudd_CountLeaves]
3759
3760	******************************************************************************/
3761	static int
3762	ddLeavesInt(
3763	DdNode * n)
3764	{
3765	int tval, eval;
3766
3767	if (Cudd_IsComplement(n->next)) {
3768	return(0);
3769	}
3770	n->next = Cudd_Not(n->next);
3771	if (cuddIsConstant(n)) {
3772	return(1);
3773	}
3774	tval = ddLeavesInt(cuddT(n));
3775	eval = ddLeavesInt(Cudd_Regular(cuddE(n)));
3776	return(tval + eval);
3777
3778	} /* end of ddLeavesInt */
3779
3780
3781	/Function******************************************************************
3782
3783	Synopsis [Performs the recursive step of Cudd_bddPickArbitraryMinterms.]
3784
3785	Description [Performs the recursive step of Cudd_bddPickArbitraryMinterms.
3786	Returns 1 if successful; 0 otherwise.]
3787
3788	SideEffects [none]
3789
3790	SeeAlso [Cudd_bddPickArbitraryMinterms]
3791
3792	******************************************************************************/
3793	static int
3794	ddPickArbitraryMinterms(
3795	DdManager *dd,
3796	DdNode *node,
3797	int nvars,
3798	int nminterms,
3799	char **string)
3800	{
3801	DdNode N, T, *E;
3802	DdNode one, bzero;
3803	int i, t, result;
3804	double min1, min2;
3805
3806	if (string == NULL \|\| node == NULL) return(0);
3807
3808	/* The constant 0 function has no on-set cubes. */
3809	one = DD_ONE(dd);
3810	bzero = Cudd_Not(one);
3811	if (nminterms == 0 \|\| node == bzero) return(1);
3812	if (node == one) {
3813	return(1);
3814	}
3815
3816	N = Cudd_Regular(node);
3817	T = cuddT(N); E = cuddE(N);
3818	if (Cudd_IsComplement(node)) {
3819	T = Cudd_Not(T); E = Cudd_Not(E);
3820	}
3821
3822	min1 = Cudd_CountMinterm(dd, T, nvars) / 2.0;
3823	if (min1 == (double)CUDD_OUT_OF_MEM) return(0);
3824	min2 = Cudd_CountMinterm(dd, E, nvars) / 2.0;
3825	if (min2 == (double)CUDD_OUT_OF_MEM) return(0);
3826
3827	t = (int)((double)nminterms * min1 / (min1 + min2) + 0.5);
3828	for (i = 0; i < t; i++)
3829	string[i][N->index] = '1';
3830	for (i = t; i < nminterms; i++)
3831	string[i][N->index] = '0';
3832
3833	result = ddPickArbitraryMinterms(dd,T,nvars,t,&string[0]);
3834	if (result == 0)
3835	return(0);
3836	result = ddPickArbitraryMinterms(dd,E,nvars,nminterms-t,&string[t]);
3837	return(result);
3838
3839	} /* end of ddPickArbitraryMinterms */
3840
3841
3842	/Function******************************************************************
3843
3844	Synopsis [Finds a representative cube of a BDD.]
3845
3846	Description [Finds a representative cube of a BDD with the weight of
3847	each variable. From the top variable, if the weight is greater than or
3848	equal to 0.0, choose THEN branch unless the child is the constant 0.
3849	Otherwise, choose ELSE branch unless the child is the constant 0.]
3850
3851	SideEffects [Cudd_SubsetWithMaskVars Cudd_bddPickOneCube]
3852
3853	******************************************************************************/
3854	static int
3855	ddPickRepresentativeCube(
3856	DdManager *dd,
3857	DdNode *node,
3858	double *weight,
3859	char *string)
3860	{
3861	DdNode N, T, *E;
3862	DdNode one, bzero;
3863
3864	if (string == NULL \|\| node == NULL) return(0);
3865
3866	/* The constant 0 function has no on-set cubes. */
3867	one = DD_ONE(dd);
3868	bzero = Cudd_Not(one);
3869	if (node == bzero) return(0);
3870
3871	if (node == DD_ONE(dd)) return(1);
3872
3873	for (;;) {
3874	N = Cudd_Regular(node);
3875	if (N == one)
3876	break;
3877	T = cuddT(N);
3878	E = cuddE(N);
3879	if (Cudd_IsComplement(node)) {
3880	T = Cudd_Not(T);
3881	E = Cudd_Not(E);
3882	}
3883	if (weight[N->index] >= 0.0) {
3884	if (T == bzero) {
3885	node = E;
3886	string[N->index] = '0';
3887	} else {
3888	node = T;
3889	string[N->index] = '1';
3890	}
3891	} else {
3892	if (E == bzero) {
3893	node = T;
3894	string[N->index] = '1';
3895	} else {
3896	node = E;
3897	string[N->index] = '0';
3898	}
3899	}
3900	}
3901	return(1);
3902
3903	} /* end of ddPickRepresentativeCube */
3904
3905
3906	/Function******************************************************************
3907
3908	Synopsis [Frees the memory used to store the minterm counts recorded
3909	in the visited table.]
3910
3911	Description [Frees the memory used to store the minterm counts
3912	recorded in the visited table. Returns ST_CONTINUE.]
3913
3914	SideEffects [None]
3915
3916	******************************************************************************/
3917	static enum st_retval
3918	ddEpdFree(
3919	char * key,
3920	char * value,
3921	char * arg)
3922	{
3923	EpDouble *epd;
3924
3925	epd = (EpDouble *) value;
3926	EpdFree(epd);
3927	return(ST_CONTINUE);
3928
3929	} /* end of ddEpdFree */

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

Context Navigation

source: vis_dev/glu-2.3/src/cuBdd/cuddUtil.c @ 104

Download in other formats: