src/cuBdd/cuddAddIte.c File Reference

#include "util.h"
#include "cuddInt.h"
Include dependency graph for cuddAddIte.c:

Go to the source code of this file.

Functions

static void addVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one, DdNode *zero)
DdNode * Cudd_addIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
DdNode * Cudd_addIteConstant (DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
DdNode * Cudd_addEvalConst (DdManager *dd, DdNode *f, DdNode *g)
DdNode * Cudd_addCmpl (DdManager *dd, DdNode *f)
int Cudd_addLeq (DdManager *dd, DdNode *f, DdNode *g)
DdNode * cuddAddIteRecur (DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
DdNode * cuddAddCmplRecur (DdManager *dd, DdNode *f)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddAddIte.c,v 1.15 2004/08/13 18:04:45 fabio Exp $"

Function Documentation

static void addVarToConst ( DdNode *  f,
DdNode **  gp,
DdNode **  hp,
DdNode *  one,
DdNode *  zero 
) [static]

AutomaticStart

Function********************************************************************

Synopsis [Replaces variables with constants if possible (part of canonical form).]

Description []

SideEffects [None]

Definition at line 621 of file cuddAddIte.c.

00627 {
00628     DdNode *g = *gp;
00629     DdNode *h = *hp;
00630 
00631     if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
00632         *gp = one;
00633     }
00634 
00635     if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
00636         *hp = zero;
00637     }
00638 
00639 } /* end of addVarToConst */

DdNode* Cudd_addCmpl ( DdManager *  dd,
DdNode *  f 
)

Function********************************************************************

Synopsis [Computes the complement of an ADD a la C language.]

Description [Computes the complement of an ADD a la C language: The complement of 0 is 1 and the complement of everything else is 0. Returns a pointer to the resulting ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addNegate]

Definition at line 343 of file cuddAddIte.c.

00346 {
00347     DdNode *res;
00348 
00349     do {
00350         dd->reordered = 0;
00351         res = cuddAddCmplRecur(dd,f);
00352     } while (dd->reordered == 1);
00353     return(res);
00354 
00355 } /* end of Cudd_addCmpl */

DdNode* Cudd_addEvalConst ( DdManager *  dd,
DdNode *  f,
DdNode *  g 
)

Function********************************************************************

Synopsis [Checks whether ADD g is constant whenever ADD f is 1.]

Description [Checks whether ADD g is constant whenever ADD f is 1. f must be a 0-1 ADD. Returns a pointer to the resulting ADD (which may or may not be constant) or DD_NON_CONSTANT. If f is identically 0, the check is assumed to be successful, and the background value is returned. No new nodes are created.]

SideEffects [None]

SeeAlso [Cudd_addIteConstant Cudd_addLeq]

Definition at line 256 of file cuddAddIte.c.

00260 {
00261     DdNode *zero;
00262     DdNode *Fv,*Fnv,*Gv,*Gnv,*r,*t,*e;
00263     unsigned int topf,topg;
00264 
00265 #ifdef DD_DEBUG
00266     assert(!Cudd_IsComplement(f));
00267 #endif
00268 
00269     statLine(dd);
00270     /* Terminal cases. */
00271     if (f == DD_ONE(dd) || cuddIsConstant(g)) {
00272         return(g);
00273     }
00274     if (f == (zero = DD_ZERO(dd))) {
00275         return(dd->background);
00276     }
00277 
00278 #ifdef DD_DEBUG
00279     assert(!cuddIsConstant(f));
00280 #endif
00281     /* From now on, f and g are known not to be constants. */
00282 
00283     topf = cuddI(dd,f->index);
00284     topg = cuddI(dd,g->index);
00285 
00286     /* Check cache. */
00287     r = cuddConstantLookup(dd,DD_ADD_EVAL_CONST_TAG,f,g,g);
00288     if (r != NULL) {
00289         return(r);
00290     }
00291 
00292     /* Compute cofactors. */
00293     if (topf <= topg) {
00294         Fv = cuddT(f); Fnv = cuddE(f);
00295     } else {
00296         Fv = Fnv = f;
00297     }
00298     if (topg <= topf) {
00299         Gv = cuddT(g); Gnv = cuddE(g);
00300     } else {
00301         Gv = Gnv = g;
00302     }
00303     
00304     /* Recursive step. */
00305     if (Fv != zero) {
00306         t = Cudd_addEvalConst(dd,Fv,Gv);
00307         if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
00308             cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
00309             return(DD_NON_CONSTANT);
00310         }
00311         if (Fnv != zero) {
00312             e = Cudd_addEvalConst(dd,Fnv,Gnv);
00313             if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {
00314                 cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
00315                 return(DD_NON_CONSTANT);
00316             }
00317         }
00318         cuddCacheInsert2(dd,Cudd_addEvalConst,f,g,t);
00319         return(t);
00320     } else { /* Fnv must be != zero */
00321         e = Cudd_addEvalConst(dd,Fnv,Gnv);
00322         cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, e);
00323         return(e);
00324     }
00325 
00326 } /* end of Cudd_addEvalConst */

