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