diff options
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 /// //////////////////////////////////////////////////////////////////////// |