summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--abclib.dsp8
-rw-r--r--src/bdd/extrab/extraBdd.h38
-rw-r--r--src/bdd/extrab/extraBddMaxMin.c1067
-rw-r--r--src/bdd/extrab/extraBddSet.c941
-rw-r--r--src/bdd/extrab/module.make2
5 files changed, 2056 insertions, 0 deletions
diff --git a/abclib.dsp b/abclib.dsp
index fe23c746..cead32bd 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -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 \