src/bdd/cudd/cuddBddAbs.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: cuddBddAbs.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


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

static int bddCheckPositiveCube ARGS((DdManager *manager, DdNode *cube));

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


DdNode *
Cudd_bddExistAbstract(
  DdManager * manager,
  DdNode * f,
  DdNode * cube)
{
    DdNode *res;

    if (bddCheckPositiveCube(manager, cube) == 0) {
        (void) fprintf(manager->err,
                       "Error: Can only abstract positive cubes\n");
        manager->errorCode = CUDD_INVALID_ARG;
        return(NULL);
    }

    do {
        manager->reordered = 0;
        res = cuddBddExistAbstractRecur(manager, f, cube);
    } while (manager->reordered == 1);

    return(res);

} /* end of Cudd_bddExistAbstract */


DdNode *
Cudd_bddXorExistAbstract(
  DdManager * manager,
  DdNode * f,
  DdNode * g,
  DdNode * cube)
{
    DdNode *res;

    if (bddCheckPositiveCube(manager, cube) == 0) {
        (void) fprintf(manager->err,
                       "Error: Can only abstract positive cubes\n");
        manager->errorCode = CUDD_INVALID_ARG;
        return(NULL);
    }

    do {
        manager->reordered = 0;
        res = cuddBddXorExistAbstractRecur(manager, f, g, cube);
    } while (manager->reordered == 1);

    return(res);

} /* end of Cudd_bddXorExistAbstract */


DdNode *
Cudd_bddUnivAbstract(
  DdManager * manager,
  DdNode * f,
  DdNode * cube)
{
    DdNode      *res;

    if (bddCheckPositiveCube(manager, cube) == 0) {
        (void) fprintf(manager->err,
                       "Error: Can only abstract positive cubes\n");
        manager->errorCode = CUDD_INVALID_ARG;
        return(NULL);
    }

    do {
        manager->reordered = 0;
        res = cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube);
    } while (manager->reordered == 1);
    if (res != NULL) res = Cudd_Not(res);

    return(res);

} /* end of Cudd_bddUnivAbstract */


DdNode *
Cudd_bddBooleanDiff(
  DdManager * manager,
  DdNode * f,
  int  x)
{
    DdNode *res, *var;

    /* If the variable is not currently in the manager, f cannot
    ** depend on it.
    */
    if (x >= manager->size) return(Cudd_Not(DD_ONE(manager)));
    var = manager->vars[x];

    do {
        manager->reordered = 0;
        res = cuddBddBooleanDiffRecur(manager, Cudd_Regular(f), var);
    } while (manager->reordered == 1);

    return(res);

} /* end of Cudd_bddBooleanDiff */


int
Cudd_bddVarIsDependent(
  DdManager *dd,                /* manager */
  DdNode *f,                    /* function */
  DdNode *var                   /* variable */)
{
    DdNode *F, *res, *zero, *ft, *fe;
    unsigned topf, level;
    DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);
    int retval;

    zero = Cudd_Not(DD_ONE(dd));
    if (Cudd_IsConstant(f)) return(f == zero);

    /* From now on f is not constant. */
    F = Cudd_Regular(f);
    topf = (unsigned) dd->perm[F->index];
    level = (unsigned) dd->perm[var->index];

    /* Check terminal case. If topf > index of var, f does not depend on var.
    ** Therefore, var is not dependent in f. */
    if (topf > level) {
        return(0);
    }

    cacheOp =
        (DdNode *(*)(DdManager *, DdNode *, DdNode *)) Cudd_bddVarIsDependent;
    res = cuddCacheLookup2(dd,cacheOp,f,var);
    if (res != NULL) {
        return(res != zero);
    }

    /* Compute cofactors. */
    ft = Cudd_NotCond(cuddT(F), f != F);
    fe = Cudd_NotCond(cuddE(F), f != F);

    if (topf == level) {
        retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe));
    } else {
        retval = Cudd_bddVarIsDependent(dd,ft,var) &&
            Cudd_bddVarIsDependent(dd,fe,var);
    }

    cuddCacheInsert2(dd,cacheOp,f,var,Cudd_NotCond(zero,retval));

    return(retval);

} /* Cudd_bddVarIsDependent */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


