Skip to content

A
abc
Commit 77d64787 by Alan Mishchenko
Options

Changes to be able to compile ABC without CUDD.

parent 1fffe8f6
Showing with 588 additions and 189 deletions
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 ///
////////////////////////////////////////////////////////////////////////
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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;
}
......
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) )
{
......
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*************************************************************
......
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
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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) )
......
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 );
}
......
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.]
......
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;
}
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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,
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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
////////////////////////////////////////////////////////////////////////
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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
......
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 )
{
......
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;
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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 ///
......
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*************************************************************
......
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 )
{
......
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 ///
......
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.]
......
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
......@@ -29,6 +32,8 @@ 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 ///
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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*************************************************************
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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 ///
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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 );
......
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 );
......
src/base/wlc/wlcNtk.c
......@@ -18,6 +18,7 @@
***********************************************************************/
#include <math.h>
#include "wlc.h"
#include "misc/vec/vecWec.h"
......
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
......
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 ///
......
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.]
......
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 );
......
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 ///
////////////////////////////////////////////////////////////////////////
......
src/bool/kit/kitDsd.c
......@@ -19,6 +19,7 @@
***********************************************************************/
#include "kit.h"
#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
......
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
......
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
......
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
......
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 ///
////////////////////////////////////////////////////////////////////////
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment