diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-08-24 19:49:18 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-08-24 19:49:18 -0700 |
commit | 77d64787e07638ac9e44ee892e4d4db5b52686e1 (patch) | |
tree | 18c1b7d3eea9e38c875afc80980352c43baef9e4 /src/base/abci | |
parent | 1fffe8f6f3274e03289a67a0abf9c7aa4028f823 (diff) | |
download | abc-77d64787e07638ac9e44ee892e4d4db5b52686e1.tar.gz abc-77d64787e07638ac9e44ee892e4d4db5b52686e1.tar.bz2 abc-77d64787e07638ac9e44ee892e4d4db5b52686e1.zip |
Changes to be able to compile ABC without CUDD.
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abcAuto.c | 11 | ||||
-rw-r--r-- | src/base/abci/abcBm.c | 4 | ||||
-rw-r--r-- | src/base/abci/abcCas.c | 11 | ||||
-rw-r--r-- | src/base/abci/abcCascade.c | 11 | ||||
-rw-r--r-- | src/base/abci/abcCollapse.c | 15 | ||||
-rw-r--r-- | src/base/abci/abcDsd.c | 13 | ||||
-rw-r--r-- | src/base/abci/abcFpga.c | 3 | ||||
-rw-r--r-- | src/base/abci/abcIf.c | 4 | ||||
-rw-r--r-- | src/base/abci/abcIvy.c | 5 | ||||
-rw-r--r-- | src/base/abci/abcLutmin.c | 11 | ||||
-rw-r--r-- | src/base/abci/abcMulti.c | 11 | ||||
-rw-r--r-- | src/base/abci/abcMv.c | 6 | ||||
-rw-r--r-- | src/base/abci/abcPrint.c | 6 | ||||
-rw-r--r-- | src/base/abci/abcProve.c | 5 | ||||
-rw-r--r-- | src/base/abci/abcReach.c | 6 | ||||
-rw-r--r-- | src/base/abci/abcReconv.c | 7 | ||||
-rw-r--r-- | src/base/abci/abcRefactor.c | 12 | ||||
-rw-r--r-- | src/base/abci/abcRenode.c | 13 | ||||
-rw-r--r-- | src/base/abci/abcReorder.c | 11 | ||||
-rw-r--r-- | src/base/abci/abcRestruct.c | 11 | ||||
-rw-r--r-- | src/base/abci/abcSat.c | 8 | ||||
-rw-r--r-- | src/base/abci/abcSweep.c | 64 | ||||
-rw-r--r-- | src/base/abci/abcSymm.c | 10 | ||||
-rw-r--r-- | src/base/abci/abcUnate.c | 10 | ||||
-rw-r--r-- | src/base/abci/abcUnreach.c | 11 |
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 /// //////////////////////////////////////////////////////////////////////// |