cuddBddAbs.c

Go to the documentation of this file.

#include "CUDD/util.h"
#include "CUDD/cuddInt.h"


/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddBddAbs.c,v 1.28 2012/02/05 01:07:18 fabio Exp $";
#endif

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


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

static int bddCheckPositiveCube (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_bddExistAbstractLimit(
  DdManager * manager,
  DdNode * f,
  DdNode * cube,
  unsigned int limit)
{
    DdNode *res;
    unsigned int saveLimit = manager->maxLive;

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

    manager->maxLive = (manager->keys - manager->dead) + 
        (manager->keysZ - manager->deadZ) + limit;
    do {
    manager->reordered = 0;
    res = cuddBddExistAbstractRecur(manager, f, cube);
    } while (manager->reordered == 1);
    manager->maxLive = saveLimit;

    return(res);

} /* end of Cudd_bddExistAbstractLimit */


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;
    DD_CTFP cacheOp;
    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 = (DD_CTFP) 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 */