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

#ifdef DD_DEBUG
static int addPermuteRecurHits;
static int bddPermuteRecurHits;
static int bddVectorComposeHits;
static int addVectorComposeHits;

static int addGeneralVectorComposeHits;
#endif

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


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

static DdNode * cuddAddPermuteRecur ARGS((DdManager *manager, DdHashTable *table, DdNode *node, int *permut));
static DdNode * cuddBddPermuteRecur ARGS((DdManager *manager, DdHashTable *table, DdNode *node, int *permut));
static DdNode * cuddBddVarMapRecur ARGS((DdManager *manager, DdNode *f));
static DdNode * cuddAddVectorComposeRecur ARGS((DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest));
static DdNode * cuddAddNonSimComposeRecur ARGS((DdManager *dd, DdNode *f, DdNode **vector, DdNode *key, DdNode *cube, int lastsub));
static DdNode * cuddBddVectorComposeRecur ARGS((DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest));
DD_INLINE static int ddIsIthAddVar ARGS((DdManager *dd, DdNode *f, unsigned int i));

static DdNode * cuddAddGeneralVectorComposeRecur ARGS((DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vectorOn, DdNode **vectorOff, int deepest));
DD_INLINE static int ddIsIthAddVarPair ARGS((DdManager *dd, DdNode *f, DdNode *g, unsigned int i));

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


DdNode *
Cudd_bddCompose(
  DdManager * dd,
  DdNode * f,
  DdNode * g,
  int  v)
{
    DdNode *proj, *res;

    /* Sanity check. */
    if (v < 0 || v > dd->size) return(NULL);

    proj =  dd->vars[v];
    do {
        dd->reordered = 0;
        res = cuddBddComposeRecur(dd,f,g,proj);
    } while (dd->reordered == 1);
    return(res);

} /* end of Cudd_bddCompose */


DdNode *
Cudd_addCompose(
  DdManager * dd,
  DdNode * f,
  DdNode * g,
  int  v)
{
    DdNode *proj, *res;

    /* Sanity check. */
    if (v < 0 || v > dd->size) return(NULL);

    proj =  dd->vars[v];
    do {
        dd->reordered = 0;
        res = cuddAddComposeRecur(dd,f,g,proj);
    } while (dd->reordered == 1);
    return(res);

} /* end of Cudd_addCompose */


DdNode *
Cudd_addPermute(
  DdManager * manager,
  DdNode * node,
  int * permut)
{
    DdHashTable         *table;
    DdNode              *res;

    do {
        manager->reordered = 0;
        table = cuddHashTableInit(manager,1,2);
        if (table == NULL) return(NULL);
        /* Recursively solve the problem. */
        res = cuddAddPermuteRecur(manager,table,node,permut);
        if (res != NULL) cuddRef(res);
        /* Dispose of local cache. */
        cuddHashTableQuit(table);
    } while (manager->reordered == 1);

    if (res != NULL) cuddDeref(res);
    return(res);

} /* end of Cudd_addPermute */


DdNode *
Cudd_addSwapVariables(
  DdManager * dd,
  DdNode * f,
  DdNode ** x,
  DdNode ** y,
  int  n)
{
    DdNode *swapped;
    int  i, j, k;
    int  *permut;

    permut = ALLOC(int,dd->size);
    if (permut == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }
    for (i = 0; i < dd->size; i++) permut[i] = i;
    for (i = 0; i < n; i++) {
        j = x[i]->index;
        k = y[i]->index;
        permut[j] = k;
        permut[k] = j;
    }

    swapped = Cudd_addPermute(dd,f,permut);
    FREE(permut);

    return(swapped);

} /* end of Cudd_addSwapVariables */


DdNode *
Cudd_bddPermute(
  DdManager * manager,
  DdNode * node,
  int * permut)
{
    DdHashTable         *table;
    DdNode              *res;

    do {
        manager->reordered = 0;
        table = cuddHashTableInit(manager,1,2);
        if (table == NULL) return(NULL);
        res = cuddBddPermuteRecur(manager,table,node,permut);
        if (res != NULL) cuddRef(res);
        /* Dispose of local cache. */
        cuddHashTableQuit(table);

    } while (manager->reordered == 1);

    if (res != NULL) cuddDeref(res);
    return(res);

} /* end of Cudd_bddPermute */


DdNode *
Cudd_bddVarMap(
  DdManager * manager /* DD manager */,
  DdNode * f /* function in which to remap variables */)
{
    DdNode *res;

    if (manager->map == NULL) return(NULL);
    do {
        manager->reordered = 0;
        res = cuddBddVarMapRecur(manager, f);
    } while (manager->reordered == 1);

    return(res);

} /* end of Cudd_bddVarMap */