DdNode *
cuddBddExistAbstractRecur(
  DdManager * manager,
  DdNode * f,
  DdNode * cube)
{
    DdNode      *F, *T, *E, *res, *res1, *res2, *one;

    statLine(manager);
    one = DD_ONE(manager);
    F = Cudd_Regular(f);

    /* Cube is guaranteed to be a cube at this point. */        
    if (cube == one || F == one) {  
        return(f);
    }
    /* From now on, f and cube are non-constant. */

    /* Abstract a variable that does not appear in f. */
    while (manager->perm[F->index] > manager->perm[cube->index]) {
        cube = cuddT(cube);
        if (cube == one) return(f);
    }

    /* Check the cache. */
    if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstract, f, cube)) != NULL) {
        return(res);
    }

    /* Compute the cofactors of f. */
    T = cuddT(F); E = cuddE(F);
    if (f != F) {
        T = Cudd_Not(T); E = Cudd_Not(E);
    }

    /* If the two indices are the same, so are their levels. */
    if (F->index == cube->index) {
        if (T == one || E == one || T == Cudd_Not(E)) {
            return(one);
        }
        res1 = cuddBddExistAbstractRecur(manager, T, cuddT(cube));
        if (res1 == NULL) return(NULL);
        if (res1 == one) {
            if (F->ref != 1)
                cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, one);
            return(one);
        }
        cuddRef(res1);
        res2 = cuddBddExistAbstractRecur(manager, E, cuddT(cube));
        if (res2 == NULL) {
            Cudd_IterDerefBdd(manager,res1);
            return(NULL);
        }
        cuddRef(res2);
        res = cuddBddAndRecur(manager, Cudd_Not(res1), Cudd_Not(res2));
        if (res == NULL) {
            Cudd_IterDerefBdd(manager, res1);
            Cudd_IterDerefBdd(manager, res2);
            return(NULL);
        }
        res = Cudd_Not(res);
        cuddRef(res);
        Cudd_IterDerefBdd(manager, res1);
        Cudd_IterDerefBdd(manager, res2);
        if (F->ref != 1)
            cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
        cuddDeref(res);
        return(res);
    } else { /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */
        res1 = cuddBddExistAbstractRecur(manager, T, cube);
        if (res1 == NULL) return(NULL);
        cuddRef(res1);
        res2 = cuddBddExistAbstractRecur(manager, E, cube);
        if (res2 == NULL) {
            Cudd_IterDerefBdd(manager, res1);
            return(NULL);
        }
        cuddRef(res2);
        /* ITE takes care of possible complementation of res1 and of the
        ** case in which res1 == res2. */
        res = cuddBddIteRecur(manager, manager->vars[F->index], res1, res2);
        if (res == NULL) {
            Cudd_IterDerefBdd(manager, res1);
            Cudd_IterDerefBdd(manager, res2);
            return(NULL);
        }
        cuddDeref(res1);
        cuddDeref(res2);
        if (F->ref != 1)
            cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
        return(res);
    }       

} /* end of cuddBddExistAbstractRecur */


