1 /**CFile***********************************************************************
2
3 FileName [cuddAddIte.c]
4
5 PackageName [cudd]
6
7 Synopsis [ADD ITE function and satellites.]
8
9 Description [External procedures included in this module:
10 <ul>
11 <li> Cudd_addIte()
12 <li> Cudd_addIteConstant()
13 <li> Cudd_addEvalConst()
14 <li> Cudd_addCmpl()
15 <li> Cudd_addLeq()
16 </ul>
17 Internal procedures included in this module:
18 <ul>
19 <li> cuddAddIteRecur()
20 <li> cuddAddCmplRecur()
21 </ul>
22 Static procedures included in this module:
23 <ul>
24 <li> addVarToConst()
25 </ul>]
26
27 Author [Fabio Somenzi]
28
29 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
30
31 All rights reserved.
32
33 Redistribution and use in source and binary forms, with or without
34 modification, are permitted provided that the following conditions
35 are met:
36
37 Redistributions of source code must retain the above copyright
38 notice, this list of conditions and the following disclaimer.
39
40 Redistributions in binary form must reproduce the above copyright
41 notice, this list of conditions and the following disclaimer in the
42 documentation and/or other materials provided with the distribution.
43
44 Neither the name of the University of Colorado nor the names of its
45 contributors may be used to endorse or promote products derived from
46 this software without specific prior written permission.
47
48 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
49 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
50 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
51 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
52 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
53 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
54 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
55 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
56 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
57 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
58 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
59 POSSIBILITY OF SUCH DAMAGE.]
60
61 ******************************************************************************/
62
63 #include "misc/util/util_hack.h"
64 #include "cuddInt.h"
65
66 ABC_NAMESPACE_IMPL_START
67
68
69
70 /*---------------------------------------------------------------------------*/
71 /* Constant declarations */
72 /*---------------------------------------------------------------------------*/
73
74
75 /*---------------------------------------------------------------------------*/
76 /* Stucture declarations */
77 /*---------------------------------------------------------------------------*/
78
79
80 /*---------------------------------------------------------------------------*/
81 /* Type declarations */
82 /*---------------------------------------------------------------------------*/
83
84
85 /*---------------------------------------------------------------------------*/
86 /* Variable declarations */
87 /*---------------------------------------------------------------------------*/
88
89 #ifndef lint
90 static char rcsid[] DD_UNUSED = "$Id: cuddAddIte.c,v 1.15 2004/08/13 18:04:45 fabio Exp $";
91 #endif
92
93
94 /*---------------------------------------------------------------------------*/
95 /* Macro declarations */
96 /*---------------------------------------------------------------------------*/
97
98
99 /**AutomaticStart*************************************************************/
100
101 /*---------------------------------------------------------------------------*/
102 /* Static function prototypes */
103 /*---------------------------------------------------------------------------*/
104
105 static void addVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one, DdNode *zero);
106
107 /**AutomaticEnd***************************************************************/
108
109
110 /*---------------------------------------------------------------------------*/
111 /* Definition of exported functions */
112 /*---------------------------------------------------------------------------*/
113
114
115 /**Function********************************************************************
116
117 Synopsis [Implements ITE(f,g,h).]
118
119 Description [Implements ITE(f,g,h). This procedure assumes that f is
120 a 0-1 ADD. Returns a pointer to the resulting ADD if successful; NULL
121 otherwise.]
122
123 SideEffects [None]
124
125 SeeAlso [Cudd_bddIte Cudd_addIteConstant Cudd_addApply]
126
127 ******************************************************************************/
128 DdNode *
Cudd_addIte(DdManager * dd,DdNode * f,DdNode * g,DdNode * h)129 Cudd_addIte(
130 DdManager * dd,
131 DdNode * f,
132 DdNode * g,
133 DdNode * h)
134 {
135 DdNode *res;
136
137 do {
138 dd->reordered = 0;
139 res = cuddAddIteRecur(dd,f,g,h);
140 } while (dd->reordered == 1);
141 return(res);
142
143 } /* end of Cudd_addIte */
144
145
146 /**Function********************************************************************
147
148 Synopsis [Implements ITEconstant for ADDs.]
149
150 Description [Implements ITEconstant for ADDs. f must be a 0-1 ADD.
151 Returns a pointer to the resulting ADD (which may or may not be
152 constant) or DD_NON_CONSTANT. No new nodes are created. This function
153 can be used, for instance, to check that g has a constant value
154 (specified by h) whenever f is 1. If the constant value is unknown,
155 then one should use Cudd_addEvalConst.]
156
157 SideEffects [None]
158
159 SeeAlso [Cudd_addIte Cudd_addEvalConst Cudd_bddIteConstant]
160
161 ******************************************************************************/
162 DdNode *
Cudd_addIteConstant(DdManager * dd,DdNode * f,DdNode * g,DdNode * h)163 Cudd_addIteConstant(
164 DdManager * dd,
165 DdNode * f,
166 DdNode * g,
167 DdNode * h)
168 {
169 DdNode *one,*zero;
170 DdNode *Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*r,*t,*e;
171 unsigned int topf,topg,toph,v;
172
173 statLine(dd);
174 /* Trivial cases. */
175 if (f == (one = DD_ONE(dd))) { /* ITE(1,G,H) = G */
176 return(g);
177 }
178 if (f == (zero = DD_ZERO(dd))) { /* ITE(0,G,H) = H */
179 return(h);
180 }
181
182 /* From now on, f is known not to be a constant. */
183 addVarToConst(f,&g,&h,one,zero);
184
185 /* Check remaining one variable cases. */
186 if (g == h) { /* ITE(F,G,G) = G */
187 return(g);
188 }
189 if (cuddIsConstant(g) && cuddIsConstant(h)) {
190 return(DD_NON_CONSTANT);
191 }
192
193 topf = cuddI(dd,f->index);
194 topg = cuddI(dd,g->index);
195 toph = cuddI(dd,h->index);
196 v = ddMin(topg,toph);
197
198 /* ITE(F,G,H) = (x,G,H) (non constant) if F = (x,1,0), x < top(G,H). */
199 if (topf < v && cuddIsConstant(cuddT(f)) && cuddIsConstant(cuddE(f))) {
200 return(DD_NON_CONSTANT);
201 }
202
203 /* Check cache. */
204 r = cuddConstantLookup(dd,DD_ADD_ITE_CONSTANT_TAG,f,g,h);
205 if (r != NULL) {
206 return(r);
207 }
208
209 /* Compute cofactors. */
210 if (topf <= v) {
211 v = ddMin(topf,v); /* v = top_var(F,G,H) */
212 Fv = cuddT(f); Fnv = cuddE(f);
213 } else {
214 Fv = Fnv = f;
215 }
216 if (topg == v) {
217 Gv = cuddT(g); Gnv = cuddE(g);
218 } else {
219 Gv = Gnv = g;
220 }
221 if (toph == v) {
222 Hv = cuddT(h); Hnv = cuddE(h);
223 } else {
224 Hv = Hnv = h;
225 }
226
227 /* Recursive step. */
228 t = Cudd_addIteConstant(dd,Fv,Gv,Hv);
229 if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
230 cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
231 return(DD_NON_CONSTANT);
232 }
233 e = Cudd_addIteConstant(dd,Fnv,Gnv,Hnv);
234 if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {
235 cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
236 return(DD_NON_CONSTANT);
237 }
238 cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, t);
239 return(t);
240
241 } /* end of Cudd_addIteConstant */
242
243
244 /**Function********************************************************************
245
246 Synopsis [Checks whether ADD g is constant whenever ADD f is 1.]
247
248 Description [Checks whether ADD g is constant whenever ADD f is 1. f
249 must be a 0-1 ADD. Returns a pointer to the resulting ADD (which may
250 or may not be constant) or DD_NON_CONSTANT. If f is identically 0,
251 the check is assumed to be successful, and the background value is
252 returned. No new nodes are created.]
253
254 SideEffects [None]
255
256 SeeAlso [Cudd_addIteConstant Cudd_addLeq]
257
258 ******************************************************************************/
259 DdNode *
Cudd_addEvalConst(DdManager * dd,DdNode * f,DdNode * g)260 Cudd_addEvalConst(
261 DdManager * dd,
262 DdNode * f,
263 DdNode * g)
264 {
265 DdNode *zero;
266 DdNode *Fv,*Fnv,*Gv,*Gnv,*r,*t,*e;
267 unsigned int topf,topg;
268
269 #ifdef DD_DEBUG
270 assert(!Cudd_IsComplement(f));
271 #endif
272
273 statLine(dd);
274 /* Terminal cases. */
275 if (f == DD_ONE(dd) || cuddIsConstant(g)) {
276 return(g);
277 }
278 if (f == (zero = DD_ZERO(dd))) {
279 return(dd->background);
280 }
281
282 #ifdef DD_DEBUG
283 assert(!cuddIsConstant(f));
284 #endif
285 /* From now on, f and g are known not to be constants. */
286
287 topf = cuddI(dd,f->index);
288 topg = cuddI(dd,g->index);
289
290 /* Check cache. */
291 r = cuddConstantLookup(dd,DD_ADD_EVAL_CONST_TAG,f,g,g);
292 if (r != NULL) {
293 return(r);
294 }
295
296 /* Compute cofactors. */
297 if (topf <= topg) {
298 Fv = cuddT(f); Fnv = cuddE(f);
299 } else {
300 Fv = Fnv = f;
301 }
302 if (topg <= topf) {
303 Gv = cuddT(g); Gnv = cuddE(g);
304 } else {
305 Gv = Gnv = g;
306 }
307
308 /* Recursive step. */
309 if (Fv != zero) {
310 t = Cudd_addEvalConst(dd,Fv,Gv);
311 if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
312 cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
313 return(DD_NON_CONSTANT);
314 }
315 if (Fnv != zero) {
316 e = Cudd_addEvalConst(dd,Fnv,Gnv);
317 if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {
318 cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
319 return(DD_NON_CONSTANT);
320 }
321 }
322 cuddCacheInsert2(dd,Cudd_addEvalConst,f,g,t);
323 return(t);
324 } else { /* Fnv must be != zero */
325 e = Cudd_addEvalConst(dd,Fnv,Gnv);
326 cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, e);
327 return(e);
328 }
329
330 } /* end of Cudd_addEvalConst */
331
332
333 /**Function********************************************************************
334
335 Synopsis [Computes the complement of an ADD a la C language.]
336
337 Description [Computes the complement of an ADD a la C language: The
338 complement of 0 is 1 and the complement of everything else is 0.
339 Returns a pointer to the resulting ADD if successful; NULL otherwise.]
340
341 SideEffects [None]
342
343 SeeAlso [Cudd_addNegate]
344
345 ******************************************************************************/
346 DdNode *
Cudd_addCmpl(DdManager * dd,DdNode * f)347 Cudd_addCmpl(
348 DdManager * dd,
349 DdNode * f)
350 {
351 DdNode *res;
352
353 do {
354 dd->reordered = 0;
355 res = cuddAddCmplRecur(dd,f);
356 } while (dd->reordered == 1);
357 return(res);
358
359 } /* end of Cudd_addCmpl */
360
361
362 /**Function********************************************************************
363
364 Synopsis [Determines whether f is less than or equal to g.]
365
366 Description [Returns 1 if f is less than or equal to g; 0 otherwise.
367 No new nodes are created. This procedure works for arbitrary ADDs.
368 For 0-1 ADDs Cudd_addEvalConst is more efficient.]
369
370 SideEffects [None]
371
372 SeeAlso [Cudd_addIteConstant Cudd_addEvalConst Cudd_bddLeq]
373
374 ******************************************************************************/
375 int
Cudd_addLeq(DdManager * dd,DdNode * f,DdNode * g)376 Cudd_addLeq(
377 DdManager * dd,
378 DdNode * f,
379 DdNode * g)
380 {
381 DdNode *tmp, *fv, *fvn, *gv, *gvn;
382 unsigned int topf, topg, res;
383
384 /* Terminal cases. */
385 if (f == g) return(1);
386
387 statLine(dd);
388 if (cuddIsConstant(f)) {
389 if (cuddIsConstant(g)) return(cuddV(f) <= cuddV(g));
390 if (f == DD_MINUS_INFINITY(dd)) return(1);
391 if (f == DD_PLUS_INFINITY(dd)) return(0); /* since f != g */
392 }
393 if (g == DD_PLUS_INFINITY(dd)) return(1);
394 if (g == DD_MINUS_INFINITY(dd)) return(0); /* since f != g */
395
396 /* Check cache. */
397 tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_addLeq,f,g);
398 if (tmp != NULL) {
399 return(tmp == DD_ONE(dd));
400 }
401
402 /* Compute cofactors. One of f and g is not constant. */
403 topf = cuddI(dd,f->index);
404 topg = cuddI(dd,g->index);
405 if (topf <= topg) {
406 fv = cuddT(f); fvn = cuddE(f);
407 } else {
408 fv = fvn = f;
409 }
410 if (topg <= topf) {
411 gv = cuddT(g); gvn = cuddE(g);
412 } else {
413 gv = gvn = g;
414 }
415
416 res = Cudd_addLeq(dd,fvn,gvn) && Cudd_addLeq(dd,fv,gv);
417
418 /* Store result in cache and return. */
419 cuddCacheInsert2(dd,(DD_CTFP) Cudd_addLeq,f,g,
420 Cudd_NotCond(DD_ONE(dd),res==0));
421 return(res);
422
423 } /* end of Cudd_addLeq */
424
425
426 /*---------------------------------------------------------------------------*/
427 /* Definition of internal functions */
428 /*---------------------------------------------------------------------------*/
429
430
431 /**Function********************************************************************
432
433 Synopsis [Implements the recursive step of Cudd_addIte(f,g,h).]
434
435 Description [Implements the recursive step of Cudd_addIte(f,g,h).
436 Returns a pointer to the resulting ADD if successful; NULL
437 otherwise.]
438
439 SideEffects [None]
440
441 SeeAlso [Cudd_addIte]
442
443 ******************************************************************************/
444 DdNode *
cuddAddIteRecur(DdManager * dd,DdNode * f,DdNode * g,DdNode * h)445 cuddAddIteRecur(
446 DdManager * dd,
447 DdNode * f,
448 DdNode * g,
449 DdNode * h)
450 {
451 DdNode *one,*zero;
452 DdNode *r,*Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*t,*e;
453 unsigned int topf,topg,toph,v;
454 int index = -1;
455
456 statLine(dd);
457 /* Trivial cases. */
458
459 /* One variable cases. */
460 if (f == (one = DD_ONE(dd))) { /* ITE(1,G,H) = G */
461 return(g);
462 }
463 if (f == (zero = DD_ZERO(dd))) { /* ITE(0,G,H) = H */
464 return(h);
465 }
466
467 /* From now on, f is known to not be a constant. */
468 addVarToConst(f,&g,&h,one,zero);
469
470 /* Check remaining one variable cases. */
471 if (g == h) { /* ITE(F,G,G) = G */
472 return(g);
473 }
474
475 if (g == one) { /* ITE(F,1,0) = F */
476 if (h == zero) return(f);
477 }
478
479 topf = cuddI(dd,f->index);
480 topg = cuddI(dd,g->index);
481 toph = cuddI(dd,h->index);
482 v = ddMin(topg,toph);
483
484 /* A shortcut: ITE(F,G,H) = (x,G,H) if F=(x,1,0), x < top(G,H). */
485 if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
486 r = cuddUniqueInter(dd,(int)f->index,g,h);
487 return(r);
488 }
489 if (topf < v && cuddT(f) == zero && cuddE(f) == one) {
490 r = cuddUniqueInter(dd,(int)f->index,h,g);
491 return(r);
492 }
493
494 /* Check cache. */
495 r = cuddCacheLookup(dd,DD_ADD_ITE_TAG,f,g,h);
496 if (r != NULL) {
497 return(r);
498 }
499
500 /* Compute cofactors. */
501 if (topf <= v) {
502 v = ddMin(topf,v); /* v = top_var(F,G,H) */
503 index = f->index;
504 Fv = cuddT(f); Fnv = cuddE(f);
505 } else {
506 Fv = Fnv = f;
507 }
508 if (topg == v) {
509 index = g->index;
510 Gv = cuddT(g); Gnv = cuddE(g);
511 } else {
512 Gv = Gnv = g;
513 }
514 if (toph == v) {
515 index = h->index;
516 Hv = cuddT(h); Hnv = cuddE(h);
517 } else {
518 Hv = Hnv = h;
519 }
520
521 /* Recursive step. */
522 t = cuddAddIteRecur(dd,Fv,Gv,Hv);
523 if (t == NULL) return(NULL);
524 cuddRef(t);
525
526 e = cuddAddIteRecur(dd,Fnv,Gnv,Hnv);
527 if (e == NULL) {
528 Cudd_RecursiveDeref(dd,t);
529 return(NULL);
530 }
531 cuddRef(e);
532
533 r = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
534 if (r == NULL) {
535 Cudd_RecursiveDeref(dd,t);
536 Cudd_RecursiveDeref(dd,e);
537 return(NULL);
538 }
539 cuddDeref(t);
540 cuddDeref(e);
541
542 cuddCacheInsert(dd,DD_ADD_ITE_TAG,f,g,h,r);
543
544 return(r);
545
546 } /* end of cuddAddIteRecur */
547
548
549 /**Function********************************************************************
550
551 Synopsis [Performs the recursive step of Cudd_addCmpl.]
552
553 Description [Performs the recursive step of Cudd_addCmpl. Returns a
554 pointer to the resulting ADD if successful; NULL otherwise.]
555
556 SideEffects [None]
557
558 SeeAlso [Cudd_addCmpl]
559
560 ******************************************************************************/
561 DdNode *
cuddAddCmplRecur(DdManager * dd,DdNode * f)562 cuddAddCmplRecur(
563 DdManager * dd,
564 DdNode * f)
565 {
566 DdNode *one,*zero;
567 DdNode *r,*Fv,*Fnv,*t,*e;
568
569 statLine(dd);
570 one = DD_ONE(dd);
571 zero = DD_ZERO(dd);
572
573 if (cuddIsConstant(f)) {
574 if (f == zero) {
575 return(one);
576 } else {
577 return(zero);
578 }
579 }
580 r = cuddCacheLookup1(dd,Cudd_addCmpl,f);
581 if (r != NULL) {
582 return(r);
583 }
584 Fv = cuddT(f);
585 Fnv = cuddE(f);
586 t = cuddAddCmplRecur(dd,Fv);
587 if (t == NULL) return(NULL);
588 cuddRef(t);
589 e = cuddAddCmplRecur(dd,Fnv);
590 if (e == NULL) {
591 Cudd_RecursiveDeref(dd,t);
592 return(NULL);
593 }
594 cuddRef(e);
595 r = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
596 if (r == NULL) {
597 Cudd_RecursiveDeref(dd, t);
598 Cudd_RecursiveDeref(dd, e);
599 return(NULL);
600 }
601 cuddDeref(t);
602 cuddDeref(e);
603 cuddCacheInsert1(dd,Cudd_addCmpl,f,r);
604 return(r);
605
606 } /* end of cuddAddCmplRecur */
607
608
609 /*---------------------------------------------------------------------------*/
610 /* Definition of static functions */
611 /*---------------------------------------------------------------------------*/
612
613
614 /**Function********************************************************************
615
616 Synopsis [Replaces variables with constants if possible (part of
617 canonical form).]
618
619 Description []
620
621 SideEffects [None]
622
623 ******************************************************************************/
624 static void
addVarToConst(DdNode * f,DdNode ** gp,DdNode ** hp,DdNode * one,DdNode * zero)625 addVarToConst(
626 DdNode * f,
627 DdNode ** gp,
628 DdNode ** hp,
629 DdNode * one,
630 DdNode * zero)
631 {
632 DdNode *g = *gp;
633 DdNode *h = *hp;
634
635 if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
636 *gp = one;
637 }
638
639 if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
640 *hp = zero;
641 }
642
643 } /* end of addVarToConst */
644
645
646 ABC_NAMESPACE_IMPL_END
647
648