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

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


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

static DdNode * cuddBddClippingAndRecur ARGS((DdManager *manager, DdNode *f, DdNode *g, int distance, int direction));
static DdNode * cuddBddClipAndAbsRecur ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int distance, int direction));

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


DdNode *
Cudd_bddClippingAnd(
  DdManager * dd /* manager */,
  DdNode * f /* first conjunct */,
  DdNode * g /* second conjunct */,
  int  maxDepth /* maximum recursion depth */,
  int  direction /* under (0) or over (1) approximation */)
{
    DdNode *res;

    do {
        dd->reordered = 0;
        res = cuddBddClippingAnd(dd,f,g,maxDepth,direction);
    } while (dd->reordered == 1);
    return(res);

} /* end of Cudd_bddClippingAnd */


DdNode *
Cudd_bddClippingAndAbstract(
  DdManager * dd /* manager */,
  DdNode * f /* first conjunct */,
  DdNode * g /* second conjunct */,
  DdNode * cube /* cube of variables to be abstracted */,
  int  maxDepth /* maximum recursion depth */,
  int  direction /* under (0) or over (1) approximation */)
{
    DdNode *res;

    do {
        dd->reordered = 0;
        res = cuddBddClippingAndAbstract(dd,f,g,cube,maxDepth,direction);
    } while (dd->reordered == 1);
    return(res);

} /* end of Cudd_bddClippingAndAbstract */


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


DdNode *
cuddBddClippingAnd(
  DdManager * dd /* manager */,
  DdNode * f /* first conjunct */,
  DdNode * g /* second conjunct */,
  int  maxDepth /* maximum recursion depth */,
  int  direction /* under (0) or over (1) approximation */)
{
    DdNode *res;

    res = cuddBddClippingAndRecur(dd,f,g,maxDepth,direction);

    return(res);

} /* end of cuddBddClippingAnd */


DdNode *
cuddBddClippingAndAbstract(
  DdManager * dd /* manager */,
  DdNode * f /* first conjunct */,
  DdNode * g /* second conjunct */,
  DdNode * cube /* cube of variables to be abstracted */,
  int  maxDepth /* maximum recursion depth */,
  int  direction /* under (0) or over (1) approximation */)
{
    DdNode *res;

    res = cuddBddClipAndAbsRecur(dd,f,g,cube,maxDepth,direction);

    return(res);

} /* end of cuddBddClippingAndAbstract */


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


static DdNode *
cuddBddClippingAndRecur(
  DdManager * manager,
  DdNode * f,
  DdNode * g,
  int  distance,
  int  direction)
{
    DdNode *F, *ft, *fe, *G, *gt, *ge;
    DdNode *one, *zero, *r, *t, *e;
    unsigned int topf, topg, index;
    DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);

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

    /* Terminal cases. */
    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
    if (f == g || g == one) return(f);
    if (f == one) return(g);
    if (distance == 0) {
        /* One last attempt at returning the right result. We sort of
        ** cheat by calling Cudd_bddLeq. */
        if (Cudd_bddLeq(manager,f,g)) return(f);
        if (Cudd_bddLeq(manager,g,f)) return(g);
        if (direction == 1) {
            if (Cudd_bddLeq(manager,f,Cudd_Not(g)) ||
                Cudd_bddLeq(manager,g,Cudd_Not(f))) return(zero);
        }
        return(Cudd_NotCond(one,(direction == 0)));
    }

    /* At this point f and g are not constant. */
    distance--;

    /* Check cache. Try to increase cache efficiency by sorting the
    ** pointers. */
    if (f > g) {
        DdNode *tmp = f;
        f = g; g = tmp;
    }
    F = Cudd_Regular(f);
    G = Cudd_Regular(g);
    cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *))
        (direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);
    if (F->ref != 1 || G->ref != 1) {
        r = cuddCacheLookup2(manager, cacheOp, f, g);
        if (r != NULL) return(r);
    }

    /* Here we can skip the use of cuddI, because the operands are known
    ** to be non-constant.
    */
    topf = manager->perm[F->index];
    topg = manager->perm[G->index];

    /* Compute cofactors. */
    if (topf <= topg) {
        index = F->index;
        ft = cuddT(F);
        fe = cuddE(F);
        if (Cudd_IsComplement(f)) {
            ft = Cudd_Not(ft);
            fe = Cudd_Not(fe);
        }
    } else {
        index = G->index;
        ft = fe = f;
    }

    if (topg <= topf) {
        gt = cuddT(G);
        ge = cuddE(G);
        if (Cudd_IsComplement(g)) {
            gt = Cudd_Not(gt);
            ge = Cudd_Not(ge);
        }
    } else {
        gt = ge = g;
    }

    t = cuddBddClippingAndRecur(manager, ft, gt, distance, direction);
    if (t == NULL) return(NULL);
    cuddRef(t);
    e = cuddBddClippingAndRecur(manager, fe, ge, distance, direction);
    if (e == NULL) {
        Cudd_RecursiveDeref(manager, t);
        return(NULL);
    }
    cuddRef(e);

    if (t == e) {
        r = t;
    } else {
        if (Cudd_IsComplement(t)) {
            r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
            if (r == NULL) {
                Cudd_RecursiveDeref(manager, t);
                Cudd_RecursiveDeref(manager, e);
                return(NULL);
            }
            r = Cudd_Not(r);
        } else {
            r = cuddUniqueInter(manager,(int)index,t,e);
            if (r == NULL) {
                Cudd_RecursiveDeref(manager, t);
                Cudd_RecursiveDeref(manager, e);
                return(NULL);
            }
        }
    }
    cuddDeref(e);
    cuddDeref(t);
    if (F->ref != 1 || G->ref != 1)
        cuddCacheInsert2(manager, cacheOp, f, g, r);
    return(r);

} /* end of cuddBddClippingAndRecur */


static DdNode *
cuddBddClipAndAbsRecur(
  DdManager * manager,
  DdNode * f,
  DdNode * g,
  DdNode * cube,
  int  distance,
  int  direction)
{
    DdNode *F, *ft, *fe, *G, *gt, *ge;
    DdNode *one, *zero, *r, *t, *e, *Cube;
    unsigned int topf, topg, topcube, top, index;
    ptruint cacheTag;

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

    /* Terminal cases. */
    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
    if (f == one && g == one)   return(one);
    if (cube == one) {
        return(cuddBddClippingAndRecur(manager, f, g, distance, direction));
    }
    if (f == one || f == g) {
        return (cuddBddExistAbstractRecur(manager, g, cube));
    }
    if (g == one) {
        return (cuddBddExistAbstractRecur(manager, f, cube));
    }
    if (distance == 0) return(Cudd_NotCond(one,(direction == 0)));

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

    /* Check cache. */
    if (f > g) { /* Try to increase cache efficiency. */
        DdNode *tmp = f;
        f = g; g = tmp;
    }
    F = Cudd_Regular(f);
    G = Cudd_Regular(g);
    cacheTag = direction ? DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG :
        DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG;
    if (F->ref != 1 || G->ref != 1) {
        r = cuddCacheLookup(manager, cacheTag,
                            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.
    */
    topf = manager->perm[F->index];
    topg = manager->perm[G->index];
    top = ddMin(topf, topg);
    topcube = manager->perm[cube->index];

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

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

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

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

    t = cuddBddClipAndAbsRecur(manager, ft, gt, Cube, distance, direction);
    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) {
        if (F->ref != 1 || G->ref != 1)
            cuddCacheInsert(manager, cacheTag, f, g, cube, one);
        return(one);
    }
    cuddRef(t);

    e = cuddBddClipAndAbsRecur(manager, fe, ge, Cube, distance, direction);
    if (e == NULL) {
        Cudd_RecursiveDeref(manager, t);
        return(NULL);
    }
    cuddRef(e);

    if (topcube == top) {       /* abstract */
        r = cuddBddClippingAndRecur(manager, Cudd_Not(t), Cudd_Not(e),
                                    distance, (direction == 0));
        if (r == NULL) {
            Cudd_RecursiveDeref(manager, t);
            Cudd_RecursiveDeref(manager, e);
            return(NULL);
        }
        r = Cudd_Not(r);
        cuddRef(r);
        Cudd_RecursiveDeref(manager, t);
        Cudd_RecursiveDeref(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_RecursiveDeref(manager, t);
                Cudd_RecursiveDeref(manager, e);
                return(NULL);
            }
            r = Cudd_Not(r);
        } else {
            r = cuddUniqueInter(manager,(int)index,t,e);
            if (r == NULL) {
                Cudd_RecursiveDeref(manager, t);
                Cudd_RecursiveDeref(manager, e);
                return(NULL);
            }
        }
        cuddDeref(e);
        cuddDeref(t);
    }
    if (F->ref != 1 || G->ref != 1)
        cuddCacheInsert(manager, cacheTag, f, g, cube, r);
    return (r);

} /* end of cuddBddClipAndAbsRecur */

---