Changes to be able to compile ABC without CUDD.

6 files changed, 30 insertions, 3 deletions

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