DdNode *
cuddBddXorExistAbstractRecur(
  DdManager * manager,
  DdNode * f,
  DdNode * g,
  DdNode * cube)
{
    DdNode *F, *fv, *fnv, *G, *gv, *gnv;
    DdNode *one, *zero, *r, *t, *e, *Cube;
    unsigned int topf, topg, topcube, top, index;

    statLine(manager);
    one = DD_ONE(manager);
    zero = Cudd_Not(one);

    /* Terminal cases. */
    if (f == g) {
        return(zero);
    }
    if (f == Cudd_Not(g)) {
        return(one);
    }
    if (cube == one) {
        return(cuddBddXorRecur(manager, f, g));
    }
    if (f == one) {
        return(cuddBddExistAbstractRecur(manager, Cudd_Not(g), cube));
    }
    if (g == one) {
        return(cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube));
    }
    if (f == zero) {
        return(cuddBddExistAbstractRecur(manager, g, cube));
    }
    if (g == zero) {
        return(cuddBddExistAbstractRecur(manager, f, cube));
    }

    /* At this point f, g, and cube are not constant. */

    if (f > g) { /* Try to increase cache efficiency. */
        DdNode *tmp = f;
        f = g;
        g = tmp;
    }

    /* Check cache. */
    r = cuddCacheLookup(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube);
    if (r != NULL) {
        return(r);
    }

    /* Here we can skip the use of cuddI, because the operands are known
    ** to be non-constant.
    */
    F = Cudd_Regular(f);
    topf = manager->perm[F->index];
    G = Cudd_Regular(g);
    topg = manager->perm[G->index];
    top = ddMin(topf, topg);
    topcube = manager->perm[cube->index];

    if (topcube < top) {
        return(cuddBddXorExistAbstractRecur(manager, f, g, cuddT(cube)));
    }
    /* Now, topcube >= top. */

    if (topf == top) {
        index = F->index;
        fv = cuddT(F);
        fnv = cuddE(F);
        if (Cudd_IsComplement(f)) {
            fv = Cudd_Not(fv);
            fnv = Cudd_Not(fnv);
        }
    } else {
        index = G->index;
        fv = fnv = f;
    }

    if (topg == top) {
        gv = cuddT(G);
        gnv = cuddE(G);
        if (Cudd_IsComplement(g)) {
            gv = Cudd_Not(gv);
            gnv = Cudd_Not(gnv);
        }
    } else {
        gv = gnv = g;
    }

    if (topcube == top) {
        Cube = cuddT(cube);
    } else {
        Cube = cube;
    }

    t = cuddBddXorExistAbstractRecur(manager, fv, gv, Cube);
    if (t == NULL) return(NULL);

    /* Special case: 1 OR anything = 1. Hence, no need to compute
    ** the else branch if t is 1.
    */
    if (t == one && topcube == top) {
        cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, one);
        return(one);
    }
    cuddRef(t);

    e = cuddBddXorExistAbstractRecur(manager, fnv, gnv, Cube);
    if (e == NULL) {
        Cudd_IterDerefBdd(manager, t);
        return(NULL);
    }
    cuddRef(e);

    if (topcube == top) {       /* abstract */
        r = cuddBddAndRecur(manager, Cudd_Not(t), Cudd_Not(e));
        if (r == NULL) {
            Cudd_IterDerefBdd(manager, t);
            Cudd_IterDerefBdd(manager, e);
            return(NULL);
        }
        r = Cudd_Not(r);
        cuddRef(r);
        Cudd_IterDerefBdd(manager, t);
        Cudd_IterDerefBdd(manager, e);
        cuddDeref(r);
    } else if (t == e) {
        r = t;
        cuddDeref(t);
        cuddDeref(e);
    } else {
        if (Cudd_IsComplement(t)) {
            r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
            if (r == NULL) {
                Cudd_IterDerefBdd(manager, t);
                Cudd_IterDerefBdd(manager, e);
                return(NULL);
            }
            r = Cudd_Not(r);
        } else {
            r = cuddUniqueInter(manager,(int)index,t,e);
            if (r == NULL) {
                Cudd_IterDerefBdd(manager, t);
                Cudd_IterDerefBdd(manager, e);
                return(NULL);
            }
        }
        cuddDeref(e);
        cuddDeref(t);
    }
    cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, r);
    return (r);

} /* end of cuddBddXorExistAbstractRecur */


DdNode *
cuddBddBooleanDiffRecur(
  DdManager * manager,
  DdNode * f,
  DdNode * var)
{
    DdNode *T, *E, *res, *res1, *res2;

    statLine(manager);
    if (cuddI(manager,f->index) > manager->perm[var->index]) {
        /* f does not depend on var. */
        return(Cudd_Not(DD_ONE(manager)));
    }

    /* From now on, f is non-constant. */

    /* If the two indices are the same, so are their levels. */
    if (f->index == var->index) {
        res = cuddBddXorRecur(manager, cuddT(f), cuddE(f));
        return(res);
    }

    /* From now on, cuddI(manager,f->index) < cuddI(manager,cube->index). */

    /* Check the cache. */
    res = cuddCacheLookup2(manager, cuddBddBooleanDiffRecur, f, var);
    if (res != NULL) {
        return(res);
    }

    /* Compute the cofactors of f. */
    T = cuddT(f); E = cuddE(f);

    res1 = cuddBddBooleanDiffRecur(manager, T, var);
    if (res1 == NULL) return(NULL);
    cuddRef(res1);
    res2 = cuddBddBooleanDiffRecur(manager, Cudd_Regular(E), var);
    if (res2 == NULL) {
        Cudd_IterDerefBdd(manager, res1);
        return(NULL);
    }
    cuddRef(res2);
    /* ITE takes care of possible complementation of res1 and of the
    ** case in which res1 == res2. */
    res = cuddBddIteRecur(manager, manager->vars[f->index], res1, res2);
    if (res == NULL) {
        Cudd_IterDerefBdd(manager, res1);
        Cudd_IterDerefBdd(manager, res2);
        return(NULL);
    }
    cuddDeref(res1);
    cuddDeref(res2);
    cuddCacheInsert2(manager, cuddBddBooleanDiffRecur, f, var, res);
    return(res);

} /* end of cuddBddBooleanDiffRecur */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

static int
bddCheckPositiveCube(
  DdManager * manager,
  DdNode * cube)
{
    if (Cudd_IsComplement(cube)) return(0);
    if (cube == DD_ONE(manager)) return(1);
    if (cuddIsConstant(cube)) return(0);
    if (cuddE(cube) == Cudd_Not(DD_ONE(manager))) {
        return(bddCheckPositiveCube(manager, cuddT(cube)));
    }
    return(0);

} /* end of bddCheckPositiveCube */

---