src/cuBdd/cuddCompose.c File Reference

#include "util.h"
#include "cuddInt.h"

Include dependency graph for cuddCompose.c:

Go to the source code of this file.

Functions
static DdNode *	cuddAddPermuteRecur (DdManager *manager, DdHashTable *table, DdNode *node, int *permut)
static DdNode *	cuddBddPermuteRecur (DdManager *manager, DdHashTable *table, DdNode *node, int *permut)
static DdNode *	cuddBddVarMapRecur (DdManager *manager, DdNode *f)
static DdNode *	cuddAddVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest)
static DdNode *	cuddAddNonSimComposeRecur (DdManager *dd, DdNode *f, DdNode **vector, DdNode *key, DdNode *cube, int lastsub)
static DdNode *	cuddBddVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vector, int deepest)
static DD_INLINE int	ddIsIthAddVar (DdManager *dd, DdNode *f, unsigned int i)
static DdNode *	cuddAddGeneralVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vectorOn, DdNode **vectorOff, int deepest)
static DD_INLINE int	ddIsIthAddVarPair (DdManager *dd, DdNode *f, DdNode *g, unsigned int i)
DdNode *	Cudd_bddCompose (DdManager *dd, DdNode *f, DdNode *g, int v)
DdNode *	Cudd_addCompose (DdManager *dd, DdNode *f, DdNode *g, int v)
DdNode *	Cudd_addPermute (DdManager *manager, DdNode *node, int *permut)
DdNode *	Cudd_addSwapVariables (DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n)
DdNode *	Cudd_bddPermute (DdManager *manager, DdNode *node, int *permut)
DdNode *	Cudd_bddVarMap (DdManager *manager, DdNode *f)
int	Cudd_SetVarMap (DdManager *manager, DdNode **x, DdNode **y, int n)
DdNode *	Cudd_bddSwapVariables (DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n)
DdNode *	Cudd_bddAdjPermuteX (DdManager *dd, DdNode *B, DdNode **x, int n)
DdNode *	Cudd_addVectorCompose (DdManager *dd, DdNode *f, DdNode **vector)
DdNode *	Cudd_addGeneralVectorCompose (DdManager *dd, DdNode *f, DdNode **vectorOn, DdNode **vectorOff)
DdNode *	Cudd_addNonSimCompose (DdManager *dd, DdNode *f, DdNode **vector)
DdNode *	Cudd_bddVectorCompose (DdManager *dd, DdNode *f, DdNode **vector)
DdNode *	cuddBddComposeRecur (DdManager *dd, DdNode *f, DdNode *g, DdNode *proj)
DdNode *	cuddAddComposeRecur (DdManager *dd, DdNode *f, DdNode *g, DdNode *proj)
Variables
static char rcsid[]	DD_UNUSED = "$Id: cuddCompose.c,v 1.45 2004/08/13 18:04:47 fabio Exp $"

---

Function Documentation

DdNode* Cudd_addCompose	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		int	v
	)

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]

Definition at line 200 of file cuddCompose.c.

{
    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_addGeneralVectorCompose	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vectorOn,
		DdNode **	vectorOff
	)

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]

Definition at line 617 of file cuddCompose.c.

{
    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
	)

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]

Definition at line 678 of file cuddCompose.c.

{
    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_addPermute	(	DdManager *	manager,
		DdNode *	node,
		int *	permut
	)

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]

Definition at line 238 of file cuddCompose.c.

{
    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
	)

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]

Definition at line 279 of file cuddCompose.c.

{
    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_addVectorCompose	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vector
	)

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]

Definition at line 559 of file cuddCompose.c.

{
    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_bddAdjPermuteX	(	DdManager *	dd,
		DdNode *	B,
		DdNode **	x,
		int	n
	)

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]

Definition at line 508 of file cuddCompose.c.

{
    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_bddCompose	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		int	v
	)

AutomaticEnd 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]

Definition at line 163 of file cuddCompose.c.

{
    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_bddPermute	(	DdManager *	manager,
		DdNode *	node,
		int *	permut
	)

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]

Definition at line 328 of file cuddCompose.c.

{
    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_bddSwapVariables	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	x,
		DdNode **	y,
		int	n
	)

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]

