diff options
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/bmc/bmcBmcAnd.c | 3 | ||||
-rw-r--r-- | src/sat/bmc/bmcChain.c | 3 | ||||
-rw-r--r-- | src/sat/bmc/bmcClp.c | 10 | ||||
-rw-r--r-- | src/sat/bmc/bmcEnum.c | 4 | ||||
-rw-r--r-- | src/sat/bmc/bmcExpand.c | 4 | ||||
-rw-r--r-- | src/sat/bmc/bmcFault.c | 2 | ||||
-rw-r--r-- | src/sat/bmc/bmcFx.c | 6 | ||||
-rw-r--r-- | src/sat/bmc/bmcGen.c | 4 | ||||
-rw-r--r-- | src/sat/bmc/bmcICheck.c | 3 |
9 files changed, 13 insertions, 26 deletions
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c index 8087046a..3490d34f 100644 --- a/src/sat/bmc/bmcBmcAnd.c +++ b/src/sat/bmc/bmcBmcAnd.c @@ -986,8 +986,7 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) { // p->pFrames = Jf_ManDeriveCnf( pTemp = p->pFrames, 1 ); Gia_ManStop( pTemp ); // p->pCnf = (Cnf_Dat_t *)p->pFrames->pData; p->pFrames->pData = NULL; - extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); - p->pCnf = Mf_ManGenerateCnf( p->pFrames, pPars->nLutSize, 1, 0, pPars->fVerbose ); + p->pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p->pFrames, pPars->nLutSize, 1, 0, 0, pPars->fVerbose ); } Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 ); // create clauses for constant node diff --git a/src/sat/bmc/bmcChain.c b/src/sat/bmc/bmcChain.c index 324c7f6d..5af54306 100644 --- a/src/sat/bmc/bmcChain.c +++ b/src/sat/bmc/bmcChain.c @@ -185,10 +185,9 @@ Gia_Man_t * Gia_ManDupPosAndPropagateInit( Gia_Man_t * p ) } sat_solver * Gia_ManDeriveSatSolver( Gia_Man_t * p, Vec_Int_t * vSatIds ) { -// extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); sat_solver * pSat; Aig_Man_t * pAig = Gia_ManToAigSimple( p ); -// Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); +// Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); Cnf_Dat_t * pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); // save SAT vars for the primary inputs if ( vSatIds ) diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index 8a69fe56..cfc608b1 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -651,7 +649,7 @@ Vec_Str_t * Bmc_CollapseOneInt2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int int iOut = 0, iLit, iVar, status, n, Count, Start; // create SAT solver - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); sat_solver * pSat[3] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), @@ -841,7 +839,7 @@ Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f { int fVeryVerbose = fVerbose; int nVars = Gia_ManCiNum(p); - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); sat_solver * pSat[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) }; sat_solver * pSatClean[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) }; Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL; @@ -1173,7 +1171,7 @@ cleanup: } Vec_Str_t * Bmc_CollapseOne3( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) { - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); sat_solver * pSat0 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); sat_solver * pSat1 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); sat_solver * pSat2 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); @@ -1507,7 +1505,7 @@ cleanup: } Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) { - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); Vec_Str_t * vSop = Bmc_CollapseOne_int( pSat, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); sat_solver_delete( pSat ); diff --git a/src/sat/bmc/bmcEnum.c b/src/sat/bmc/bmcEnum.c index 5fe2c1ed..45aeb2b3 100644 --- a/src/sat/bmc/bmcEnum.c +++ b/src/sat/bmc/bmcEnum.c @@ -29,8 +29,6 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -169,7 +167,7 @@ void Gia_ManDeriveOneTest( Gia_Man_t * p ) Gia_Man_t * pNew; Gia_Obj_t * pObj, * pRoot; Vec_Int_t * vValues = Vec_IntStart( Gia_ManCiNum(p) ); - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); int i, iVar, nIter, iPoVarBeg = pCnf->nVars - Gia_ManCiNum(p); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); Vec_Int_t * vLits = Vec_IntAlloc( 100 ); diff --git a/src/sat/bmc/bmcExpand.c b/src/sat/bmc/bmcExpand.c index f3ec999e..6c7a5988 100644 --- a/src/sat/bmc/bmcExpand.c +++ b/src/sat/bmc/bmcExpand.c @@ -33,8 +33,6 @@ ABC_NAMESPACE_IMPL_START // iterator thought the cubes #define Bmc_SopForEachCube( pSop, nVars, pCube ) for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 ) -extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -93,7 +91,7 @@ int Abc_ObjExpandCubes( Vec_Str_t * vSop, Gia_Man_t * p, int nVars ) int fReverse = 0; Vec_Int_t * vVars = Vec_IntAlloc( nVars ); - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); int v, n, iLit, status, nCubesNew, iCiVarBeg = sat_solver_nvars(pSat) - nVars; diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c index 8dc2a57f..71eef2c4 100644 --- a/src/sat/bmc/bmcFault.c +++ b/src/sat/bmc/bmcFault.c @@ -280,7 +280,7 @@ static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p ) pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); Aig_ManStop( pAig ); return pCnf; -// return Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); +// return (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); } /**Function************************************************************* diff --git a/src/sat/bmc/bmcFx.c b/src/sat/bmc/bmcFx.c index 9cd37c88..15ea4f05 100644 --- a/src/sat/bmc/bmcFx.c +++ b/src/sat/bmc/bmcFx.c @@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -598,7 +596,7 @@ int Bmc_FxCompute( Gia_Man_t * p ) extern Gia_Man_t * Gia_ManDupOnsetOffset( Gia_Man_t * p ); Gia_Man_t * p2 = Gia_ManDupOnsetOffset( p ); // create SAT solver - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p2, 8, 0, 0, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p2, 8, 0, 0, 0, 0 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); // compute parameters int nOuts = Gia_ManCoNum(p); @@ -674,7 +672,7 @@ int Bmc_FxComputeOne( Gia_Man_t * p, int nIterMax, int nDiv2Add ) { int Extra = 1000; // create SAT solver - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); // compute parameters int nCiVars = Gia_ManCiNum(p); // PI count diff --git a/src/sat/bmc/bmcGen.c b/src/sat/bmc/bmcGen.c index 74af1b78..5d84ce87 100644 --- a/src/sat/bmc/bmcGen.c +++ b/src/sat/bmc/bmcGen.c @@ -29,8 +29,6 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -131,7 +129,7 @@ void Gia_ManMoFindSimulate( Gia_Man_t * p, int nWords ) int Gia_ManTestSatEnum( Gia_Man_t * p ) { abctime clk = Abc_Clock(), clk2, clkTotal = 0; - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); int i, v, status, iLit, nWords = 1, iOutVar = 1, Count = 0; Vec_Int_t * vVars = Vec_IntAlloc( 1000 ); diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c index a779b1ed..8d8c7c6b 100644 --- a/src/sat/bmc/bmcICheck.c +++ b/src/sat/bmc/bmcICheck.c @@ -392,11 +392,10 @@ int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fRev pCnf = Cnf_DeriveGiaRemapped( pMiter ); else { - extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); //pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 ); //Gia_ManStop( pTemp ); //pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL; - pCnf = Mf_ManGenerateCnf( pMiter, 8, 0, 0, 0 ); + pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pMiter, 8, 0, 0, 0, 0 ); } /* // collect positive literals |