summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abcAuto.c11
-rw-r--r--src/base/abci/abcBm.c4
-rw-r--r--src/base/abci/abcCas.c11
-rw-r--r--src/base/abci/abcCascade.c11
-rw-r--r--src/base/abci/abcCollapse.c15
-rw-r--r--src/base/abci/abcDsd.c13
-rw-r--r--src/base/abci/abcFpga.c3
-rw-r--r--src/base/abci/abcIf.c4
-rw-r--r--src/base/abci/abcIvy.c5
-rw-r--r--src/base/abci/abcLutmin.c11
-rw-r--r--src/base/abci/abcMulti.c11
-rw-r--r--src/base/abci/abcMv.c6
-rw-r--r--src/base/abci/abcPrint.c6
-rw-r--r--src/base/abci/abcProve.c5
-rw-r--r--src/base/abci/abcReach.c6
-rw-r--r--src/base/abci/abcReconv.c7
-rw-r--r--src/base/abci/abcRefactor.c12
-rw-r--r--src/base/abci/abcRenode.c13
-rw-r--r--src/base/abci/abcReorder.c11
-rw-r--r--src/base/abci/abcRestruct.c11
-rw-r--r--src/base/abci/abcSat.c8
-rw-r--r--src/base/abci/abcSweep.c64
-rw-r--r--src/base/abci/abcSymm.c10
-rw-r--r--src/base/abci/abcUnate.c10
-rw-r--r--src/base/abci/abcUnreach.c11
25 files changed, 246 insertions, 33 deletions
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 ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 04:26:05 +0000