DdNode* Cudd_addIte ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
DdNode *  h 
)

AutomaticEnd Function********************************************************************

Synopsis [Implements ITE(f,g,h).]

Description [Implements ITE(f,g,h). This procedure assumes that f is a 0-1 ADD. Returns a pointer to the resulting ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddIte Cudd_addIteConstant Cudd_addApply]

Definition at line 125 of file cuddAddIte.c.

00130 {
00131     DdNode *res;
00132 
00133     do {
00134         dd->reordered = 0;
00135         res = cuddAddIteRecur(dd,f,g,h);
00136     } while (dd->reordered == 1);
00137     return(res);
00138 
00139 } /* end of Cudd_addIte */

DdNode* Cudd_addIteConstant ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
DdNode *  h 
)

Function********************************************************************

Synopsis [Implements ITEconstant for ADDs.]

Description [Implements ITEconstant for ADDs. f must be a 0-1 ADD. Returns a pointer to the resulting ADD (which may or may not be constant) or DD_NON_CONSTANT. No new nodes are created. This function can be used, for instance, to check that g has a constant value (specified by h) whenever f is 1. If the constant value is unknown, then one should use Cudd_addEvalConst.]

SideEffects [None]

SeeAlso [Cudd_addIte Cudd_addEvalConst Cudd_bddIteConstant]

Definition at line 159 of file cuddAddIte.c.

00164 {
00165     DdNode *one,*zero;
00166     DdNode *Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*r,*t,*e;
00167     unsigned int topf,topg,toph,v;
00168 
00169     statLine(dd);
00170     /* Trivial cases. */
00171     if (f == (one = DD_ONE(dd))) {      /* ITE(1,G,H) = G */
00172         return(g);
00173     }
00174     if (f == (zero = DD_ZERO(dd))) {    /* ITE(0,G,H) = H */
00175         return(h);
00176     }
00177 
00178     /* From now on, f is known not to be a constant. */
00179     addVarToConst(f,&g,&h,one,zero);
00180 
00181     /* Check remaining one variable cases. */
00182     if (g == h) {                       /* ITE(F,G,G) = G */
00183         return(g);
00184     }
00185     if (cuddIsConstant(g) && cuddIsConstant(h)) {
00186         return(DD_NON_CONSTANT);
00187     }
00188 
00189     topf = cuddI(dd,f->index);
00190     topg = cuddI(dd,g->index);
00191     toph = cuddI(dd,h->index);
00192     v = ddMin(topg,toph);
00193 
00194     /* ITE(F,G,H) = (x,G,H) (non constant) if F = (x,1,0), x < top(G,H). */
00195     if (topf < v && cuddIsConstant(cuddT(f)) && cuddIsConstant(cuddE(f))) {
00196         return(DD_NON_CONSTANT);
00197     }
00198 
00199     /* Check cache. */
00200     r = cuddConstantLookup(dd,DD_ADD_ITE_CONSTANT_TAG,f,g,h);
00201     if (r != NULL) {
00202         return(r);
00203     }
00204 
00205     /* Compute cofactors. */
00206     if (topf <= v) {
00207         v = ddMin(topf,v);      /* v = top_var(F,G,H) */
00208         Fv = cuddT(f); Fnv = cuddE(f);
00209     } else {
00210         Fv = Fnv = f;
00211     }
00212     if (topg == v) {
00213         Gv = cuddT(g); Gnv = cuddE(g);
00214     } else {
00215         Gv = Gnv = g;
00216     }
00217     if (toph == v) {
00218         Hv = cuddT(h); Hnv = cuddE(h);
00219     } else {
00220         Hv = Hnv = h;
00221     }
00222     
00223     /* Recursive step. */
00224     t = Cudd_addIteConstant(dd,Fv,Gv,Hv);
00225     if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
00226         cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
00227         return(DD_NON_CONSTANT);
00228     }
00229     e = Cudd_addIteConstant(dd,Fnv,Gnv,Hnv);
00230     if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {
00231         cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
00232         return(DD_NON_CONSTANT);
00233     }
00234     cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, t);
00235     return(t);
00236 
00237 } /* end of Cudd_addIteConstant */

