diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2010-11-01 01:35:04 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2010-11-01 01:35:04 -0700 |
| commit | 6130e39b18b5f53902e4eab14f6d5cdde5219563 (patch) | |
| tree | 0db0628479a1b750e9af1f66cb8379ebd0913d31 /src/base/abci/abcProve.c | |
| parent | f0e77f6797c0504b0da25a56152b707d3357f386 (diff) | |
| download | abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.gz abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.bz2 abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.zip | |
initial commit of public abc
Diffstat (limited to 'src/base/abci/abcProve.c')
| -rw-r--r-- | src/base/abci/abcProve.c | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c index 5a546ab1..35c1ee29 100644 --- a/src/base/abci/abcProve.c +++ b/src/base/abci/abcProve.c @@ -22,11 +22,14 @@ #include "fraig.h" #include "math.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose ); +extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose ); extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, ABC_INT64_T nInspLimit, int * pRetValue, int * pNumFails, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects ); @@ -53,7 +56,7 @@ static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fV ***********************************************************************/ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars ) { - Prove_Params_t * pParams = pPars; + Prove_Params_t * pParams = (Prove_Params_t *)pPars; Abc_Ntk_t * pNtk, * pNtkTemp; int RetValue = -1, nIter, nSatFails, Counter, clk; //, timeStart = clock(); ABC_INT64_T nSatConfs, nSatInspects, nInspectLimit; @@ -195,7 +198,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars ) if ( pNtk ) { Abc_NtkDelete( pNtkTemp ); - RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero(pNtk->pManFunc)) ); + RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero((DdManager *)pNtk->pManFunc)) ); } else pNtk = pNtkTemp; @@ -264,7 +267,7 @@ Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, ABC_INT64_T nInsp pParams->nInspLimit = nInspLimit; // transform the target into a fraig - pMan = Abc_NtkToFraig( pNtk, pParams, 0, 0 ); + pMan = (Fraig_Man_t *)Abc_NtkToFraig( pNtk, pParams, 0, 0 ); Fraig_ManProveMiter( pMan ); RetValue = Fraig_ManCheckMiter( pMan ); @@ -339,3 +342,5 @@ Abc_Ntk_t * Abc_NtkMiterRwsat( Abc_Ntk_t * pNtk ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + |