diff options
Diffstat (limited to 'src/bdd/cudd/cuddCompose.c')
| -rw-r--r-- | src/bdd/cudd/cuddCompose.c | 942 |
1 files changed, 486 insertions, 456 deletions
diff --git a/src/bdd/cudd/cuddCompose.c b/src/bdd/cudd/cuddCompose.c index 6fc4fa48..e3b2e556 100644 --- a/src/bdd/cudd/cuddCompose.c +++ b/src/bdd/cudd/cuddCompose.c @@ -7,38 +7,38 @@ 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> + <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 @@ -48,10 +48,37 @@ 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.] + 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.] ******************************************************************************/ @@ -62,6 +89,7 @@ ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -79,7 +107,7 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddCompose.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddCompose.c,v 1.45 2004/08/13 18:04:47 fabio Exp $"; #endif #ifdef DD_DEBUG @@ -102,16 +130,16 @@ static int addGeneralVectorComposeHits; /* 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 * 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); +DD_INLINE static int ddIsIthAddVar (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)); +static DdNode * cuddAddGeneralVectorComposeRecur (DdManager *dd, DdHashTable *table, DdNode *f, DdNode **vectorOn, DdNode **vectorOff, int deepest); +DD_INLINE static int ddIsIthAddVarPair (DdManager *dd, DdNode *f, DdNode *g, unsigned int i); /**AutomaticEnd***************************************************************/ @@ -145,12 +173,12 @@ Cudd_bddCompose( DdNode *proj, *res; /* Sanity check. */ - if (v < 0 || v > dd->size) return(NULL); + if (v < 0 || v >= dd->size) return(NULL); proj = dd->vars[v]; do { - dd->reordered = 0; - res = cuddBddComposeRecur(dd,f,g,proj); + dd->reordered = 0; + res = cuddBddComposeRecur(dd,f,g,proj); } while (dd->reordered == 1); return(res); @@ -182,12 +210,12 @@ Cudd_addCompose( DdNode *proj, *res; /* Sanity check. */ - if (v < 0 || v > dd->size) return(NULL); + if (v < 0 || v >= dd->size) return(NULL); proj = dd->vars[v]; do { - dd->reordered = 0; - res = cuddAddComposeRecur(dd,f,g,proj); + dd->reordered = 0; + res = cuddAddComposeRecur(dd,f,g,proj); } while (dd->reordered == 1); return(res); @@ -216,18 +244,18 @@ Cudd_addPermute( DdNode * node, int * permut) { - DdHashTable *table; - DdNode *res; + 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); + 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); @@ -260,20 +288,20 @@ Cudd_addSwapVariables( int n) { DdNode *swapped; - int i, j, k; - int *permut; + int i, j, k; + int *permut; permut = ABC_ALLOC(int,dd->size); if (permut == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(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; + j = x[i]->index; + k = y[i]->index; + permut[j] = k; + permut[k] = j; } swapped = Cudd_addPermute(dd,f,permut); @@ -306,17 +334,17 @@ Cudd_bddPermute( DdNode * node, int * permut) { - DdHashTable *table; - DdNode *res; + 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); + 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); @@ -350,8 +378,8 @@ Cudd_bddVarMap( if (manager->map == NULL) return(NULL); do { - manager->reordered = 0; - res = cuddBddVarMapRecur(manager, f); + manager->reordered = 0; + res = cuddBddVarMapRecur(manager, f); } while (manager->reordered == 1); return(res); @@ -394,23 +422,23 @@ Cudd_SetVarMap ( int i; if (manager->map != NULL) { - cuddCacheFlush(manager); + cuddCacheFlush(manager); } else { - manager->map = ABC_ALLOC(int,manager->maxSize); - if (manager->map == NULL) { - manager->errorCode = CUDD_MEMORY_OUT; - return(0); - } - manager->memused += sizeof(int) * manager->maxSize; + manager->map = ABC_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; + 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; + manager->map[x[i]->index] = y[i]->index; + manager->map[y[i]->index] = x[i]->index; } return(1); @@ -441,20 +469,20 @@ Cudd_bddSwapVariables( int n) { DdNode *swapped; - int i, j, k; - int *permut; + int i, j, k; + int *permut; permut = ABC_ALLOC(int,dd->size); if (permut == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(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; + j = x[i]->index; + k = y[i]->index; + permut[j] = k; + permut[k] = j; } swapped = Cudd_bddPermute(dd,f,permut); @@ -488,20 +516,20 @@ Cudd_bddAdjPermuteX( int n) { DdNode *swapped; - int i, j, k; - int *permut; + int i, j, k; + int *permut; permut = ABC_ALLOC(int,dd->size); if (permut == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(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; + j = x[i]->index; + k = x[i+1]->index; + permut[j] = k; + permut[k] = j; } swapped = Cudd_bddPermute(dd,B,permut); @@ -537,31 +565,31 @@ Cudd_addVectorCompose( DdNode * f, DdNode ** vector) { - DdHashTable *table; - DdNode *res; - int deepest; + 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; + 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); + /* Recursively solve the problem. */ + res = cuddAddVectorComposeRecur(dd,table,f,vector,deepest); + if (res != NULL) cuddRef(res); - /* Dispose of local cache. */ - cuddHashTableQuit(table); + /* Dispose of local cache. */ + cuddHashTableQuit(table); } while (dd->reordered == 1); if (res != NULL) cuddDeref(res); @@ -596,32 +624,32 @@ Cudd_addGeneralVectorCompose( DdNode ** vectorOn, DdNode ** vectorOff) { - DdHashTable *table; - DdNode *res; - int deepest; + 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; + 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); + /* Recursively solve the problem. */ + res = cuddAddGeneralVectorComposeRecur(dd,table,f,vectorOn, + vectorOff,deepest); + if (res != NULL) cuddRef(res); - /* Dispose of local cache. */ - cuddHashTableQuit(table); + /* Dispose of local cache. */ + cuddHashTableQuit(table); } while (dd->reordered == 1); if (res != NULL) cuddDeref(res); @@ -656,9 +684,9 @@ Cudd_addNonSimCompose( DdNode * f, DdNode ** vector) { - DdNode *cube, *key, *var, *tmp, *piece; - DdNode *res; - int i, lastsub; + 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 @@ -675,61 +703,61 @@ Cudd_addNonSimCompose( 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); + 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); - 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) { + 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); - return(NULL); - } - cuddRef(tmp); - Cudd_RecursiveDeref(dd,key); - Cudd_RecursiveDeref(dd,piece); - key = tmp; + 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; + /* 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); + /* 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); @@ -765,31 +793,31 @@ Cudd_bddVectorCompose( DdNode * f, DdNode ** vector) { - DdHashTable *table; - DdNode *res; - int deepest; + 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; + 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); + /* Recursively solve the problem. */ + res = cuddBddVectorComposeRecur(dd,table,f,vector, deepest); + if (res != NULL) cuddRef(res); - /* Dispose of local cache. */ - cuddHashTableQuit(table); + /* Dispose of local cache. */ + cuddHashTableQuit(table); } while (dd->reordered == 1); if (res != NULL) cuddDeref(res); @@ -825,9 +853,9 @@ cuddBddComposeRecur( DdNode * g, DdNode * proj) { - DdNode *F, *G, *f1, *f0, *g1, *g0, *r, *t, *e; + DdNode *F, *G, *f1, *f0, *g1, *g0, *r, *t, *e; unsigned int v, topf, topg, topindex; - int comple; + int comple; statLine(dd); v = dd->perm[proj->index]; @@ -845,60 +873,60 @@ cuddBddComposeRecur( /* Check cache. */ r = cuddCacheLookup(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj); if (r != NULL) { - return(Cudd_NotCond(r,comple)); + 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; + /* Compose. */ f1 = cuddT(F); f0 = cuddE(F); - } - if (topg > topf) { - g1 = g0 = g; + r = cuddBddIteRecur(dd, g, f1, f0); + if (r == NULL) return(NULL); } else { - g1 = cuddT(G); - g0 = cuddE(G); - if (g != G) { - g1 = Cudd_Not(g1); - g0 = Cudd_Not(g0); + /* 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); } - } - /* 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); + 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); + 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); - return(NULL); - } - cuddRef(r); - Cudd_IterDerefBdd(dd, t); /* t & e not necessarily part of r */ - Cudd_IterDerefBdd(dd, e); - cuddDeref(r); + cuddDeref(r); } cuddCacheInsert(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj,r); @@ -940,57 +968,57 @@ cuddAddComposeRecur( /* Check cache. */ r = cuddCacheLookup(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj); if (r != NULL) { - return(r); + 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; + /* Compose. */ 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; + r = cuddAddIteRecur(dd, g, f1, f0); + if (r == NULL) return(NULL); } else { - r = cuddUniqueInter(dd, (int) topindex, t, e); - if (r == NULL) { - Cudd_RecursiveDeref(dd, t); - Cudd_RecursiveDeref(dd, e); - return(NULL); + /* 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); } - } - cuddDeref(t); - cuddDeref(e); + 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); @@ -1032,22 +1060,22 @@ cuddAddPermuteRecur( DdNode * node /* ADD to be reordered */, int * permut /* permutation array */) { - DdNode *T,*E; - DdNode *res,*var; - int index; + DdNode *T,*E; + DdNode *res,*var; + int index; statLine(manager); /* Check for terminal case of constant node. */ if (cuddIsConstant(node)) { - return(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++; + addPermuteRecurHits++; #endif - return(res); + return(res); } /* Split and recur on children of this node. */ @@ -1056,8 +1084,8 @@ cuddAddPermuteRecur( cuddRef(T); E = cuddAddPermuteRecur(manager,table,cuddE(node),permut); if (E == NULL) { - Cudd_RecursiveDeref(manager, T); - return(NULL); + Cudd_RecursiveDeref(manager, T); + return(NULL); } cuddRef(E); @@ -1071,10 +1099,10 @@ cuddAddPermuteRecur( 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); + Cudd_RecursiveDeref(manager,var); + Cudd_RecursiveDeref(manager, T); + Cudd_RecursiveDeref(manager, E); + return(NULL); } cuddRef(res); Cudd_RecursiveDeref(manager,var); @@ -1085,12 +1113,12 @@ cuddAddPermuteRecur( ** 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); - } + ptrint fanout = (ptrint) node->ref; + cuddSatDec(fanout); + if (!cuddHashTableInsert1(table,node,res,fanout)) { + Cudd_RecursiveDeref(manager, res); + return(NULL); + } } cuddDeref(res); return(res); @@ -1125,24 +1153,24 @@ cuddBddPermuteRecur( DdNode * node /* BDD to be reordered */, int * permut /* permutation array */) { - DdNode *N,*T,*E; - DdNode *res; - int index; + 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); + return(node); } /* If problem already solved, look up answer and return. */ if (N->ref != 1 && (res = cuddHashTableLookup1(table,N)) != NULL) { #ifdef DD_DEBUG - bddPermuteRecurHits++; + bddPermuteRecurHits++; #endif - return(Cudd_NotCond(res,N != node)); + return(Cudd_NotCond(res,N != node)); } /* Split and recur on children of this node. */ @@ -1151,8 +1179,8 @@ cuddBddPermuteRecur( cuddRef(T); E = cuddBddPermuteRecur(manager,table,cuddE(N),permut); if (E == NULL) { - Cudd_IterDerefBdd(manager, T); - return(NULL); + Cudd_IterDerefBdd(manager, T); + return(NULL); } cuddRef(E); @@ -1163,9 +1191,9 @@ cuddBddPermuteRecur( 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); + Cudd_IterDerefBdd(manager, T); + Cudd_IterDerefBdd(manager, E); + return(NULL); } cuddRef(res); Cudd_IterDerefBdd(manager, T); @@ -1175,12 +1203,12 @@ cuddBddPermuteRecur( ** 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); - } + 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)); @@ -1205,22 +1233,22 @@ cuddBddVarMapRecur( DdManager *manager /* DD manager */, DdNode *f /* BDD to be remapped */) { - DdNode *F, *T, *E; - DdNode *res; - int index; + 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); + 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)); + (res = cuddCacheLookup1(manager,Cudd_bddVarMap,F)) != NULL) { + return(Cudd_NotCond(res,F != f)); } /* Split and recur on children of this node. */ @@ -1229,8 +1257,8 @@ cuddBddVarMapRecur( cuddRef(T); E = cuddBddVarMapRecur(manager,cuddE(F)); if (E == NULL) { - Cudd_IterDerefBdd(manager, T); - return(NULL); + Cudd_IterDerefBdd(manager, T); + return(NULL); } cuddRef(E); @@ -1241,9 +1269,9 @@ cuddBddVarMapRecur( 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); + Cudd_IterDerefBdd(manager, T); + Cudd_IterDerefBdd(manager, E); + return(NULL); } cuddRef(res); Cudd_IterDerefBdd(manager, T); @@ -1253,7 +1281,7 @@ cuddBddVarMapRecur( ** it will not be visited again. */ if (F->ref != 1) { - cuddCacheInsert1(manager,Cudd_bddVarMap,F,res); + cuddCacheInsert1(manager,Cudd_bddVarMap,F,res); } cuddDeref(res); return(Cudd_NotCond(res,F != f)); @@ -1280,20 +1308,20 @@ cuddAddVectorComposeRecur( DdNode ** vector /* functions to substitute */, int deepest /* depth of deepest substitution */) { - DdNode *T,*E; - DdNode *res; + DdNode *T,*E; + DdNode *res; statLine(dd); /* If we are past the deepest substitution, return f. */ if (cuddI(dd,f->index) > deepest) { - return(f); + return(f); } if ((res = cuddHashTableLookup1(table,f)) != NULL) { #ifdef DD_DEBUG - addVectorComposeHits++; + addVectorComposeHits++; #endif - return(res); + return(res); } /* Split and recur on children of this node. */ @@ -1302,8 +1330,8 @@ cuddAddVectorComposeRecur( cuddRef(T); E = cuddAddVectorComposeRecur(dd,table,cuddE(f),vector,deepest); if (E == NULL) { - Cudd_RecursiveDeref(dd, T); - return(NULL); + Cudd_RecursiveDeref(dd, T); + return(NULL); } cuddRef(E); @@ -1312,9 +1340,9 @@ cuddAddVectorComposeRecur( */ res = cuddAddIteRecur(dd,vector[f->index],T,E); if (res == NULL) { - Cudd_RecursiveDeref(dd, T); - Cudd_RecursiveDeref(dd, E); - return(NULL); + Cudd_RecursiveDeref(dd, T); + Cudd_RecursiveDeref(dd, E); + return(NULL); } cuddRef(res); Cudd_RecursiveDeref(dd, T); @@ -1324,12 +1352,12 @@ cuddAddVectorComposeRecur( ** 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); - } + ptrint fanout = (ptrint) f->ref; + cuddSatDec(fanout); + if (!cuddHashTableInsert1(table,f,res,fanout)) { + Cudd_RecursiveDeref(dd, res); + return(NULL); + } } cuddDeref(res); return(res); @@ -1357,31 +1385,31 @@ cuddAddGeneralVectorComposeRecur( DdNode ** vectorOff /* functions to substitute for x_i' */, int deepest /* depth of deepest substitution */) { - DdNode *T,*E,*t,*e; - DdNode *res; + DdNode *T,*E,*t,*e; + DdNode *res; /* If we are past the deepest substitution, return f. */ if (cuddI(dd,f->index) > deepest) { - return(f); + return(f); } if ((res = cuddHashTableLookup1(table,f)) != NULL) { #ifdef DD_DEBUG - addGeneralVectorComposeHits++; + addGeneralVectorComposeHits++; #endif - return(res); + return(res); } /* Split and recur on children of this node. */ T = cuddAddGeneralVectorComposeRecur(dd,table,cuddT(f), - vectorOn,vectorOff,deepest); + vectorOn,vectorOff,deepest); if (T == NULL) return(NULL); cuddRef(T); E = cuddAddGeneralVectorComposeRecur(dd,table,cuddE(f), - vectorOn,vectorOff,deepest); + vectorOn,vectorOff,deepest); if (E == NULL) { - Cudd_RecursiveDeref(dd, T); - return(NULL); + Cudd_RecursiveDeref(dd, T); + return(NULL); } cuddRef(E); @@ -1421,12 +1449,12 @@ cuddAddGeneralVectorComposeRecur( ** 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); - } + ptrint fanout = (ptrint) f->ref; + cuddSatDec(fanout); + if (!cuddHashTableInsert1(table,f,res,fanout)) { + Cudd_RecursiveDeref(dd, res); + return(NULL); + } } cuddDeref(res); return(res); @@ -1466,13 +1494,13 @@ cuddAddNonSimComposeRecur( statLine(dd); /* If we are past the deepest substitution, return f. */ if (cube == DD_ONE(dd) || cuddIsConstant(f)) { - return(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); + return(r); } /* Find top variable. we just need to look at f, key, and cube, @@ -1487,69 +1515,69 @@ cuddAddNonSimComposeRecur( /* Compute the cofactors. */ if (topf == top) { - f1 = cuddT(f); - f0 = cuddE(f); + f1 = cuddT(f); + f0 = cuddE(f); } else { - f1 = f0 = f; + 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) { + 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); - return(NULL); - } - cuddRef(key1); - Cudd_RecursiveDeref(dd,var); - key0 = key1; + key0 = key1; } else { - cube1 = cube; - if (topk == top) { - key1 = cuddT(key); - key0 = cuddE(key); - } else { - key1 = key0 = key; - } - cuddRef(key1); + 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 = ABC_ALLOC(DdNode *,lastsub); if (vect1 == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - Cudd_RecursiveDeref(dd,key1); - return(NULL); + dd->errorCode = CUDD_MEMORY_OUT; + Cudd_RecursiveDeref(dd,key1); + return(NULL); } vect0 = ABC_ALLOC(DdNode *,lastsub); if (vect0 == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - Cudd_RecursiveDeref(dd,key1); - ABC_FREE(vect1); - return(NULL); + dd->errorCode = CUDD_MEMORY_OUT; + Cudd_RecursiveDeref(dd,key1); + ABC_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; - } + 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; @@ -1557,17 +1585,17 @@ cuddAddNonSimComposeRecur( T = cuddAddNonSimComposeRecur(dd,f1,vect1,key1,cube1,lastsub); ABC_FREE(vect1); if (T == NULL) { - Cudd_RecursiveDeref(dd,key1); - ABC_FREE(vect0); - return(NULL); + Cudd_RecursiveDeref(dd,key1); + ABC_FREE(vect0); + return(NULL); } cuddRef(T); E = cuddAddNonSimComposeRecur(dd,f0,vect0,key0,cube1,lastsub); ABC_FREE(vect0); if (E == NULL) { - Cudd_RecursiveDeref(dd,key1); - Cudd_RecursiveDeref(dd,T); - return(NULL); + Cudd_RecursiveDeref(dd,key1); + Cudd_RecursiveDeref(dd,T); + return(NULL); } cuddRef(E); Cudd_RecursiveDeref(dd,key1); @@ -1577,9 +1605,9 @@ cuddAddNonSimComposeRecur( */ r = cuddAddIteRecur(dd,vector[index],T,E); if (r == NULL) { - Cudd_RecursiveDeref(dd,T); - Cudd_RecursiveDeref(dd,E); - return(NULL); + Cudd_RecursiveDeref(dd,T); + Cudd_RecursiveDeref(dd,E); + return(NULL); } cuddRef(r); Cudd_RecursiveDeref(dd,T); @@ -1613,23 +1641,23 @@ cuddBddVectorComposeRecur( DdNode ** vector /* functions to be composed */, int deepest /* depth of the deepest substitution */) { - DdNode *F,*T,*E; - DdNode *res; + 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); + return(f); } /* If problem already solved, look up answer and return. */ if ((res = cuddHashTableLookup1(table,F)) != NULL) { #ifdef DD_DEBUG - bddVectorComposeHits++; + bddVectorComposeHits++; #endif - return(Cudd_NotCond(res,F != f)); + return(Cudd_NotCond(res,F != f)); } /* Split and recur on children of this node. */ @@ -1638,8 +1666,8 @@ cuddBddVectorComposeRecur( cuddRef(T); E = cuddBddVectorComposeRecur(dd,table,cuddE(F),vector, deepest); if (E == NULL) { - Cudd_IterDerefBdd(dd, T); - return(NULL); + Cudd_IterDerefBdd(dd, T); + return(NULL); } cuddRef(E); @@ -1648,24 +1676,24 @@ cuddBddVectorComposeRecur( */ res = cuddBddIteRecur(dd,vector[F->index],T,E); if (res == NULL) { - Cudd_IterDerefBdd(dd, T); - Cudd_IterDerefBdd(dd, E); - return(NULL); + Cudd_IterDerefBdd(dd, T); + Cudd_IterDerefBdd(dd, E); + return(NULL); } cuddRef(res); Cudd_IterDerefBdd(dd, T); - Cudd_IterDerefBdd(dd, E); + 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); - } + 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)); @@ -1719,9 +1747,11 @@ ddIsIthAddVarPair( 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)); + cuddT(f) == DD_ONE(dd) && cuddE(f) == DD_ZERO(dd) && + cuddT(g) == DD_ZERO(dd) && cuddE(g) == DD_ONE(dd)); } /* end of ddIsIthAddVarPair */ + + ABC_NAMESPACE_IMPL_END |