1 /**
2 @file
3
4 @ingroup cudd
5
6 @brief %BDD ITE function and satellites.
7
8 @author Fabio Somenzi
9
10 @copyright@parblock
11 Copyright (c) 1995-2015, Regents of the University of Colorado
12
13 All rights reserved.
14
15 Redistribution and use in source and binary forms, with or without
16 modification, are permitted provided that the following conditions
17 are met:
18
19 Redistributions of source code must retain the above copyright
20 notice, this list of conditions and the following disclaimer.
21
22 Redistributions in binary form must reproduce the above copyright
23 notice, this list of conditions and the following disclaimer in the
24 documentation and/or other materials provided with the distribution.
25
26 Neither the name of the University of Colorado nor the names of its
27 contributors may be used to endorse or promote products derived from
28 this software without specific prior written permission.
29
30 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
31 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
32 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
33 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
34 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
35 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
36 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
37 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
38 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
39 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
40 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
41 POSSIBILITY OF SUCH DAMAGE.
42 @endparblock
43
44 */
45
46 #include "util.h"
47 #include "cuddInt.h"
48
49
50 /*---------------------------------------------------------------------------*/
51 /* Constant declarations */
52 /*---------------------------------------------------------------------------*/
53
54
55 /*---------------------------------------------------------------------------*/
56 /* Stucture declarations */
57 /*---------------------------------------------------------------------------*/
58
59
60 /*---------------------------------------------------------------------------*/
61 /* Type declarations */
62 /*---------------------------------------------------------------------------*/
63
64
65 /*---------------------------------------------------------------------------*/
66 /* Variable declarations */
67 /*---------------------------------------------------------------------------*/
68
69
70 /*---------------------------------------------------------------------------*/
71 /* Macro declarations */
72 /*---------------------------------------------------------------------------*/
73
74 /** \cond */
75
76 /*---------------------------------------------------------------------------*/
77 /* Static function prototypes */
78 /*---------------------------------------------------------------------------*/
79
80 static void bddVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one);
81 static int bddVarToCanonical (DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, int *topfp, int *topgp, int *tophp);
82 static int bddVarToCanonicalSimple (DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, int *topfp, int *topgp, int *tophp);
83
84 /** \endcond */
85
86
87 /*---------------------------------------------------------------------------*/
88 /* Definition of exported functions */
89 /*---------------------------------------------------------------------------*/
90
91
92 /**
93 @brief Implements ITE(f,g,h).
94
95 @return a pointer to the resulting %BDD if successful; NULL if the
96 intermediate result blows up.
97
98 @sideeffect None
99
100 @see Cudd_addIte Cudd_bddIteConstant Cudd_bddIntersect
101
102 */
103 DdNode *
Cudd_bddIte(DdManager * dd,DdNode * f,DdNode * g,DdNode * h)104 Cudd_bddIte(
105 DdManager * dd /**< manager */,
106 DdNode * f /**< first operand */,
107 DdNode * g /**< second operand */,
108 DdNode * h /**< third operand */)
109 {
110 DdNode *res;
111
112 do {
113 dd->reordered = 0;
114 res = cuddBddIteRecur(dd,f,g,h);
115 } while (dd->reordered == 1);
116 if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
117 dd->timeoutHandler(dd, dd->tohArg);
118 }
119 return(res);
120
121 } /* end of Cudd_bddIte */
122
123
124 /**
125 @brief Implements ITE(f,g,h) unless too many nodes are required.
126
127 @return a pointer to the resulting %BDD if successful; NULL if the
128 intermediate result blows up or more new nodes than `limit` are
129 required.
130
131 @sideeffect None
132
133 @see Cudd_bddIte
134
135 */
136 DdNode *
Cudd_bddIteLimit(DdManager * dd,DdNode * f,DdNode * g,DdNode * h,unsigned int limit)137 Cudd_bddIteLimit(
138 DdManager * dd /**< manager */,
139 DdNode * f /**< first operand */,
140 DdNode * g /**< second operand */,
141 DdNode * h /**< third operand */,
142 unsigned int limit /**< maximum number of new nodes */)
143 {
144 DdNode *res;
145 unsigned int saveLimit = dd->maxLive;
146
147 dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + limit;
148 do {
149 dd->reordered = 0;
150 res = cuddBddIteRecur(dd,f,g,h);
151 } while (dd->reordered == 1);
152 dd->maxLive = saveLimit;
153 if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
154 dd->timeoutHandler(dd, dd->tohArg);
155 }
156 return(res);
157
158 } /* end of Cudd_bddIteLimit */
159
160
161 /**
162 @brief Implements ITEconstant(f,g,h).
163
164 @return a pointer to the resulting %BDD (which may or may not be
165 constant) or DD_NON_CONSTANT.
166
167 @details No new nodes are created.
168
169 @sideeffect None
170
171 @see Cudd_bddIte Cudd_bddIntersect Cudd_bddLeq Cudd_addIteConstant
172
173 */
174 DdNode *
Cudd_bddIteConstant(DdManager * dd,DdNode * f,DdNode * g,DdNode * h)175 Cudd_bddIteConstant(
176 DdManager * dd /**< manager */,
177 DdNode * f /**< first operand */,
178 DdNode * g /**< second operand */,
179 DdNode * h /**< thord operand */)
180 {
181 DdNode *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
182 DdNode *one = DD_ONE(dd);
183 DdNode *zero = Cudd_Not(one);
184 int comple;
185 int topf, topg, toph, v;
186
187 statLine(dd);
188 /* Trivial cases. */
189 if (f == one) /* ITE(1,G,H) => G */
190 return(g);
191
192 if (f == zero) /* ITE(0,G,H) => H */
193 return(h);
194
195 /* f now not a constant. */
196 bddVarToConst(f, &g, &h, one); /* possibly convert g or h */
197 /* to constants */
198
199 if (g == h) /* ITE(F,G,G) => G */
200 return(g);
201
202 if (Cudd_IsConstantInt(g) && Cudd_IsConstantInt(h))
203 return(DD_NON_CONSTANT); /* ITE(F,1,0) or ITE(F,0,1) */
204 /* => DD_NON_CONSTANT */
205
206 if (g == Cudd_Not(h))
207 return(DD_NON_CONSTANT); /* ITE(F,G,G') => DD_NON_CONSTANT */
208 /* if F != G and F != G' */
209
210 comple = bddVarToCanonical(dd, &f, &g, &h, &topf, &topg, &toph);
211
212 /* Cache lookup. */
213 r = cuddConstantLookup(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h);
214 if (r != NULL) {
215 return(Cudd_NotCond(r,comple && r != DD_NON_CONSTANT));
216 }
217
218 v = ddMin(topg, toph);
219
220 /* ITE(F,G,H) = (v,G,H) (non constant) if F = (v,1,0), v < top(G,H). */
221 if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
222 return(DD_NON_CONSTANT);
223 }
224
225 /* Compute cofactors. */
226 if (topf <= v) {
227 v = ddMin(topf, v); /* v = top_var(F,G,H) */
228 Fv = cuddT(f); Fnv = cuddE(f);
229 } else {
230 Fv = Fnv = f;
231 }
232
233 if (topg == v) {
234 Gv = cuddT(g); Gnv = cuddE(g);
235 } else {
236 Gv = Gnv = g;
237 }
238
239 if (toph == v) {
240 H = Cudd_Regular(h);
241 Hv = cuddT(H); Hnv = cuddE(H);
242 if (Cudd_IsComplement(h)) {
243 Hv = Cudd_Not(Hv);
244 Hnv = Cudd_Not(Hnv);
245 }
246 } else {
247 Hv = Hnv = h;
248 }
249
250 /* Recursion. */
251 t = Cudd_bddIteConstant(dd, Fv, Gv, Hv);
252 if (t == DD_NON_CONSTANT || !Cudd_IsConstantInt(t)) {
253 cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
254 return(DD_NON_CONSTANT);
255 }
256 e = Cudd_bddIteConstant(dd, Fnv, Gnv, Hnv);
257 if (e == DD_NON_CONSTANT || !Cudd_IsConstantInt(e) || t != e) {
258 cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
259 return(DD_NON_CONSTANT);
260 }
261 cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, t);
262 return(Cudd_NotCond(t,comple));
263
264 } /* end of Cudd_bddIteConstant */
265
266
267 /**
268 @brief Returns a function included in the intersection of f and g.
269
270 @details The function computed (if not zero) is a witness that the
271 intersection is not empty. Cudd_bddIntersect tries to build as few
272 new nodes as possible. If the only result of interest is whether f
273 and g intersect, Cudd_bddLeq should be used instead.
274
275 @sideeffect None
276
277 @see Cudd_bddLeq Cudd_bddIteConstant
278
279 */
280 DdNode *
Cudd_bddIntersect(DdManager * dd,DdNode * f,DdNode * g)281 Cudd_bddIntersect(
282 DdManager * dd /**< manager */,
283 DdNode * f /**< first operand */,
284 DdNode * g /**< second operand */)
285 {
286 DdNode *res;
287
288 do {
289 dd->reordered = 0;
290 res = cuddBddIntersectRecur(dd,f,g);
291 } while (dd->reordered == 1);
292 if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
293 dd->timeoutHandler(dd, dd->tohArg);
294 }
295
296 return(res);
297
298 } /* end of Cudd_bddIntersect */
299
300
301 /**
302 @brief Computes the conjunction of two BDDs f and g.
303
304 @return a pointer to the resulting %BDD if successful; NULL if the
305 intermediate result blows up.
306
307 @sideeffect None
308
309 @see Cudd_bddIte Cudd_addApply Cudd_bddAndAbstract Cudd_bddIntersect
310 Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor
311
312 */
313 DdNode *
Cudd_bddAnd(DdManager * dd,DdNode * f,DdNode * g)314 Cudd_bddAnd(
315 DdManager * dd /**< manager */,
316 DdNode * f /**< first operand */,
317 DdNode * g /**< second operand */)
318 {
319 DdNode *res;
320
321 do {
322 dd->reordered = 0;
323 res = cuddBddAndRecur(dd,f,g);
324 } while (dd->reordered == 1);
325 if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
326 dd->timeoutHandler(dd, dd->tohArg);
327 }
328 return(res);
329
330 } /* end of Cudd_bddAnd */
331
332
333 /**
334 @brief Computes the conjunction of two BDDs f and g unless too many
335 nodes are required.
336
337 @return a pointer to the resulting %BDD if successful; NULL if the
338 intermediate result blows up or more new nodes than `limit` are
339 required.
340
341 @sideeffect None
342
343 @see Cudd_bddAnd
344
345 */
346 DdNode *
Cudd_bddAndLimit(DdManager * dd,DdNode * f,DdNode * g,unsigned int limit)347 Cudd_bddAndLimit(
348 DdManager * dd /**< manager */,
349 DdNode * f /**< first operand */,
350 DdNode * g /**< second operand */,
351 unsigned int limit /**< maximum number of new nodes */)
352 {
353 DdNode *res;
354 unsigned int saveLimit = dd->maxLive;
355
356 dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + limit;
357 do {
358 dd->reordered = 0;
359 res = cuddBddAndRecur(dd,f,g);
360 } while (dd->reordered == 1);
361 dd->maxLive = saveLimit;
362 if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
363 dd->timeoutHandler(dd, dd->tohArg);
364 }
365 return(res);
366
367 } /* end of Cudd_bddAndLimit */
368
369
370 /**
371 @brief Computes the disjunction of two BDDs f and g.
372
373 @return a pointer to the resulting %BDD if successful; NULL if the
374 intermediate result blows up.
375
376 @sideeffect None
377
378 @see Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddNand Cudd_bddNor
379 Cudd_bddXor Cudd_bddXnor
380
381 */
382 DdNode *
Cudd_bddOr(DdManager * dd,DdNode * f,DdNode * g)383 Cudd_bddOr(
384 DdManager * dd /**< manager */,
385 DdNode * f /**< first operand */,
386 DdNode * g /**< second operand */)
387 {
388 DdNode *res;
389
390 do {
391 dd->reordered = 0;
392 res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g));
393 } while (dd->reordered == 1);
394 if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
395 dd->timeoutHandler(dd, dd->tohArg);
396 }
397 res = Cudd_NotCond(res,res != NULL);
398 return(res);
399
400 } /* end of Cudd_bddOr */
401
402
403 /**
404 @brief Computes the disjunction of two BDDs f and g unless too many
405 nodes are required.
406
407 @return a pointer to the resulting %BDD if successful; NULL if the
408 intermediate result blows up or more new nodes than `limit` are
409 required.
410
411 @sideeffect None
412
413 @see Cudd_bddOr
414
415 */
416 DdNode *
Cudd_bddOrLimit(DdManager * dd,DdNode * f,DdNode * g,unsigned int limit)417 Cudd_bddOrLimit(
418 DdManager * dd /**< manager */,
419 DdNode * f /**< first operand */,
420 DdNode * g /**< second operand */,
421 unsigned int limit /**< maximum number of new nodes */)
422 {
423 DdNode *res;
424 unsigned int saveLimit = dd->maxLive;
425
426 dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + limit;
427 do {
428 dd->reordered = 0;
429 res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g));
430 } while (dd->reordered == 1);
431 dd->maxLive = saveLimit;
432 if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
433 dd->timeoutHandler(dd, dd->tohArg);
434 }
435 res = Cudd_NotCond(res,res != NULL);
436 return(res);
437
438 } /* end of Cudd_bddOrLimit */
439
440
441 /**
442 @brief Computes the NAND of two BDDs f and g.
443
444 @return a pointer to the resulting %BDD if successful; NULL if the
445 intermediate result blows up.
446
447 @sideeffect None
448
449 @see Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNor
450 Cudd_bddXor Cudd_bddXnor
451
452 */
453 DdNode *
Cudd_bddNand(DdManager * dd,DdNode * f,DdNode * g)454 Cudd_bddNand(
455 DdManager * dd /**< manager */,
456 DdNode * f /**< first operand */,
457 DdNode * g /** second operand */)
458 {
459 DdNode *res;
460
461 do {
462 dd->reordered = 0;
463 res = cuddBddAndRecur(dd,f,g);
464 } while (dd->reordered == 1);
465 if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
466 dd->timeoutHandler(dd, dd->tohArg);
467 }
468 res = Cudd_NotCond(res,res != NULL);
469 return(res);
470
471 } /* end of Cudd_bddNand */
472
473
474 /**
475 @brief Computes the NOR of two BDDs f and g.
476
477 @return a pointer to the resulting %BDD if successful; NULL if the
478 intermediate result blows up.
479
480 @sideeffect None
481
482 @see Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNand
483 Cudd_bddXor Cudd_bddXnor
484
485 */
486 DdNode *
Cudd_bddNor(DdManager * dd,DdNode * f,DdNode * g)487 Cudd_bddNor(
488 DdManager * dd /**< manager */,
489 DdNode * f /**< first operand */,
490 DdNode * g /**< second operand */)
491 {
492 DdNode *res;
493
494 do {
495 dd->reordered = 0;
496 res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g));
497 } while (dd->reordered == 1);
498 if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
499 dd->timeoutHandler(dd, dd->tohArg);
500 }
501 return(res);
502
503 } /* end of Cudd_bddNor */
504
505
506 /**
507 @brief Computes the exclusive OR of two BDDs f and g.
508
509 @return a pointer to the resulting %BDD if successful; NULL if the
510 intermediate result blows up.
511
512 @sideeffect None
513
514 @see Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr
515 Cudd_bddNand Cudd_bddNor Cudd_bddXnor
516
517 */
518 DdNode *
Cudd_bddXor(DdManager * dd,DdNode * f,DdNode * g)519 Cudd_bddXor(
520 DdManager * dd /**< manager */,
521 DdNode * f /**< first operand */,
522 DdNode * g /**< second operand */)
523 {
524 DdNode *res;
525
526 do {
527 dd->reordered = 0;
528 res = cuddBddXorRecur(dd,f,g);
529 } while (dd->reordered == 1);
530 if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
531 dd->timeoutHandler(dd, dd->tohArg);
532 }
533 return(res);
534
535 } /* end of Cudd_bddXor */
536
537
538 /**
539 @brief Computes the exclusive NOR of two BDDs f and g.
540
541 @return a pointer to the resulting %BDD if successful; NULL if the
542 intermediate result blows up.
543
544 @sideeffect None
545
546 @see Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr
547 Cudd_bddNand Cudd_bddNor Cudd_bddXor
548
549 */
550 DdNode *
Cudd_bddXnor(DdManager * dd,DdNode * f,DdNode * g)551 Cudd_bddXnor(
552 DdManager * dd /**< manager */,
553 DdNode * f /**< first operand */,
554 DdNode * g /**< second operand */)
555 {
556 DdNode *res;
557
558 do {
559 dd->reordered = 0;
560 res = cuddBddXorRecur(dd,f,Cudd_Not(g));
561 } while (dd->reordered == 1);
562 if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
563 dd->timeoutHandler(dd, dd->tohArg);
564 }
565 return(res);
566
567 } /* end of Cudd_bddXnor */
568
569
570 /**
571 @brief Computes the exclusive NOR of two BDDs f and g unless too
572 many nodes are required.
573
574 @return a pointer to the resulting %BDD if successful; NULL if the
575 intermediate result blows up or more new nodes than `limit` are
576 required.
577
578 @sideeffect None
579
580 @see Cudd_bddXnor
581
582 */
583 DdNode *
Cudd_bddXnorLimit(DdManager * dd,DdNode * f,DdNode * g,unsigned int limit)584 Cudd_bddXnorLimit(
585 DdManager * dd /**< manager */,
586 DdNode * f /**< first operand */,
587 DdNode * g /**< second operand */,
588 unsigned int limit /**< maximum number of new nodes */)
589 {
590 DdNode *res;
591 unsigned int saveLimit = dd->maxLive;
592
593 dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + limit;
594 do {
595 dd->reordered = 0;
596 res = cuddBddXorRecur(dd,f,Cudd_Not(g));
597 } while (dd->reordered == 1);
598 dd->maxLive = saveLimit;
599 if (dd->errorCode == CUDD_TIMEOUT_EXPIRED && dd->timeoutHandler) {
600 dd->timeoutHandler(dd, dd->tohArg);
601 }
602 return(res);
603
604 } /* end of Cudd_bddXnorLimit */
605
606
607 /**
608 @brief Checks whether f is less than or equal to g.
609
610 @return 1 if f is less than or equal to g; 0 otherwise.
611
612 @details No new nodes are created.
613
614 @sideeffect None
615
616 @see Cudd_bddIteConstant Cudd_addEvalConst
617
618 */
619 int
Cudd_bddLeq(DdManager * dd,DdNode * f,DdNode * g)620 Cudd_bddLeq(
621 DdManager * dd /**< manager */,
622 DdNode * f /**< first operand */,
623 DdNode * g /**< second operand */)
624 {
625 DdNode *one, *zero, *tmp, *F, *fv, *fvn, *gv, *gvn;
626 int topf, topg, res;
627
628 statLine(dd);
629 /* Terminal cases and normalization. */
630 if (f == g) return(1);
631
632 if (Cudd_IsComplement(g)) {
633 /* Special case: if f is regular and g is complemented,
634 ** f(1,...,1) = 1 > 0 = g(1,...,1).
635 */
636 if (!Cudd_IsComplement(f)) return(0);
637 /* Both are complemented: Swap and complement because
638 ** f <= g <=> g' <= f' and we want the second argument to be regular.
639 */
640 tmp = g;
641 g = Cudd_Not(f);
642 f = Cudd_Not(tmp);
643 } else if (Cudd_IsComplement(f) && g < f) {
644 tmp = g;
645 g = Cudd_Not(f);
646 f = Cudd_Not(tmp);
647 }
648
649 /* Now g is regular. */
650 one = DD_ONE(dd);
651 if (g == one) return(1); /* no need to test against zero */
652 if (f == one) return(0); /* since at this point g != one */
653 if (Cudd_Not(f) == g) return(0); /* because neither is constant */
654 zero = Cudd_Not(one);
655 if (f == zero) return(1);
656
657 /* Here neither f nor g is constant. */
658
659 /* Check cache. */
660 F = Cudd_Regular(f);
661 if (F->ref != 1 || g->ref != 1) {
662 tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_bddLeq,f,g);
663 if (tmp != NULL) {
664 return(tmp == one);
665 }
666 }
667
668 /* Compute cofactors. */
669 topf = dd->perm[F->index];
670 topg = dd->perm[g->index];
671 if (topf <= topg) {
672 fv = cuddT(F); fvn = cuddE(F);
673 if (f != F) {
674 fv = Cudd_Not(fv);
675 fvn = Cudd_Not(fvn);
676 }
677 } else {
678 fv = fvn = f;
679 }
680 if (topg <= topf) {
681 gv = cuddT(g); gvn = cuddE(g);
682 } else {
683 gv = gvn = g;
684 }
685
686 /* Recursive calls. Since we want to maximize the probability of
687 ** the special case f(1,...,1) > g(1,...,1), we consider the negative
688 ** cofactors first. Indeed, the complementation parity of the positive
689 ** cofactors is the same as the one of the parent functions.
690 */
691 res = Cudd_bddLeq(dd,fvn,gvn) && Cudd_bddLeq(dd,fv,gv);
692
693 /* Store result in cache and return. */
694 if (F->ref !=1 || g->ref != 1)
695 cuddCacheInsert2(dd,(DD_CTFP)Cudd_bddLeq,f,g,(res ? one : zero));
696 return(res);
697
698 } /* end of Cudd_bddLeq */
699
700
701 /*---------------------------------------------------------------------------*/
702 /* Definition of internal functions */
703 /*---------------------------------------------------------------------------*/
704
705
706 /**
707 @brief Implements the recursive step of Cudd_bddIte.
708
709 @return a pointer to the resulting %BDD. NULL if the intermediate
710 result blows up or if reordering occurs.
711
712 @sideeffect None
713
714 */
715 DdNode *
cuddBddIteRecur(DdManager * dd,DdNode * f,DdNode * g,DdNode * h)716 cuddBddIteRecur(
717 DdManager * dd,
718 DdNode * f,
719 DdNode * g,
720 DdNode * h)
721 {
722 DdNode *one, *zero, *res;
723 DdNode *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
724 int topf, topg, toph, v;
725 unsigned int index;
726 int comple;
727
728 statLine(dd);
729 /* Terminal cases. */
730
731 /* One variable cases. */
732 if (f == (one = DD_ONE(dd))) /* ITE(1,G,H) = G */
733 return(g);
734
735 if (f == (zero = Cudd_Not(one))) /* ITE(0,G,H) = H */
736 return(h);
737
738 /* From now on, f is known not to be a constant. */
739 if (g == one || f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
740 if (h == zero) { /* ITE(F,1,0) = F */
741 return(f);
742 } else {
743 res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(h));
744 return(Cudd_NotCond(res,res != NULL));
745 }
746 } else if (g == zero || f == Cudd_Not(g)) { /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */
747 if (h == one) { /* ITE(F,0,1) = !F */
748 return(Cudd_Not(f));
749 } else {
750 res = cuddBddAndRecur(dd,Cudd_Not(f),h);
751 return(res);
752 }
753 }
754 if (h == zero || f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
755 res = cuddBddAndRecur(dd,f,g);
756 return(res);
757 } else if (h == one || f == Cudd_Not(h)) { /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */
758 res = cuddBddAndRecur(dd,f,Cudd_Not(g));
759 return(Cudd_NotCond(res,res != NULL));
760 }
761
762 /* Check remaining one variable case. */
763 if (g == h) { /* ITE(F,G,G) = G */
764 return(g);
765 } else if (g == Cudd_Not(h)) { /* ITE(F,G,!G) = F <-> G */
766 res = cuddBddXorRecur(dd,f,h);
767 return(res);
768 }
769
770 /* From here, there are no constants. */
771 comple = bddVarToCanonicalSimple(dd, &f, &g, &h, &topf, &topg, &toph);
772
773 /* f & g are now regular pointers */
774
775 v = ddMin(topg, toph);
776
777 /* A shortcut: ITE(F,G,H) = (v,G,H) if F = (v,1,0), v < top(G,H). */
778 if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
779 r = cuddUniqueInter(dd, (int) f->index, g, h);
780 return(Cudd_NotCond(r,comple && r != NULL));
781 }
782
783 /* Check cache. */
784 r = cuddCacheLookup(dd, DD_BDD_ITE_TAG, f, g, h);
785 if (r != NULL) {
786 return(Cudd_NotCond(r,comple));
787 }
788
789 checkWhetherToGiveUp(dd);
790
791 /* Compute cofactors. */
792 index = f->index;
793 if (topf <= v) {
794 v = ddMin(topf, v); /* v = top_var(F,G,H) */
795 Fv = cuddT(f); Fnv = cuddE(f);
796 } else {
797 Fv = Fnv = f;
798 }
799 if (topg == v) {
800 index = g->index;
801 Gv = cuddT(g); Gnv = cuddE(g);
802 } else {
803 Gv = Gnv = g;
804 }
805 if (toph == v) {
806 H = Cudd_Regular(h);
807 index = H->index;
808 Hv = cuddT(H); Hnv = cuddE(H);
809 if (Cudd_IsComplement(h)) {
810 Hv = Cudd_Not(Hv);
811 Hnv = Cudd_Not(Hnv);
812 }
813 } else {
814 Hv = Hnv = h;
815 }
816
817 /* Recursive step. */
818 t = cuddBddIteRecur(dd,Fv,Gv,Hv);
819 if (t == NULL) return(NULL);
820 cuddRef(t);
821
822 e = cuddBddIteRecur(dd,Fnv,Gnv,Hnv);
823 if (e == NULL) {
824 Cudd_IterDerefBdd(dd,t);
825 return(NULL);
826 }
827 cuddRef(e);
828
829 r = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
830 if (r == NULL) {
831 Cudd_IterDerefBdd(dd,t);
832 Cudd_IterDerefBdd(dd,e);
833 return(NULL);
834 }
835 cuddDeref(t);
836 cuddDeref(e);
837
838 cuddCacheInsert(dd, DD_BDD_ITE_TAG, f, g, h, r);
839 return(Cudd_NotCond(r,comple));
840
841 } /* end of cuddBddIteRecur */
842
843
844 /**
845 @brief Implements the recursive step of Cudd_bddIntersect.
846
847 @sideeffect None
848
849 @see Cudd_bddIntersect
850
851 */
852 DdNode *
cuddBddIntersectRecur(DdManager * dd,DdNode * f,DdNode * g)853 cuddBddIntersectRecur(
854 DdManager * dd,
855 DdNode * f,
856 DdNode * g)
857 {
858 DdNode *res;
859 DdNode *F, *G, *t, *e;
860 DdNode *fv, *fnv, *gv, *gnv;
861 DdNode *one, *zero;
862 unsigned int index;
863 int topf, topg;
864
865 statLine(dd);
866 one = DD_ONE(dd);
867 zero = Cudd_Not(one);
868
869 /* Terminal cases. */
870 if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
871 if (f == g || g == one) return(f);
872 if (f == one) return(g);
873
874 /* At this point f and g are not constant. */
875 if (f > g) { DdNode *tmp = f; f = g; g = tmp; }
876 res = cuddCacheLookup2(dd,Cudd_bddIntersect,f,g);
877 if (res != NULL) return(res);
878
879 checkWhetherToGiveUp(dd);
880
881 /* Find splitting variable. Here we can skip the use of cuddI,
882 ** because the operands are known to be non-constant.
883 */
884 F = Cudd_Regular(f);
885 topf = dd->perm[F->index];
886 G = Cudd_Regular(g);
887 topg = dd->perm[G->index];
888
889 /* Compute cofactors. */
890 if (topf <= topg) {
891 index = F->index;
892 fv = cuddT(F);
893 fnv = cuddE(F);
894 if (Cudd_IsComplement(f)) {
895 fv = Cudd_Not(fv);
896 fnv = Cudd_Not(fnv);
897 }
898 } else {
899 index = G->index;
900 fv = fnv = f;
901 }
902
903 if (topg <= topf) {
904 gv = cuddT(G);
905 gnv = cuddE(G);
906 if (Cudd_IsComplement(g)) {
907 gv = Cudd_Not(gv);
908 gnv = Cudd_Not(gnv);
909 }
910 } else {
911 gv = gnv = g;
912 }
913
914 /* Compute partial results. */
915 t = cuddBddIntersectRecur(dd,fv,gv);
916 if (t == NULL) return(NULL);
917 cuddRef(t);
918 if (t != zero) {
919 e = zero;
920 } else {
921 e = cuddBddIntersectRecur(dd,fnv,gnv);
922 if (e == NULL) {
923 Cudd_IterDerefBdd(dd, t);
924 return(NULL);
925 }
926 }
927 cuddRef(e);
928
929 if (t == e) { /* both equal zero */
930 res = t;
931 } else if (Cudd_IsComplement(t)) {
932 res = cuddUniqueInter(dd,(int)index,Cudd_Not(t),Cudd_Not(e));
933 if (res == NULL) {
934 Cudd_IterDerefBdd(dd, t);
935 Cudd_IterDerefBdd(dd, e);
936 return(NULL);
937 }
938 res = Cudd_Not(res);
939 } else {
940 res = cuddUniqueInter(dd,(int)index,t,e);
941 if (res == NULL) {
942 Cudd_IterDerefBdd(dd, t);
943 Cudd_IterDerefBdd(dd, e);
944 return(NULL);
945 }
946 }
947 cuddDeref(e);
948 cuddDeref(t);
949
950 cuddCacheInsert2(dd,Cudd_bddIntersect,f,g,res);
951
952 return(res);
953
954 } /* end of cuddBddIntersectRecur */
955
956
957 /**
958 @brief Implements the recursive step of Cudd_bddAnd.
959
960 @details Takes the conjunction of two BDDs.
961
962 @return a pointer to the result is successful; NULL otherwise.
963
964 @sideeffect None
965
966 @see Cudd_bddAnd
967
968 */
969 DdNode *
cuddBddAndRecur(DdManager * manager,DdNode * f,DdNode * g)970 cuddBddAndRecur(
971 DdManager * manager,
972 DdNode * f,
973 DdNode * g)
974 {
975 DdNode *F, *fv, *fnv, *G, *gv, *gnv;
976 DdNode *one, *r, *t, *e;
977 int topf, topg;
978 unsigned int index;
979
980 statLine(manager);
981 one = DD_ONE(manager);
982
983 /* Terminal cases. */
984 F = Cudd_Regular(f);
985 G = Cudd_Regular(g);
986 if (F == G) {
987 if (f == g) return(f);
988 else return(Cudd_Not(one));
989 }
990 if (F == one) {
991 if (f == one) return(g);
992 else return(f);
993 }
994 if (G == one) {
995 if (g == one) return(f);
996 else return(g);
997 }
998
999 /* At this point f and g are not constant. */
1000 if (f > g) { /* Try to increase cache efficiency. */
1001 DdNode *tmp = f;
1002 f = g;
1003 g = tmp;
1004 F = Cudd_Regular(f);
1005 G = Cudd_Regular(g);
1006 }
1007
1008 /* Check cache. */
1009 if (F->ref != 1 || G->ref != 1) {
1010 r = cuddCacheLookup2(manager, Cudd_bddAnd, f, g);
1011 if (r != NULL) return(r);
1012 }
1013
1014 checkWhetherToGiveUp(manager);
1015
1016 /* Here we can skip the use of cuddI, because the operands are known
1017 ** to be non-constant.
1018 */
1019 topf = manager->perm[F->index];
1020 topg = manager->perm[G->index];
1021
1022 /* Compute cofactors. */
1023 if (topf <= topg) {
1024 index = F->index;
1025 fv = cuddT(F);
1026 fnv = cuddE(F);
1027 if (Cudd_IsComplement(f)) {
1028 fv = Cudd_Not(fv);
1029 fnv = Cudd_Not(fnv);
1030 }
1031 } else {
1032 index = G->index;
1033 fv = fnv = f;
1034 }
1035
1036 if (topg <= topf) {
1037 gv = cuddT(G);
1038 gnv = cuddE(G);
1039 if (Cudd_IsComplement(g)) {
1040 gv = Cudd_Not(gv);
1041 gnv = Cudd_Not(gnv);
1042 }
1043 } else {
1044 gv = gnv = g;
1045 }
1046
1047 t = cuddBddAndRecur(manager, fv, gv);
1048 if (t == NULL) return(NULL);
1049 cuddRef(t);
1050
1051 e = cuddBddAndRecur(manager, fnv, gnv);
1052 if (e == NULL) {
1053 Cudd_IterDerefBdd(manager, t);
1054 return(NULL);
1055 }
1056 cuddRef(e);
1057
1058 if (t == e) {
1059 r = t;
1060 } else {
1061 if (Cudd_IsComplement(t)) {
1062 r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
1063 if (r == NULL) {
1064 Cudd_IterDerefBdd(manager, t);
1065 Cudd_IterDerefBdd(manager, e);
1066 return(NULL);
1067 }
1068 r = Cudd_Not(r);
1069 } else {
1070 r = cuddUniqueInter(manager,(int)index,t,e);
1071 if (r == NULL) {
1072 Cudd_IterDerefBdd(manager, t);
1073 Cudd_IterDerefBdd(manager, e);
1074 return(NULL);
1075 }
1076 }
1077 }
1078 cuddDeref(e);
1079 cuddDeref(t);
1080 if (F->ref != 1 || G->ref != 1)
1081 cuddCacheInsert2(manager, Cudd_bddAnd, f, g, r);
1082 return(r);
1083
1084 } /* end of cuddBddAndRecur */
1085
1086
1087 /**
1088 @brief Implements the recursive step of Cudd_bddXor.
1089
1090 @details Takes the exclusive OR of two BDDs.
1091
1092 @return a pointer to the result is successful; NULL otherwise.
1093
1094 @sideeffect None
1095
1096 @see Cudd_bddXor
1097
1098 */
1099 DdNode *
cuddBddXorRecur(DdManager * manager,DdNode * f,DdNode * g)1100 cuddBddXorRecur(
1101 DdManager * manager,
1102 DdNode * f,
1103 DdNode * g)
1104 {
1105 DdNode *fv, *fnv, *G, *gv, *gnv;
1106 DdNode *one, *zero, *r, *t, *e;
1107 int topf, topg;
1108 unsigned int index;
1109
1110 statLine(manager);
1111 one = DD_ONE(manager);
1112 zero = Cudd_Not(one);
1113
1114 /* Terminal cases. */
1115 if (f == g) return(zero);
1116 if (f == Cudd_Not(g)) return(one);
1117 if (f > g) { /* Try to increase cache efficiency and simplify tests. */
1118 DdNode *tmp = f;
1119 f = g;
1120 g = tmp;
1121 }
1122 if (g == zero) return(f);
1123 if (g == one) return(Cudd_Not(f));
1124 if (Cudd_IsComplement(f)) {
1125 f = Cudd_Not(f);
1126 g = Cudd_Not(g);
1127 }
1128 /* Now the first argument is regular. */
1129 if (f == one) return(Cudd_Not(g));
1130
1131 /* At this point f and g are not constant. */
1132
1133 /* Check cache. */
1134 r = cuddCacheLookup2(manager, Cudd_bddXor, f, g);
1135 if (r != NULL) return(r);
1136
1137 checkWhetherToGiveUp(manager);
1138
1139 /* Here we can skip the use of cuddI, because the operands are known
1140 ** to be non-constant.
1141 */
1142 topf = manager->perm[f->index];
1143 G = Cudd_Regular(g);
1144 topg = manager->perm[G->index];
1145
1146 /* Compute cofactors. */
1147 if (topf <= topg) {
1148 index = f->index;
1149 fv = cuddT(f);
1150 fnv = cuddE(f);
1151 } else {
1152 index = G->index;
1153 fv = fnv = f;
1154 }
1155
1156 if (topg <= topf) {
1157 gv = cuddT(G);
1158 gnv = cuddE(G);
1159 if (Cudd_IsComplement(g)) {
1160 gv = Cudd_Not(gv);
1161 gnv = Cudd_Not(gnv);
1162 }
1163 } else {
1164 gv = gnv = g;
1165 }
1166
1167 t = cuddBddXorRecur(manager, fv, gv);
1168 if (t == NULL) return(NULL);
1169 cuddRef(t);
1170
1171 e = cuddBddXorRecur(manager, fnv, gnv);
1172 if (e == NULL) {
1173 Cudd_IterDerefBdd(manager, t);
1174 return(NULL);
1175 }
1176 cuddRef(e);
1177
1178 if (t == e) {
1179 r = t;
1180 } else {
1181 if (Cudd_IsComplement(t)) {
1182 r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
1183 if (r == NULL) {
1184 Cudd_IterDerefBdd(manager, t);
1185 Cudd_IterDerefBdd(manager, e);
1186 return(NULL);
1187 }
1188 r = Cudd_Not(r);
1189 } else {
1190 r = cuddUniqueInter(manager,(int)index,t,e);
1191 if (r == NULL) {
1192 Cudd_IterDerefBdd(manager, t);
1193 Cudd_IterDerefBdd(manager, e);
1194 return(NULL);
1195 }
1196 }
1197 }
1198 cuddDeref(e);
1199 cuddDeref(t);
1200 cuddCacheInsert2(manager, Cudd_bddXor, f, g, r);
1201 return(r);
1202
1203 } /* end of cuddBddXorRecur */
1204
1205
1206 /*---------------------------------------------------------------------------*/
1207 /* Definition of static functions */
1208 /*---------------------------------------------------------------------------*/
1209
1210
1211 /**
1212 @brief Replaces variables with constants if possible.
1213
1214 @details This function performs part of the transformation to
1215 standard form by replacing variables with constants if possible.
1216
1217 @sideeffect None
1218
1219 @see bddVarToCanonical bddVarToCanonicalSimple
1220
1221 */
1222 static void
bddVarToConst(DdNode * f,DdNode ** gp,DdNode ** hp,DdNode * one)1223 bddVarToConst(
1224 DdNode * f,
1225 DdNode ** gp,
1226 DdNode ** hp,
1227 DdNode * one)
1228 {
1229 DdNode *g = *gp;
1230 DdNode *h = *hp;
1231
1232 if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
1233 *gp = one;
1234 } else if (f == Cudd_Not(g)) { /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */
1235 *gp = Cudd_Not(one);
1236 }
1237 if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
1238 *hp = Cudd_Not(one);
1239 } else if (f == Cudd_Not(h)) { /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */
1240 *hp = one;
1241 }
1242
1243 } /* end of bddVarToConst */
1244
1245
1246 /**
1247 @brief Picks unique member from equiv expressions.
1248
1249 @details Reduces 2 variable expressions to canonical form.
1250
1251 @sideeffect None
1252
1253 @see bddVarToConst bddVarToCanonicalSimple
1254
1255 */
1256 static int
bddVarToCanonical(DdManager * dd,DdNode ** fp,DdNode ** gp,DdNode ** hp,int * topfp,int * topgp,int * tophp)1257 bddVarToCanonical(
1258 DdManager * dd,
1259 DdNode ** fp,
1260 DdNode ** gp,
1261 DdNode ** hp,
1262 int * topfp,
1263 int * topgp,
1264 int * tophp)
1265 {
1266 DdNode *F, *G, *H, *r, *f, *g, *h;
1267 DdNode *one = dd->one;
1268 int topf, topg, toph;
1269 int comple, change;
1270
1271 f = *fp;
1272 g = *gp;
1273 h = *hp;
1274 F = Cudd_Regular(f);
1275 G = Cudd_Regular(g);
1276 H = Cudd_Regular(h);
1277 topf = cuddI(dd,F->index);
1278 topg = cuddI(dd,G->index);
1279 toph = cuddI(dd,H->index);
1280
1281 change = 0;
1282
1283 if (G == one) { /* ITE(F,c,H) */
1284 if ((topf > toph) || (topf == toph && f > h)) {
1285 r = h;
1286 h = f;
1287 f = r; /* ITE(F,1,H) = ITE(H,1,F) */
1288 if (g != one) { /* g == zero */
1289 f = Cudd_Not(f); /* ITE(F,0,H) = ITE(!H,0,!F) */
1290 h = Cudd_Not(h);
1291 }
1292 change = 1;
1293 }
1294 } else if (H == one) { /* ITE(F,G,c) */
1295 if ((topf > topg) || (topf == topg && f > g)) {
1296 r = g;
1297 g = f;
1298 f = r; /* ITE(F,G,0) = ITE(G,F,0) */
1299 if (h == one) {
1300 f = Cudd_Not(f); /* ITE(F,G,1) = ITE(!G,!F,1) */
1301 g = Cudd_Not(g);
1302 }
1303 change = 1;
1304 }
1305 } else if (g == Cudd_Not(h)) { /* ITE(F,G,!G) = ITE(G,F,!F) */
1306 if ((topf > topg) || (topf == topg && f > g)) {
1307 r = f;
1308 f = g;
1309 g = r;
1310 h = Cudd_Not(r);
1311 change = 1;
1312 }
1313 }
1314 /* adjust pointers so that the first 2 arguments to ITE are regular */
1315 if (Cudd_IsComplement(f) != 0) { /* ITE(!F,G,H) = ITE(F,H,G) */
1316 f = Cudd_Not(f);
1317 r = g;
1318 g = h;
1319 h = r;
1320 change = 1;
1321 }
1322 comple = 0;
1323 if (Cudd_IsComplement(g) != 0) { /* ITE(F,!G,H) = !ITE(F,G,!H) */
1324 g = Cudd_Not(g);
1325 h = Cudd_Not(h);
1326 change = 1;
1327 comple = 1;
1328 }
1329 if (change != 0) {
1330 *fp = f;
1331 *gp = g;
1332 *hp = h;
1333 }
1334 *topfp = cuddI(dd,f->index);
1335 *topgp = cuddI(dd,g->index);
1336 *tophp = cuddI(dd,Cudd_Regular(h)->index);
1337
1338 return(comple);
1339
1340 } /* end of bddVarToCanonical */
1341
1342
1343 /**
1344 @brief Picks unique member from equiv expressions.
1345
1346 @details Makes sure the first two pointers are regular. This
1347 mat require the complementation of the result, which is signaled by
1348 returning 1 instead of 0. This function is simpler than the general
1349 case because it assumes that no two arguments are the same or
1350 complementary, and no argument is constant.
1351
1352 @sideeffect None
1353
1354 @see bddVarToConst bddVarToCanonical
1355
1356 */
1357 static int
bddVarToCanonicalSimple(DdManager * dd,DdNode ** fp,DdNode ** gp,DdNode ** hp,int * topfp,int * topgp,int * tophp)1358 bddVarToCanonicalSimple(
1359 DdManager * dd,
1360 DdNode ** fp,
1361 DdNode ** gp,
1362 DdNode ** hp,
1363 int * topfp,
1364 int * topgp,
1365 int * tophp)
1366 {
1367 DdNode *r, *f, *g, *h;
1368 int comple, change;
1369
1370 f = *fp;
1371 g = *gp;
1372 h = *hp;
1373
1374 change = 0;
1375
1376 /* adjust pointers so that the first 2 arguments to ITE are regular */
1377 if (Cudd_IsComplement(f)) { /* ITE(!F,G,H) = ITE(F,H,G) */
1378 f = Cudd_Not(f);
1379 r = g;
1380 g = h;
1381 h = r;
1382 change = 1;
1383 }
1384 comple = 0;
1385 if (Cudd_IsComplement(g)) { /* ITE(F,!G,H) = !ITE(F,G,!H) */
1386 g = Cudd_Not(g);
1387 h = Cudd_Not(h);
1388 change = 1;
1389 comple = 1;
1390 }
1391 if (change) {
1392 *fp = f;
1393 *gp = g;
1394 *hp = h;
1395 }
1396
1397 /* Here we can skip the use of cuddI, because the operands are known
1398 ** to be non-constant.
1399 */
1400 *topfp = dd->perm[f->index];
1401 *topgp = dd->perm[g->index];
1402 *tophp = dd->perm[Cudd_Regular(h)->index];
1403
1404 return(comple);
1405
1406 } /* end of bddVarToCanonicalSimple */
1407