Definition at line 460 of file cuddCompose.c.

{
    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_bddVarMap	(	DdManager *	manager,
		DdNode *	f
	)

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]

Definition at line 369 of file cuddCompose.c.

{
    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 */

DdNode* Cudd_bddVectorCompose	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vector
	)

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]

Definition at line 787 of file cuddCompose.c.

{
    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 */

int Cudd_SetVarMap	(	DdManager *	manager,
		DdNode **	x,
		DdNode **	y,
		int	n
	)

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]

Definition at line 412 of file cuddCompose.c.

{
    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* cuddAddComposeRecur	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		DdNode *	proj
	)

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]

Definition at line 948 of file cuddCompose.c.

{
    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 */

static DdNode * cuddAddGeneralVectorComposeRecur	(	DdManager *	dd,
		DdHashTable *	table,
		DdNode *	f,
		DdNode **	vectorOn,
		DdNode **	vectorOff,
		int	deepest
	)			[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_addGeneralVectorCompose.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 1376 of file cuddCompose.c.

{
    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
	)			[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_addNonSimCompose.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 1473 of file cuddCompose.c.

{
    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 * cuddAddPermuteRecur	(	DdManager *	manager,
		DdHashTable *	table,
		DdNode *	node,
		int *	permut
	)			[static]

AutomaticStart

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.

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]

Definition at line 1053 of file cuddCompose.c.

{
    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 * cuddAddVectorComposeRecur	(	DdManager *	dd,
		DdHashTable *	table,
		DdNode *	f,
		DdNode **	vector,
		int	deepest
	)			[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_addVectorCompose.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 1300 of file cuddCompose.c.

{
    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 */

DdNode* cuddBddComposeRecur	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		DdNode *	proj
	)

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]

Definition at line 846 of file cuddCompose.c.

{
    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 */

static DdNode * cuddBddPermuteRecur	(	DdManager *	manager,
		DdHashTable *	table,
		DdNode *	node,
		int *	permut
	)			[static]

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.

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]

Definition at line 1146 of file cuddCompose.c.

{
    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,
		DdNode *	f
	)			[static]

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]

Definition at line 1228 of file cuddCompose.c.

{
    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 * cuddBddVectorComposeRecur	(	DdManager *	dd,
		DdHashTable *	table,
		DdNode *	f,
		DdNode **	vector,
		int	deepest
	)			[static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_bddVectorCompose.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 1633 of file cuddCompose.c.

{
    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 */

static DD_INLINE int ddIsIthAddVar	(	DdManager *	dd,
		DdNode *	f,
		unsigned int	i
	)			[static]

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 []

Definition at line 1714 of file cuddCompose.c.

{
    return(f->index == i && cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd));

} /* end of ddIsIthAddVar */

static DD_INLINE int ddIsIthAddVarPair	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		unsigned int	i
	)			[static]

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 []

Definition at line 1739 of file cuddCompose.c.

{
    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 */

---

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddCompose.c,v 1.45 2004/08/13 18:04:47 fabio Exp $" [static]

CFile***********************************************************************

FileName [cuddCompose.c]

PackageName [cudd]

Synopsis [Functional composition and variable permutation of DDs.]

Description [External procedures included in this module:

• Cudd_bddCompose()
• Cudd_addCompose()
• Cudd_addPermute()
• Cudd_addSwapVariables()
• Cudd_bddPermute()
• Cudd_bddVarMap()
• Cudd_SetVarMap()
• Cudd_bddSwapVariables()
• Cudd_bddAdjPermuteX()
• Cudd_addVectorCompose()
• Cudd_addGeneralVectorCompose()
• Cudd_addNonSimCompose()
• Cudd_bddVectorCompose()

Internal procedures included in this module:

• cuddBddComposeRecur()
• cuddAddComposeRecur()

Static procedures included in this module:

• cuddAddPermuteRecur()
• cuddBddPermuteRecur()
• cuddBddVarMapRecur()
• cuddAddVectorComposeRecur()
• cuddAddGeneralVectorComposeRecur()
• cuddAddNonSimComposeRecur()
• cuddBddVectorComposeRecur()
• ddIsIthAddVar()
• ddIsIthAddVarPair()

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 [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 106 of file cuddCompose.c.