1 /**CFile***********************************************************************
2
3 FileName [cuddBddAbs.c]
4
5 PackageName [cudd]
6
7 Synopsis [Quantification functions for BDDs.]
8
9 Description [External procedures included in this module:
10 <ul>
11 <li> Cudd_bddExistAbstract()
12 <li> Cudd_bddXorExistAbstract()
13 <li> Cudd_bddUnivAbstract()
14 <li> Cudd_bddBooleanDiff()
15 <li> Cudd_bddVarIsDependent()
16 </ul>
17 Internal procedures included in this module:
18 <ul>
19 <li> cuddBddExistAbstractRecur()
20 <li> cuddBddXorExistAbstractRecur()
21 <li> cuddBddBooleanDiffRecur()
22 </ul>
23 Static procedures included in this module:
24 <ul>
25 <li> bddCheckPositiveCube()
26 </ul>
27 ]
28
29 Author [Fabio Somenzi]
30
31 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
32
33 All rights reserved.
34
35 Redistribution and use in source and binary forms, with or without
36 modification, are permitted provided that the following conditions
37 are met:
38
39 Redistributions of source code must retain the above copyright
40 notice, this list of conditions and the following disclaimer.
41
42 Redistributions in binary form must reproduce the above copyright
43 notice, this list of conditions and the following disclaimer in the
44 documentation and/or other materials provided with the distribution.
45
46 Neither the name of the University of Colorado nor the names of its
47 contributors may be used to endorse or promote products derived from
48 this software without specific prior written permission.
49
50 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
51 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
52 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
53 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
54 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
55 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
56 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
57 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
58 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
59 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
60 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
61 POSSIBILITY OF SUCH DAMAGE.]
62
63 ******************************************************************************/
64
65 #include "misc/util/util_hack.h"
66 #include "cuddInt.h"
67
68 ABC_NAMESPACE_IMPL_START
69
70
71
72
73 /*---------------------------------------------------------------------------*/
74 /* Constant declarations */
75 /*---------------------------------------------------------------------------*/
76
77
78 /*---------------------------------------------------------------------------*/
79 /* Stucture declarations */
80 /*---------------------------------------------------------------------------*/
81
82
83 /*---------------------------------------------------------------------------*/
84 /* Type declarations */
85 /*---------------------------------------------------------------------------*/
86
87
88 /*---------------------------------------------------------------------------*/
89 /* Variable declarations */
90 /*---------------------------------------------------------------------------*/
91
92 #ifndef lint
93 static char rcsid[] DD_UNUSED = "$Id: cuddBddAbs.c,v 1.26 2004/08/13 18:04:46 fabio Exp $";
94 #endif
95
96 /*---------------------------------------------------------------------------*/
97 /* Macro declarations */
98 /*---------------------------------------------------------------------------*/
99
100
101 /**AutomaticStart*************************************************************/
102
103 /*---------------------------------------------------------------------------*/
104 /* Static function prototypes */
105 /*---------------------------------------------------------------------------*/
106
107 static int bddCheckPositiveCube (DdManager *manager, DdNode *cube);
108
109 /**AutomaticEnd***************************************************************/
110
111
112 /*---------------------------------------------------------------------------*/
113 /* Definition of exported functions */
114 /*---------------------------------------------------------------------------*/
115
116
117 /**Function********************************************************************
118
119 Synopsis [Existentially abstracts all the variables in cube from f.]
120
121 Description [Existentially abstracts all the variables in cube from f.
122 Returns the abstracted BDD if successful; NULL otherwise.]
123
124 SideEffects [None]
125
126 SeeAlso [Cudd_bddUnivAbstract Cudd_addExistAbstract]
127
128 ******************************************************************************/
129 DdNode *
Cudd_bddExistAbstract(DdManager * manager,DdNode * f,DdNode * cube)130 Cudd_bddExistAbstract(
131 DdManager * manager,
132 DdNode * f,
133 DdNode * cube)
134 {
135 DdNode *res;
136
137 if (bddCheckPositiveCube(manager, cube) == 0) {
138 (void) fprintf(manager->err,
139 "Error: Can only abstract positive cubes\n");
140 manager->errorCode = CUDD_INVALID_ARG;
141 return(NULL);
142 }
143
144 do {
145 manager->reordered = 0;
146 res = cuddBddExistAbstractRecur(manager, f, cube);
147 } while (manager->reordered == 1);
148
149 return(res);
150
151 } /* end of Cudd_bddExistAbstract */
152
153
154 /**Function********************************************************************
155
156 Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the
157 variables in cube.]
158
159 Description [Takes the exclusive OR of two BDDs and simultaneously abstracts
160 the variables in cube. The variables are existentially abstracted. Returns a
161 pointer to the result is successful; NULL otherwise.]
162
163 SideEffects [None]
164
165 SeeAlso [Cudd_bddUnivAbstract Cudd_bddExistAbstract Cudd_bddAndAbstract]
166
167 ******************************************************************************/
168 DdNode *
Cudd_bddXorExistAbstract(DdManager * manager,DdNode * f,DdNode * g,DdNode * cube)169 Cudd_bddXorExistAbstract(
170 DdManager * manager,
171 DdNode * f,
172 DdNode * g,
173 DdNode * cube)
174 {
175 DdNode *res;
176
177 if (bddCheckPositiveCube(manager, cube) == 0) {
178 (void) fprintf(manager->err,
179 "Error: Can only abstract positive cubes\n");
180 manager->errorCode = CUDD_INVALID_ARG;
181 return(NULL);
182 }
183
184 do {
185 manager->reordered = 0;
186 res = cuddBddXorExistAbstractRecur(manager, f, g, cube);
187 } while (manager->reordered == 1);
188
189 return(res);
190
191 } /* end of Cudd_bddXorExistAbstract */
192
193
194 /**Function********************************************************************
195
196 Synopsis [Universally abstracts all the variables in cube from f.]
197
198 Description [Universally abstracts all the variables in cube from f.
199 Returns the abstracted BDD if successful; NULL otherwise.]
200
201 SideEffects [None]
202
203 SeeAlso [Cudd_bddExistAbstract Cudd_addUnivAbstract]
204
205 ******************************************************************************/
206 DdNode *
Cudd_bddUnivAbstract(DdManager * manager,DdNode * f,DdNode * cube)207 Cudd_bddUnivAbstract(
208 DdManager * manager,
209 DdNode * f,
210 DdNode * cube)
211 {
212 DdNode *res;
213
214 if (bddCheckPositiveCube(manager, cube) == 0) {
215 (void) fprintf(manager->err,
216 "Error: Can only abstract positive cubes\n");
217 manager->errorCode = CUDD_INVALID_ARG;
218 return(NULL);
219 }
220
221 do {
222 manager->reordered = 0;
223 res = cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube);
224 } while (manager->reordered == 1);
225 if (res != NULL) res = Cudd_Not(res);
226
227 return(res);
228
229 } /* end of Cudd_bddUnivAbstract */
230
231
232 /**Function********************************************************************
233
234 Synopsis [Computes the boolean difference of f with respect to x.]
235
236 Description [Computes the boolean difference of f with respect to the
237 variable with index x. Returns the BDD of the boolean difference if
238 successful; NULL otherwise.]
239
240 SideEffects [None]
241
242 SeeAlso []
243
244 ******************************************************************************/
245 DdNode *
Cudd_bddBooleanDiff(DdManager * manager,DdNode * f,int x)246 Cudd_bddBooleanDiff(
247 DdManager * manager,
248 DdNode * f,
249 int x)
250 {
251 DdNode *res, *var;
252
253 /* If the variable is not currently in the manager, f cannot
254 ** depend on it.
255 */
256 if (x >= manager->size) return(Cudd_Not(DD_ONE(manager)));
257 var = manager->vars[x];
258
259 do {
260 manager->reordered = 0;
261 res = cuddBddBooleanDiffRecur(manager, Cudd_Regular(f), var);
262 } while (manager->reordered == 1);
263
264 return(res);
265
266 } /* end of Cudd_bddBooleanDiff */
267
268
269 /**Function********************************************************************
270
271 Synopsis [Checks whether a variable is dependent on others in a
272 function.]
273
274 Description [Checks whether a variable is dependent on others in a
275 function. Returns 1 if the variable is dependent; 0 otherwise. No
276 new nodes are created.]
277
278 SideEffects [None]
279
280 SeeAlso []
281
282 ******************************************************************************/
283 int
Cudd_bddVarIsDependent(DdManager * dd,DdNode * f,DdNode * var)284 Cudd_bddVarIsDependent(
285 DdManager *dd, /* manager */
286 DdNode *f, /* function */
287 DdNode *var /* variable */)
288 {
289 DdNode *F, *res, *zero, *ft, *fe;
290 unsigned topf, level;
291 DD_CTFP cacheOp;
292 int retval;
293
294 zero = Cudd_Not(DD_ONE(dd));
295 if (Cudd_IsConstant(f)) return(f == zero);
296
297 /* From now on f is not constant. */
298 F = Cudd_Regular(f);
299 topf = (unsigned) dd->perm[F->index];
300 level = (unsigned) dd->perm[var->index];
301
302 /* Check terminal case. If topf > index of var, f does not depend on var.
303 ** Therefore, var is not dependent in f. */
304 if (topf > level) {
305 return(0);
306 }
307
308 cacheOp = (DD_CTFP) Cudd_bddVarIsDependent;
309 res = cuddCacheLookup2(dd,cacheOp,f,var);
310 if (res != NULL) {
311 return(res != zero);
312 }
313
314 /* Compute cofactors. */
315 ft = Cudd_NotCond(cuddT(F), f != F);
316 fe = Cudd_NotCond(cuddE(F), f != F);
317
318 if (topf == level) {
319 retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe));
320 } else {
321 retval = Cudd_bddVarIsDependent(dd,ft,var) &&
322 Cudd_bddVarIsDependent(dd,fe,var);
323 }
324
325 cuddCacheInsert2(dd,cacheOp,f,var,Cudd_NotCond(zero,retval));
326
327 return(retval);
328
329 } /* Cudd_bddVarIsDependent */
330
331
332 /*---------------------------------------------------------------------------*/
333 /* Definition of internal functions */
334 /*---------------------------------------------------------------------------*/
335
336
337 /**Function********************************************************************
338
339 Synopsis [Performs the recursive steps of Cudd_bddExistAbstract.]
340
341 Description [Performs the recursive steps of Cudd_bddExistAbstract.
342 Returns the BDD obtained by abstracting the variables
343 of cube from f if successful; NULL otherwise. It is also used by
344 Cudd_bddUnivAbstract.]
345
346 SideEffects [None]
347
348 SeeAlso [Cudd_bddExistAbstract Cudd_bddUnivAbstract]
349
350 ******************************************************************************/
351 DdNode *
cuddBddExistAbstractRecur(DdManager * manager,DdNode * f,DdNode * cube)352 cuddBddExistAbstractRecur(
353 DdManager * manager,
354 DdNode * f,
355 DdNode * cube)
356 {
357 DdNode *F, *T, *E, *res, *res1, *res2, *one;
358
359 statLine(manager);
360 one = DD_ONE(manager);
361 F = Cudd_Regular(f);
362
363 /* Cube is guaranteed to be a cube at this point. */
364 if (cube == one || F == one) {
365 return(f);
366 }
367 /* From now on, f and cube are non-constant. */
368
369 /* Abstract a variable that does not appear in f. */
370 while (manager->perm[F->index] > manager->perm[cube->index]) {
371 cube = cuddT(cube);
372 if (cube == one) return(f);
373 }
374
375 /* Check the cache. */
376 if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstract, f, cube)) != NULL) {
377 return(res);
378 }
379
380 /* Compute the cofactors of f. */
381 T = cuddT(F); E = cuddE(F);
382 if (f != F) {
383 T = Cudd_Not(T); E = Cudd_Not(E);
384 }
385
386 /* If the two indices are the same, so are their levels. */
387 if (F->index == cube->index) {
388 if (T == one || E == one || T == Cudd_Not(E)) {
389 return(one);
390 }
391 res1 = cuddBddExistAbstractRecur(manager, T, cuddT(cube));
392 if (res1 == NULL) return(NULL);
393 if (res1 == one) {
394 if (F->ref != 1)
395 cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, one);
396 return(one);
397 }
398 cuddRef(res1);
399 res2 = cuddBddExistAbstractRecur(manager, E, cuddT(cube));
400 if (res2 == NULL) {
401 Cudd_IterDerefBdd(manager,res1);
402 return(NULL);
403 }
404 cuddRef(res2);
405 res = cuddBddAndRecur(manager, Cudd_Not(res1), Cudd_Not(res2));
406 if (res == NULL) {
407 Cudd_IterDerefBdd(manager, res1);
408 Cudd_IterDerefBdd(manager, res2);
409 return(NULL);
410 }
411 res = Cudd_Not(res);
412 cuddRef(res);
413 Cudd_IterDerefBdd(manager, res1);
414 Cudd_IterDerefBdd(manager, res2);
415 if (F->ref != 1)
416 cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
417 cuddDeref(res);
418 return(res);
419 } else { /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */
420 res1 = cuddBddExistAbstractRecur(manager, T, cube);
421 if (res1 == NULL) return(NULL);
422 cuddRef(res1);
423 res2 = cuddBddExistAbstractRecur(manager, E, cube);
424 if (res2 == NULL) {
425 Cudd_IterDerefBdd(manager, res1);
426 return(NULL);
427 }
428 cuddRef(res2);
429 /* ITE takes care of possible complementation of res1 and of the
430 ** case in which res1 == res2. */
431 res = cuddBddIteRecur(manager, manager->vars[F->index], res1, res2);
432 if (res == NULL) {
433 Cudd_IterDerefBdd(manager, res1);
434 Cudd_IterDerefBdd(manager, res2);
435 return(NULL);
436 }
437 cuddRef(res); //Added
438 Cudd_IterDerefBdd(manager, res1); //cuddDeref(res1);
439 Cudd_IterDerefBdd(manager, res2); //cuddDeref(res2);
440 cuddDeref(res); //Added
441 if (F->ref != 1)
442 cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
443 return(res);
444 }
445
446 } /* end of cuddBddExistAbstractRecur */
447
448
449 /**Function********************************************************************
450
451 Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the
452 variables in cube.]
453
454 Description [Takes the exclusive OR of two BDDs and simultaneously abstracts
455 the variables in cube. The variables are existentially abstracted. Returns a
456 pointer to the result is successful; NULL otherwise.]
457
458 SideEffects [None]
459
460 SeeAlso [Cudd_bddAndAbstract]
461
462 ******************************************************************************/
463 DdNode *
cuddBddXorExistAbstractRecur(DdManager * manager,DdNode * f,DdNode * g,DdNode * cube)464 cuddBddXorExistAbstractRecur(
465 DdManager * manager,
466 DdNode * f,
467 DdNode * g,
468 DdNode * cube)
469 {
470 DdNode *F, *fv, *fnv, *G, *gv, *gnv;
471 DdNode *one, *zero, *r, *t, *e, *Cube;
472 unsigned int topf, topg, topcube, top, index;
473
474 statLine(manager);
475 one = DD_ONE(manager);
476 zero = Cudd_Not(one);
477
478 /* Terminal cases. */
479 if (f == g) {
480 return(zero);
481 }
482 if (f == Cudd_Not(g)) {
483 return(one);
484 }
485 if (cube == one) {
486 return(cuddBddXorRecur(manager, f, g));
487 }
488 if (f == one) {
489 return(cuddBddExistAbstractRecur(manager, Cudd_Not(g), cube));
490 }
491 if (g == one) {
492 return(cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube));
493 }
494 if (f == zero) {
495 return(cuddBddExistAbstractRecur(manager, g, cube));
496 }
497 if (g == zero) {
498 return(cuddBddExistAbstractRecur(manager, f, cube));
499 }
500
501 /* At this point f, g, and cube are not constant. */
502
503 if (cuddF2L(f) > cuddF2L(g)) { /* Try to increase cache efficiency. */
504 DdNode *tmp = f;
505 f = g;
506 g = tmp;
507 }
508
509 /* Check cache. */
510 r = cuddCacheLookup(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube);
511 if (r != NULL) {
512 return(r);
513 }
514
515 /* Here we can skip the use of cuddI, because the operands are known
516 ** to be non-constant.
517 */
518 F = Cudd_Regular(f);
519 topf = manager->perm[F->index];
520 G = Cudd_Regular(g);
521 topg = manager->perm[G->index];
522 top = ddMin(topf, topg);
523 topcube = manager->perm[cube->index];
524
525 if (topcube < top) {
526 return(cuddBddXorExistAbstractRecur(manager, f, g, cuddT(cube)));
527 }
528 /* Now, topcube >= top. */
529
530 if (topf == top) {
531 index = F->index;
532 fv = cuddT(F);
533 fnv = cuddE(F);
534 if (Cudd_IsComplement(f)) {
535 fv = Cudd_Not(fv);
536 fnv = Cudd_Not(fnv);
537 }
538 } else {
539 index = G->index;
540 fv = fnv = f;
541 }
542
543 if (topg == top) {
544 gv = cuddT(G);
545 gnv = cuddE(G);
546 if (Cudd_IsComplement(g)) {
547 gv = Cudd_Not(gv);
548 gnv = Cudd_Not(gnv);
549 }
550 } else {
551 gv = gnv = g;
552 }
553
554 if (topcube == top) {
555 Cube = cuddT(cube);
556 } else {
557 Cube = cube;
558 }
559
560 t = cuddBddXorExistAbstractRecur(manager, fv, gv, Cube);
561 if (t == NULL) return(NULL);
562
563 /* Special case: 1 OR anything = 1. Hence, no need to compute
564 ** the else branch if t is 1.
565 */
566 if (t == one && topcube == top) {
567 cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, one);
568 return(one);
569 }
570 cuddRef(t);
571
572 e = cuddBddXorExistAbstractRecur(manager, fnv, gnv, Cube);
573 if (e == NULL) {
574 Cudd_IterDerefBdd(manager, t);
575 return(NULL);
576 }
577 cuddRef(e);
578
579 if (topcube == top) { /* abstract */
580 r = cuddBddAndRecur(manager, Cudd_Not(t), Cudd_Not(e));
581 if (r == NULL) {
582 Cudd_IterDerefBdd(manager, t);
583 Cudd_IterDerefBdd(manager, e);
584 return(NULL);
585 }
586 r = Cudd_Not(r);
587 cuddRef(r);
588 Cudd_IterDerefBdd(manager, t);
589 Cudd_IterDerefBdd(manager, e);
590 cuddDeref(r);
591 } else if (t == e) {
592 r = t;
593 cuddDeref(t);
594 cuddDeref(e);
595 } else {
596 if (Cudd_IsComplement(t)) {
597 r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
598 if (r == NULL) {
599 Cudd_IterDerefBdd(manager, t);
600 Cudd_IterDerefBdd(manager, e);
601 return(NULL);
602 }
603 r = Cudd_Not(r);
604 } else {
605 r = cuddUniqueInter(manager,(int)index,t,e);
606 if (r == NULL) {
607 Cudd_IterDerefBdd(manager, t);
608 Cudd_IterDerefBdd(manager, e);
609 return(NULL);
610 }
611 }
612 cuddDeref(e);
613 cuddDeref(t);
614 }
615 cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, r);
616 return (r);
617
618 } /* end of cuddBddXorExistAbstractRecur */
619
620
621 /**Function********************************************************************
622
623 Synopsis [Performs the recursive steps of Cudd_bddBoleanDiff.]
624
625 Description [Performs the recursive steps of Cudd_bddBoleanDiff.
626 Returns the BDD obtained by XORing the cofactors of f with respect to
627 var if successful; NULL otherwise. Exploits the fact that dF/dx =
628 dF'/dx.]
629
630 SideEffects [None]
631
632 SeeAlso []
633
634 ******************************************************************************/
635 DdNode *
cuddBddBooleanDiffRecur(DdManager * manager,DdNode * f,DdNode * var)636 cuddBddBooleanDiffRecur(
637 DdManager * manager,
638 DdNode * f,
639 DdNode * var)
640 {
641 DdNode *T, *E, *res, *res1, *res2;
642
643 statLine(manager);
644 if (cuddI(manager,f->index) > manager->perm[var->index]) {
645 /* f does not depend on var. */
646 return(Cudd_Not(DD_ONE(manager)));
647 }
648
649 /* From now on, f is non-constant. */
650
651 /* If the two indices are the same, so are their levels. */
652 if (f->index == var->index) {
653 res = cuddBddXorRecur(manager, cuddT(f), cuddE(f));
654 return(res);
655 }
656
657 /* From now on, cuddI(manager,f->index) < cuddI(manager,cube->index). */
658
659 /* Check the cache. */
660 res = cuddCacheLookup2(manager, cuddBddBooleanDiffRecur, f, var);
661 if (res != NULL) {
662 return(res);
663 }
664
665 /* Compute the cofactors of f. */
666 T = cuddT(f); E = cuddE(f);
667
668 res1 = cuddBddBooleanDiffRecur(manager, T, var);
669 if (res1 == NULL) return(NULL);
670 cuddRef(res1);
671 res2 = cuddBddBooleanDiffRecur(manager, Cudd_Regular(E), var);
672 if (res2 == NULL) {
673 Cudd_IterDerefBdd(manager, res1);
674 return(NULL);
675 }
676 cuddRef(res2);
677 /* ITE takes care of possible complementation of res1 and of the
678 ** case in which res1 == res2. */
679 res = cuddBddIteRecur(manager, manager->vars[f->index], res1, res2);
680 if (res == NULL) {
681 Cudd_IterDerefBdd(manager, res1);
682 Cudd_IterDerefBdd(manager, res2);
683 return(NULL);
684 }
685 cuddDeref(res1);
686 cuddDeref(res2);
687 cuddCacheInsert2(manager, cuddBddBooleanDiffRecur, f, var, res);
688 return(res);
689
690 } /* end of cuddBddBooleanDiffRecur */
691
692
693 /*---------------------------------------------------------------------------*/
694 /* Definition of static functions */
695 /*---------------------------------------------------------------------------*/
696
697 /**Function********************************************************************
698
699 Synopsis [Checks whether cube is an BDD representing the product of
700 positive literals.]
701
702 Description [Returns 1 in case of success; 0 otherwise.]
703
704 SideEffects [None]
705
706 ******************************************************************************/
707 static int
bddCheckPositiveCube(DdManager * manager,DdNode * cube)708 bddCheckPositiveCube(
709 DdManager * manager,
710 DdNode * cube)
711 {
712 if (Cudd_IsComplement(cube)) return(0);
713 if (cube == DD_ONE(manager)) return(1);
714 if (cuddIsConstant(cube)) return(0);
715 if (cuddE(cube) == Cudd_Not(DD_ONE(manager))) {
716 return(bddCheckPositiveCube(manager, cuddT(cube)));
717 }
718 return(0);
719
720 } /* end of bddCheckPositiveCube */
721
722
723 ABC_NAMESPACE_IMPL_END
724
725
726