source: vis_dev/glu-2.3/src/cuBdd/cuddAddIte.c @ 100

Last change on this file since 100 was 13, checked in by cecile, 13 years ago

library glu 2.3

File size: 17.2 KB
Line 
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 "util.h"
64#include "cuddInt.h"
65
66/*---------------------------------------------------------------------------*/
67/* Constant declarations                                                     */
68/*---------------------------------------------------------------------------*/
69
70
71/*---------------------------------------------------------------------------*/
72/* Stucture declarations                                                     */
73/*---------------------------------------------------------------------------*/
74
75
76/*---------------------------------------------------------------------------*/
77/* Type declarations                                                         */
78/*---------------------------------------------------------------------------*/
79
80
81/*---------------------------------------------------------------------------*/
82/* Variable declarations                                                     */
83/*---------------------------------------------------------------------------*/
84
85#ifndef lint
86static char rcsid[] DD_UNUSED = "$Id: cuddAddIte.c,v 1.15 2004/08/13 18:04:45 fabio Exp $";
87#endif
88
89
90/*---------------------------------------------------------------------------*/
91/* Macro declarations                                                        */
92/*---------------------------------------------------------------------------*/
93
94
95/**AutomaticStart*************************************************************/
96
97/*---------------------------------------------------------------------------*/
98/* Static function prototypes                                                */
99/*---------------------------------------------------------------------------*/
100
101static void addVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one, DdNode *zero);
102
103/**AutomaticEnd***************************************************************/
104
105
106/*---------------------------------------------------------------------------*/
107/* Definition of exported functions                                          */
108/*---------------------------------------------------------------------------*/
109
110
111/**Function********************************************************************
112
113  Synopsis    [Implements ITE(f,g,h).]
114
115  Description [Implements ITE(f,g,h). This procedure assumes that f is
116  a 0-1 ADD.  Returns a pointer to the resulting ADD if successful; NULL
117  otherwise.]
118
119  SideEffects [None]
120
121  SeeAlso     [Cudd_bddIte Cudd_addIteConstant Cudd_addApply]
122
123******************************************************************************/
124DdNode *
125Cudd_addIte(
126  DdManager * dd,
127  DdNode * f,
128  DdNode * g,
129  DdNode * h)
130{
131    DdNode *res;
132
133    do {
134        dd->reordered = 0;
135        res = cuddAddIteRecur(dd,f,g,h);
136    } while (dd->reordered == 1);
137    return(res);
138
139} /* end of Cudd_addIte */
140
141
142/**Function********************************************************************
143
144  Synopsis    [Implements ITEconstant for ADDs.]
145
146  Description [Implements ITEconstant for ADDs.  f must be a 0-1 ADD.
147  Returns a pointer to the resulting ADD (which may or may not be
148  constant) or DD_NON_CONSTANT. No new nodes are created. This function
149  can be used, for instance, to check that g has a constant value
150  (specified by h) whenever f is 1. If the constant value is unknown,
151  then one should use Cudd_addEvalConst.]
152
153  SideEffects [None]
154
155  SeeAlso     [Cudd_addIte Cudd_addEvalConst Cudd_bddIteConstant]
156
157******************************************************************************/
158DdNode *
159Cudd_addIteConstant(
160  DdManager * dd,
161  DdNode * f,
162  DdNode * g,
163  DdNode * h)
164{
165    DdNode *one,*zero;
166    DdNode *Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*r,*t,*e;
167    unsigned int topf,topg,toph,v;
168
169    statLine(dd);
170    /* Trivial cases. */
171    if (f == (one = DD_ONE(dd))) {      /* ITE(1,G,H) = G */
172        return(g);
173    }
174    if (f == (zero = DD_ZERO(dd))) {    /* ITE(0,G,H) = H */
175        return(h);
176    }
177
178    /* From now on, f is known not to be a constant. */
179    addVarToConst(f,&g,&h,one,zero);
180
181    /* Check remaining one variable cases. */
182    if (g == h) {                       /* ITE(F,G,G) = G */
183        return(g);
184    }
185    if (cuddIsConstant(g) && cuddIsConstant(h)) {
186        return(DD_NON_CONSTANT);
187    }
188
189    topf = cuddI(dd,f->index);
190    topg = cuddI(dd,g->index);
191    toph = cuddI(dd,h->index);
192    v = ddMin(topg,toph);
193
194    /* ITE(F,G,H) = (x,G,H) (non constant) if F = (x,1,0), x < top(G,H). */
195    if (topf < v && cuddIsConstant(cuddT(f)) && cuddIsConstant(cuddE(f))) {
196        return(DD_NON_CONSTANT);
197    }
198
199    /* Check cache. */
200    r = cuddConstantLookup(dd,DD_ADD_ITE_CONSTANT_TAG,f,g,h);
201    if (r != NULL) {
202        return(r);
203    }
204
205    /* Compute cofactors. */
206    if (topf <= v) {
207        v = ddMin(topf,v);      /* v = top_var(F,G,H) */
208        Fv = cuddT(f); Fnv = cuddE(f);
209    } else {
210        Fv = Fnv = f;
211    }
212    if (topg == v) {
213        Gv = cuddT(g); Gnv = cuddE(g);
214    } else {
215        Gv = Gnv = g;
216    }
217    if (toph == v) {
218        Hv = cuddT(h); Hnv = cuddE(h);
219    } else {
220        Hv = Hnv = h;
221    }
222   
223    /* Recursive step. */
224    t = Cudd_addIteConstant(dd,Fv,Gv,Hv);
225    if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
226        cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
227        return(DD_NON_CONSTANT);
228    }
229    e = Cudd_addIteConstant(dd,Fnv,Gnv,Hnv);
230    if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {
231        cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
232        return(DD_NON_CONSTANT);
233    }
234    cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, t);
235    return(t);
236
237} /* end of Cudd_addIteConstant */
238
239
240/**Function********************************************************************
241
242  Synopsis    [Checks whether ADD g is constant whenever ADD f is 1.]
243
244  Description [Checks whether ADD g is constant whenever ADD f is 1.  f
245  must be a 0-1 ADD.  Returns a pointer to the resulting ADD (which may
246  or may not be constant) or DD_NON_CONSTANT. If f is identically 0,
247  the check is assumed to be successful, and the background value is
248  returned. No new nodes are created.]
249
250  SideEffects [None]
251
252  SeeAlso     [Cudd_addIteConstant Cudd_addLeq]
253
254******************************************************************************/
255DdNode *
256Cudd_addEvalConst(
257  DdManager * dd,
258  DdNode * f,
259  DdNode * g)
260{
261    DdNode *zero;
262    DdNode *Fv,*Fnv,*Gv,*Gnv,*r,*t,*e;
263    unsigned int topf,topg;
264
265#ifdef DD_DEBUG
266    assert(!Cudd_IsComplement(f));
267#endif
268
269    statLine(dd);
270    /* Terminal cases. */
271    if (f == DD_ONE(dd) || cuddIsConstant(g)) {
272        return(g);
273    }
274    if (f == (zero = DD_ZERO(dd))) {
275        return(dd->background);
276    }
277
278#ifdef DD_DEBUG
279    assert(!cuddIsConstant(f));
280#endif
281    /* From now on, f and g are known not to be constants. */
282
283    topf = cuddI(dd,f->index);
284    topg = cuddI(dd,g->index);
285
286    /* Check cache. */
287    r = cuddConstantLookup(dd,DD_ADD_EVAL_CONST_TAG,f,g,g);
288    if (r != NULL) {
289        return(r);
290    }
291
292    /* Compute cofactors. */
293    if (topf <= topg) {
294        Fv = cuddT(f); Fnv = cuddE(f);
295    } else {
296        Fv = Fnv = f;
297    }
298    if (topg <= topf) {
299        Gv = cuddT(g); Gnv = cuddE(g);
300    } else {
301        Gv = Gnv = g;
302    }
303   
304    /* Recursive step. */
305    if (Fv != zero) {
306        t = Cudd_addEvalConst(dd,Fv,Gv);
307        if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
308            cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
309            return(DD_NON_CONSTANT);
310        }
311        if (Fnv != zero) {
312            e = Cudd_addEvalConst(dd,Fnv,Gnv);
313            if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {
314                cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
315                return(DD_NON_CONSTANT);
316            }
317        }
318        cuddCacheInsert2(dd,Cudd_addEvalConst,f,g,t);
319        return(t);
320    } else { /* Fnv must be != zero */
321        e = Cudd_addEvalConst(dd,Fnv,Gnv);
322        cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, e);
323        return(e);
324    }
325
326} /* end of Cudd_addEvalConst */
327
328
329/**Function********************************************************************
330
331  Synopsis    [Computes the complement of an ADD a la C language.]
332
333  Description [Computes the complement of an ADD a la C language: The
334  complement of 0 is 1 and the complement of everything else is 0.
335  Returns a pointer to the resulting ADD if successful; NULL otherwise.]
336
337  SideEffects [None]
338
339  SeeAlso     [Cudd_addNegate]
340
341******************************************************************************/
342DdNode *
343Cudd_addCmpl(
344  DdManager * dd,
345  DdNode * f)
346{
347    DdNode *res;
348
349    do {
350        dd->reordered = 0;
351        res = cuddAddCmplRecur(dd,f);
352    } while (dd->reordered == 1);
353    return(res);
354
355} /* end of Cudd_addCmpl */
356
357
358/**Function********************************************************************
359
360  Synopsis    [Determines whether f is less than or equal to g.]
361
362  Description [Returns 1 if f is less than or equal to g; 0 otherwise.
363  No new nodes are created. This procedure works for arbitrary ADDs.
364  For 0-1 ADDs Cudd_addEvalConst is more efficient.]
365
366  SideEffects [None]
367
368  SeeAlso     [Cudd_addIteConstant Cudd_addEvalConst Cudd_bddLeq]
369
370******************************************************************************/
371int
372Cudd_addLeq(
373  DdManager * dd,
374  DdNode * f,
375  DdNode * g)
376{
377    DdNode *tmp, *fv, *fvn, *gv, *gvn;
378    unsigned int topf, topg, res;
379
380    /* Terminal cases. */
381    if (f == g) return(1);
382
383    statLine(dd);
384    if (cuddIsConstant(f)) {
385        if (cuddIsConstant(g)) return(cuddV(f) <= cuddV(g));
386        if (f == DD_MINUS_INFINITY(dd)) return(1);
387        if (f == DD_PLUS_INFINITY(dd)) return(0); /* since f != g */
388    }
389    if (g == DD_PLUS_INFINITY(dd)) return(1);
390    if (g == DD_MINUS_INFINITY(dd)) return(0); /* since f != g */
391
392    /* Check cache. */
393    tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_addLeq,f,g);
394    if (tmp != NULL) {
395        return(tmp == DD_ONE(dd));
396    }
397
398    /* Compute cofactors. One of f and g is not constant. */
399    topf = cuddI(dd,f->index);
400    topg = cuddI(dd,g->index);
401    if (topf <= topg) {
402        fv = cuddT(f); fvn = cuddE(f);
403    } else {
404        fv = fvn = f;
405    }
406    if (topg <= topf) {
407        gv = cuddT(g); gvn = cuddE(g);
408    } else {
409        gv = gvn = g;
410    }
411
412    res = Cudd_addLeq(dd,fvn,gvn) && Cudd_addLeq(dd,fv,gv);
413
414    /* Store result in cache and return. */
415    cuddCacheInsert2(dd,(DD_CTFP) Cudd_addLeq,f,g,
416                     Cudd_NotCond(DD_ONE(dd),res==0));
417    return(res);
418
419} /* end of Cudd_addLeq */
420
421
422/*---------------------------------------------------------------------------*/
423/* Definition of internal functions                                          */
424/*---------------------------------------------------------------------------*/
425
426
427/**Function********************************************************************
428
429  Synopsis    [Implements the recursive step of Cudd_addIte(f,g,h).]
430
431  Description [Implements the recursive step of Cudd_addIte(f,g,h).
432  Returns a pointer to the resulting ADD if successful; NULL
433  otherwise.]
434
435  SideEffects [None]
436
437  SeeAlso     [Cudd_addIte]
438
439******************************************************************************/
440DdNode *
441cuddAddIteRecur(
442  DdManager * dd,
443  DdNode * f,
444  DdNode * g,
445  DdNode * h)
446{
447    DdNode *one,*zero;
448    DdNode *r,*Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*t,*e;
449    unsigned int topf,topg,toph,v;
450    int index;
451
452    statLine(dd);
453    /* Trivial cases. */
454
455    /* One variable cases. */
456    if (f == (one = DD_ONE(dd))) {      /* ITE(1,G,H) = G */
457        return(g);
458    }
459    if (f == (zero = DD_ZERO(dd))) {    /* ITE(0,G,H) = H */
460        return(h);
461    }
462
463    /* From now on, f is known to not be a constant. */
464    addVarToConst(f,&g,&h,one,zero);
465
466    /* Check remaining one variable cases. */
467    if (g == h) {                       /* ITE(F,G,G) = G */
468        return(g);
469    }
470
471    if (g == one) {                     /* ITE(F,1,0) = F */
472        if (h == zero) return(f);
473    }
474
475    topf = cuddI(dd,f->index);
476    topg = cuddI(dd,g->index);
477    toph = cuddI(dd,h->index);
478    v = ddMin(topg,toph);
479
480    /* A shortcut: ITE(F,G,H) = (x,G,H) if F=(x,1,0), x < top(G,H). */
481    if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
482        r = cuddUniqueInter(dd,(int)f->index,g,h);
483        return(r);
484    }
485    if (topf < v && cuddT(f) == zero && cuddE(f) == one) {
486        r = cuddUniqueInter(dd,(int)f->index,h,g);
487        return(r);
488    }
489
490    /* Check cache. */
491    r = cuddCacheLookup(dd,DD_ADD_ITE_TAG,f,g,h);
492    if (r != NULL) {
493        return(r);
494    }
495
496    /* Compute cofactors. */
497    if (topf <= v) {
498        v = ddMin(topf,v);      /* v = top_var(F,G,H) */
499        index = f->index;
500        Fv = cuddT(f); Fnv = cuddE(f);
501    } else {
502        Fv = Fnv = f;
503    }
504    if (topg == v) {
505        index = g->index;
506        Gv = cuddT(g); Gnv = cuddE(g);
507    } else {
508        Gv = Gnv = g;
509    }
510    if (toph == v) {
511        index = h->index;
512        Hv = cuddT(h); Hnv = cuddE(h);
513    } else {
514        Hv = Hnv = h;
515    }
516   
517    /* Recursive step. */
518    t = cuddAddIteRecur(dd,Fv,Gv,Hv);
519    if (t == NULL) return(NULL);
520    cuddRef(t);
521
522    e = cuddAddIteRecur(dd,Fnv,Gnv,Hnv);
523    if (e == NULL) {
524        Cudd_RecursiveDeref(dd,t);
525        return(NULL);
526    }
527    cuddRef(e);
528
529    r = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
530    if (r == NULL) {
531        Cudd_RecursiveDeref(dd,t);
532        Cudd_RecursiveDeref(dd,e);
533        return(NULL);
534    }
535    cuddDeref(t);
536    cuddDeref(e);
537
538    cuddCacheInsert(dd,DD_ADD_ITE_TAG,f,g,h,r);
539
540    return(r);
541
542} /* end of cuddAddIteRecur */
543
544
545/**Function********************************************************************
546
547  Synopsis    [Performs the recursive step of Cudd_addCmpl.]
548
549  Description [Performs the recursive step of Cudd_addCmpl. Returns a
550  pointer to the resulting ADD if successful; NULL otherwise.]
551
552  SideEffects [None]
553
554  SeeAlso     [Cudd_addCmpl]
555
556******************************************************************************/
557DdNode *
558cuddAddCmplRecur(
559  DdManager * dd,
560  DdNode * f)
561{
562    DdNode *one,*zero;
563    DdNode *r,*Fv,*Fnv,*t,*e;
564
565    statLine(dd);
566    one = DD_ONE(dd);
567    zero = DD_ZERO(dd); 
568
569    if (cuddIsConstant(f)) {
570        if (f == zero) {
571            return(one);
572        } else {
573            return(zero);
574        }
575    }
576    r = cuddCacheLookup1(dd,Cudd_addCmpl,f);
577    if (r != NULL) {
578        return(r);
579    }
580    Fv = cuddT(f);
581    Fnv = cuddE(f);
582    t = cuddAddCmplRecur(dd,Fv);
583    if (t == NULL) return(NULL);
584    cuddRef(t);
585    e = cuddAddCmplRecur(dd,Fnv);
586    if (e == NULL) {
587        Cudd_RecursiveDeref(dd,t);
588        return(NULL);
589    }
590    cuddRef(e);
591    r = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
592    if (r == NULL) {
593        Cudd_RecursiveDeref(dd, t);
594        Cudd_RecursiveDeref(dd, e);
595        return(NULL);
596    }
597    cuddDeref(t);
598    cuddDeref(e);
599    cuddCacheInsert1(dd,Cudd_addCmpl,f,r);
600    return(r);
601
602} /* end of cuddAddCmplRecur */
603
604
605/*---------------------------------------------------------------------------*/
606/* Definition of static functions                                            */
607/*---------------------------------------------------------------------------*/
608
609
610/**Function********************************************************************
611
612  Synopsis [Replaces variables with constants if possible (part of
613  canonical form).]
614
615  Description []
616
617  SideEffects [None]
618
619******************************************************************************/
620static void
621addVarToConst(
622  DdNode * f,
623  DdNode ** gp,
624  DdNode ** hp,
625  DdNode * one,
626  DdNode * zero)
627{
628    DdNode *g = *gp;
629    DdNode *h = *hp;
630
631    if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
632        *gp = one;
633    }
634
635    if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
636        *hp = zero;
637    }
638
639} /* end of addVarToConst */
Note: See TracBrowser for help on using the repository browser.