Extending extra library with additional ZDD-based procedures.

4 files changed, 2048 insertions, 0 deletions

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 \