diff options
| -rw-r--r-- | abclib.dsp | 8 | ||||
| -rw-r--r-- | src/bdd/extrab/extraBdd.h | 38 | ||||
| -rw-r--r-- | src/bdd/extrab/extraBddMaxMin.c | 1067 | ||||
| -rw-r--r-- | src/bdd/extrab/extraBddSet.c | 941 | ||||
| -rw-r--r-- | src/bdd/extrab/module.make | 2 |
5 files changed, 2056 insertions, 0 deletions
@@ -1167,10 +1167,18 @@ SOURCE=.\src\bdd\extrab\extraBddKmap.c # End Source File # Begin Source File +SOURCE=.\src\bdd\extrab\extraBddMaxMin.c +# End Source File +# Begin Source File + SOURCE=.\src\bdd\extrab\extraBddMisc.c # End Source File # Begin Source File +SOURCE=.\src\bdd\extrab\extraBddSet.c +# End Source File +# Begin Source File + SOURCE=.\src\bdd\extrab\extraBddSymm.c # End Source File # Begin Source File diff --git a/src/bdd/extrab/extraBdd.h b/src/bdd/extrab/extraBdd.h index e7a65a94..d5dfc85b 100644 --- a/src/bdd/extrab/extraBdd.h +++ b/src/bdd/extrab/extraBdd.h @@ -206,6 +206,44 @@ extern DdNode * extraBddTuples( DdManager * dd, DdNode * bVarsK, DdNode * b #define ABC_PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n") #endif +/*=== extraMaxMin.c ==============================================================*/ + +/* maximal/minimimal */ +extern DdNode * Extra_zddMaximal (DdManager *dd, DdNode *S); +extern DdNode * extraZddMaximal (DdManager *dd, DdNode *S); +extern DdNode * Extra_zddMinimal (DdManager *dd, DdNode *S); +extern DdNode * extraZddMinimal (DdManager *dd, DdNode *S); +/* maximal/minimal of the union of two sets of subsets */ +extern DdNode * Extra_zddMaxUnion (DdManager *dd, DdNode *S, DdNode *T); +extern DdNode * extraZddMaxUnion (DdManager *dd, DdNode *S, DdNode *T); +extern DdNode * Extra_zddMinUnion (DdManager *dd, DdNode *S, DdNode *T); +extern DdNode * extraZddMinUnion (DdManager *dd, DdNode *S, DdNode *T); +/* dot/cross products */ +extern DdNode * Extra_zddDotProduct (DdManager *dd, DdNode *S, DdNode *T); +extern DdNode * extraZddDotProduct (DdManager *dd, DdNode *S, DdNode *T); +extern DdNode * Extra_zddCrossProduct (DdManager *dd, DdNode *S, DdNode *T); +extern DdNode * extraZddCrossProduct (DdManager *dd, DdNode *S, DdNode *T); +extern DdNode * Extra_zddMaxDotProduct (DdManager *dd, DdNode *S, DdNode *T); +extern DdNode * extraZddMaxDotProduct (DdManager *dd, DdNode *S, DdNode *T); + +/*=== extraBddSet.c ==============================================================*/ + +/* subset/supset operations */ +extern DdNode * Extra_zddSubSet (DdManager *dd, DdNode *X, DdNode *Y); +extern DdNode * extraZddSubSet (DdManager *dd, DdNode *X, DdNode *Y); +extern DdNode * Extra_zddSupSet (DdManager *dd, DdNode *X, DdNode *Y); +extern DdNode * extraZddSupSet (DdManager *dd, DdNode *X, DdNode *Y); +extern DdNode * Extra_zddNotSubSet (DdManager *dd, DdNode *X, DdNode *Y); +extern DdNode * extraZddNotSubSet (DdManager *dd, DdNode *X, DdNode *Y); +extern DdNode * Extra_zddNotSupSet (DdManager *dd, DdNode *X, DdNode *Y); +extern DdNode * extraZddNotSupSet (DdManager *dd, DdNode *X, DdNode *Y); +extern DdNode * Extra_zddMaxNotSupSet (DdManager *dd, DdNode *X, DdNode *Y); +extern DdNode * extraZddMaxNotSupSet (DdManager *dd, DdNode *X, DdNode *Y); +/* check whether the empty combination belongs to the set of subsets */ +extern int Extra_zddEmptyBelongs (DdManager *dd, DdNode* zS); +/* check whether the set consists of one subset only */ +extern int Extra_zddIsOneSubset (DdManager *dd, DdNode* zS); + /*=== extraBddKmap.c ================================================================*/ /* displays the Karnaugh Map of a function */ diff --git a/src/bdd/extrab/extraBddMaxMin.c b/src/bdd/extrab/extraBddMaxMin.c new file mode 100644 index 00000000..fc424f80 --- /dev/null +++ b/src/bdd/extrab/extraBddMaxMin.c @@ -0,0 +1,1067 @@ +/**CFile*********************************************************************** + + FileName [zMaxMin.c] + + PackageName [extra] + + Synopsis [Experimental version of some ZDD operators.] + + Description [External procedures included in this module: + <ul> + <li> Extra_zddMaximal(); + <li> Extra_zddMinimal(); + <li> Extra_zddMaxUnion(); + <li> Extra_zddMinUnion(); + <li> Extra_zddDotProduct(); + <li> Extra_zddCrossProduct(); + <li> Extra_zddMaxDotProduct(); + </ul> + Internal procedures included in this module: + <ul> + <li> extraZddMaximal(); + <li> extraZddMinimal(); + <li> extraZddMaxUnion(); + <li> extraZddMinUnion(); + <li> extraZddDotProduct(); + <li> extraZddCrossProduct(); + <li> extraZddMaxDotProduct(); + </ul> + StaTc procedures included in this module: + <ul> + </ul> + + DotProduct and MaxDotProduct were introduced + by O.Coudert to solve problems arising in two-level planar routing + See O. Coudert, C.-J. R. Shi. Exact Multi-Layer Topological Planar + Routing. Proc. of IEEE Custom Integrated Circuit Conference '96, + pp. 179-182. + ] + + SeeAlso [] + + Author [Alan Mishchenko] + + Copyright [] + + ReviSon [$zMaxMin.c, v.1.2, November 26, 2000, alanmi $] + +******************************************************************************/ + +#include "extraBdd.h" + +ABC_NAMESPACE_IMPL_START + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaTcStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* StaTc Function prototypes */ +/*---------------------------------------------------------------------------*/ + +/**AutomaTcEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported Functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Computes the maximal of a set represented by its ZDD.] + + Description [] + + SideEffects [] + + SeeAlso [Extra_zddMinimal] + +******************************************************************************/ +DdNode * +Extra_zddMaximal( + DdManager * dd, + DdNode * S) +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddMaximal(dd, S); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddMaximal */ + + +/**Function******************************************************************** + + Synopsis [Computes the minimal of a set represented by its ZDD.] + + Description [] + + SideEffects [] + + SeeAlso [Extra_zddMaximal] + +******************************************************************************/ +DdNode * +Extra_zddMinimal( + DdManager * dd, + DdNode * S) +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddMinimal(dd, S); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddMinimal */ + + +/**Function******************************************************************** + + Synopsis [Computes the maximal of the union of two sets represented by ZDDs.] + + Description [] + + SideEffects [] + + SeeAlso [Extra_zddMaximal Extra_zddMimimal Extra_zddMinUnion] + +******************************************************************************/ +DdNode * +Extra_zddMaxUnion( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddMaxUnion(dd, S, T); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddMaxUnion */ + + +/**Function******************************************************************** + + Synopsis [Computes the minimal of the union of two sets represented by ZDDs.] + + Description [] + + SideEffects [] + + SeeAlso [Extra_zddMaximal Extra_zddMimimal Extra_zddMaxUnion] + +******************************************************************************/ +DdNode * +Extra_zddMinUnion( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddMinUnion(dd, S, T); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddMinUnion */ + + +/**Function******************************************************************** + + Synopsis [Computes the dot product of two sets of subsets represented by ZDDs.] + + Description [The dot product is defined as a set of pair-wise unions of subsets + belonging to the arguments.] + + SideEffects [] + + SeeAlso [Extra_zddCrossProduct] + +******************************************************************************/ +DdNode * +Extra_zddDotProduct( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddDotProduct(dd, S, T); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddDotProduct */ + + +/**Function******************************************************************** + + Synopsis [Computes the cross product of two sets of subsets represented by ZDDs.] + + Description [The cross product is defined as a set of pair-wise intersections of subsets + belonging to the arguments.] + + SideEffects [] + + SeeAlso [Extra_zddDotProduct] + +******************************************************************************/ +DdNode * +Extra_zddCrossProduct( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddCrossProduct(dd, S, T); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddCrossProduct */ + + +/**Function******************************************************************** + + Synopsis [Computes the maximal of the DotProduct of the union of two sets represented by ZDDs.] + + Description [] + + SideEffects [] + + SeeAlso [Extra_zddDotProduct Extra_zddMaximal Extra_zddMinCrossProduct] + +******************************************************************************/ +DdNode * +Extra_zddMaxDotProduct( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddMaxDotProduct(dd, S, T); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddMaxDotProduct */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal Functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddMaximal.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraZddMaximal( + DdManager * dd, + DdNode * zSet) +{ + DdNode *zRes; + statLine(dd); + + /* consider terminal cases */ + if ( zSet == z0 || zSet == z1 ) + return zSet; + + /* check cache */ + zRes = cuddCacheLookup1Zdd(dd, extraZddMaximal, zSet); + if (zRes) + return(zRes); + else + { + DdNode *zSet0, *zSet1, *zRes0, *zRes1; + + /* compute maximal for subsets without the top-most element */ + zSet0 = extraZddMaximal(dd, cuddE(zSet)); + if ( zSet0 == NULL ) + return NULL; + cuddRef( zSet0 ); + + /* compute maximal for subsets with the top-most element */ + zSet1 = extraZddMaximal(dd, cuddT(zSet)); + if ( zSet1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + return NULL; + } + cuddRef( zSet1 ); + + /* remove subsets without this element covered by subsets with this element */ + zRes0 = extraZddNotSubSet(dd, zSet0, zSet1); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + return NULL; + } + cuddRef( zRes0 ); + Cudd_RecursiveDerefZdd(dd, zSet0); + + /* subset with this element remains unchanged */ + zRes1 = zSet1; + + /* create the new node */ + zRes = cuddZddGetNode( dd, zSet->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + + /* insert the result into cache */ + cuddCacheInsert1(dd, extraZddMaximal, zSet, zRes); + return zRes; + } +} /* end of extraZddMaximal */ + + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddMinimal.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraZddMinimal( + DdManager * dd, + DdNode * zSet) +{ + DdNode *zRes; + statLine(dd); + + /* consider terminal cases */ + if ( zSet == z0 ) + return zSet; + /* the empty combinaTon, if present, is the only minimal combinaTon */ + if ( Extra_zddEmptyBelongs(dd, zSet) ) + return z1; + + /* check cache */ + zRes = cuddCacheLookup1Zdd(dd, extraZddMinimal, zSet); + if (zRes) + return(zRes); + else + { + DdNode *zSet0, *zSet1, *zRes0, *zRes1; + + /* compute minimal for subsets without the top-most element */ + zSet0 = extraZddMinimal(dd, cuddE(zSet)); + if ( zSet0 == NULL ) + return NULL; + cuddRef( zSet0 ); + + /* compute minimal for subsets with the top-most element */ + zSet1 = extraZddMinimal(dd, cuddT(zSet)); + if ( zSet1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + return NULL; + } + cuddRef( zSet1 ); + + /* subset without this element remains unchanged */ + zRes0 = zSet0; + + /* remove subsets with this element that contain subsets without this element */ + zRes1 = extraZddNotSupSet(dd, zSet1, zSet0); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd(dd, zSet1); + + /* create the new node */ + zRes = cuddZddGetNode( dd, zSet->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + + /* insert the result into cache */ + cuddCacheInsert1(dd, extraZddMinimal, zSet, zRes); + return zRes; + } +} /* end of extraZddMinimal */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddMaxUnion.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraZddMaxUnion( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *zRes; + int TopS, TopT; + statLine(dd); + + /* consider terminal cases */ + if ( S == z0 ) + return T; + if ( T == z0 ) + return S; + if ( S == T ) + return S; + if ( S == z1 ) + return T; + if ( T == z1 ) + return S; + + /* the operation is commutative - normalize the problem */ + TopS = dd->permZ[S->index]; + TopT = dd->permZ[T->index]; + + if ( TopS > TopT || (TopS == TopT && (unsigned)S > (unsigned)T) ) + return extraZddMaxUnion(dd, T, S); + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddMaxUnion, S, T); + if (zRes) + return zRes; + else + { + DdNode *zSet0, *zSet1, *zRes0, *zRes1; + + if ( TopS == TopT ) + { + /* compute maximal for subsets without the top-most element */ + zSet0 = extraZddMaxUnion(dd, cuddE(S), cuddE(T) ); + if ( zSet0 == NULL ) + return NULL; + cuddRef( zSet0 ); + + /* compute maximal for subsets with the top-most element */ + zSet1 = extraZddMaxUnion(dd, cuddT(S), cuddT(T) ); + if ( zSet1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + return NULL; + } + cuddRef( zSet1 ); + } + else /* if ( TopS < TopT ) */ + { + /* compute maximal for subsets without the top-most element */ + zSet0 = extraZddMaxUnion(dd, cuddE(S), T ); + if ( zSet0 == NULL ) + return NULL; + cuddRef( zSet0 ); + + /* subset with this element is just the cofactor of S */ + zSet1 = cuddT(S); + cuddRef( zSet1 ); + } + + /* remove subsets without this element covered by subsets with this element */ + zRes0 = extraZddNotSubSet(dd, zSet0, zSet1); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + return NULL; + } + cuddRef( zRes0 ); + Cudd_RecursiveDerefZdd(dd, zSet0); + + /* subset with this element remains unchanged */ + zRes1 = zSet1; + + /* create the new node */ + zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddMaxUnion, S, T, zRes); + return zRes; + } +} /* end of extraZddMaxUnion */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddMinUnion.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraZddMinUnion( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *zRes; + int TopS, TopT; + statLine(dd); + + /* consider terminal cases */ + if ( S == z0 ) + return T; + if ( T == z0 ) + return S; + if ( S == T ) + return S; + /* the empty combination, if present, is the only minimal combination */ + if ( Extra_zddEmptyBelongs(dd, S) || Extra_zddEmptyBelongs(dd, T) ) + return z1; + + /* the operation is commutative - normalize the problem */ + TopS = dd->permZ[S->index]; + TopT = dd->permZ[T->index]; + + if ( TopS > TopT || (TopS == TopT && (unsigned)S > (unsigned)T) ) + return extraZddMinUnion(dd, T, S); + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddMinUnion, S, T); + if (zRes) + return(zRes); + else + { + DdNode *zSet0, *zSet1, *zRes0, *zRes1; + if ( TopS == TopT ) + { + /* compute maximal for subsets without the top-most element */ + zSet0 = extraZddMinUnion(dd, cuddE(S), cuddE(T) ); + if ( zSet0 == NULL ) + return NULL; + cuddRef( zSet0 ); + + /* compute maximal for subsets with the top-most element */ + zSet1 = extraZddMinUnion(dd, cuddT(S), cuddT(T) ); + if ( zSet1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + return NULL; + } + cuddRef( zSet1 ); + } + else /* if ( TopS < TopT ) */ + { + /* compute maximal for subsets without the top-most element */ + zSet0 = extraZddMinUnion(dd, cuddE(S), T ); + if ( zSet0 == NULL ) + return NULL; + cuddRef( zSet0 ); + + /* subset with this element is just the cofactor of S */ + zSet1 = cuddT(S); + cuddRef( zSet1 ); + } + + /* subset without this element remains unchanged */ + zRes0 = zSet0; + + /* remove subsets with this element that contain subsets without this element */ + zRes1 = extraZddNotSupSet(dd, zSet1, zSet0); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd(dd, zSet1); + + /* create the new node */ + zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddMinUnion, S, T, zRes); + return zRes; + } +} /* end of extraZddMinUnion */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddDotProduct.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraZddDotProduct( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *zRes; + int TopS, TopT; + statLine(dd); + + /* consider terminal cases */ + if ( S == z0 || T == z0 ) + return z0; + if ( S == z1 ) + return T; + if ( T == z1 ) + return S; + + /* the operation is commutative - normalize the problem */ + TopS = dd->permZ[S->index]; + TopT = dd->permZ[T->index]; + + if ( TopS > TopT || (TopS == TopT && (unsigned)S > (unsigned)T) ) + return extraZddDotProduct(dd, T, S); + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddDotProduct, S, T); + if (zRes) + return zRes; + else + { + DdNode *zSet0, *zSet1, *zRes0, *zRes1, *zTemp; + if ( TopS == TopT ) + { + /* compute the union of two cofactors of T (T0+T1) */ + zTemp = cuddZddUnion(dd, cuddE(T), cuddT(T) ); + if ( zTemp == NULL ) + return NULL; + cuddRef( zTemp ); + + /* compute DotProduct with the top element for subsets (S1, T0+T1) */ + zSet0 = extraZddDotProduct(dd, cuddT(S), zTemp ); + if ( zSet0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zTemp); + return NULL; + } + cuddRef( zSet0 ); + Cudd_RecursiveDerefZdd(dd, zTemp); + + /* compute DotProduct with the top element for subsets (S0, T1) */ + zSet1 = extraZddDotProduct(dd, cuddE(S), cuddT(T) ); + if ( zSet1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + return NULL; + } + cuddRef( zSet1 ); + + /* compute the union of these two partial results (zSet0 + zSet1) */ + zRes1 = cuddZddUnion(dd, zSet0, zSet1 ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + + /* compute DotProduct for subsets without the top-most element */ + zRes0 = extraZddDotProduct(dd, cuddE(S), cuddE(T) ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddRef( zRes0 ); + } + else /* if ( TopS < TopT ) */ + { + /* compute DotProduct with the top element for subsets (S1, T) */ + zRes1 = extraZddDotProduct(dd, cuddT(S), T ); + if ( zRes1 == NULL ) + return NULL; + cuddRef( zRes1 ); + + /* compute DotProduct for subsets without the top-most element */ + zRes0 = extraZddDotProduct(dd, cuddE(S), T ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddRef( zRes0 ); + } + + /* create the new node */ + zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddDotProduct, S, T, zRes); + return zRes; + } +} /* end of extraZddDotProduct */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddCrossProduct.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraZddCrossProduct( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *zRes; + int TopS, TopT; + statLine(dd); + + /* consider terminal cases */ + if ( S == z0 || T == z0 ) + return z0; + if ( S == z1 || T == z1 ) + return z1; + + /* the operation is commutative - normalize the problem */ + TopS = dd->permZ[S->index]; + TopT = dd->permZ[T->index]; + + if ( TopS > TopT || (TopS == TopT && (unsigned)S > (unsigned)T) ) + return extraZddCrossProduct(dd, T, S); + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddCrossProduct, S, T); + if (zRes) + return zRes; + else + { + DdNode *zSet0, *zSet1, *zRes0, *zRes1, *zTemp; + + if ( TopS == TopT ) + { + /* compute the union of two cofactors of T (T0+T1) */ + zTemp = cuddZddUnion(dd, cuddE(T), cuddT(T) ); + if ( zTemp == NULL ) + return NULL; + cuddRef( zTemp ); + + /* compute CrossProduct without the top element for subsets (S0, T0+T1) */ + zSet0 = extraZddCrossProduct(dd, cuddE(S), zTemp ); + if ( zSet0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zTemp); + return NULL; + } + cuddRef( zSet0 ); + Cudd_RecursiveDerefZdd(dd, zTemp); + + /* compute CrossProduct without the top element for subsets (S1, T0) */ + zSet1 = extraZddCrossProduct(dd, cuddT(S), cuddE(T) ); + if ( zSet1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + return NULL; + } + cuddRef( zSet1 ); + + /* compute the union of these two partial results (zSet0 + zSet1) */ + zRes0 = cuddZddUnion(dd, zSet0, zSet1 ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + return NULL; + } + cuddRef( zRes0 ); + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + + /* compute CrossProduct for subsets with the top-most element */ + zRes1 = extraZddCrossProduct(dd, cuddT(S), cuddT(T) ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes0); + return NULL; + } + cuddRef( zRes1 ); + + /* create the new node */ + zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + else /* if ( TopS < TopT ) */ + { + /* compute CrossProduct without the top element (S0, T) */ + zSet0 = extraZddCrossProduct(dd, cuddE(S), T ); + if ( zSet0 == NULL ) + return NULL; + cuddRef( zSet0 ); + + /* compute CrossProduct without the top element (S1, T) */ + zSet1 = extraZddCrossProduct(dd, cuddT(S), T ); + if ( zSet1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + return NULL; + } + cuddRef( zSet1 ); + + /* compute the union of these two partial results (zSet0 + zSet1) */ + zRes = cuddZddUnion(dd, zSet0, zSet1 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + cuddDeref( zRes ); + } + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddCrossProduct, S, T, zRes); + return zRes; + } +} /* end of extraZddCrossProduct */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddMaxDotProduct.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraZddMaxDotProduct( + DdManager * dd, + DdNode * S, + DdNode * T) +{ + DdNode *zRes; + int TopS, TopT; + statLine(dd); + + /* consider terminal cases */ + if ( S == z0 || T == z0 ) + return z0; + if ( S == z1 ) + return T; + if ( T == z1 ) + return S; + + /* the operation is commutative - normalize the problem */ + TopS = dd->permZ[S->index]; + TopT = dd->permZ[T->index]; + + if ( TopS > TopT || (TopS == TopT && (unsigned)S > (unsigned)T) ) + return extraZddMaxDotProduct(dd, T, S); + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddMaxDotProduct, S, T); + if (zRes) + return zRes; + else + { + DdNode *zSet0, *zSet1, *zRes0, *zRes1, *zTemp; + if ( TopS == TopT ) + { + /* compute the union of two cofactors of T (T0+T1) */ + zTemp = extraZddMaxUnion(dd, cuddE(T), cuddT(T) ); + if ( zTemp == NULL ) + return NULL; + cuddRef( zTemp ); + + /* compute MaxDotProduct with the top element for subsets (S1, T0+T1) */ + zSet0 = extraZddMaxDotProduct(dd, cuddT(S), zTemp ); + if ( zSet0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zTemp); + return NULL; + } + cuddRef( zSet0 ); + Cudd_RecursiveDerefZdd(dd, zTemp); + + /* compute MaxDotProduct with the top element for subsets (S0, T1) */ + zSet1 = extraZddMaxDotProduct(dd, cuddE(S), cuddT(T) ); + if ( zSet1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + return NULL; + } + cuddRef( zSet1 ); + + /* compute the union of these two partial results (zSet0 + zSet1) */ + zRes1 = extraZddMaxUnion(dd, zSet0, zSet1 ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd(dd, zSet0); + Cudd_RecursiveDerefZdd(dd, zSet1); + + /* compute MaxDotProduct for subsets without the top-most element */ + zRes0 = extraZddMaxDotProduct(dd, cuddE(S), cuddE(T) ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddRef( zRes0 ); + } + else /* if ( TopS < TopT ) */ + { + /* compute MaxDotProduct with the top element for subsets (S1, T) */ + zRes1 = extraZddMaxDotProduct(dd, cuddT(S), T ); + if ( zRes1 == NULL ) + return NULL; + cuddRef( zRes1 ); + + /* compute MaxDotProduct for subsets without the top-most element */ + zRes0 = extraZddMaxDotProduct(dd, cuddE(S), T ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddRef( zRes0 ); + } + + /* remove subsets without this element covered by subsets with this element */ + zRes0 = extraZddNotSubSet(dd, zTemp = zRes0, zRes1); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zTemp); + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddRef( zRes0 ); + Cudd_RecursiveDerefZdd(dd, zTemp); + + /* create the new node */ + zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddMaxDotProduct, S, T, zRes); + return zRes; + } +} /* end of extraZddMaxDotProduct */ + +/*---------------------------------------------------------------------------*/ +/* Definition of staTc Functions */ +/*---------------------------------------------------------------------------*/ + +ABC_NAMESPACE_IMPL_END diff --git a/src/bdd/extrab/extraBddSet.c b/src/bdd/extrab/extraBddSet.c new file mode 100644 index 00000000..882c474a --- /dev/null +++ b/src/bdd/extrab/extraBddSet.c @@ -0,0 +1,941 @@ +/**CFile*********************************************************************** + + FileName [zSubSet.c] + + PackageName [extra] + + Synopsis [Experimental version of some ZDD operators.] + + Description [External procedures included in this module: + <ul> + <li> Extra_zddSubSet(); + <li> Extra_zddSupSet(); + <li> Extra_zddNotSubSet(); + <li> Extra_zddNotSupSet(); + <li> Extra_zddMaxNotSupSet(); + <li> Extra_zddEmptyBelongs(); + <li> Extra_zddIsOneSubset(); + </ul> + Internal procedures included in this module: + <ul> + <li> extraZddSubSet(); + <li> extraZddSupSet(); + <li> extraZddNotSubSet(); + <li> extraZddNotSupSet(); + <li> extraZddMaxNotSupSet(); + </ul> + Static procedures included in this module: + <ul> + </ul> + + SubSet, SupSet, NotSubSet, NotSupSet were introduced + by O.Coudert to solve problems arising in two-level SOP + minimization. See O. Coudert, "Two-Level Logic Minimization: + An Overview", Integration. Vol. 17, No. 2, pp. 97-140, Oct 1994. + ] + + SeeAlso [] + + Author [Alan Mishchenko] + + Copyright [] + + Revision [$zSubSet.c, v.1.2, November 16, 2000, alanmi $] + +******************************************************************************/ + +#include "extraBdd.h" + +ABC_NAMESPACE_IMPL_START + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Computes subsets in X that are contained in some of the subsets of Y.] + + Description [] + + SideEffects [] + + SeeAlso [Extra_zddNotSubSet, Extra_zddSupSet, Extra_zddNotSupSet] + +******************************************************************************/ +DdNode * +Extra_zddSubSet( + DdManager * dd, + DdNode * X, + DdNode * Y) +{ + DdNode *res; + int autoDynZ; + + autoDynZ = dd->autoDynZ; + dd->autoDynZ = 0; + + do { + dd->reordered = 0; + res = extraZddSubSet(dd, X, Y); + } while (dd->reordered == 1); + dd->autoDynZ = autoDynZ; + return(res); + +} /* end of Extra_zddSubSet */ + + +/**Function******************************************************************** + + Synopsis [Computes subsets in X that contain some of the subsets of Y.] + + Description [] + + SideEffects [] + + SeeAlso [Extra_zddSubSet, Extra_zddNotSubSet, Extra_zddNotSupSet] + +******************************************************************************/ +DdNode * +Extra_zddSupSet( + DdManager * dd, + DdNode * X, + DdNode * Y) +{ + DdNode *res; + int autoDynZ; + + autoDynZ = dd->autoDynZ; + dd->autoDynZ = 0; + + do { + dd->reordered = 0; + res = extraZddSupSet(dd, X, Y); + } while (dd->reordered == 1); + dd->autoDynZ = autoDynZ; + return(res); + +} /* end of Extra_zddSupSet */ + +/**Function******************************************************************** + + Synopsis [Computes subsets in X that are not contained in any of the subsets of Y.] + + Description [] + + SideEffects [] + + SeeAlso [Extra_zddSubSet, Extra_zddSupSet, Extra_zddNotSupSet] + +******************************************************************************/ +DdNode * +Extra_zddNotSubSet( + DdManager * dd, + DdNode * X, + DdNode * Y) +{ + DdNode *res; + int autoDynZ; + + autoDynZ = dd->autoDynZ; + dd->autoDynZ = 0; + + do { + dd->reordered = 0; + res = extraZddNotSubSet(dd, X, Y); + } while (dd->reordered == 1); + dd->autoDynZ = autoDynZ; + return(res); + +} /* end of Extra_zddNotSubSet */ + + +/**Function******************************************************************** + + Synopsis [Computes subsets in X that do not contain any of the subsets of Y.] + + Description [] + + SideEffects [] + + SeeAlso [Extra_zddSubSet, Extra_zddSupSet, Extra_zddNotSubSet] + +******************************************************************************/ +DdNode * +Extra_zddNotSupSet( + DdManager * dd, + DdNode * X, + DdNode * Y) +{ + DdNode *res; + int autoDynZ; + + autoDynZ = dd->autoDynZ; + dd->autoDynZ = 0; + + do { + dd->reordered = 0; + res = extraZddNotSupSet(dd, X, Y); + } while (dd->reordered == 1); + dd->autoDynZ = autoDynZ; + return(res); + +} /* end of Extra_zddNotSupSet */ + + + +/**Function******************************************************************** + + Synopsis [Computes the maximal of subsets in X not contained in any of the subsets of Y.] + + Description [] + + SideEffects [] + + SeeAlso [Extra_zddSubSet, Extra_zddSupSet, Extra_zddSubSet, Extra_zddNotSupSet] + +******************************************************************************/ +DdNode * +Extra_zddMaxNotSupSet( + DdManager * dd, + DdNode * X, + DdNode * Y) +{ + DdNode *res; + int autoDynZ; + + autoDynZ = dd->autoDynZ; + dd->autoDynZ = 0; + + do { + dd->reordered = 0; + res = extraZddMaxNotSupSet(dd, X, Y); + } while (dd->reordered == 1); + dd->autoDynZ = autoDynZ; + return(res); + +} /* end of Extra_zddMaxNotSupSet */ + + +/**Function******************************************************************** + + Synopsis [Returns 1 if ZDD contains the empty combination; 0 otherwise.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int +Extra_zddEmptyBelongs( + DdManager *dd, + DdNode* zS ) +{ + while ( zS->index != CUDD_MAXINDEX ) + zS = cuddE( zS ); + return (int)( zS == z1 ); + +} /* end of Extra_zddEmptyBelongs */ + + +/**Function******************************************************************** + + Synopsis [Returns 1 if the set is empty or consists of one subset only.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int +Extra_zddIsOneSubset( + DdManager * dd, + DdNode * zS ) +{ + while ( zS->index != CUDD_MAXINDEX ) + { + assert( cuddT(zS) != z0 ); + if ( cuddE(zS) != z0 ) + return 0; + zS = cuddT( zS ); + } + return (int)( zS == z1 ); + +} /* end of Extra_zddEmptyBelongs */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddSubSet.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode* extraZddSubSet( DdManager *dd, DdNode *X, DdNode *Y ) +{ + DdNode *zRes; + statLine(dd); + /* any comb is a subset of itself */ + if ( X == Y ) + return X; + /* if X is empty, the result is empty */ + if ( X == z0 ) + return z0; + /* combs in X are notsubsets of non-existant combs in Y */ + if ( Y == z0 ) + return z0; + /* the empty comb is contained in all combs of Y */ + if ( X == z1 ) + return z1; + /* only {()} is the subset of {()} */ + if ( Y == z1 ) /* check whether the empty combination is present in X */ + return ( Extra_zddEmptyBelongs( dd, X )? z1: z0 ); + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddSubSet, X, Y); + if (zRes) + return(zRes); + else + { + DdNode *zRes0, *zRes1, *zTemp; + int TopLevelX = dd->permZ[ X->index ]; + int TopLevelY = dd->permZ[ Y->index ]; + + if ( TopLevelX < TopLevelY ) + { + /* compute combs of X without var that are notsubsets of combs with Y */ + zRes = extraZddSubSet( dd, cuddE( X ), Y ); + if ( zRes == NULL ) return NULL; + } + else if ( TopLevelX == TopLevelY ) + { + /* merge combs of Y with and without var */ + zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) ); + if ( zTemp == NULL ) + return NULL; + cuddRef( zTemp ); + + /* compute combs of X without var that are notsubsets of combs is Temp */ + zRes0 = extraZddSubSet( dd, cuddE( X ), zTemp ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + return NULL; + } + cuddRef( zRes0 ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + + /* combs of X with var that are notsubsets of combs in Y with var */ + zRes1 = extraZddSubSet( dd, cuddT( X ), cuddT( Y ) ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + else /* if ( TopLevelX > TopLevelY ) */ + { + /* merge combs of Y with and without var */ + zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) ); + if ( zTemp == NULL ) return NULL; + cuddRef( zTemp ); + + /* compute combs that are notsubsets of Temp */ + zRes = extraZddSubSet( dd, X, zTemp ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + cuddDeref( zRes ); + } + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddSubSet, X, Y, zRes); + return zRes; + } +} /* end of extraZddSubSet */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddSupSet.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode* extraZddSupSet( DdManager *dd, DdNode *X, DdNode *Y ) +{ + DdNode *zRes; + statLine(dd); + /* any comb is a superset of itself */ + if ( X == Y ) + return X; + /* no comb in X is superset of non-existing combs */ + if ( Y == z0 ) + return z0; + /* any comb in X is the superset of the empty comb */ + if ( Extra_zddEmptyBelongs( dd, Y ) ) + return X; + /* if X is empty, the result is empty */ + if ( X == z0 ) + return z0; + /* if X is the empty comb (and Y does not contain it!), return empty */ + if ( X == z1 ) + return z0; + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddSupSet, X, Y); + if (zRes) + return(zRes); + else + { + DdNode *zRes0, *zRes1, *zTemp; + int TopLevelX = dd->permZ[ X->index ]; + int TopLevelY = dd->permZ[ Y->index ]; + + if ( TopLevelX < TopLevelY ) + { + /* combinations of X without label that are supersets of combinations with Y */ + zRes0 = extraZddSupSet( dd, cuddE( X ), Y ); + if ( zRes0 == NULL ) return NULL; + cuddRef( zRes0 ); + + /* combinations of X with label that are supersets of combinations with Y */ + zRes1 = extraZddSupSet( dd, cuddT( X ), Y ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + else if ( TopLevelX == TopLevelY ) + { + /* combs of X without var that are supersets of combs of Y without var */ + zRes0 = extraZddSupSet( dd, cuddE( X ), cuddE( Y ) ); + if ( zRes0 == NULL ) return NULL; + cuddRef( zRes0 ); + + /* merge combs of Y with and without var */ + zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) ); + if ( zTemp == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zTemp ); + + /* combs of X with label that are supersets of combs in Temp */ + zRes1 = extraZddSupSet( dd, cuddT( X ), zTemp ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + else /* if ( TopLevelX > TopLevelY ) */ + { + /* combs of X that are supersets of combs of Y without label */ + zRes = extraZddSupSet( dd, X, cuddE( Y ) ); + if ( zRes == NULL ) return NULL; + } + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddSupSet, X, Y, zRes); + return zRes; + } +} /* end of extraZddSupSet */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddNotSubSet.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode* extraZddNotSubSet( DdManager *dd, DdNode *X, DdNode *Y ) +{ + DdNode *zRes; + statLine(dd); + /* any comb is a subset of itself */ + if ( X == Y ) + return z0; + /* combs in X are notsubsets of non-existant combs in Y */ + if ( Y == z0 ) + return X; + /* only {()} is the subset of {()} */ + if ( Y == z1 ) /* remove empty combination from X */ + return cuddZddDiff( dd, X, z1 ); + /* if X is empty, the result is empty */ + if ( X == z0 ) + return z0; + /* the empty comb is contained in all combs of Y */ + if ( X == z1 ) + return z0; + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddNotSubSet, X, Y); + if (zRes) + return(zRes); + else + { + DdNode *zRes0, *zRes1, *zTemp; + int TopLevelX = dd->permZ[ X->index ]; + int TopLevelY = dd->permZ[ Y->index ]; + + if ( TopLevelX < TopLevelY ) + { + /* compute combs of X without var that are notsubsets of combs with Y */ + zRes0 = extraZddNotSubSet( dd, cuddE( X ), Y ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + /* combs of X with var cannot be subsets of combs without var in Y */ + zRes1 = cuddT( X ); + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddDeref( zRes0 ); + } + else if ( TopLevelX == TopLevelY ) + { + /* merge combs of Y with and without var */ + zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) ); + if ( zTemp == NULL ) + return NULL; + cuddRef( zTemp ); + + /* compute combs of X without var that are notsubsets of combs is Temp */ + zRes0 = extraZddNotSubSet( dd, cuddE( X ), zTemp ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + return NULL; + } + cuddRef( zRes0 ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + + /* combs of X with var that are notsubsets of combs in Y with var */ + zRes1 = extraZddNotSubSet( dd, cuddT( X ), cuddT( Y ) ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + else /* if ( TopLevelX > TopLevelY ) */ + { + /* merge combs of Y with and without var */ + zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) ); + if ( zTemp == NULL ) + return NULL; + cuddRef( zTemp ); + + /* compute combs that are notsubsets of Temp */ + zRes = extraZddNotSubSet( dd, X, zTemp ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + cuddDeref( zRes ); + } + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddNotSubSet, X, Y, zRes); + return zRes; + } +} /* end of extraZddNotSubSet */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddNotSupSet.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode* extraZddNotSupSet( DdManager *dd, DdNode *X, DdNode *Y ) +{ + DdNode *zRes; + statLine(dd); + /* any comb is a superset of itself */ + if ( X == Y ) + return z0; + /* no comb in X is superset of non-existing combs */ + if ( Y == z0 ) + return X; + /* any comb in X is the superset of the empty comb */ + if ( Extra_zddEmptyBelongs( dd, Y ) ) + return z0; + /* if X is empty, the result is empty */ + if ( X == z0 ) + return z0; + /* if X is the empty comb (and Y does not contain it!), return it */ + if ( X == z1 ) + return z1; + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddNotSupSet, X, Y); + if (zRes) + return(zRes); + else + { + DdNode *zRes0, *zRes1, *zTemp; + int TopLevelX = dd->permZ[ X->index ]; + int TopLevelY = dd->permZ[ Y->index ]; + + if ( TopLevelX < TopLevelY ) + { + /* combinations of X without label that are supersets of combinations of Y */ + zRes0 = extraZddNotSupSet( dd, cuddE( X ), Y ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + /* combinations of X with label that are supersets of combinations of Y */ + zRes1 = extraZddNotSupSet( dd, cuddT( X ), Y ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + else if ( TopLevelX == TopLevelY ) + { + /* combs of X without var that are not supersets of combs of Y without var */ + zRes0 = extraZddNotSupSet( dd, cuddE( X ), cuddE( Y ) ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + /* merge combs of Y with and without var */ + zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) ); + if ( zTemp == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zTemp ); + + /* combs of X with label that are supersets of combs in Temp */ + zRes1 = extraZddNotSupSet( dd, cuddT( X ), zTemp ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + else /* if ( TopLevelX > TopLevelY ) */ + { + /* combs of X that are supersets of combs of Y without label */ + zRes = extraZddNotSupSet( dd, X, cuddE( Y ) ); + if ( zRes == NULL ) return NULL; + } + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddNotSupSet, X, Y, zRes); + return zRes; + } +} /* end of extraZddNotSupSet */ + + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Extra_zddMaxNotSupSet.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode* extraZddMaxNotSupSet( DdManager *dd, DdNode *X, DdNode *Y ) +{ + DdNode *zRes; + statLine(dd); + /* any comb is a superset of itself */ + if ( X == Y ) + return z0; + /* no comb in X is superset of non-existing combs */ + if ( Y == z0 ) + return extraZddMaximal( dd, X ); + /* any comb in X is the superset of the empty comb */ + if ( Extra_zddEmptyBelongs( dd, Y ) ) + return z0; + /* if X is empty, the result is empty */ + if ( X == z0 ) + return z0; + /* if X is the empty comb (and Y does not contain it!), return it */ + if ( X == z1 ) + return z1; + + /* check cache */ + zRes = cuddCacheLookup2Zdd(dd, extraZddMaxNotSupSet, X, Y); + if (zRes) + return(zRes); + else + { + DdNode *zRes0, *zRes1, *zTemp; + int TopLevelX = dd->permZ[ X->index ]; + int TopLevelY = dd->permZ[ Y->index ]; + + if ( TopLevelX < TopLevelY ) + { + /* combinations of X without label that are supersets of combinations with Y */ + zRes0 = extraZddMaxNotSupSet( dd, cuddE( X ), Y ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + /* combinations of X with label that are supersets of combinations with Y */ + zRes1 = extraZddMaxNotSupSet( dd, cuddT( X ), Y ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + + /* ---------------------------------------------------- */ + /* remove subsets without this element covered by subsets with this element */ + zRes0 = extraZddNotSubSet(dd, zTemp = zRes0, zRes1); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zTemp); + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddRef( zRes0 ); + Cudd_RecursiveDerefZdd(dd, zTemp); + /* ---------------------------------------------------- */ + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + else if ( TopLevelX == TopLevelY ) + { + /* combs of X without var that are supersets of combs of Y without var */ + zRes0 = extraZddMaxNotSupSet( dd, cuddE( X ), cuddE( Y ) ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + /* merge combs of Y with and without var */ + zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) ); + if ( zTemp == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zTemp ); + + /* combs of X with label that are supersets of combs in Temp */ + zRes1 = extraZddMaxNotSupSet( dd, cuddT( X ), zTemp ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + + /* ---------------------------------------------------- */ + /* remove subsets without this element covered by subsets with this element */ + zRes0 = extraZddNotSubSet(dd, zTemp = zRes0, zRes1); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zTemp); + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddRef( zRes0 ); + Cudd_RecursiveDerefZdd(dd, zTemp); + /* ---------------------------------------------------- */ + + /* compose Res0 and Res1 with the given ZDD variable */ + zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + else /* if ( TopLevelX > TopLevelY ) */ + { + /* combs of X that are supersets of combs of Y without label */ + zRes = extraZddMaxNotSupSet( dd, X, cuddE( Y ) ); + if ( zRes == NULL ) return NULL; + } + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddMaxNotSupSet, X, Y, zRes); + return zRes; + } +} /* end of extraZddMaxNotSupSet */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + + +ABC_NAMESPACE_IMPL_END diff --git a/src/bdd/extrab/module.make b/src/bdd/extrab/module.make index 62b578f7..cee5ac80 100644 --- a/src/bdd/extrab/module.make +++ b/src/bdd/extrab/module.make @@ -2,7 +2,9 @@ SRC += src/bdd/extrab/extraBddAuto.c \ src/bdd/extrab/extraBddCas.c \ src/bdd/extrab/extraBddImage.c \ src/bdd/extrab/extraBddKmap.c \ + src/bdd/extrab/extraBddMaxMin.c \ src/bdd/extrab/extraBddMisc.c \ + src/bdd/extrab/extraBddSet.c \ src/bdd/extrab/extraBddSymm.c \ src/bdd/extrab/extraBddThresh.c \ src/bdd/extrab/extraBddTime.c \ |