diff options
Diffstat (limited to 'src/bdd/cudd/cuddAddFind.c')
| -rw-r--r-- | src/bdd/cudd/cuddAddFind.c | 283 |
1 files changed, 0 insertions, 283 deletions
diff --git a/src/bdd/cudd/cuddAddFind.c b/src/bdd/cudd/cuddAddFind.c deleted file mode 100644 index 0469b014..00000000 --- a/src/bdd/cudd/cuddAddFind.c +++ /dev/null @@ -1,283 +0,0 @@ -/**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: - <ul> - <li> Cudd_addFindMax() - <li> Cudd_addFindMin() - <li> Cudd_addIthBit() - </ul> - Static functions included in this module: - <ul> - <li> addDoIthBit() - </ul>] - - Author [Fabio Somenzi] - - Copyright [This file was created at the University of Colorado at - Boulder. The University of Colorado at Boulder makes no warranty - about the suitability of this software for any purpose. It is - presented on an AS IS basis.] - -******************************************************************************/ - -#include "util_hack.h" -#include "cuddInt.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -#ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddAddFind.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $"; -#endif - - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static DdNode * addDoIthBit ARGS((DdManager *dd, DdNode *f, DdNode *index)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Finds the maximum discriminant of f.] - - Description [Returns a pointer to a constant ADD.] - - SideEffects [None] - -******************************************************************************/ -DdNode * -Cudd_addFindMax( - DdManager * dd, - DdNode * f) -{ - DdNode *t, *e, *res; - - statLine(dd); - if (cuddIsConstant(f)) { - return(f); - } - - res = cuddCacheLookup1(dd,Cudd_addFindMax,f); - if (res != NULL) { - return(res); - } - - t = Cudd_addFindMax(dd,cuddT(f)); - if (t == DD_PLUS_INFINITY(dd)) return(t); - - e = Cudd_addFindMax(dd,cuddE(f)); - - res = (cuddV(t) >= cuddV(e)) ? t : e; - - cuddCacheInsert1(dd,Cudd_addFindMax,f,res); - - return(res); - -} /* end of Cudd_addFindMax */ - - -/**Function******************************************************************** - - Synopsis [Finds the minimum discriminant of f.] - - Description [Returns a pointer to a constant ADD.] - - SideEffects [None] - -******************************************************************************/ -DdNode * -Cudd_addFindMin( - DdManager * dd, - DdNode * f) -{ - DdNode *t, *e, *res; - - statLine(dd); - if (cuddIsConstant(f)) { - return(f); - } - - res = cuddCacheLookup1(dd,Cudd_addFindMin,f); - if (res != NULL) { - return(res); - } - - t = Cudd_addFindMin(dd,cuddT(f)); - if (t == DD_MINUS_INFINITY(dd)) return(t); - - e = Cudd_addFindMin(dd,cuddE(f)); - - res = (cuddV(t) <= cuddV(e)) ? t : e; - - cuddCacheInsert1(dd,Cudd_addFindMin,f,res); - - return(res); - -} /* end of Cudd_addFindMin */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_addIthBit( - DdManager * dd, - DdNode * f, - int bit) -{ - DdNode *res; - DdNode *index; - - /* Use a constant node to remember the bit, so that we can use the - ** global cache. - */ - index = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) bit); - if (index == NULL) return(NULL); - cuddRef(index); - - do { - dd->reordered = 0; - res = addDoIthBit(dd, f, index); - } while (dd->reordered == 1); - - if (res == NULL) { - Cudd_RecursiveDeref(dd, index); - return(NULL); - } - cuddRef(res); - Cudd_RecursiveDeref(dd, index); - cuddDeref(res); - return(res); - -} /* end of Cudd_addIthBit */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - - -/**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 [] - -******************************************************************************/ -static DdNode * -addDoIthBit( - DdManager * dd, - DdNode * f, - DdNode * index) -{ - DdNode *res, *T, *E; - DdNode *fv, *fvn; - int mask, value; - int v; - - statLine(dd); - /* Check terminal case. */ - if (cuddIsConstant(f)) { - mask = 1 << ((int) cuddV(index)); - value = (int) cuddV(f); - return((value & mask) == 0 ? DD_ZERO(dd) : DD_ONE(dd)); - } - - /* Check cache. */ - res = cuddCacheLookup2(dd,addDoIthBit,f,index); - if (res != NULL) return(res); - - /* Recursive step. */ - v = f->index; - fv = cuddT(f); fvn = cuddE(f); - - T = addDoIthBit(dd,fv,index); - if (T == NULL) return(NULL); - cuddRef(T); - - E = addDoIthBit(dd,fvn,index); - if (E == NULL) { - Cudd_RecursiveDeref(dd, T); - return(NULL); - } - cuddRef(E); - - res = (T == E) ? T : cuddUniqueInter(dd,v,T,E); - if (res == NULL) { - Cudd_RecursiveDeref(dd, T); - Cudd_RecursiveDeref(dd, E); - return(NULL); - } - cuddDeref(T); - cuddDeref(E); - - /* Store result. */ - cuddCacheInsert2(dd,addDoIthBit,f,index,res); - - return(res); - -} /* end of addDoIthBit */ - |