Changes to be able to compile ABC without CUDD.

50 files changed, 589 insertions, 190 deletions

diff --git a/src/aig/aig/aigSplit.c b/src/aig/aig/aigSplit.c
index 90884b8b..33b353a5 100644
--- a/src/aig/aig/aigSplit.c
+++ b/src/aig/aig/aigSplit.c
@@ -20,7 +20,10 @@
 
 #include "aig.h"
 #include "aig/saig/saig.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -33,6 +36,8 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 /**Function*************************************************************
 
   Synopsis    [Converts the node to MUXes.]
@@ -307,6 +312,15 @@ Aig_Man_t * Aig_ManSplit( Aig_Man_t * p, int nVars, int fVerbose )
     return pRes;
 }
 
+#else
+
+Aig_Man_t * Aig_ManSplit( Aig_Man_t * p, int nVars, int fVerbose )
+{
+    return NULL;
+}
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaClp.c b/src/aig/gia/giaClp.c
index 7e8b3456..d67c57eb 100644
--- a/src/aig/gia/giaClp.c
+++ b/src/aig/gia/giaClp.c
@@ -19,8 +19,11 @@
 ***********************************************************************/
 
 #include "gia.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
 #include "bdd/dsd/dsd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -28,6 +31,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 extern int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
 extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
 extern int Abc_NtkDeriveFlatGiaSop( Gia_Man_t * pGia, int * gFanins, char * pSop );
@@ -399,6 +404,15 @@ void Gia_ManCollapseTestTest( Gia_Man_t * p )
     Gia_ManStop( pNew );
 }
 
+#else
+
+Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
+{
+    return NULL;
+}
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcBlifMv.c b/src/base/abc/abcBlifMv.c
index ab0966a9..30602be1 100644
--- a/src/base/abc/abcBlifMv.c
+++ b/src/base/abc/abcBlifMv.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -953,6 +956,7 @@ Abc_Ntk_t * Abc_NtkInsertBlifMv( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtkLogic )
 ***********************************************************************/
 int Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk )
 {
+#ifdef ABC_USE_CUDD
     Mem_Flex_t * pMmFlex;
     Abc_Obj_t * pNode;
     Vec_Str_t * vCube;
@@ -1011,6 +1015,7 @@ int Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk )
     pNtk->pManFunc = pMmFlex;
 
     Vec_StrFree( vCube );
+#endif
     return 1;
 }
 
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index fca3b8dc..53baa905 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -20,7 +20,10 @@
 
 #include "abc.h"
 #include "base/main/main.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -543,12 +546,14 @@ int Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
     }
     else if ( Abc_NtkHasBdd(pNtk) )
     {
+#ifdef ABC_USE_CUDD
         int nSuppSize = Cudd_SupportSize((DdManager *)pNtk->pManFunc, (DdNode *)pNode->pData);
         if ( nSuppSize > Abc_ObjFaninNum(pNode) )
         {
             fprintf( stdout, "NodeCheck: BDD of the node \"%s\" has incorrect support size.\n", Abc_ObjNameNet(pNode) );
             return 0;
         }
+#endif
     }
     else if ( !Abc_NtkHasMapping(pNtk) && !Abc_NtkHasBlifMv(pNtk) && !Abc_NtkHasAig(pNtk) )
     {
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 919cfbc3..a8fb352d 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -21,7 +21,10 @@
 #include "abc.h"
 #include "base/main/main.h"
 #include "map/mio/mio.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -32,10 +35,12 @@ ABC_NAMESPACE_IMPL_START
 
 #define ABC_MAX_CUBES   100000
 
-int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
-static DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot);
 static Hop_Obj_t * Abc_ConvertSopToAig( Hop_Man_t * pMan, char * pSop );
 
+#ifdef ABC_USE_CUDD
+
+int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
+static DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot);
 extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
 
 ////////////////////////////////////////////////////////////////////////
@@ -623,128 +628,6 @@ int Abc_CountZddCubes( DdManager * dd, DdNode * zCover )
     return nCubes;
 }
 
-
-/**Function*************************************************************
-
-  Synopsis    [Converts the network from SOP to AIG representation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkSopToAig( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pNode;
-    Hop_Man_t * pMan;
-    int i;
-
-    assert( Abc_NtkHasSop(pNtk) ); 
-
-    // make dist1-free and SCC-free
-//    Abc_NtkMakeLegit( pNtk );
-
-    // start the functionality manager
-    pMan = Hop_ManStart();
-
-    // convert each node from SOP to BDD
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        if ( Abc_ObjIsBarBuf(pNode) )
-            continue;
-        assert( pNode->pData );
-        pNode->pData = Abc_ConvertSopToAig( pMan, (char *)pNode->pData );
-        if ( pNode->pData == NULL )
-        {
-            Hop_ManStop( pMan );
-            printf( "Abc_NtkSopToAig: Error while converting SOP into AIG.\n" );
-            return 0;
-        }
-    }
-    Mem_FlexStop( (Mem_Flex_t *)pNtk->pManFunc, 0 );
-    pNtk->pManFunc = pMan;
-
-    // update the network type
-    pNtk->ntkFunc = ABC_FUNC_AIG;
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Strashes one logic node using its SOP.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Abc_ConvertSopToAigInternal( Hop_Man_t * pMan, char * pSop )
-{
-    Hop_Obj_t * pAnd, * pSum;
-    int i, Value, nFanins;
-    char * pCube;
-    // get the number of variables
-    nFanins = Abc_SopGetVarNum(pSop);
-    if ( Abc_SopIsExorType(pSop) )
-    {
-        pSum = Hop_ManConst0(pMan); 
-        for ( i = 0; i < nFanins; i++ )
-            pSum = Hop_Exor( pMan, pSum, Hop_IthVar(pMan,i) );
-    }
-    else
-    {
-        // go through the cubes of the node's SOP
-        pSum = Hop_ManConst0(pMan); 
-        Abc_SopForEachCube( pSop, nFanins, pCube )
-        {
-            // create the AND of literals
-            pAnd = Hop_ManConst1(pMan);
-            Abc_CubeForEachVar( pCube, Value, i )
-            {
-                if ( Value == '1' )
-                    pAnd = Hop_And( pMan, pAnd, Hop_IthVar(pMan,i) );
-                else if ( Value == '0' )
-                    pAnd = Hop_And( pMan, pAnd, Hop_Not(Hop_IthVar(pMan,i)) );
-            }
-            // add to the sum of cubes
-            pSum = Hop_Or( pMan, pSum, pAnd );
-        }
-    }
-    // decide whether to complement the result
-    if ( Abc_SopIsComplement(pSop) )
-        pSum = Hop_Not(pSum);
-    return pSum;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converts the network from AIG to BDD representation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Abc_ConvertSopToAig( Hop_Man_t * pMan, char * pSop )
-{
-    extern Hop_Obj_t * Dec_GraphFactorSop( Hop_Man_t * pMan, char * pSop );
-    int fUseFactor = 1;
-    // consider the constant node
-    if ( Abc_SopGetVarNum(pSop) == 0 )
-        return Hop_NotCond( Hop_ManConst1(pMan), Abc_SopIsConst0(pSop) );
-    // decide when to use factoring
-    if ( fUseFactor && Abc_SopGetVarNum(pSop) > 2 && Abc_SopGetCubeNum(pSop) > 1 && !Abc_SopIsExorType(pSop) )
-        return Dec_GraphFactorSop( pMan, pSop );
-    return Abc_ConvertSopToAigInternal( pMan, pSop );
-}
-
 /**Function*************************************************************
 
   Synopsis    [Converts the network from AIG to BDD representation.]
@@ -903,6 +786,136 @@ DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot )
     return bFunc;
 }
 
+#else
+
+int  Abc_NtkSopToBdd( Abc_Ntk_t * pNtk ) { return 1; }
+int  Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit ) { return 1; }
+void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Mem_Flex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 ) {}
+void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ) {}
+int  Abc_NtkAigToBdd( Abc_Ntk_t * pNtk ) { return 1; }
+
+#endif
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from SOP to AIG representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkSopToAig( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    Hop_Man_t * pMan;
+    int i;
+
+    assert( Abc_NtkHasSop(pNtk) ); 
+
+    // make dist1-free and SCC-free
+//    Abc_NtkMakeLegit( pNtk );
+
+    // start the functionality manager
+    pMan = Hop_ManStart();
+
+    // convert each node from SOP to BDD
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_ObjIsBarBuf(pNode) )
+            continue;
+        assert( pNode->pData );
+        pNode->pData = Abc_ConvertSopToAig( pMan, (char *)pNode->pData );
+        if ( pNode->pData == NULL )
+        {
+            Hop_ManStop( pMan );
+            printf( "Abc_NtkSopToAig: Error while converting SOP into AIG.\n" );
+            return 0;
+        }
+    }
+    Mem_FlexStop( (Mem_Flex_t *)pNtk->pManFunc, 0 );
+    pNtk->pManFunc = pMan;
+
+    // update the network type
+    pNtk->ntkFunc = ABC_FUNC_AIG;
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_ConvertSopToAigInternal( Hop_Man_t * pMan, char * pSop )
+{
+    Hop_Obj_t * pAnd, * pSum;
+    int i, Value, nFanins;
+    char * pCube;
+    // get the number of variables
+    nFanins = Abc_SopGetVarNum(pSop);
+    if ( Abc_SopIsExorType(pSop) )
+    {
+        pSum = Hop_ManConst0(pMan); 
+        for ( i = 0; i < nFanins; i++ )
+            pSum = Hop_Exor( pMan, pSum, Hop_IthVar(pMan,i) );
+    }
+    else
+    {
+        // go through the cubes of the node's SOP
+        pSum = Hop_ManConst0(pMan); 
+        Abc_SopForEachCube( pSop, nFanins, pCube )
+        {
+            // create the AND of literals
+            pAnd = Hop_ManConst1(pMan);
+            Abc_CubeForEachVar( pCube, Value, i )
+            {
+                if ( Value == '1' )
+                    pAnd = Hop_And( pMan, pAnd, Hop_IthVar(pMan,i) );
+                else if ( Value == '0' )
+                    pAnd = Hop_And( pMan, pAnd, Hop_Not(Hop_IthVar(pMan,i)) );
+            }
+            // add to the sum of cubes
+            pSum = Hop_Or( pMan, pSum, pAnd );
+        }
+    }
+    // decide whether to complement the result
+    if ( Abc_SopIsComplement(pSop) )
+        pSum = Hop_Not(pSum);
+    return pSum;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from AIG to BDD representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_ConvertSopToAig( Hop_Man_t * pMan, char * pSop )
+{
+    extern Hop_Obj_t * Dec_GraphFactorSop( Hop_Man_t * pMan, char * pSop );
+    int fUseFactor = 1;
+    // consider the constant node
+    if ( Abc_SopGetVarNum(pSop) == 0 )
+        return Hop_NotCond( Hop_ManConst1(pMan), Abc_SopIsConst0(pSop) );
+    // decide when to use factoring
+    if ( fUseFactor && Abc_SopGetVarNum(pSop) > 2 && Abc_SopGetCubeNum(pSop) > 1 && !Abc_SopIsExorType(pSop) )
+        return Dec_GraphFactorSop( pMan, pSop );
+    return Abc_ConvertSopToAigInternal( pMan, pSop );
+}
 
 
 /**Function*************************************************************
diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index a77a87a1..1edeb049 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -292,8 +295,10 @@ void Abc_NtkNodeConvertToMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t *
     Abc_ObjAddFanin( pMux, pNode0 );
     if ( Abc_NtkHasSop(pNtk) )
         pMux->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, "11- 1\n0-1 1\n" );
+#ifdef ABC_USE_CUDD
     else if ( Abc_NtkHasBdd(pNtk) )
         pMux->pData = Cudd_bddIte((DdManager *)pNtk->pManFunc,Cudd_bddIthVar((DdManager *)pNtk->pManFunc,0),Cudd_bddIthVar((DdManager *)pNtk->pManFunc,1),Cudd_bddIthVar((DdManager *)pNtk->pManFunc,2)), Cudd_Ref( (DdNode *)pMux->pData );
+#endif
     else if ( Abc_NtkHasAig(pNtk) )
         pMux->pData = Hop_Mux((Hop_Man_t *)pNtk->pManFunc,Hop_IthVar((Hop_Man_t *)pNtk->pManFunc,0),Hop_IthVar((Hop_Man_t *)pNtk->pManFunc,1),Hop_IthVar((Hop_Man_t *)pNtk->pManFunc,2));
     else
diff --git a/src/base/abc/abcMinBase.c b/src/base/abc/abcMinBase.c
index b6a32885..b7ee005c 100644
--- a/src/base/abc/abcMinBase.c
+++ b/src/base/abc/abcMinBase.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -28,6 +31,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
  
+#ifdef ABC_USE_CUDD
+
 extern int Abc_NodeSupport( DdNode * bFunc, Vec_Str_t * vSupport, int nVars );
 
 ////////////////////////////////////////////////////////////////////////
@@ -816,6 +821,17 @@ int Abc_NtkEliminateSpecial( Abc_Ntk_t * pNtk, int nMaxSize, int fVerbose )
     return 1;
 }
 
+#else
+
+int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk )     { return 0; }
+int Abc_NodeMinimumBase( Abc_Obj_t * pNode )   { return 0; }
+int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk ) { return 0; }
+int Abc_NtkEliminateSpecial( Abc_Ntk_t * pNtk, int nMaxSize, int fVerbose ) { return 0; }
+int Abc_NtkEliminate( Abc_Ntk_t * pNtk, int nMaxSize, int fReverse, int fVerbose ) { return 0; }
+int Abc_NtkEliminate1( Abc_Ntk_t * pNtk, int ElimValue, int nMaxSize, int nIterMax, int fReverse, int fVerbose ) { return 0; }
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 89a7d22c..d66bb393 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -23,7 +23,10 @@
 #include "base/main/main.h"
 #include "map/mio/mio.h"
 #include "aig/gia/gia.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -75,8 +78,10 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan
         pNtk->pManFunc = Abc_AigAlloc( pNtk );
     else if ( Abc_NtkHasSop(pNtk) || Abc_NtkHasBlifMv(pNtk) )
         pNtk->pManFunc = Mem_FlexStart();
+#ifdef ABC_USE_CUDD
     else if ( Abc_NtkHasBdd(pNtk) )
         pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+#endif
     else if ( Abc_NtkHasAig(pNtk) )
         pNtk->pManFunc = Hop_ManStart();
     else if ( Abc_NtkHasMapping(pNtk) )
@@ -1292,8 +1297,10 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     // dereference the BDDs
     if ( Abc_NtkHasBdd(pNtk) )
     {
+#ifdef ABC_USE_CUDD
         Abc_NtkForEachNode( pNtk, pObj, i )
             Cudd_RecursiveDeref( (DdManager *)pNtk->pManFunc, (DdNode *)pObj->pData );
+#endif
     }
     // make sure all the marks are clean
     Abc_NtkForEachObj( pNtk, pObj, i )
@@ -1356,8 +1363,10 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
         Abc_AigFree( (Abc_Aig_t *)pNtk->pManFunc );
     else if ( Abc_NtkHasSop(pNtk) || Abc_NtkHasBlifMv(pNtk) )
         Mem_FlexStop( (Mem_Flex_t *)pNtk->pManFunc, 0 );
+#ifdef ABC_USE_CUDD
     else if ( Abc_NtkHasBdd(pNtk) )
         Extra_StopManager( (DdManager *)pNtk->pManFunc );
+#endif
     else if ( Abc_NtkHasAig(pNtk) )
         { if ( pNtk->pManFunc ) Hop_ManStop( (Hop_Man_t *)pNtk->pManFunc ); }
     else if ( Abc_NtkHasMapping(pNtk) )
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 91d89026..c6e78c68 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -22,7 +22,10 @@
 #include "abcInt.h"
 #include "base/main/main.h"
 #include "map/mio/mio.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -213,8 +216,10 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
         case ABC_OBJ_NET:  
             break;
         case ABC_OBJ_NODE: 
+#ifdef ABC_USE_CUDD
             if ( Abc_NtkHasBdd(pNtk) )
                 Cudd_RecursiveDeref( (DdManager *)pNtk->pManFunc, (DdNode *)pObj->pData );
+#endif
             pObj->pData = NULL;
             break;
         case ABC_OBJ_LATCH:     
@@ -372,8 +377,10 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName
             {}
             else if ( Abc_NtkHasSop(pNtkNew) || Abc_NtkHasBlifMv(pNtkNew) )
                 pObjNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, (char *)pObj->pData );
+#ifdef ABC_USE_CUDD
             else if ( Abc_NtkHasBdd(pNtkNew) )
                 pObjNew->pData = Cudd_bddTransfer((DdManager *)pObj->pNtk->pManFunc, (DdManager *)pNtkNew->pManFunc, (DdNode *)pObj->pData), Cudd_Ref((DdNode *)pObjNew->pData);
+#endif
             else if ( Abc_NtkHasAig(pNtkNew) )
                 pObjNew->pData = Hop_Transfer((Hop_Man_t *)pObj->pNtk->pManFunc, (Hop_Man_t *)pNtkNew->pManFunc, (Hop_Obj_t *)pObj->pData, Abc_ObjFaninNum(pObj));
             else if ( Abc_NtkHasMapping(pNtkNew) )
@@ -608,8 +615,10 @@ Abc_Obj_t * Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk )
     pNode = Abc_NtkCreateNode( pNtk );   
     if ( Abc_NtkHasSop(pNtk) || Abc_NtkHasBlifMv(pNtk) )
         pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 0\n" );
+#ifdef ABC_USE_CUDD
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_ReadLogicZero((DdManager *)pNtk->pManFunc), Cudd_Ref( (DdNode *)pNode->pData );
+#endif
     else if ( Abc_NtkHasAig(pNtk) )
         pNode->pData = Hop_ManConst0((Hop_Man_t *)pNtk->pManFunc);
     else if ( Abc_NtkHasMapping(pNtk) )
@@ -637,8 +646,10 @@ Abc_Obj_t * Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk )
     pNode = Abc_NtkCreateNode( pNtk );   
     if ( Abc_NtkHasSop(pNtk) || Abc_NtkHasBlifMv(pNtk) )
         pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 1\n" );
+#ifdef ABC_USE_CUDD
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_ReadOne((DdManager *)pNtk->pManFunc), Cudd_Ref( (DdNode *)pNode->pData );
+#endif
     else if ( Abc_NtkHasAig(pNtk) )
         pNode->pData = Hop_ManConst1((Hop_Man_t *)pNtk->pManFunc);
     else if ( Abc_NtkHasMapping(pNtk) )
@@ -667,8 +678,10 @@ Abc_Obj_t * Abc_NtkCreateNodeInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
     if ( pFanin ) Abc_ObjAddFanin( pNode, pFanin );
     if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, "0 1\n" );
+#ifdef ABC_USE_CUDD
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_Not(Cudd_bddIthVar((DdManager *)pNtk->pManFunc,0)), Cudd_Ref( (DdNode *)pNode->pData );
+#endif
     else if ( Abc_NtkHasAig(pNtk) )
         pNode->pData = Hop_Not(Hop_IthVar((Hop_Man_t *)pNtk->pManFunc,0));
     else if ( Abc_NtkHasMapping(pNtk) )
@@ -697,8 +710,10 @@ Abc_Obj_t * Abc_NtkCreateNodeBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
     if ( pFanin ) Abc_ObjAddFanin( pNode, pFanin );
     if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, "1 1\n" );
+#ifdef ABC_USE_CUDD
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_bddIthVar((DdManager *)pNtk->pManFunc,0), Cudd_Ref( (DdNode *)pNode->pData );
+#endif
     else if ( Abc_NtkHasAig(pNtk) )
         pNode->pData = Hop_IthVar((Hop_Man_t *)pNtk->pManFunc,0);
     else if ( Abc_NtkHasMapping(pNtk) )
@@ -729,8 +744,10 @@ Abc_Obj_t * Abc_NtkCreateNodeAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
         Abc_ObjAddFanin( pNode, (Abc_Obj_t *)vFanins->pArray[i] );
     if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtk->pManFunc, Vec_PtrSize(vFanins), NULL );
+#ifdef ABC_USE_CUDD
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Extra_bddCreateAnd( (DdManager *)pNtk->pManFunc, Vec_PtrSize(vFanins) ), Cudd_Ref((DdNode *)pNode->pData); 
+#endif
     else if ( Abc_NtkHasAig(pNtk) )
         pNode->pData = Hop_CreateAnd( (Hop_Man_t *)pNtk->pManFunc, Vec_PtrSize(vFanins) ); 
     else
@@ -759,8 +776,10 @@ Abc_Obj_t * Abc_NtkCreateNodeOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
         Abc_ObjAddFanin( pNode, (Abc_Obj_t *)vFanins->pArray[i] );
     if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopCreateOr( (Mem_Flex_t *)pNtk->pManFunc, Vec_PtrSize(vFanins), NULL );
+#ifdef ABC_USE_CUDD
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Extra_bddCreateOr( (DdManager *)pNtk->pManFunc, Vec_PtrSize(vFanins) ), Cudd_Ref((DdNode *)pNode->pData); 
+#endif
     else if ( Abc_NtkHasAig(pNtk) )
         pNode->pData = Hop_CreateOr( (Hop_Man_t *)pNtk->pManFunc, Vec_PtrSize(vFanins) ); 
     else
@@ -789,8 +808,10 @@ Abc_Obj_t * Abc_NtkCreateNodeExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
         Abc_ObjAddFanin( pNode, (Abc_Obj_t *)vFanins->pArray[i] );
     if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopCreateXorSpecial( (Mem_Flex_t *)pNtk->pManFunc, Vec_PtrSize(vFanins) );
+#ifdef ABC_USE_CUDD
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Extra_bddCreateExor( (DdManager *)pNtk->pManFunc, Vec_PtrSize(vFanins) ), Cudd_Ref((DdNode *)pNode->pData); 
+#endif
     else if ( Abc_NtkHasAig(pNtk) )
         pNode->pData = Hop_CreateExor( (Hop_Man_t *)pNtk->pManFunc, Vec_PtrSize(vFanins) ); 
     else
@@ -819,8 +840,10 @@ Abc_Obj_t * Abc_NtkCreateNodeMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_
     Abc_ObjAddFanin( pNode, pNode0 );
     if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, "11- 1\n0-1 1\n" );
+#ifdef ABC_USE_CUDD
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_bddIte((DdManager *)pNtk->pManFunc,Cudd_bddIthVar((DdManager *)pNtk->pManFunc,0),Cudd_bddIthVar((DdManager *)pNtk->pManFunc,1),Cudd_bddIthVar((DdManager *)pNtk->pManFunc,2)), Cudd_Ref( (DdNode *)pNode->pData );
+#endif
     else if ( Abc_NtkHasAig(pNtk) )
         pNode->pData = Hop_Mux((Hop_Man_t *)pNtk->pManFunc,Hop_IthVar((Hop_Man_t *)pNtk->pManFunc,0),Hop_IthVar((Hop_Man_t *)pNtk->pManFunc,1),Hop_IthVar((Hop_Man_t *)pNtk->pManFunc,2));
     else
@@ -866,8 +889,10 @@ int Abc_NodeIsConst0( Abc_Obj_t * pNode )
         return 0;
     if ( Abc_NtkHasSop(pNtk) )
         return Abc_SopIsConst0((char *)pNode->pData);
+#ifdef ABC_USE_CUDD
     if ( Abc_NtkHasBdd(pNtk) )
         return Cudd_IsComplement(pNode->pData);
+#endif
     if ( Abc_NtkHasAig(pNtk) )
         return Hop_IsComplement((Hop_Obj_t *)pNode->pData)? 1:0;
     if ( Abc_NtkHasMapping(pNtk) )
@@ -896,8 +921,10 @@ int Abc_NodeIsConst1( Abc_Obj_t * pNode )
         return 0;
     if ( Abc_NtkHasSop(pNtk) )
         return Abc_SopIsConst1((char *)pNode->pData);
+#ifdef ABC_USE_CUDD
     if ( Abc_NtkHasBdd(pNtk) )
         return !Cudd_IsComplement(pNode->pData);
+#endif
     if ( Abc_NtkHasAig(pNtk) )
         return !Hop_IsComplement((Hop_Obj_t *)pNode->pData);
     if ( Abc_NtkHasMapping(pNtk) )
@@ -926,8 +953,10 @@ int Abc_NodeIsBuf( Abc_Obj_t * pNode )
         return 0;
     if ( Abc_NtkHasSop(pNtk) )
         return Abc_SopIsBuf((char *)pNode->pData);
+#ifdef ABC_USE_CUDD
     if ( Abc_NtkHasBdd(pNtk) )
         return !Cudd_IsComplement(pNode->pData);
+#endif
     if ( Abc_NtkHasAig(pNtk) )
         return !Hop_IsComplement((Hop_Obj_t *)pNode->pData);
     if ( Abc_NtkHasMapping(pNtk) )
@@ -956,8 +985,10 @@ int Abc_NodeIsInv( Abc_Obj_t * pNode )
         return 0;
     if ( Abc_NtkHasSop(pNtk) )
         return Abc_SopIsInv((char *)pNode->pData);
+#ifdef ABC_USE_CUDD
     if ( Abc_NtkHasBdd(pNtk) )
         return Cudd_IsComplement(pNode->pData);
+#endif
     if ( Abc_NtkHasAig(pNtk) )
         return Hop_IsComplement((Hop_Obj_t *)pNode->pData)? 1:0;
     if ( Abc_NtkHasMapping(pNtk) )
@@ -985,8 +1016,10 @@ void Abc_NodeComplement( Abc_Obj_t * pNode )
         Abc_SopComplement( (char *)pNode->pData );
     else if ( Abc_NtkHasAig(pNode->pNtk) )
         pNode->pData = Hop_Not( (Hop_Obj_t *)pNode->pData );
+#ifdef ABC_USE_CUDD
     else if ( Abc_NtkHasBdd(pNode->pNtk) )
         pNode->pData = Cudd_Not( pNode->pData );
+#endif
     else
         assert( 0 );
 }
@@ -1015,6 +1048,7 @@ void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin )
         Abc_SopComplementVar( (char *)pNode->pData, iFanin );
     else if ( Abc_NtkHasAig(pNode->pNtk) )
         pNode->pData = Hop_Complement( (Hop_Man_t *)pNode->pNtk->pManFunc, (Hop_Obj_t *)pNode->pData, iFanin );
+#ifdef ABC_USE_CUDD
     else if ( Abc_NtkHasBdd(pNode->pNtk) )
     {
         DdManager * dd = (DdManager *)pNode->pNtk->pManFunc;
@@ -1027,6 +1061,7 @@ void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin )
         Cudd_RecursiveDeref( dd, bCof0 );
         Cudd_RecursiveDeref( dd, bCof1 );
     }
+#endif
     else
         assert( 0 );
 }
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index 32a2f428..9753eef1 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -28,7 +28,10 @@
 #include "abc.h"
 #include "base/main/main.h"
 #include "base/io/ioAbc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -44,6 +47,8 @@ static void Abc_ShowGetFileName( char * pName, char * pBuffer );
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 /**Function*************************************************************
 
   Synopsis    [Visualizes BDD of the node.]
@@ -55,32 +60,17 @@ static void Abc_ShowGetFileName( char * pName, char * pBuffer );
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeShowBdd( Abc_Obj_t * pNode )
+void Abc_NodeShowBddOne( DdManager * dd, DdNode * bFunc )
 {
+    char * FileNameDot = "temp.dot";
     FILE * pFile;
-    Vec_Ptr_t * vNamesIn;
-    char FileNameDot[200];
-    char * pNameOut;
-
-    assert( Abc_NtkIsBddLogic(pNode->pNtk) );
-    // create the file name
-    Abc_ShowGetFileName( Abc_ObjName(pNode), FileNameDot );
-    // check that the file can be opened
     if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
     {
         fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
         return;
     }
-
-    // set the node names 
-    vNamesIn = Abc_NodeGetFaninNames( pNode );
-    pNameOut = Abc_ObjName(pNode);
-    Cudd_DumpDot( (DdManager *)pNode->pNtk->pManFunc, 1, (DdNode **)&pNode->pData, (char **)vNamesIn->pArray, &pNameOut, pFile );
-    Abc_NodeFreeNames( vNamesIn );
-    Abc_NtkCleanCopy( pNode->pNtk );
+    Cudd_DumpDot( dd, 1, (DdNode **)&bFunc, NULL, NULL, pFile );
     fclose( pFile );
-
-    // visualize the file 
     Abc_ShowFile( FileNameDot );
 }
 
@@ -95,19 +85,39 @@ void Abc_NodeShowBdd( Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeShowBddOne( DdManager * dd, DdNode * bFunc )
+void Abc_NodeShowBdd( Abc_Obj_t * pNode )
 {
-    char * FileNameDot = "temp.dot";
     FILE * pFile;
+    Vec_Ptr_t * vNamesIn;
+    char FileNameDot[200];
+    char * pNameOut;
+
+    assert( Abc_NtkIsBddLogic(pNode->pNtk) );
+    // create the file name
+    Abc_ShowGetFileName( Abc_ObjName(pNode), FileNameDot );
+    // check that the file can be opened
     if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
     {
         fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
         return;
     }
-    Cudd_DumpDot( dd, 1, (DdNode **)&bFunc, NULL, NULL, pFile );
+
+    // set the node names 
+    vNamesIn = Abc_NodeGetFaninNames( pNode );
+    pNameOut = Abc_ObjName(pNode);
+    Cudd_DumpDot( (DdManager *)pNode->pNtk->pManFunc, 1, (DdNode **)&pNode->pData, (char **)vNamesIn->pArray, &pNameOut, pFile );
+    Abc_NodeFreeNames( vNamesIn );
+    Abc_NtkCleanCopy( pNode->pNtk );
     fclose( pFile );
+
+    // visualize the file 
     Abc_ShowFile( FileNameDot );
 }
+
+#else
+void Abc_NodeShowBdd( Abc_Obj_t * pNode ) {}
+#endif
+
 /**Function*************************************************************
 
   Synopsis    [Visualizes a reconvergence driven cut at the node.]
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index b1fc6855..706201cb 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -22,9 +22,12 @@
 #include "base/main/main.h"
 #include "map/mio/mio.h"
 #include "bool/dec/dec.h"
-#include "misc/extra/extraBdd.h"
 #include "opt/fxu/fxu.h"
 
+#ifdef ABC_USE_CUDD
+#include "misc/extra/extraBdd.h"
+#endif
+
 ABC_NAMESPACE_IMPL_START
 
 
@@ -241,8 +244,10 @@ int Abc_NtkGetMultiRefNum( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk )
 {
+    int nNodes = 0;
+#ifdef ABC_USE_CUDD
     Abc_Obj_t * pNode;
-    int i, nNodes = 0;
+    int i;
     assert( Abc_NtkIsBddLogic(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
@@ -251,6 +256,7 @@ int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk )
             continue;
         nNodes += pNode->pData? -1 + Cudd_DagSize( (DdNode *)pNode->pData ) : 0;
     }
+#endif
     return nNodes;
 }
 
@@ -294,11 +300,13 @@ int Abc_NtkGetAigNodeNum( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 int Abc_NtkGetClauseNum( Abc_Ntk_t * pNtk )
 {
+    int nClauses = 0;
+#ifdef ABC_USE_CUDD
     extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
     Abc_Obj_t * pNode;
     DdNode * bCover, * zCover, * bFunc;
     DdManager * dd = (DdManager *)pNtk->pManFunc;
-    int i, nClauses = 0;
+    int i;
     assert( Abc_NtkIsBddLogic(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
@@ -319,6 +327,7 @@ int Abc_NtkGetClauseNum( Abc_Ntk_t * pNtk )
         Cudd_RecursiveDeref( dd, bCover );
         Cudd_RecursiveDerefZdd( dd, zCover );
     }
+#endif
     return nClauses;
 }
 
diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c
index 390442fe..5f02b6d2 100644
--- a/src/base/abci/abcAuto.c
+++ b/src/base/abci/abcAuto.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -28,6 +31,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 static void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int nOutputs, char * pInputNames[], char * pOutputNames[], int fNaive );
 static void Abc_NtkAutoPrintOne( DdManager * dd, int nInputs, DdNode * pbOutputs[], int Output, char * pInputNames[], char * pOutputNames[], int fNaive );
  
@@ -236,6 +241,12 @@ void Abc_NtkAutoPrintOne( DdManager * dd, int nInputs, DdNode * pbOutputs[], int
     Cudd_RecursiveDerefZdd( dd, zEquations );
 }
 
+#else
+
+void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose ) {}
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcBm.c b/src/base/abci/abcBm.c
index 60051f64..ce1582dd 100644
--- a/src/base/abci/abcBm.c
+++ b/src/base/abci/abcBm.c
@@ -30,10 +30,12 @@
 #include "base/abc/abc.h"
 #include "opt/sim/sim.h"
 #include "sat/bsat/satSolver.h"
-#include "misc/extra/extraBdd.h"
+//#include "misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
+#define FALSE 0
+#define TRUE  1
 
 int match1by1(Abc_Ntk_t * pNtk1, Vec_Ptr_t ** nodesInLevel1, Vec_Int_t ** iMatch1, Vec_Int_t ** iDep1, Vec_Int_t * matchedInputs1, int * iGroup1, Vec_Int_t ** oMatch1, int * oGroup1,
                Abc_Ntk_t * pNtk2, Vec_Ptr_t ** nodesInLevel2, Vec_Int_t ** iMatch2, Vec_Int_t ** iDep2, Vec_Int_t * matchedInputs2, int * iGroup2, Vec_Int_t ** oMatch2, int * oGroup2,
diff --git a/src/base/abci/abcCas.c b/src/base/abci/abcCas.c
index 1ded2f27..17aa99cb 100644
--- a/src/base/abci/abcCas.c
+++ b/src/base/abci/abcCas.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -35,6 +38,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 extern int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutputs, int nInputs, int nOutputs, int nLutSize, int fCheck, int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
@@ -108,6 +113,12 @@ Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVer
     return pNtkNew;
 }
 
+#else
+
+Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVerbose ) { return NULL; }
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcCascade.c b/src/base/abci/abcCascade.c
index ccae60a5..9ba10c34 100644
--- a/src/base/abci/abcCascade.c
+++ b/src/base/abci/abcCascade.c
@@ -19,8 +19,11 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "bdd/reo/reo.h"
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -28,6 +31,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 #define BDD_FUNC_MAX 256
 
 //extern void Abc_NodeShowBddOne( DdManager * dd, DdNode * bFunc );
@@ -1042,6 +1047,12 @@ Abc_NtkExploreCofs( dd, bFunc, dd->vars, Abc_NtkCiNum(pNtk), 6 );
     return pNtkNew;
 }
 
+#else
+
+Abc_Ntk_t * Abc_NtkBddDec( Abc_Ntk_t * pNtk, int fVerbose ) { return NULL; }
+
+#endif
+
 ABC_NAMESPACE_IMPL_END
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index dada7765..cc3d74c2 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -19,15 +19,19 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk );
 static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc );
 
@@ -277,6 +281,15 @@ Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode
     return pNodeNew;
 }
 
+#else
+
+Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
+{
+    return NULL;
+}
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 609bce99..44475cca 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -19,8 +19,11 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
 #include "bdd/dsd/dsd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -29,6 +32,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
  
+#ifdef ABC_USE_CUDD
+
 static Abc_Ntk_t *     Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, int fVerbose, int fPrint, int fShort );
 static void            Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 static Abc_Obj_t *     Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew, int * pCounters );
@@ -688,6 +693,14 @@ Abc_Ntk_t * Abc_NtkSparsify( Abc_Ntk_t * pNtk, int nPerc, int fVerbose )
     return pNtkNew;
 }
 
+#else
+
+Abc_Ntk_t * Abc_NtkSparsify( Abc_Ntk_t * pNtk, int nPerc, int fVerbose )                { return NULL; }
+Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, int fVerbose, int fPrint, int fShort )  { return NULL; }
+int         Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, int fVerbose, int fRecursive )           { return 0;    }
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c
index 965bd5f8..a9c3baee 100644
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -20,7 +20,10 @@
 
 #include "base/abc/abc.h"
 #include "map/fpga/fpgaInt.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 9ad5e41e..c45eaec5 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -470,12 +470,16 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
         if ( pIfMan->pPars->fUseBdds )
         { 
             // transform truth table into the BDD 
+#ifdef ABC_USE_CUDD
             pNodeNew->pData = Kit_TruthToBdd( (DdManager *)pNtkNew->pManFunc, If_CutTruth(pIfMan, pCutBest), If_CutLeaveNum(pCutBest), 0 );  Cudd_Ref((DdNode *)pNodeNew->pData); 
+#endif
         }
         else if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
         { 
             // transform truth table into the BDD 
+#ifdef ABC_USE_CUDD
             pNodeNew->pData = Kit_TruthToBdd( (DdManager *)pNtkNew->pManFunc, If_CutTruth(pIfMan, pCutBest), If_CutLeaveNum(pCutBest), 1 );  Cudd_Ref((DdNode *)pNodeNew->pData); 
+#endif
         }
         else if ( pIfMan->pPars->fUseSops || pIfMan->pPars->nGateSize > 0 ) 
         {
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 27926af4..94b339bc 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -25,7 +25,10 @@
 #include "proof/fraig/fraig.h"
 #include "map/mio/mio.h"
 #include "aig/aig/aig.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -589,6 +592,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
     }
 
     // try to prove it using brute force BDDs
+#ifdef ABC_USE_CUDD
     if ( RetValue < 0 && pParams->fUseBdds )
     {
         if ( pParams->fVerbose )
@@ -605,6 +609,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
         else 
             pNtk = pNtkTemp;
     }
+#endif
 
     // return the result
     *ppNtk = pNtk;
diff --git a/src/base/abci/abcLutmin.c b/src/base/abci/abcLutmin.c
index acbeee70..219f2357 100644
--- a/src/base/abci/abcLutmin.c
+++ b/src/base/abci/abcLutmin.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -38,6 +41,8 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 /**Function*************************************************************
 
   Synopsis    [Check if a LUT can absort a fanin.]
@@ -765,6 +770,12 @@ Abc_Ntk_t * Abc_NtkLutmin( Abc_Ntk_t * pNtkInit, int nLutSize, int fVerbose )
     return pNtkNew;
 }
 
+#else
+
+Abc_Ntk_t * Abc_NtkLutmin( Abc_Ntk_t * pNtkInit, int nLutSize, int fVerbose ) { return NULL; }
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcMulti.c b/src/base/abci/abcMulti.c
index 8e4bbf28..53e4005a 100644
--- a/src/base/abci/abcMulti.c
+++ b/src/base/abci/abcMulti.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -28,6 +31,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 static void        Abc_NtkMultiInt( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 static Abc_Obj_t * Abc_NtkMulti_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld );
 
@@ -640,6 +645,12 @@ void Abc_NtkMultiCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone )
     Abc_NtkMultiCone_rec( Abc_ObjFanin(pNode,1), vCone );
 }
 
+#else
+
+Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor ) { return NULL; }
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcMv.c b/src/base/abci/abcMv.c
index d589c3e7..3f597fcd 100644
--- a/src/base/abci/abcMv.c
+++ b/src/base/abci/abcMv.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -28,6 +31,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 typedef struct Mv_Man_t_ Mv_Man_t;
 struct Mv_Man_t_
 {
@@ -365,6 +370,7 @@ void Abc_MvDecompose( Mv_Man_t * p )
 
     Cudd_RecursiveDeref( p->dd, bCube );
 }
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index a50b522c..cab24877 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -25,7 +25,10 @@
 #include "map/mio/mio.h"
 #include "aig/aig/aig.h"
 #include "map/if/if.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 #ifdef WIN32
 #include <windows.h>
@@ -1030,6 +1033,7 @@ void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode )
 ***********************************************************************/
 void Abc_NodePrintKMap( Abc_Obj_t * pNode, int fUseRealNames )
 {
+#ifdef ABC_USE_CUDD
     Vec_Ptr_t * vNamesIn;
     if ( fUseRealNames )
     {
@@ -1041,7 +1045,7 @@ void Abc_NodePrintKMap( Abc_Obj_t * pNode, int fUseRealNames )
     else
         Extra_PrintKMap( stdout, (DdManager *)pNode->pNtk->pManFunc, (DdNode *)pNode->pData, Cudd_Not(pNode->pData),
             Abc_ObjFaninNum(pNode), NULL, 0, NULL );
-
+#endif
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index 909cc46b..4be3a398 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -22,7 +22,10 @@
 
 #include "base/abc/abc.h"
 #include "proof/fraig/fraig.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -189,6 +192,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
     }    
 
     // try to prove it using brute force SAT
+#ifdef ABC_USE_CUDD
     if ( RetValue < 0 && pParams->fUseBdds )
     {
         if ( pParams->fVerbose )
@@ -207,6 +211,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
             pNtk = pNtkTemp;
         Abc_NtkMiterPrint( pNtk, "BDD building", clk, pParams->fVerbose );
     }
+#endif
 
     if ( RetValue < 0 )
     {
diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c
index e91a1d5a..97ee158f 100644
--- a/src/base/abci/abcReach.c
+++ b/src/base/abci/abcReach.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -32,6 +35,8 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 /**Function*************************************************************
 
   Synopsis    [Computes the initial state and sets up the variable map.]
@@ -311,6 +316,7 @@ void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fP
     fflush( stdout );
 }
 
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c
index 56c2251a..f13930bb 100644
--- a/src/base/abci/abcReconv.c
+++ b/src/base/abci/abcReconv.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -484,6 +487,8 @@ void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
     Vec_PtrPush( vVisited, pNode );
 }
 
+#ifdef ABC_USE_CUDD
+
 /**Function*************************************************************
 
   Synopsis    [Returns BDD representing the logic function of the cone.]
@@ -574,6 +579,8 @@ DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY,
     return bResult;
 }
  
+#endif
+
 /**Function*************************************************************
 
   Synopsis    [Starts the resynthesis manager.]
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 891deff9..8ff1d470 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -20,7 +20,10 @@
 
 #include "base/abc/abc.h"
 #include "bool/dec/dec.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -28,7 +31,9 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
- 
+
+#ifdef ABC_USE_CUDD
+
 typedef struct Abc_ManRef_t_   Abc_ManRef_t;
 struct Abc_ManRef_t_
 {
@@ -381,6 +386,11 @@ void Abc_NtkManRefPrintStats( Abc_ManRef_t * p )
     ABC_PRT( "TOTAL      ", p->timeTotal );
 }
 
+#else
+
+int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose ) { return 1; }
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index ad97aa22..5995f36d 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -19,10 +19,13 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
-#include "bdd/reo/reo.h"
 #include "map/if/if.h"
 #include "bool/kit/kit.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#include "bdd/reo/reo.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -31,6 +34,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 static int Abc_NtkRenodeEvalAig( If_Man_t * p, If_Cut_t * pCut );
 static int Abc_NtkRenodeEvalBdd( If_Man_t * p, If_Cut_t * pCut );
 static int Abc_NtkRenodeEvalSop( If_Man_t * p, If_Cut_t * pCut );
@@ -306,6 +311,12 @@ int Abc_NtkRenodeEvalMv( If_Man_t * p, If_Cut_t * pCut )
     return RetValue;
 }
 
+#else
+
+Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fUseMv, int fVerbose ) { return NULL; }
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcReorder.c b/src/base/abci/abcReorder.c
index 4f8d50fa..cf8759c7 100644
--- a/src/base/abci/abcReorder.c
+++ b/src/base/abci/abcReorder.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "bdd/reo/reo.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -31,6 +34,8 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 /**Function*************************************************************
 
   Synopsis    [Reorders BDD of the local function of the node.]
@@ -97,6 +102,12 @@ void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose )
     Extra_ReorderQuit( p );
 }
 
+#else
+
+void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose ) {}
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index 1863c629..87ba3712 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -21,8 +21,11 @@
 #include "base/abc/abc.h"
 #include "bool/dec/dec.h"
 #include "opt/cut/cut.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
 #include "bdd/dsd/dsd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -31,6 +34,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
   
+#ifdef ABC_USE_CUDD
+
 #define RST_RANDOM_UNSIGNED   ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
 
 typedef struct Abc_ManRst_t_   Abc_ManRst_t;
@@ -1491,6 +1496,12 @@ Dec_Graph_t * Abc_NodeResubstitute( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut
     return pGraphBest;
 }
 
+#else
+
+int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, int fUpdateLevel, int fUseZeros, int fVerbose ) { return 1; }
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 349ebc55..e2b8864c 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -22,7 +22,10 @@
 #include "base/main/main.h"
 #include "base/cmd/cmd.h"
 #include "sat/bsat/satSolver.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -657,6 +660,7 @@ sat_solver_store_mark_roots( pSat );
 
 
 
+#ifdef ABC_USE_CUDD
 
 /**Function*************************************************************
 
@@ -889,7 +893,11 @@ finish:
     return pSat;
 }
 
+#else
+
+sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes ) { return NULL; }
 
+#endif
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 7eae3587..49450e99 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -21,7 +21,10 @@
 #include "base/abc/abc.h"
 #include "base/main/main.h"
 #include "proof/fraig/fraig.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -38,7 +41,6 @@ static int            Abc_NodeDroppingCost( Abc_Obj_t * pNode );
 
 static int            Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes );
 static void           Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose );
-static void           Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, int fConst0 );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -560,6 +562,36 @@ int Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes )
 
 
 
+#ifdef ABC_USE_CUDD
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces the local function by its cofactor.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, int fConst0 )
+{
+    DdManager * dd = (DdManager *)pNode->pNtk->pManFunc;
+    DdNode * bVar, * bTemp;
+    int iFanin;
+    assert( Abc_NtkIsBddLogic(pNode->pNtk) ); 
+    if ( (iFanin = Vec_IntFind( &pNode->vFanins, pFanin->Id )) == -1 )
+    {
+        printf( "Node %s should be among", Abc_ObjName(pFanin) );
+        printf( " the fanins of node %s...\n", Abc_ObjName(pNode) );
+        return;
+    }
+    bVar = Cudd_NotCond( Cudd_bddIthVar(dd, iFanin), fConst0 );
+    pNode->pData = Cudd_Cofactor( dd, bTemp = (DdNode *)pNode->pData, bVar );   Cudd_Ref( (DdNode *)pNode->pData );
+    Cudd_RecursiveDeref( dd, bTemp );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Tranditional sweep of the network.]
@@ -655,33 +687,11 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
 }
 
 
-/**Function*************************************************************
-
-  Synopsis    [Replaces the local function by its cofactor.]
-
-  Description []
-               
-  SideEffects []
+#else
 
-  SeeAlso     []
+int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose ) { return 1; }
 
-***********************************************************************/
-void Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, int fConst0 )
-{
-    DdManager * dd = (DdManager *)pNode->pNtk->pManFunc;
-    DdNode * bVar, * bTemp;
-    int iFanin;
-    assert( Abc_NtkIsBddLogic(pNode->pNtk) ); 
-    if ( (iFanin = Vec_IntFind( &pNode->vFanins, pFanin->Id )) == -1 )
-    {
-        printf( "Node %s should be among", Abc_ObjName(pFanin) );
-        printf( " the fanins of node %s...\n", Abc_ObjName(pNode) );
-        return;
-    }
-    bVar = Cudd_NotCond( Cudd_bddIthVar(dd, iFanin), fConst0 );
-    pNode->pData = Cudd_Cofactor( dd, bTemp = (DdNode *)pNode->pData, bVar );   Cudd_Ref( (DdNode *)pNode->pData );
-    Cudd_RecursiveDeref( dd, bTemp );
-}
+#endif
 
 
 /**Function*************************************************************
@@ -1011,8 +1021,6 @@ int Abc_NtkSweepBufsInvs( Abc_Ntk_t * pNtk, int fVerbose )
 
 
 
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c
index 03226770..224c3968 100644
--- a/src/base/abci/abcSymm.c
+++ b/src/base/abci/abcSymm.c
@@ -20,7 +20,10 @@
 
 #include "base/abc/abc.h"
 #include "opt/sim/sim.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -29,6 +32,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
  
+#ifdef ABC_USE_CUDD
+
 static void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fReorder, int fVerbose );
 static void Abc_NtkSymmetriesUsingSandS( Abc_Ntk_t * pNtk, int fVerbose );
 static void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVerbose );
@@ -226,6 +231,11 @@ void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms )
     ABC_FREE( pVarTaken );
 }
 
+#else
+
+void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fReorder, int fVerbose ) {}
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c
index 01b9cf51..0998bd86 100644
--- a/src/base/abci/abcUnate.c
+++ b/src/base/abci/abcUnate.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -27,6 +30,7 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
+#ifdef ABC_USE_CUDD
 
 static void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose );
 static void Abc_NtkPrintUnateSat( Abc_Ntk_t * pNtk, int fVerbose );
@@ -153,6 +157,12 @@ void Abc_NtkPrintUnateSat( Abc_Ntk_t * pNtk, int fVerbose )
 {
 }
 
+#else
+
+void Abc_NtkPrintUnate( Abc_Ntk_t * pNtk, int fUseBdds, int fUseNaive, int fVerbose ){}
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index f7b4cfa3..08fc2809 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -28,6 +31,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 static DdNode *    Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose );
 static DdNode *    Abc_NtkInitStateAndVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose );
 static DdNode *    Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bRelation, DdNode * bInitial, int fVerbose );
@@ -346,6 +351,12 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
 //    return NULL;
 }
 
+#else
+
+int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, int fVerbose ) { return 1; }
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioWritePla.c b/src/base/io/ioWritePla.c
index ea06e113..389e4efa 100644
--- a/src/base/io/ioWritePla.c
+++ b/src/base/io/ioWritePla.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "ioAbc.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -191,6 +194,7 @@ int Io_WritePla( Abc_Ntk_t * pNtk, char * pFileName )
     return 1;
 }
 
+#ifdef ABC_USE_CUDD
 
 /**Function*************************************************************
 
@@ -441,6 +445,12 @@ int Io_WriteMoPla( Abc_Ntk_t * pNtk, char * pFileName )
     return 1;
 }
 
+#else
+
+int Io_WriteMoPla( Abc_Ntk_t * pNtk, char * pFileName ) { return 1; }
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 42a1da81..c91a5d55 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -21,9 +21,11 @@
 #include "base/abc/abc.h"
 #include "mainInt.h"
 #include "bool/dec/dec.h"
-#include "misc/extra/extraBdd.h"
 #include "map/if/if.h"
 
+#ifdef ABC_USE_CUDD
+#include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -57,7 +59,9 @@ void *      Abc_FrameReadLibGen()                            { return s_GlobalFr
 void *      Abc_FrameReadLibGen2()                           { return s_GlobalFrame->pLibGen2;     } 
 void *      Abc_FrameReadLibSuper()                          { return s_GlobalFrame->pLibSuper;    } 
 void *      Abc_FrameReadLibScl()                            { return s_GlobalFrame->pLibScl;      } 
+#ifdef ABC_USE_CUDD
 void *      Abc_FrameReadManDd()                             { if ( s_GlobalFrame->dd == NULL )      s_GlobalFrame->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );  return s_GlobalFrame->dd;      } 
+#endif
 void *      Abc_FrameReadManDec()                            { if ( s_GlobalFrame->pManDec == NULL ) s_GlobalFrame->pManDec = Dec_ManStart();                                        return s_GlobalFrame->pManDec; } 
 void *      Abc_FrameReadManDsd()                            { return s_GlobalFrame->pManDsd;      } 
 void *      Abc_FrameReadManDsd2()                           { return s_GlobalFrame->pManDsd2;     } 
@@ -190,7 +194,9 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     if ( p->vPoEquivs )  Vec_VecFree( (Vec_Vec_t *)p->vPoEquivs );
     if ( p->vStatuses )  Vec_IntFree( p->vStatuses );
     if ( p->pManDec   )  Dec_ManStop( (Dec_Man_t *)p->pManDec );
+#ifdef ABC_USE_CUDD
     if ( p->dd        )  Extra_StopManager( p->dd );
+#endif
     if ( p->vStore    )  Vec_PtrFree( p->vStore );
     if ( p->pSave1    )  Aig_ManStop( (Aig_Man_t *)p->pSave1 );
     if ( p->pSave2    )  Aig_ManStop( (Aig_Man_t *)p->pSave2 );
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 8f446cfd..baf3b82e 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -33,9 +33,10 @@
 #include "aig/gia/gia.h"
 #include "proof/ssw/ssw.h"
 #include "proof/fra/fra.h"
-//#include "aig/nwk/nwkMerge.h"
-//#include "aig/ntl/ntlnwk.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_HEADER_START
 
@@ -86,7 +87,6 @@ struct Abc_Frame_t_
     void *          pManDec;       // decomposition manager
     void *          pManDsd;       // decomposition manager
     void *          pManDsd2;      // decomposition manager
-    DdManager *     dd;            // temporary BDD package
     // libraries for mapping
     void *          pLibLut;       // the current LUT library
     void *          pLibBox;       // the current box library
@@ -130,6 +130,9 @@ struct Abc_Frame_t_
     void *          pAbcBac;
     void *          pAbcCba;
     void *          pAbcPla;
+#ifdef ABC_USE_CUDD
+    DdManager *     dd;            // temporary BDD package
+#endif
 };
 
 typedef void (*Abc_Frame_Initialization_Func)( Abc_Frame_t * pAbc );
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index ee413727..f1062112 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -18,6 +18,7 @@
 
 ***********************************************************************/
 
+#include <math.h>
 #include "wlc.h"
 #include "misc/vec/vecWec.h"
 
diff --git a/src/bool/bdc/bdcSpfd.c b/src/bool/bdc/bdcSpfd.c
index 8a00b02f..02e932fe 100644
--- a/src/bool/bdc/bdcSpfd.c
+++ b/src/bool/bdc/bdcSpfd.c
@@ -20,6 +20,7 @@
 
 #include "bdcInt.h"
 #include "aig/aig/aig.h"
+#include "misc/extra/extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/bool/dec/decFactor.c b/src/bool/dec/decFactor.c
index 391496e1..59ea6f26 100644
--- a/src/bool/dec/decFactor.c
+++ b/src/bool/dec/decFactor.c
@@ -19,9 +19,12 @@
 #include "base/abc/abc.h"
 #include "base/main/main.h"
 #include "misc/mvc/mvc.h"
-#include "misc/extra/extraBdd.h"
 #include "dec.h"
 
+#ifdef ABC_USE_CUDD
+#include "misc/extra/extraBdd.h"
+#endif
+
 ABC_NAMESPACE_IMPL_START
 
 
@@ -352,6 +355,8 @@ Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
     return pMvc;
 }
 