int
Cudd_SetVarMap (
  DdManager *manager /* DD manager */,
  DdNode **x /* first array of variables */,
  DdNode **y /* second array of variables */,
  int n /* length of both arrays */)
{
    int i;

    if (manager->map != NULL) {
        cuddCacheFlush(manager);
    } else {
        manager->map = ALLOC(int,manager->maxSize);
        if (manager->map == NULL) {
            manager->errorCode = CUDD_MEMORY_OUT;
            return(0);
        }
        manager->memused += sizeof(int) * manager->maxSize;
    }
    /* Initialize the map to the identity. */
    for (i = 0; i < manager->size; i++) {
        manager->map[i] = i;
    }
    /* Create the map. */
    for (i = 0; i < n; i++) {
        manager->map[x[i]->index] = y[i]->index;
        manager->map[y[i]->index] = x[i]->index;
    }
    return(1);

} /* end of Cudd_SetVarMap */


DdNode *
Cudd_bddSwapVariables(
  DdManager * dd,
  DdNode * f,
  DdNode ** x,
  DdNode ** y,
  int  n)
{
    DdNode *swapped;
    int  i, j, k;
    int  *permut;

    permut = ALLOC(int,dd->size);
    if (permut == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }
    for (i = 0; i < dd->size; i++) permut[i] = i;
    for (i = 0; i < n; i++) {
        j = x[i]->index;
        k = y[i]->index;
        permut[j] = k;
        permut[k] = j;
    }

    swapped = Cudd_bddPermute(dd,f,permut);
    FREE(permut);

    return(swapped);

} /* end of Cudd_bddSwapVariables */


DdNode *
Cudd_bddAdjPermuteX(
  DdManager * dd,
  DdNode * B,
  DdNode ** x,
  int  n)
{
    DdNode *swapped;
    int  i, j, k;
    int  *permut;

    permut = ALLOC(int,dd->size);
    if (permut == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }
    for (i = 0; i < dd->size; i++) permut[i] = i;
    for (i = 0; i < n-2; i += 3) {
        j = x[i]->index;
        k = x[i+1]->index;
        permut[j] = k;
        permut[k] = j;
    }

    swapped = Cudd_bddPermute(dd,B,permut);
    FREE(permut);

    return(swapped);

} /* end of Cudd_bddAdjPermuteX */


DdNode *
Cudd_addVectorCompose(
  DdManager * dd,
  DdNode * f,
  DdNode ** vector)
{
    DdHashTable         *table;
    DdNode              *res;
    int                 deepest;
    int                 i;

    do {
        dd->reordered = 0;
        /* Initialize local cache. */
        table = cuddHashTableInit(dd,1,2);
        if (table == NULL) return(NULL);

        /* Find deepest real substitution. */
        for (deepest = dd->size - 1; deepest >= 0; deepest--) {
            i = dd->invperm[deepest];
            if (!ddIsIthAddVar(dd,vector[i],i)) {
                break;
            }
        }

        /* Recursively solve the problem. */
        res = cuddAddVectorComposeRecur(dd,table,f,vector,deepest);
        if (res != NULL) cuddRef(res);

        /* Dispose of local cache. */
        cuddHashTableQuit(table);
    } while (dd->reordered == 1);

    if (res != NULL) cuddDeref(res);
    return(res);

} /* end of Cudd_addVectorCompose */


DdNode *
Cudd_addGeneralVectorCompose(
  DdManager * dd,
  DdNode * f,
  DdNode ** vectorOn,
  DdNode ** vectorOff)
{
    DdHashTable         *table;
    DdNode              *res;
    int                 deepest;
    int                 i;

    do {
        dd->reordered = 0;
        /* Initialize local cache. */
        table = cuddHashTableInit(dd,1,2);
        if (table == NULL) return(NULL);

        /* Find deepest real substitution. */
        for (deepest = dd->size - 1; deepest >= 0; deepest--) {
            i = dd->invperm[deepest];
            if (!ddIsIthAddVarPair(dd,vectorOn[i],vectorOff[i],i)) {
                break;
            }
        }

        /* Recursively solve the problem. */
        res = cuddAddGeneralVectorComposeRecur(dd,table,f,vectorOn,
                                               vectorOff,deepest);
        if (res != NULL) cuddRef(res);

        /* Dispose of local cache. */
        cuddHashTableQuit(table);
    } while (dd->reordered == 1);

    if (res != NULL) cuddDeref(res);
    return(res);

} /* end of Cudd_addGeneralVectorCompose */


DdNode *
Cudd_addNonSimCompose(
  DdManager * dd,
  DdNode * f,
  DdNode ** vector)
{
    DdNode              *cube, *key, *var, *tmp, *piece;
    DdNode              *res;
    int                 i, lastsub;

    /* The cache entry for this function is composed of three parts:
    ** f itself, the replacement relation, and the cube of the
    ** variables being substituted.
    ** The replacement relation is the product of the terms (yi EXNOR gi).
    ** This apporach allows us to use the global cache for this function,
    ** with great savings in memory with respect to using arrays for the
    ** cache entries.
    ** First we build replacement relation and cube of substituted
    ** variables from the vector specifying the desired composition.
    */
    key = DD_ONE(dd);
    cuddRef(key);
    cube = DD_ONE(dd);
    cuddRef(cube);
    for (i = (int) dd->size - 1; i >= 0; i--) {
        if (ddIsIthAddVar(dd,vector[i],(unsigned int)i)) {
            continue;
        }
        var = Cudd_addIthVar(dd,i);
        if (var == NULL) {
            Cudd_RecursiveDeref(dd,key);
            Cudd_RecursiveDeref(dd,cube);
            return(NULL);
        }
        cuddRef(var);
        /* Update cube. */
        tmp = Cudd_addApply(dd,Cudd_addTimes,var,cube);
        if (tmp == NULL) {
            Cudd_RecursiveDeref(dd,key);
            Cudd_RecursiveDeref(dd,cube);
            Cudd_RecursiveDeref(dd,var);
            return(NULL);
        }
        cuddRef(tmp);
        Cudd_RecursiveDeref(dd,cube);
        cube = tmp;
        /* Update replacement relation. */
        piece = Cudd_addApply(dd,Cudd_addXnor,var,vector[i]);
        if (piece == NULL) {
            Cudd_RecursiveDeref(dd,key);
            Cudd_RecursiveDeref(dd,var);
            return(NULL);
        }
        cuddRef(piece);
        Cudd_RecursiveDeref(dd,var);
        tmp = Cudd_addApply(dd,Cudd_addTimes,key,piece);
        if (tmp == NULL) {
            Cudd_RecursiveDeref(dd,key);
            Cudd_RecursiveDeref(dd,piece);
            return(NULL);
        }
        cuddRef(tmp);
        Cudd_RecursiveDeref(dd,key);
        Cudd_RecursiveDeref(dd,piece);
        key = tmp;
    }

    /* Now try composition, until no reordering occurs. */
    do {
        /* Find real substitution with largest index. */
        for (lastsub = dd->size - 1; lastsub >= 0; lastsub--) {
            if (!ddIsIthAddVar(dd,vector[lastsub],(unsigned int)lastsub)) {
                break;
            }
        }

        /* Recursively solve the problem. */
        dd->reordered = 0;
        res = cuddAddNonSimComposeRecur(dd,f,vector,key,cube,lastsub+1);
        if (res != NULL) cuddRef(res);

    } while (dd->reordered == 1);

    Cudd_RecursiveDeref(dd,key);
    Cudd_RecursiveDeref(dd,cube);
    if (res != NULL) cuddDeref(res);
    return(res);

} /* end of Cudd_addNonSimCompose */


DdNode *
Cudd_bddVectorCompose(
  DdManager * dd,
  DdNode * f,
  DdNode ** vector)
{
    DdHashTable         *table;
    DdNode              *res;
    int                 deepest;
    int                 i;

    do {
        dd->reordered = 0;
        /* Initialize local cache. */
        table = cuddHashTableInit(dd,1,2);
        if (table == NULL) return(NULL);

        /* Find deepest real substitution. */
        for (deepest = dd->size - 1; deepest >= 0; deepest--) {
            i = dd->invperm[deepest];
            if (vector[i] != dd->vars[i]) {
                break;
            }
        }

        /* Recursively solve the problem. */
        res = cuddBddVectorComposeRecur(dd,table,f,vector, deepest);
        if (res != NULL) cuddRef(res);

        /* Dispose of local cache. */
        cuddHashTableQuit(table);
    } while (dd->reordered == 1);

    if (res != NULL) cuddDeref(res);
    return(res);

} /* end of Cudd_bddVectorCompose */


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


