Version abc70930

1 files changed, 0 insertions, 1722 deletions

diff --git a/src/bdd/cudd/cuddCompose.c b/src/bdd/cudd/cuddCompose.c
deleted file mode 100644
index 8c858051..00000000
--- a/src/bdd/cudd/cuddCompose.c
+++ /dev/null
@@ -1,1722 +0,0 @@
-/**CFile***********************************************************************
-
-  FileName    [cuddCompose.c]
-
-  PackageName [cudd]
-
-  Synopsis    [Functional composition and variable permutation of DDs.]
-
-  Description [External procedures included in this module:
-        <ul>
-        <li> Cudd_bddCompose()
-        <li> Cudd_addCompose()
-        <li> Cudd_addPermute()
-        <li> Cudd_addSwapVariables()
-        <li> Cudd_bddPermute()
-        <li> Cudd_bddVarMap()
-        <li> Cudd_SetVarMap()
-        <li> Cudd_bddSwapVariables()
-        <li> Cudd_bddAdjPermuteX()
-        <li> Cudd_addVectorCompose()
-        <li> Cudd_addGeneralVectorCompose()
-        <li> Cudd_addNonSimCompose()
-        <li> Cudd_bddVectorCompose()
-        </ul>
-           Internal procedures included in this module:
-        <ul>
-        <li> cuddBddComposeRecur()
-        <li> cuddAddComposeRecur()
-        </ul>
-           Static procedures included in this module:
-        <ul>
-        <li> cuddAddPermuteRecur()
-        <li> cuddBddPermuteRecur()
-        <li> cuddBddVarMapRecur()
-        <li> cuddAddVectorComposeRecur()
-        <li> cuddAddGeneralVectorComposeRecur()
-        <li> cuddAddNonSimComposeRecur()
-        <li> cuddBddVectorComposeRecur()
-        <li> ddIsIthAddVar()
-        <li> ddIsIthAddVarPair()
-           </ul>
-  The permutation functions use a local cache because the results to
-  be remembered depend on the permutation being applied.  Since the
-  permutation is just an array, it cannot be stored in the global
-  cache. There are different procedured for BDDs and ADDs. This is
-  because bddPermuteRecur uses cuddBddIteRecur. If this were changed,
-  the procedures could be merged.]
-
-  Author      [Fabio Somenzi and Kavita Ravi]
-
-  Copyright   [This file was created at the University of Colorado at
-  Boulder.  The University of Colorado at Boulder makes no warranty
-  about the suitability of this software for any purpose.  It is
-  presented on an AS IS basis.]
-
-******************************************************************************/
-
-#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                                                        */
-/*---------------------------------------------------------------------------*/
-
-
-/**AutomaticStart*************************************************************/
-
-/*---------------------------------------------------------------------------*/
-/* 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));
-
-/**AutomaticEnd***************************************************************/
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of exported functions                                          */
-/*---------------------------------------------------------------------------*/
-
-
-/**Function********************************************************************
-
-  Synopsis    [Substitutes g for x_v in the BDD for f.]
-
-  Description [Substitutes g for x_v in the BDD for f. v is the index of the
-  variable to be substituted. Cudd_bddCompose passes the corresponding
-  projection function to the recursive procedure, so that the cache may
-  be used.  Returns the composed BDD if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_addCompose]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Substitutes g for x_v in the ADD for f.]
-
-  Description [Substitutes g for x_v in the ADD for f. v is the index of the
-  variable to be substituted. g must be a 0-1 ADD. Cudd_bddCompose passes
-  the corresponding projection function to the recursive procedure, so
-  that the cache may be used.  Returns the composed ADD if successful;
-  NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Permutes the variables of an ADD.]
-
-  Description [Given a permutation in array permut, creates a new ADD
-  with permuted variables. There should be an entry in array permut
-  for each variable in the manager. The i-th entry of permut holds the
-  index of the variable that is to substitute the i-th
-  variable. Returns a pointer to the resulting ADD if successful; NULL
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddPermute Cudd_addSwapVariables]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis [Swaps two sets of variables of the same size (x and y) in
-  the ADD f.]
-
-  Description [Swaps two sets of variables of the same size (x and y) in
-  the ADD f.  The size is given by n. The two sets of variables are
-  assumed to be disjoint. Returns a pointer to the resulting ADD if
-  successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_addPermute Cudd_bddSwapVariables]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Permutes the variables of a BDD.]
-
-  Description [Given a permutation in array permut, creates a new BDD
-  with permuted variables. There should be an entry in array permut
-  for each variable in the manager. The i-th entry of permut holds the
-  index of the variable that is to substitute the i-th variable.
-  Returns a pointer to the resulting BDD if successful; NULL
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_addPermute Cudd_bddSwapVariables]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Remaps the variables of a BDD using the default variable map.]
-
-  Description [Remaps the variables of a BDD using the default
-  variable map.  A typical use of this function is to swap two sets of
-  variables.  The variable map must be registered with Cudd_SetVarMap.
-  Returns a pointer to the resulting BDD if successful; NULL
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddPermute Cudd_bddSwapVariables Cudd_SetVarMap]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis [Registers a variable mapping with the manager.]
-
-  Description [Registers with the manager a variable mapping described
-  by two sets of variables.  This variable mapping is then used by
-  functions like Cudd_bddVarMap.  This function is convenient for
-  those applications that perform the same mapping several times.
-  However, if several different permutations are used, it may be more
-  efficient not to rely on the registered mapping, because changing
-  mapping causes the cache to be cleared.  (The initial setting,
-  however, does not clear the cache.) The two sets of variables (x and
-  y) must have the same size (x and y).  The size is given by n. The
-  two sets of variables are normally disjoint, but this restriction is
-  not imposeded by the function. When new variables are created, the
-  map is automatically extended (each new variable maps to
-  itself). The typical use, however, is to wait until all variables
-  are created, and then create the map.  Returns 1 if the mapping is
-  successfully registered with the manager; 0 otherwise.]
-
-  SideEffects [Modifies the manager. May clear the cache.]
-
-  SeeAlso     [Cudd_bddVarMap Cudd_bddPermute Cudd_bddSwapVariables]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis [Swaps two sets of variables of the same size (x and y) in
-  the BDD f.]
-
-  Description [Swaps two sets of variables of the same size (x and y)
-  in the BDD f. The size is given by n. The two sets of variables are
-  assumed to be disjoint.  Returns a pointer to the resulting BDD if
-  successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddPermute Cudd_addSwapVariables]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis [Rearranges a set of variables in the BDD B.]
-
-  Description [Rearranges a set of variables in the BDD B. The size of
-  the set is given by n. This procedure is intended for the
-  `randomization' of the priority functions. Returns a pointer to the
-  BDD if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddPermute Cudd_bddSwapVariables
-  Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_PrioritySelect]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Composes an ADD with a vector of 0-1 ADDs.]
-
-  Description [Given a vector of 0-1 ADDs, creates a new ADD by
-  substituting the 0-1 ADDs for the variables of the ADD f.  There
-  should be an entry in vector for each variable in the manager.
-  If no substitution is sought for a given variable, the corresponding
-  projection function should be specified in the vector.
-  This function implements simultaneous composition.
-  Returns a pointer to the resulting ADD if successful; NULL
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_addNonSimCompose Cudd_addPermute Cudd_addCompose
-  Cudd_bddVectorCompose]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Composes an ADD with a vector of ADDs.]
-
-  Description [Given a vector of ADDs, creates a new ADD by substituting the
-  ADDs for the variables of the ADD f. vectorOn contains ADDs to be substituted
-  for the x_v and vectorOff the ADDs to be substituted for x_v'. There should
-  be an entry in vector for each variable in the manager.  If no substitution
-  is sought for a given variable, the corresponding projection function should
-  be specified in the vector.  This function implements simultaneous
-  composition.  Returns a pointer to the resulting ADD if successful; NULL
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso [Cudd_addVectorCompose Cudd_addNonSimCompose Cudd_addPermute
-  Cudd_addCompose Cudd_bddVectorCompose]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Composes an ADD with a vector of 0-1 ADDs.]
-
-  Description [Given a vector of 0-1 ADDs, creates a new ADD by
-  substituting the 0-1 ADDs for the variables of the ADD f.  There
-  should be an entry in vector for each variable in the manager.
-  This function implements non-simultaneous composition. If any of the
-  functions being composed depends on any of the variables being
-  substituted, then the result depends on the order of composition,
-  which in turn depends on the variable order: The variables farther from
-  the roots in the order are substituted first.
-  Returns a pointer to the resulting ADD if successful; NULL
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_addVectorCompose Cudd_addPermute Cudd_addCompose]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Composes a BDD with a vector of BDDs.]
-
-  Description [Given a vector of BDDs, creates a new BDD by
-  substituting the BDDs for the variables of the BDD f.  There
-  should be an entry in vector for each variable in the manager.
-  If no substitution is sought for a given variable, the corresponding
-  projection function should be specified in the vector.
-  This function implements simultaneous composition.
-  Returns a pointer to the resulting BDD if successful; NULL
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddPermute Cudd_bddCompose Cudd_addVectorCompose]
-
-******************************************************************************/
-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                                          */
-/*---------------------------------------------------------------------------*/
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive step of Cudd_bddCompose.]
-
-  Description [Performs the recursive step of Cudd_bddCompose.
-  Exploits the fact that the composition of f' with g
-  produces the complement of the composition of f with g to better
-  utilize the cache.  Returns the composed BDD if successful; NULL
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddCompose]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive step of Cudd_addCompose.]
-
-  Description [Performs the recursive step of Cudd_addCompose.
-  Returns the composed BDD if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_addCompose]
-
-******************************************************************************/
-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                                            */
-/*---------------------------------------------------------------------------*/
-
-
-/**Function********************************************************************
-
-  Synopsis    [Implements the recursive step of Cudd_addPermute.]
-
-  Description [ Recursively puts the ADD in the order given in the
-  array permut. Checks for trivial cases to terminate recursion, then
-  splits on the children of this node.  Once the solutions for the
-  children are obtained, it puts into the current position the node
-  from the rest of the ADD that should be here. Then returns this ADD.
-  The key here is that the node being visited is NOT put in its proper
-  place by this instance, but rather is switched when its proper
-  position is reached in the recursion tree.<p>
-  The DdNode * that is returned is the same ADD as passed in as node,
-  but in the new order.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_addPermute cuddBddPermuteRecur]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Implements the recursive step of Cudd_bddPermute.]
-
-  Description [ Recursively puts the BDD in the order given in the array permut.
-  Checks for trivial cases to terminate recursion, then splits on the
-  children of this node.  Once the solutions for the children are
-  obtained, it puts into the current position the node from the rest of
-  the BDD that should be here. Then returns this BDD.
-  The key here is that the node being visited is NOT put in its proper
-  place by this instance, but rather is switched when its proper position
-  is reached in the recursion tree.<p>
-  The DdNode * that is returned is the same BDD as passed in as node,
-  but in the new order.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddPermute 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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Implements the recursive step of Cudd_bddVarMap.]
-
-  Description [Implements the recursive step of Cudd_bddVarMap.
-  Returns a pointer to the result if successful; NULL otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     [Cudd_bddVarMap]
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive step of Cudd_addVectorCompose.]
-
-  Description []
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive step of Cudd_addGeneralVectorCompose.]
-
-  Description []
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive step of Cudd_addNonSimCompose.]
-
-  Description []
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the recursive step of Cudd_bddVectorCompose.]
-
-  Description []
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Comparison of a function to the i-th ADD variable.]
-
-  Description [Comparison of a function to the i-th ADD variable. Returns 1 if
-  the function is the i-th ADD variable; 0 otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-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 */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Comparison of a pair of functions to the i-th ADD variable.]
-
-  Description [Comparison of a pair of functions to the i-th ADD
-  variable. Returns 1 if the functions are the i-th ADD variable and its
-  complement; 0 otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-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 */