+#ifdef ABC_USE_CUDD
+
 /**Function*************************************************************
 
   Synopsis    [Verifies that the factoring is correct.]
@@ -387,6 +392,7 @@ int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm )
     return RetValue;
 }
 
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/bool/dec/decUtil.c b/src/bool/dec/decUtil.c
index d64aa4fa..eade1f5b 100644
--- a/src/bool/dec/decUtil.c
+++ b/src/bool/dec/decUtil.c
@@ -17,9 +17,12 @@
 ***********************************************************************/
 
 #include "base/abc/abc.h"
-#include "misc/extra/extraBdd.h"
 #include "dec.h"
 
+#ifdef ABC_USE_CUDD
+#include "misc/extra/extraBdd.h"
+#endif
+
 ABC_NAMESPACE_IMPL_START
 
 
@@ -31,6 +34,8 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 /**Function*************************************************************
 
   Synopsis    [Converts graph to BDD.]
@@ -81,6 +86,8 @@ DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph )
     return Cudd_NotCond( bFunc, Dec_GraphIsComplement(pGraph) );
 }
 
+#endif
+
 /**Function*************************************************************
 
   Synopsis    [Derives the truth table.]
diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h
index 35a2cae8..29d23d68 100644
--- a/src/bool/kit/kit.h
+++ b/src/bool/kit/kit.h
@@ -32,9 +32,12 @@
 #include <assert.h>
 
 #include "misc/vec/vec.h"
-#include "misc/extra/extraBdd.h"
 #include "cloud.h"
 
+#ifdef ABC_USE_CUDD
+#include "misc/extra/extraBdd.h"
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
@@ -509,9 +512,11 @@ static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar )
 ////////////////////////////////////////////////////////////////////////
 
 /*=== kitBdd.c ==========================================================*/