DdNode *
cuddBddComposeRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * g,
  DdNode * proj)
{
    DdNode      *F, *G, *f1, *f0, *g1, *g0, *r, *t, *e;
    unsigned int v, topf, topg, topindex;
    int         comple;

    statLine(dd);
    v = dd->perm[proj->index];
    F = Cudd_Regular(f);
    topf = cuddI(dd,F->index);

    /* Terminal case. Subsumes the test for constant f. */
    if (topf > v) return(f);

    /* We solve the problem for a regular pointer, and then complement
    ** the result if the pointer was originally complemented.
    */
    comple = Cudd_IsComplement(f);

    /* Check cache. */
    r = cuddCacheLookup(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj);
    if (r != NULL) {
        return(Cudd_NotCond(r,comple));
    }

    if (topf == v) {
        /* Compose. */
        f1 = cuddT(F);
        f0 = cuddE(F);
        r = cuddBddIteRecur(dd, g, f1, f0);
        if (r == NULL) return(NULL);
    } else {
        /* Compute cofactors of f and g. Remember the index of the top
        ** variable.
        */
        G = Cudd_Regular(g);
        topg = cuddI(dd,G->index);
        if (topf > topg) {
            topindex = G->index;
            f1 = f0 = F;
        } else {
            topindex = F->index;
            f1 = cuddT(F);
            f0 = cuddE(F);
        }
        if (topg > topf) {
            g1 = g0 = g;
        } else {
            g1 = cuddT(G);
            g0 = cuddE(G);
            if (g != G) {
                g1 = Cudd_Not(g1);
                g0 = Cudd_Not(g0);
            }
        }
        /* Recursive step. */
        t = cuddBddComposeRecur(dd, f1, g1, proj);
        if (t == NULL) return(NULL);
        cuddRef(t);
        e = cuddBddComposeRecur(dd, f0, g0, proj);
        if (e == NULL) {
            Cudd_IterDerefBdd(dd, t);
            return(NULL);
        }
        cuddRef(e);

        r = cuddBddIteRecur(dd, dd->vars[topindex], t, e);
        if (r == NULL) {
            Cudd_IterDerefBdd(dd, t);
            Cudd_IterDerefBdd(dd, e);
            return(NULL);
        }
        cuddRef(r);
        Cudd_IterDerefBdd(dd, t); /* t & e not necessarily part of r */
        Cudd_IterDerefBdd(dd, e);
        cuddDeref(r);
    }

    cuddCacheInsert(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj,r);

    return(Cudd_NotCond(r,comple));

} /* end of cuddBddComposeRecur */


DdNode *
cuddAddComposeRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * g,
  DdNode * proj)
{
    DdNode *f1, *f0, *g1, *g0, *r, *t, *e;
    unsigned int v, topf, topg, topindex;

    statLine(dd);
    v = dd->perm[proj->index];
    topf = cuddI(dd,f->index);

    /* Terminal case. Subsumes the test for constant f. */
    if (topf > v) return(f);

    /* Check cache. */
    r = cuddCacheLookup(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj);
    if (r != NULL) {
        return(r);
    }

    if (topf == v) {
        /* Compose. */
        f1 = cuddT(f);
        f0 = cuddE(f);
        r = cuddAddIteRecur(dd, g, f1, f0);
        if (r == NULL) return(NULL);
    } else {
        /* Compute cofactors of f and g. Remember the index of the top
        ** variable.
        */
        topg = cuddI(dd,g->index);
        if (topf > topg) {
            topindex = g->index;
            f1 = f0 = f;
        } else {
            topindex = f->index;
            f1 = cuddT(f);
            f0 = cuddE(f);
        }
        if (topg > topf) {
            g1 = g0 = g;
        } else {
            g1 = cuddT(g);
            g0 = cuddE(g);
        }
        /* Recursive step. */
        t = cuddAddComposeRecur(dd, f1, g1, proj);
        if (t == NULL) return(NULL);
        cuddRef(t);
        e = cuddAddComposeRecur(dd, f0, g0, proj);
        if (e == NULL) {
            Cudd_RecursiveDeref(dd, t);
            return(NULL);
        }
        cuddRef(e);

        if (t == e) {
            r = t;
        } else {
            r = cuddUniqueInter(dd, (int) topindex, t, e);
            if (r == NULL) {
                Cudd_RecursiveDeref(dd, t);
                Cudd_RecursiveDeref(dd, e);
                return(NULL);
            }
        }
        cuddDeref(t);
        cuddDeref(e);
    }

    cuddCacheInsert(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj,r);

    return(r);

} /* end of cuddAddComposeRecur */


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