int Cudd_addLeq ( DdManager *  dd,
DdNode *  f,
DdNode *  g 
)

Function********************************************************************

Synopsis [Determines whether f is less than or equal to g.]

Description [Returns 1 if f is less than or equal to g; 0 otherwise. No new nodes are created. This procedure works for arbitrary ADDs. For 0-1 ADDs Cudd_addEvalConst is more efficient.]

SideEffects [None]

SeeAlso [Cudd_addIteConstant Cudd_addEvalConst Cudd_bddLeq]

Definition at line 372 of file cuddAddIte.c.

00376 {
00377     DdNode *tmp, *fv, *fvn, *gv, *gvn;
00378     unsigned int topf, topg, res;
00379 
00380     /* Terminal cases. */
00381     if (f == g) return(1);
00382 
00383     statLine(dd);
00384     if (cuddIsConstant(f)) {
00385         if (cuddIsConstant(g)) return(cuddV(f) <= cuddV(g));
00386         if (f == DD_MINUS_INFINITY(dd)) return(1);
00387         if (f == DD_PLUS_INFINITY(dd)) return(0); /* since f != g */
00388     }
00389     if (g == DD_PLUS_INFINITY(dd)) return(1);
00390     if (g == DD_MINUS_INFINITY(dd)) return(0); /* since f != g */
00391 
00392     /* Check cache. */
00393     tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_addLeq,f,g);
00394     if (tmp != NULL) {
00395         return(tmp == DD_ONE(dd));
00396     }
00397 
00398     /* Compute cofactors. One of f and g is not constant. */
00399     topf = cuddI(dd,f->index);
00400     topg = cuddI(dd,g->index);
00401     if (topf <= topg) {
00402         fv = cuddT(f); fvn = cuddE(f);
00403     } else {
00404         fv = fvn = f;
00405     }
00406     if (topg <= topf) {
00407         gv = cuddT(g); gvn = cuddE(g);
00408     } else {
00409         gv = gvn = g;
00410     }
00411 
00412     res = Cudd_addLeq(dd,fvn,gvn) && Cudd_addLeq(dd,fv,gv);
00413 
00414     /* Store result in cache and return. */
00415     cuddCacheInsert2(dd,(DD_CTFP) Cudd_addLeq,f,g,
00416                      Cudd_NotCond(DD_ONE(dd),res==0));
00417     return(res);
00418 
00419 } /* end of Cudd_addLeq */

DdNode* cuddAddCmplRecur ( DdManager *  dd,
DdNode *  f 
)

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_addCmpl.]

Description [Performs the recursive step of Cudd_addCmpl. Returns a pointer to the resulting ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addCmpl]

Definition at line 558 of file cuddAddIte.c.

00561 {
00562     DdNode *one,*zero;
00563     DdNode *r,*Fv,*Fnv,*t,*e;
00564 
00565     statLine(dd);
00566     one = DD_ONE(dd);
00567     zero = DD_ZERO(dd); 
00568 
00569     if (cuddIsConstant(f)) {
00570         if (f == zero) {
00571             return(one);
00572         } else {
00573             return(zero);
00574         }
00575     }
00576     r = cuddCacheLookup1(dd,Cudd_addCmpl,f);
00577     if (r != NULL) {
00578         return(r);
00579     }
00580     Fv = cuddT(f);
00581     Fnv = cuddE(f);
00582     t = cuddAddCmplRecur(dd,Fv);
00583     if (t == NULL) return(NULL);
00584     cuddRef(t);
00585     e = cuddAddCmplRecur(dd,Fnv);
00586     if (e == NULL) {
00587         Cudd_RecursiveDeref(dd,t);
00588         return(NULL);
00589     }
00590     cuddRef(e);
00591     r = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
00592     if (r == NULL) {
00593         Cudd_RecursiveDeref(dd, t);
00594         Cudd_RecursiveDeref(dd, e);
00595         return(NULL);
00596     }
00597     cuddDeref(t);
00598     cuddDeref(e);
00599     cuddCacheInsert1(dd,Cudd_addCmpl,f,r);
00600     return(r);
00601 
00602 } /* end of cuddAddCmplRecur */