+#ifdef ABC_USE_CUDD
 extern DdNode *        Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars );
 extern DdNode *        Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph );
 extern DdNode *        Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop );
+#endif
 /*=== kitCloud.c ==========================================================*/
 extern CloudNode *     Kit_TruthToCloud( CloudManager * dd, unsigned * pTruth, int nVars );
 extern unsigned *      Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore, int fInv );
diff --git a/src/bool/kit/kitBdd.c b/src/bool/kit/kitBdd.c
index 9b6cb09f..9c7c918d 100644
--- a/src/bool/kit/kitBdd.c
+++ b/src/bool/kit/kitBdd.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "kit.h"
+
+#ifdef ABC_USE_CUDD
 #include "misc/extra/extraBdd.h"
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -32,6 +35,8 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef ABC_USE_CUDD
+
 /**Function*************************************************************
 
   Synopsis    [Derives the BDD for the given SOP.]
@@ -227,6 +232,8 @@ int Kit_SopFactorVerify( Vec_Int_t * vCover, Kit_Graph_t * pFForm, int nVars )
     return RetValue;
 }
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/bool/kit/kitDsd.c b/src/bool/kit/kitDsd.c
index d026afbc..0150a549 100644
--- a/src/bool/kit/kitDsd.c
+++ b/src/bool/kit/kitDsd.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "kit.h"
+#include "misc/extra/extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/map/mapper/mapperInt.h b/src/map/mapper/mapperInt.h
index fdfece30..28f40a82 100644
--- a/src/map/mapper/mapperInt.h
+++ b/src/map/mapper/mapperInt.h
@@ -28,10 +28,11 @@
 #include <stdlib.h>
 #include <string.h>
 #include <float.h>
+#include <math.h>
+
 #include "base/main/main.h"
 #include "map/mio/mio.h"
 #include "mapper.h"
-#include "misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_HEADER_START
 
diff --git a/src/map/scl/sclLibScl.c b/src/map/scl/sclLibScl.c
index f47c1721..2e4e1deb 100644
--- a/src/map/scl/sclLibScl.c
+++ b/src/map/scl/sclLibScl.c
@@ -22,6 +22,7 @@
 #include "misc/st/st.h"
 #include "map/mio/mio.h"
 #include "bool/kit/kit.h"
+#include "misc/extra/extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/misc/extra/extraUtilPrime.c b/src/misc/extra/extraUtilPrime.c
index 48aa5580..215de367 100644
--- a/src/misc/extra/extraUtilPrime.c
+++ b/src/misc/extra/extraUtilPrime.c
@@ -25,6 +25,7 @@
 #include "misc/vec/vec.h"
 #include "misc/vec/vecHsh.h"
 #include "bool/kit/kit.h"
+#include "misc/extra/extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/proof/llb/llbInt.h b/src/proof/llb/llbInt.h
index 0c53c01f..e2afe59a 100644
--- a/src/proof/llb/llbInt.h
+++ b/src/proof/llb/llbInt.h
@@ -30,9 +30,10 @@
 #include "aig/aig/aig.h"
 #include "aig/saig/saig.h"
 #include "proof/ssw/ssw.h"
-#include "misc/extra/extraBdd.h"
 #include "llb.h"
 
+#include "misc/extra/extraBdd.h"
+
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////