static DdNode *
cuddAddPermuteRecur(
  DdManager * manager /* DD manager */,
  DdHashTable * table /* computed table */,
  DdNode * node /* ADD to be reordered */,
  int * permut /* permutation array */)
{
    DdNode      *T,*E;
    DdNode      *res,*var;
    int         index;
    
    statLine(manager);
    /* Check for terminal case of constant node. */
    if (cuddIsConstant(node)) {
        return(node);
    }

    /* If problem already solved, look up answer and return. */
    if (node->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
#ifdef DD_DEBUG
        addPermuteRecurHits++;
#endif
        return(res);
    }

    /* Split and recur on children of this node. */
    T = cuddAddPermuteRecur(manager,table,cuddT(node),permut);
    if (T == NULL) return(NULL);
    cuddRef(T);
    E = cuddAddPermuteRecur(manager,table,cuddE(node),permut);
    if (E == NULL) {
        Cudd_RecursiveDeref(manager, T);
        return(NULL);
    }
    cuddRef(E);

    /* Move variable that should be in this position to this position
    ** by creating a single var ADD for that variable, and calling
    ** cuddAddIteRecur with the T and E we just created.
    */
    index = permut[node->index];
    var = cuddUniqueInter(manager,index,DD_ONE(manager),DD_ZERO(manager));
    if (var == NULL) return(NULL);
    cuddRef(var);
    res = cuddAddIteRecur(manager,var,T,E);
    if (res == NULL) {
        Cudd_RecursiveDeref(manager,var);
        Cudd_RecursiveDeref(manager, T);
        Cudd_RecursiveDeref(manager, E);
        return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(manager,var);
    Cudd_RecursiveDeref(manager, T);
    Cudd_RecursiveDeref(manager, E);

    /* Do not keep the result if the reference count is only 1, since
    ** it will not be visited again.
    */
    if (node->ref != 1) {
        ptrint fanout = (ptrint) node->ref;
        cuddSatDec(fanout);
        if (!cuddHashTableInsert1(table,node,res,fanout)) {
            Cudd_RecursiveDeref(manager, res);
            return(NULL);
        }
    }
    cuddDeref(res);
    return(res);

} /* end of cuddAddPermuteRecur */


static DdNode *
cuddBddPermuteRecur(
  DdManager * manager /* DD manager */,
  DdHashTable * table /* computed table */,
  DdNode * node /* BDD to be reordered */,
  int * permut /* permutation array */)
{
    DdNode      *N,*T,*E;
    DdNode      *res;
    int         index;

    statLine(manager);
    N = Cudd_Regular(node);

    /* Check for terminal case of constant node. */
    if (cuddIsConstant(N)) {
        return(node);
    }

    /* If problem already solved, look up answer and return. */
    if (N->ref != 1 && (res = cuddHashTableLookup1(table,N)) != NULL) {
#ifdef DD_DEBUG
        bddPermuteRecurHits++;
#endif
        return(Cudd_NotCond(res,N != node));
    }

    /* Split and recur on children of this node. */
    T = cuddBddPermuteRecur(manager,table,cuddT(N),permut);
    if (T == NULL) return(NULL);
    cuddRef(T);
    E = cuddBddPermuteRecur(manager,table,cuddE(N),permut);
    if (E == NULL) {
        Cudd_IterDerefBdd(manager, T);
        return(NULL);
    }
    cuddRef(E);

    /* Move variable that should be in this position to this position
    ** by retrieving the single var BDD for that variable, and calling
    ** cuddBddIteRecur with the T and E we just created.
    */
    index = permut[N->index];
    res = cuddBddIteRecur(manager,manager->vars[index],T,E);
    if (res == NULL) {
        Cudd_IterDerefBdd(manager, T);
        Cudd_IterDerefBdd(manager, E);
        return(NULL);
    }
    cuddRef(res);
    Cudd_IterDerefBdd(manager, T);
    Cudd_IterDerefBdd(manager, E);

    /* Do not keep the result if the reference count is only 1, since
    ** it will not be visited again.
    */
    if (N->ref != 1) {
        ptrint fanout = (ptrint) N->ref;
        cuddSatDec(fanout);
        if (!cuddHashTableInsert1(table,N,res,fanout)) {
            Cudd_IterDerefBdd(manager, res);
            return(NULL);
        }
    }
    cuddDeref(res);
    return(Cudd_NotCond(res,N != node));

} /* end of cuddBddPermuteRecur */


static DdNode *
cuddBddVarMapRecur(
  DdManager *manager /* DD manager */,
  DdNode *f /* BDD to be remapped */)
{
    DdNode      *F, *T, *E;
    DdNode      *res;
    int         index;

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

    /* Check for terminal case of constant node. */
    if (cuddIsConstant(F)) {
        return(f);
    }

    /* If problem already solved, look up answer and return. */
    if (F->ref != 1 &&
        (res = cuddCacheLookup1(manager,Cudd_bddVarMap,F)) != NULL) {
        return(Cudd_NotCond(res,F != f));
    }

    /* Split and recur on children of this node. */
    T = cuddBddVarMapRecur(manager,cuddT(F));
    if (T == NULL) return(NULL);
    cuddRef(T);
    E = cuddBddVarMapRecur(manager,cuddE(F));
    if (E == NULL) {
        Cudd_IterDerefBdd(manager, T);
        return(NULL);
    }
    cuddRef(E);

    /* Move variable that should be in this position to this position
    ** by retrieving the single var BDD for that variable, and calling
    ** cuddBddIteRecur with the T and E we just created.
    */
    index = manager->map[F->index];
    res = cuddBddIteRecur(manager,manager->vars[index],T,E);
    if (res == NULL) {
        Cudd_IterDerefBdd(manager, T);
        Cudd_IterDerefBdd(manager, E);
        return(NULL);
    }
    cuddRef(res);
    Cudd_IterDerefBdd(manager, T);
    Cudd_IterDerefBdd(manager, E);

    /* Do not keep the result if the reference count is only 1, since
    ** it will not be visited again.
    */
    if (F->ref != 1) {
        cuddCacheInsert1(manager,Cudd_bddVarMap,F,res);
    }
    cuddDeref(res);
    return(Cudd_NotCond(res,F != f));

} /* end of cuddBddVarMapRecur */


static DdNode *
cuddAddVectorComposeRecur(
  DdManager * dd /* DD manager */,
  DdHashTable * table /* computed table */,
  DdNode * f /* ADD in which to compose */,
  DdNode ** vector /* functions to substitute */,
  int  deepest /* depth of deepest substitution */)
{
    DdNode      *T,*E;
    DdNode      *res;

    statLine(dd);
    /* If we are past the deepest substitution, return f. */
    if (cuddI(dd,f->index) > deepest) {
        return(f);
    }

    if ((res = cuddHashTableLookup1(table,f)) != NULL) {
#ifdef DD_DEBUG
        addVectorComposeHits++;
#endif
        return(res);
    }

    /* Split and recur on children of this node. */
    T = cuddAddVectorComposeRecur(dd,table,cuddT(f),vector,deepest);
    if (T == NULL)  return(NULL);
    cuddRef(T);
    E = cuddAddVectorComposeRecur(dd,table,cuddE(f),vector,deepest);
    if (E == NULL) {
        Cudd_RecursiveDeref(dd, T);
        return(NULL);
    }
    cuddRef(E);

    /* Retrieve the 0-1 ADD for the current top variable and call
    ** cuddAddIteRecur with the T and E we just created.
    */
    res = cuddAddIteRecur(dd,vector[f->index],T,E);
    if (res == NULL) {
        Cudd_RecursiveDeref(dd, T);
        Cudd_RecursiveDeref(dd, E);
        return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(dd, T);
    Cudd_RecursiveDeref(dd, E);

    /* Do not keep the result if the reference count is only 1, since
    ** it will not be visited again
    */
    if (f->ref != 1) {
        ptrint fanout = (ptrint) f->ref;
        cuddSatDec(fanout);
        if (!cuddHashTableInsert1(table,f,res,fanout)) {
            Cudd_RecursiveDeref(dd, res);
            return(NULL);
        }
    }
    cuddDeref(res);
    return(res);

} /* end of cuddAddVectorComposeRecur */


static DdNode *
cuddAddGeneralVectorComposeRecur(
  DdManager * dd /* DD manager */,
  DdHashTable * table /* computed table */,
  DdNode * f /* ADD in which to compose */,
  DdNode ** vectorOn /* functions to substitute for x_i */,
  DdNode ** vectorOff /* functions to substitute for x_i' */,
  int  deepest /* depth of deepest substitution */)
{
    DdNode      *T,*E,*t,*e;
    DdNode      *res;

    /* If we are past the deepest substitution, return f. */
    if (cuddI(dd,f->index) > deepest) {
        return(f);
    }

    if ((res = cuddHashTableLookup1(table,f)) != NULL) {
#ifdef DD_DEBUG
        addGeneralVectorComposeHits++;
#endif
        return(res);
    }

    /* Split and recur on children of this node. */
    T = cuddAddGeneralVectorComposeRecur(dd,table,cuddT(f),
                                         vectorOn,vectorOff,deepest);
    if (T == NULL)  return(NULL);
    cuddRef(T);
    E = cuddAddGeneralVectorComposeRecur(dd,table,cuddE(f),
                                         vectorOn,vectorOff,deepest);
    if (E == NULL) {
        Cudd_RecursiveDeref(dd, T);
        return(NULL);
    }
    cuddRef(E);

    /* Retrieve the compose ADDs for the current top variable and call
    ** cuddAddApplyRecur with the T and E we just created.
    */
    t = cuddAddApplyRecur(dd,Cudd_addTimes,vectorOn[f->index],T);
    if (t == NULL) {
      Cudd_RecursiveDeref(dd,T);
      Cudd_RecursiveDeref(dd,E);
      return(NULL);
    }
    cuddRef(t);
    e = cuddAddApplyRecur(dd,Cudd_addTimes,vectorOff[f->index],E);
    if (e == NULL) {
      Cudd_RecursiveDeref(dd,T);
      Cudd_RecursiveDeref(dd,E);
      Cudd_RecursiveDeref(dd,t);
      return(NULL);
    }
    cuddRef(e);
    res = cuddAddApplyRecur(dd,Cudd_addPlus,t,e);
    if (res == NULL) {
      Cudd_RecursiveDeref(dd,T);
      Cudd_RecursiveDeref(dd,E);
      Cudd_RecursiveDeref(dd,t);
      Cudd_RecursiveDeref(dd,e);
      return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(dd,T);
    Cudd_RecursiveDeref(dd,E);
    Cudd_RecursiveDeref(dd,t);
    Cudd_RecursiveDeref(dd,e);

    /* Do not keep the result if the reference count is only 1, since
    ** it will not be visited again
    */
    if (f->ref != 1) {
        ptrint fanout = (ptrint) f->ref;
        cuddSatDec(fanout);
        if (!cuddHashTableInsert1(table,f,res,fanout)) {
            Cudd_RecursiveDeref(dd, res);
            return(NULL);
        }
    }
    cuddDeref(res);
    return(res);

} /* end of cuddAddGeneralVectorComposeRecur */


static DdNode *
cuddAddNonSimComposeRecur(
  DdManager * dd,
  DdNode * f,
  DdNode ** vector,
  DdNode * key,
  DdNode * cube,
  int  lastsub)
{
    DdNode *f1, *f0, *key1, *key0, *cube1, *var;
    DdNode *T,*E;
    DdNode *r;
    unsigned int top, topf, topk, topc;
    unsigned int index;
    int i;
    DdNode **vect1;
    DdNode **vect0;

    statLine(dd);
    /* If we are past the deepest substitution, return f. */
    if (cube == DD_ONE(dd) || cuddIsConstant(f)) {
        return(f);
    }

    /* If problem already solved, look up answer and return. */
    r = cuddCacheLookup(dd,DD_ADD_NON_SIM_COMPOSE_TAG,f,key,cube);
    if (r != NULL) {
        return(r);
    }

    /* Find top variable. we just need to look at f, key, and cube,
    ** because all the varibles in the gi are in key.
    */
    topf = cuddI(dd,f->index);
    topk = cuddI(dd,key->index);
    top = ddMin(topf,topk);
    topc = cuddI(dd,cube->index);
    top = ddMin(top,topc);
    index = dd->invperm[top];

    /* Compute the cofactors. */
    if (topf == top) {
        f1 = cuddT(f);
        f0 = cuddE(f);
    } else {
        f1 = f0 = f;
    }
    if (topc == top) {
        cube1 = cuddT(cube);
        /* We want to eliminate vector[index] from key. Otherwise
        ** cache performance is severely affected. Hence we
        ** existentially quantify the variable with index "index" from key.
        */
        var = Cudd_addIthVar(dd, (int) index);
        if (var == NULL) {
            return(NULL);
        }
        cuddRef(var);
        key1 = cuddAddExistAbstractRecur(dd, key, var);
        if (key1 == NULL) {
            Cudd_RecursiveDeref(dd,var);
            return(NULL);
        }
        cuddRef(key1);
        Cudd_RecursiveDeref(dd,var);
        key0 = key1;
    } else {
        cube1 = cube;
        if (topk == top) {
            key1 = cuddT(key);
            key0 = cuddE(key);
        } else {
            key1 = key0 = key;
        }
        cuddRef(key1);
    }

    /* Allocate two new vectors for the cofactors of vector. */
    vect1 = ALLOC(DdNode *,lastsub);
    if (vect1 == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        Cudd_RecursiveDeref(dd,key1);
        return(NULL);
    }
    vect0 = ALLOC(DdNode *,lastsub);
    if (vect0 == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        Cudd_RecursiveDeref(dd,key1);
        FREE(vect1);
        return(NULL);
    }

    /* Cofactor the gi. Eliminate vect1[index] and vect0[index], because
    ** we do not need them.
    */
    for (i = 0; i < lastsub; i++) {
        DdNode *gi = vector[i];
        if (gi == NULL) {
            vect1[i] = vect0[i] = NULL;
        } else if (gi->index == index) {
            vect1[i] = cuddT(gi);
            vect0[i] = cuddE(gi);
        } else {
            vect1[i] = vect0[i] = gi;
        }
    }
    vect1[index] = vect0[index] = NULL;

    /* Recur on children. */
    T = cuddAddNonSimComposeRecur(dd,f1,vect1,key1,cube1,lastsub);
    FREE(vect1);
    if (T == NULL) {
        Cudd_RecursiveDeref(dd,key1);
        FREE(vect0);
        return(NULL);
    }
    cuddRef(T);
    E = cuddAddNonSimComposeRecur(dd,f0,vect0,key0,cube1,lastsub);
    FREE(vect0);
    if (E == NULL) {
        Cudd_RecursiveDeref(dd,key1);
        Cudd_RecursiveDeref(dd,T);
        return(NULL);
    }
    cuddRef(E);
    Cudd_RecursiveDeref(dd,key1);

    /* Retrieve the 0-1 ADD for the current top variable from vector,
    ** and call cuddAddIteRecur with the T and E we just created.
    */
    r = cuddAddIteRecur(dd,vector[index],T,E);
    if (r == NULL) {
        Cudd_RecursiveDeref(dd,T);
        Cudd_RecursiveDeref(dd,E);
        return(NULL);
    }
    cuddRef(r);
    Cudd_RecursiveDeref(dd,T);
    Cudd_RecursiveDeref(dd,E);
    cuddDeref(r);

    /* Store answer to trim recursion. */
    cuddCacheInsert(dd,DD_ADD_NON_SIM_COMPOSE_TAG,f,key,cube,r);

    return(r);

} /* end of cuddAddNonSimComposeRecur */


static DdNode *
cuddBddVectorComposeRecur(
  DdManager * dd /* DD manager */,
  DdHashTable * table /* computed table */,
  DdNode * f /* BDD in which to compose */,
  DdNode ** vector /* functions to be composed */,
  int deepest /* depth of the deepest substitution */)
{
    DdNode      *F,*T,*E;
    DdNode      *res;

    statLine(dd);
    F = Cudd_Regular(f);

    /* If we are past the deepest substitution, return f. */
    if (cuddI(dd,F->index) > deepest) {
        return(f);
    }

    /* If problem already solved, look up answer and return. */
    if ((res = cuddHashTableLookup1(table,F)) != NULL) {
#ifdef DD_DEBUG
        bddVectorComposeHits++;
#endif
        return(Cudd_NotCond(res,F != f));
    }

    /* Split and recur on children of this node. */
    T = cuddBddVectorComposeRecur(dd,table,cuddT(F),vector, deepest);
    if (T == NULL) return(NULL);
    cuddRef(T);
    E = cuddBddVectorComposeRecur(dd,table,cuddE(F),vector, deepest);
    if (E == NULL) {
        Cudd_IterDerefBdd(dd, T);
        return(NULL);
    }
    cuddRef(E);

    /* Call cuddBddIteRecur with the BDD that replaces the current top
    ** variable and the T and E we just created.
    */
    res = cuddBddIteRecur(dd,vector[F->index],T,E);
    if (res == NULL) {
        Cudd_IterDerefBdd(dd, T);
        Cudd_IterDerefBdd(dd, E);
        return(NULL);
    }
    cuddRef(res);
    Cudd_IterDerefBdd(dd, T);
    Cudd_IterDerefBdd(dd, E);   

    /* Do not keep the result if the reference count is only 1, since
    ** it will not be visited again.
    */
    if (F->ref != 1) {
        ptrint fanout = (ptrint) F->ref;
        cuddSatDec(fanout);
        if (!cuddHashTableInsert1(table,F,res,fanout)) {
            Cudd_IterDerefBdd(dd, res);
            return(NULL);
        }
    }
    cuddDeref(res);
    return(Cudd_NotCond(res,F != f));

} /* end of cuddBddVectorComposeRecur */


DD_INLINE
static int
ddIsIthAddVar(
  DdManager * dd,
  DdNode * f,
  unsigned int  i)
{
    return(f->index == i && cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd));

} /* end of ddIsIthAddVar */


DD_INLINE
static int
ddIsIthAddVarPair(
  DdManager * dd,
  DdNode * f,
  DdNode * g,
  unsigned int  i)
{
    return(f->index == i && g->index == i && 
           cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd) &&
           cuddT(g) == DD_ZERO(dd) && cuddE(g) == DD_ONE(dd));

} /* end of ddIsIthAddVarPair */

---