2 files changed, 93 insertions, 2 deletions
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 8b20daae..8f08eaff 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -166,6 +166,9 @@ extern DdNode *     Extra_bddComputeRangeCube( DdManager * dd, int iStart, int i
 extern DdNode *     Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst );
 extern DdNode *     Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f );
 extern int          Extra_bddIsVar( DdNode * bFunc );
+extern DdNode *     Extra_bddCreateAnd( DdManager * dd, int nVars );
+extern DdNode *     Extra_bddCreateOr( DdManager * dd, int nVars );
+extern DdNode *     Extra_bddCreateExor( DdManager * dd, int nVars );
 
 /*=== extraBddKmap.c ================================================================*/
 
@@ -525,6 +528,18 @@ extern unsigned Extra_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, i
 
 /*=== extraUtilUtil.c ================================================================*/
 
+#ifndef ABS
+#define ABS(a)            ((a) < 0 ? -(a) : (a))
+#endif
+
+#ifndef MAX
+#define MAX(a,b)        ((a) > (b) ? (a) : (b))
+#endif
+
+#ifndef MIN
+#define MIN(a,b)        ((a) < (b) ? (a) : (b))
+#endif
+
 #ifndef ALLOC
 #define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
 #endif
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 00e2ac94..1c720061 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -802,9 +802,9 @@ DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f )
 
   Description []
 
-  SideEffects [None]
+  SideEffects []
 
-  SeeAlso     [Cudd_VectorSupport Cudd_Support]
+  SeeAlso     []
 
 ******************************************************************************/
 int Extra_bddIsVar( DdNode * bFunc )
@@ -815,6 +815,82 @@ int Extra_bddIsVar( DdNode * bFunc )
     return cuddIsConstant( cuddT(bFunc) ) && cuddIsConstant( Cudd_Regular(cuddE(bFunc)) );
 }
 
+/**Function********************************************************************
+
+  Synopsis    [Creates AND composed of the first nVars of the manager.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_bddCreateAnd( DdManager * dd, int nVars )
+{
+    DdNode * bFunc, * bTemp;
+    int i;
+    bFunc = Cudd_ReadOne(dd); Cudd_Ref( bFunc );
+    for ( i = 0; i < nVars; i++ )
+    {
+        bFunc = Cudd_bddAnd( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) );  Cudd_Ref( bFunc );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Creates OR composed of the first nVars of the manager.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_bddCreateOr( DdManager * dd, int nVars )
+{
+    DdNode * bFunc, * bTemp;
+    int i;
+    bFunc = Cudd_ReadLogicZero(dd); Cudd_Ref( bFunc );
+    for ( i = 0; i < nVars; i++ )
+    {
+        bFunc = Cudd_bddOr( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) );  Cudd_Ref( bFunc );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Creates EXOR composed of the first nVars of the manager.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_bddCreateExor( DdManager * dd, int nVars )
+{
+    DdNode * bFunc, * bTemp;
+    int i;
+    bFunc = Cudd_ReadLogicZero(dd); Cudd_Ref( bFunc );
+    for ( i = 0; i < nVars; i++ )
+    {
+        bFunc = Cudd_bddXor( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) );  Cudd_Ref( bFunc );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
 /*---------------------------------------------------------------------------*/