src/bdd/cudd/cuddAddFind.c

Go to the documentation of this file.

#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                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static DdNode * addDoIthBit ARGS((DdManager *dd, DdNode *f, DdNode *index));

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

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 */


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 */


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                                            */
/*---------------------------------------------------------------------------*/


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 */

---