DdNode* cuddAddIteRecur ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
DdNode *  h 
)

Function********************************************************************

Synopsis [Implements the recursive step of Cudd_addIte(f,g,h).]

Description [Implements the recursive step of Cudd_addIte(f,g,h). Returns a pointer to the resulting ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addIte]

Definition at line 441 of file cuddAddIte.c.

00446 {
00447     DdNode *one,*zero;
00448     DdNode *r,*Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*t,*e;
00449     unsigned int topf,topg,toph,v;
00450     int index;
00451 
00452     statLine(dd);
00453     /* Trivial cases. */
00454 
00455     /* One variable cases. */
00456     if (f == (one = DD_ONE(dd))) {      /* ITE(1,G,H) = G */
00457         return(g);
00458     }
00459     if (f == (zero = DD_ZERO(dd))) {    /* ITE(0,G,H) = H */
00460         return(h);
00461     }
00462 
00463     /* From now on, f is known to not be a constant. */
00464     addVarToConst(f,&g,&h,one,zero);
00465 
00466     /* Check remaining one variable cases. */
00467     if (g == h) {                       /* ITE(F,G,G) = G */
00468         return(g);
00469     }
00470 
00471     if (g == one) {                     /* ITE(F,1,0) = F */
00472         if (h == zero) return(f);
00473     }
00474 
00475     topf = cuddI(dd,f->index);
00476     topg = cuddI(dd,g->index);
00477     toph = cuddI(dd,h->index);
00478     v = ddMin(topg,toph);
00479 
00480     /* A shortcut: ITE(F,G,H) = (x,G,H) if F=(x,1,0), x < top(G,H). */
00481     if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
00482         r = cuddUniqueInter(dd,(int)f->index,g,h);
00483         return(r);
00484     }
00485     if (topf < v && cuddT(f) == zero && cuddE(f) == one) {
00486         r = cuddUniqueInter(dd,(int)f->index,h,g);
00487         return(r);
00488     }
00489 
00490     /* Check cache. */
00491     r = cuddCacheLookup(dd,DD_ADD_ITE_TAG,f,g,h);
00492     if (r != NULL) {
00493         return(r);
00494     }
00495 
00496     /* Compute cofactors. */
00497     if (topf <= v) {
00498         v = ddMin(topf,v);      /* v = top_var(F,G,H) */
00499         index = f->index;
00500         Fv = cuddT(f); Fnv = cuddE(f);
00501     } else {
00502         Fv = Fnv = f;
00503     }
00504     if (topg == v) {
00505         index = g->index;
00506         Gv = cuddT(g); Gnv = cuddE(g);
00507     } else {
00508         Gv = Gnv = g;
00509     }
00510     if (toph == v) {
00511         index = h->index;
00512         Hv = cuddT(h); Hnv = cuddE(h);
00513     } else {
00514         Hv = Hnv = h;
00515     }
00516     
00517     /* Recursive step. */
00518     t = cuddAddIteRecur(dd,Fv,Gv,Hv);
00519     if (t == NULL) return(NULL);
00520     cuddRef(t);
00521 
00522     e = cuddAddIteRecur(dd,Fnv,Gnv,Hnv);
00523     if (e == NULL) {
00524         Cudd_RecursiveDeref(dd,t);
00525         return(NULL);
00526     }
00527     cuddRef(e);
00528 
00529     r = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
00530     if (r == NULL) {
00531         Cudd_RecursiveDeref(dd,t);
00532         Cudd_RecursiveDeref(dd,e);
00533         return(NULL);
00534     }
00535     cuddDeref(t);
00536     cuddDeref(e);
00537 
00538     cuddCacheInsert(dd,DD_ADD_ITE_TAG,f,g,h,r);
00539 
00540     return(r);
00541 
00542 } /* end of cuddAddIteRecur */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddAddIte.c,v 1.15 2004/08/13 18:04:45 fabio Exp $" [static]

CFile***********************************************************************

FileName [cuddAddIte.c]

PackageName [cudd]

Synopsis [ADD ITE function and satellites.]

Description [External procedures included in this module:

Internal procedures included in this module:

Static procedures included in this module:

]

Author [Fabio Somenzi]

Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 86 of file cuddAddIte.c.

Generated on Tue Jan 12 13:57:17 2010 for glu-2.2 by  doxygen 1.6.1