src/cuBdd/cuddAddFind.c File Reference

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

Go to the source code of this file.

Functions

static DdNode * addDoIthBit (DdManager *dd, DdNode *f, DdNode *index)
DdNode * Cudd_addFindMax (DdManager *dd, DdNode *f)
DdNode * Cudd_addFindMin (DdManager *dd, DdNode *f)
DdNode * Cudd_addIthBit (DdManager *dd, DdNode *f, int bit)

Variables

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

Function Documentation

static DdNode * addDoIthBit ( DdManager *  dd,
DdNode *  f,
DdNode *  index 
) [static]

AutomaticStart

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

Synopsis [Performs the recursive step for Cudd_addIthBit.]

Description [Performs the recursive step for Cudd_addIthBit. Returns a pointer to the BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 264 of file cuddAddFind.c.

00268 {
00269     DdNode *res, *T, *E;
00270     DdNode *fv, *fvn;
00271     int mask, value;
00272     int v;
00273 
00274     statLine(dd);
00275     /* Check terminal case. */
00276     if (cuddIsConstant(f)) {
00277         mask = 1 << ((int) cuddV(index));
00278         value = (int) cuddV(f);
00279         return((value & mask) == 0 ? DD_ZERO(dd) : DD_ONE(dd));
00280     }
00281 
00282     /* Check cache. */
00283     res = cuddCacheLookup2(dd,addDoIthBit,f,index);
00284     if (res != NULL) return(res);
00285 
00286     /* Recursive step. */
00287     v = f->index;
00288     fv = cuddT(f); fvn = cuddE(f);
00289 
00290     T = addDoIthBit(dd,fv,index);
00291     if (T == NULL) return(NULL);
00292     cuddRef(T);
00293 
00294     E = addDoIthBit(dd,fvn,index);
00295     if (E == NULL) {
00296         Cudd_RecursiveDeref(dd, T);
00297         return(NULL);
00298     }
00299     cuddRef(E);
00300 
00301     res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00302     if (res == NULL) {
00303         Cudd_RecursiveDeref(dd, T);
00304         Cudd_RecursiveDeref(dd, E);
00305         return(NULL);
00306     }
00307     cuddDeref(T);
00308     cuddDeref(E);
00309 
00310     /* Store result. */
00311     cuddCacheInsert2(dd,addDoIthBit,f,index,res);
00312 
00313     return(res);
00314 
00315 } /* end of addDoIthBit */

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

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

Synopsis [Finds the maximum discriminant of f.]

Description [Returns a pointer to a constant ADD.]

SideEffects [None]

Definition at line 120 of file cuddAddFind.c.

00123 {
00124     DdNode *t, *e, *res;
00125 
00126     statLine(dd);
00127     if (cuddIsConstant(f)) {
00128         return(f);
00129     }
00130 
00131     res = cuddCacheLookup1(dd,Cudd_addFindMax,f);
00132     if (res != NULL) {
00133         return(res);
00134     }
00135 
00136     t  = Cudd_addFindMax(dd,cuddT(f));
00137     if (t == DD_PLUS_INFINITY(dd)) return(t);
00138 
00139     e  = Cudd_addFindMax(dd,cuddE(f));
00140 
00141     res = (cuddV(t) >= cuddV(e)) ? t : e;
00142 
00143     cuddCacheInsert1(dd,Cudd_addFindMax,f,res);
00144 
00145     return(res);
00146 
00147 } /* end of Cudd_addFindMax */

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

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

Synopsis [Finds the minimum discriminant of f.]

Description [Returns a pointer to a constant ADD.]

SideEffects [None]

Definition at line 160 of file cuddAddFind.c.

00163 {
00164     DdNode *t, *e, *res;
00165 
00166     statLine(dd);
00167     if (cuddIsConstant(f)) {
00168         return(f);
00169     }
00170 
00171     res = cuddCacheLookup1(dd,Cudd_addFindMin,f);
00172     if (res != NULL) {
00173         return(res);
00174     }
00175 
00176     t  = Cudd_addFindMin(dd,cuddT(f));
00177     if (t == DD_MINUS_INFINITY(dd)) return(t);
00178 
00179     e  = Cudd_addFindMin(dd,cuddE(f));
00180 
00181     res = (cuddV(t) <= cuddV(e)) ? t : e;
00182 
00183     cuddCacheInsert1(dd,Cudd_addFindMin,f,res);
00184 
00185     return(res);
00186 
00187 } /* end of Cudd_addFindMin */

DdNode* Cudd_addIthBit ( DdManager *  dd,
DdNode *  f,
int  bit 
)

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

Synopsis [Extracts the i-th bit from an ADD.]

Description [Produces an ADD from another ADD by replacing all discriminants whose i-th bit is equal to 1 with 1, and all other discriminants with 0. The i-th bit refers to the integer representation of the leaf value. If the value is has a fractional part, it is ignored. Repeated calls to this procedure allow one to transform an integer-valued ADD into an array of ADDs, one for each bit of the leaf values. Returns a pointer to the resulting ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addBddIthBit]

Definition at line 209 of file cuddAddFind.c.

00213 {
00214     DdNode *res;
00215     DdNode *index;
00216     
00217     /* Use a constant node to remember the bit, so that we can use the
00218     ** global cache.
00219     */
00220     index = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) bit);
00221     if (index == NULL) return(NULL);
00222     cuddRef(index);
00223 
00224     do {
00225         dd->reordered = 0;
00226         res = addDoIthBit(dd, f, index);
00227     } while (dd->reordered == 1);
00228 
00229     if (res == NULL) {
00230         Cudd_RecursiveDeref(dd, index);
00231         return(NULL);
00232     }
00233     cuddRef(res);
00234     Cudd_RecursiveDeref(dd, index);
00235     cuddDeref(res);
00236     return(res);
00237 
00238 } /* end of Cudd_addIthBit */

Variable Documentation

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

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

FileName [cuddAddFind.c]

PackageName [cudd]

Synopsis [Functions to find maximum and minimum in an ADD and to extract the i-th bit.]

Description [External procedures included in this module:

Static functions 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 80 of file cuddAddFind.c.

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