From d335ee096e902844b9a94076e8ce5855f74d9bde Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 10 Feb 2017 11:05:00 -0800 Subject: Standardizing the use of new CNF generator. Adding CNF variable connectivity information. --- src/aig/gia/gia.h | 2 ++ src/aig/gia/giaMf.c | 58 ++++++++++++++++++++++++++++++++++++++------- src/aig/gia/giaQbf.c | 12 ++++------ src/aig/gia/giaSatoko.c | 4 +--- src/base/abci/abcCollapse.c | 4 +--- src/base/abci/abcDetect.c | 3 +-- src/proof/cec/cecCec.c | 3 +-- src/proof/pdr/pdrInv.c | 8 +++---- src/sat/bmc/bmcBmcAnd.c | 3 +-- src/sat/bmc/bmcChain.c | 3 +-- src/sat/bmc/bmcClp.c | 10 ++++---- src/sat/bmc/bmcEnum.c | 4 +--- src/sat/bmc/bmcExpand.c | 4 +--- src/sat/bmc/bmcFault.c | 2 +- src/sat/bmc/bmcFx.c | 6 ++--- src/sat/bmc/bmcGen.c | 4 +--- src/sat/bmc/bmcICheck.c | 3 +-- 17 files changed, 76 insertions(+), 57 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 3bc97e6b..6677e0ad 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -311,6 +311,7 @@ struct Jf_Par_t_ int fGenCnf; int fCnfObjIds; int fAddOrCla; + int fCnfMapping; int fPureAig; int fDoAverage; int fCutHashing; @@ -1405,6 +1406,7 @@ extern int Gia_MmStepReadMemUsage( Gia_MmStep_t * p ); /*=== giaMf.c ===========================================================*/ extern void Mf_ManSetDefaultPars( Jf_Par_t * pPars ); extern Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ); +extern void * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose ); /*=== giaMini.c ===========================================================*/ extern Gia_Man_t * Gia_ManReadMiniAig( char * pFileName ); extern void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName ); diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c index a500a839..24c1e6a0 100644 --- a/src/aig/gia/giaMf.c +++ b/src/aig/gia/giaMf.c @@ -388,6 +388,8 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) Gia_ManForEachCoId( p->pGia, Id, i ) pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[Id], 0); } + if ( p->pPars->fCnfMapping ) + pCnf->vMapping = Vec_IntStart( nVars ); // add clauses for the COs Gia_ManForEachCo( p->pGia, pObj, i ) { @@ -401,6 +403,14 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) pCnf->pClauses[iCla++] = pCnf->pClauses[0] + iLit; pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[Id], 1); pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[DriId], Gia_ObjFaninC0(pObj)); + // generate mapping + if ( pCnf->vMapping ) + { + Vec_IntWriteEntry( pCnf->vMapping, pCnfIds[Id], Vec_IntSize(pCnf->vMapping) ); + Vec_IntPush( pCnf->vMapping, 1 ); + Vec_IntPush( pCnf->vMapping, pCnfIds[DriId] ); + Vec_IntPush( pCnf->vMapping, Gia_ObjFaninC0(pObj) ? 0x55555555 : 0xAAAAAAAA ); + } } // add clauses for the mapping Gia_ManForEachAndReverseId( p->pGia, Id ) @@ -427,6 +437,35 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) if ( Mf_CubeLit(pCubes[c], k) ) pCnf->pClauses[0][iLit++] = Abc_Var2Lit( pFanins[k], Mf_CubeLit(pCubes[c], k) == 2 ); } + // generate mapping + if ( pCnf->vMapping ) + { + word pTruth[4], * pTruthP = Vec_MemReadEntry(p->vTtMem, iFunc); + assert( p->pPars->nLutSize <= 8 ); + Abc_TtCopy( pTruth, pTruthP, Abc_Truth6WordNum(p->pPars->nLutSize), Abc_LitIsCompl(iFunc) ); + assert( pCnfIds[Id] >= 0 && pCnfIds[Id] < nVars ); + Vec_IntWriteEntry( pCnf->vMapping, pCnfIds[Id], Vec_IntSize(pCnf->vMapping) ); + Vec_IntPush( pCnf->vMapping, Mf_CutSize(pCut) ); + for ( k = 0; k < Mf_CutSize(pCut); k++ ) + Vec_IntPush( pCnf->vMapping, pCnfIds[pCut[k+1]] ); + Vec_IntPush( pCnf->vMapping, (unsigned)pTruth[0] ); + if ( Mf_CutSize(pCut) >= 6 ) + { + Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[0] >> 32) ); + if ( Mf_CutSize(pCut) >= 7 ) + { + Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[1]) ); + Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[1] >> 32) ); + } + if ( Mf_CutSize(pCut) >= 8 ) + { + Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[2]) ); + Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[2] >> 32) ); + Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[3]) ); + Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[3] >> 32) ); + } + } + } } // constant clause pCnf->pClauses[iCla++] = pCnf->pClauses[0] + iLit; @@ -1636,28 +1675,29 @@ Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ) +void * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose ) { Gia_Man_t * pNew; Jf_Par_t Pars, * pPars = &Pars; assert( nLutSize >= 3 && nLutSize <= 8 ); Mf_ManSetDefaultPars( pPars ); - pPars->fGenCnf = 1; - pPars->fCoarsen = !fCnfObjIds; - pPars->nLutSize = nLutSize; - pPars->fCnfObjIds = fCnfObjIds; - pPars->fAddOrCla = fAddOrCla; - pPars->fVerbose = fVerbose; + pPars->fGenCnf = 1; + pPars->fCoarsen = !fCnfObjIds; + pPars->nLutSize = nLutSize; + pPars->fCnfObjIds = fCnfObjIds; + pPars->fAddOrCla = fAddOrCla; + pPars->fCnfMapping = fMapping; + pPars->fVerbose = fVerbose; pNew = Mf_ManPerformMapping( pGia, pPars ); Gia_ManStopP( &pNew ); // Cnf_DataPrint( (Cnf_Dat_t *)pGia->pData, 1 ); - return (Cnf_Dat_t*)pGia->pData; + return pGia->pData; } void Mf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ) { abctime clk = Abc_Clock(); Cnf_Dat_t * pCnf; - pCnf = Mf_ManGenerateCnf( p, nLutSize, fCnfObjIds, fAddOrCla, fVerbose ); + pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, nLutSize, fCnfObjIds, fAddOrCla, 0, fVerbose ); Cnf_DataWriteIntoFile( pCnf, pFileName, 0, NULL, NULL ); // if ( fVerbose ) { diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index 4ca0bac3..2dfd83fc 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -48,8 +48,6 @@ struct Qbf_Man_t_ abctime clkSat; // SAT solver time }; -extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -192,7 +190,7 @@ int Gia_ManSatEnum( Gia_Man_t * pGia, int nConfLimit, int nTimeOut, int fVerbose int i, iLit, iParVarBeg, Iter; int nSolutions = 0, RetValue = 0; abctime clkStart = Abc_Clock(); - pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 ); + pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 ); pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1; Cnf_DataFree( pCnf ); @@ -247,7 +245,7 @@ void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars ) { // original problem: \exists p \forall x \exists y. M(p,x,y) // negated problem: \forall p \exists x \exists y. !M(p,x,y) - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 ); Vec_Int_t * vVarMap, * vForAlls, * vExists; Gia_Obj_t * pObj; char * pFileName; @@ -291,7 +289,7 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose ) Qbf_Man_t * p; Cnf_Dat_t * pCnf; Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) ); - pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 ); + pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 ); Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) ); p = ABC_CALLOC( Qbf_Man_t, 1 ); p->clkStart = Abc_Clock(); @@ -426,7 +424,7 @@ Gia_Man_t * Gia_QbfCofactor( Gia_Man_t * p, int nPars, Vec_Int_t * vValues, Vec_ /* int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof ) { - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 1, 0, 0 ); int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof);// - 1; pCnf->pMan = NULL; Cnf_DataLift( pCnf, sat_solver_nvars(p->pSatSyn) ); @@ -459,7 +457,7 @@ void Cnf_SpecialDataLift( Cnf_Dat_t * p, int nVarsPlus, int firstPiVar, int last int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof ) { - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 1, 0, 0 ); int i, useold = 0; int iFirstVar = useold ? sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) : pCnf->nVars - Gia_ManPiNum(pCof); //-1 pCnf->pMan = NULL; diff --git a/src/aig/gia/giaSatoko.c b/src/aig/gia/giaSatoko.c index fc8e5c28..db81bd85 100644 --- a/src/aig/gia/giaSatoko.c +++ b/src/aig/gia/giaSatoko.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 /// //////////////////////////////////////////////////////////////////////// @@ -50,7 +48,7 @@ extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfOb satoko_t * Gia_ManCreateSatoko( Gia_Man_t * p ) { satoko_t * pSat = satoko_create(); - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 1, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 1, 0, 0 ); int i, status; //sat_solver_setnvars( pSat, p->nVars ); for ( i = 0; i < pCnf->nClauses; i++ ) diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index 8c2b3b39..1542c25a 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -537,8 +537,6 @@ extern Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose ); extern int Gia_ManCoLargestSupp( Gia_Man_t * p, Vec_Wec_t * vSupps ); extern Vec_Wec_t * Gia_ManIsoStrashReduceInt( Gia_Man_t * p, Vec_Wec_t * vSupps, int fVerbose ); -extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); - /**Function************************************************************* Synopsis [Derives GIA for the network.] @@ -802,7 +800,7 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v if ( fCnfShared ) { vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); - pCnf = Mf_ManGenerateCnf( p, 8, 1, 0, 0 ); + pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 1, 0, 0, 0 ); } vSopsRepr = Vec_PtrStart( Vec_IntSize(vReprs) ); pProgress = Extra_ProgressBarStart( stdout, Vec_IntSize(vReprs) ); diff --git a/src/base/abci/abcDetect.c b/src/base/abci/abcDetect.c index 8b8bba64..7adbed5d 100644 --- a/src/base/abci/abcDetect.c +++ b/src/base/abci/abcDetect.c @@ -901,8 +901,7 @@ Vec_Int_t * Abc_NtkFinCheckPair( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t } else { - extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); if ( pSat == NULL ) { diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index f7e45c57..be6df65f 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -225,8 +225,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) ***********************************************************************/ int Cec_ManVerifyNaive( Gia_Man_t * p, Cec_ParCec_t * pPars ) { - extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, 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 ); Gia_Obj_t * pObj0, * pObj1; abctime clkStart = Abc_Clock(); diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index 95adb10c..fe759fff 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -626,8 +626,6 @@ Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce ) ***********************************************************************/ #define Pdr_ForEachCube( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 1 ) -extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); - Vec_Int_t * Pdr_InvMap( Vec_Int_t * vCounts ) { int i, k = 0, Count; @@ -779,7 +777,7 @@ int Pdr_InvCheck_int( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose, sat_solver int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) { int RetValue; - 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 ); assert( sat_solver_nvars(pSat) == pCnf->nVars ); Cnf_DataFree( pCnf ); @@ -796,7 +794,7 @@ Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) int n, i, k, status, nLits, fFailed = 0, fCannot = 0, nRemoved = 0; Vec_Int_t * vRes = NULL; // 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 ); int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0]; // create variables @@ -914,7 +912,7 @@ Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) Vec_Int_t * vRes = NULL; abctime clk = Abc_Clock(); int i, k, nLits = 0, * pCube, * pList = Vec_IntArray(vInv), nRemoved = 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 * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); Pdr_ForEachCube( pList, pCube, i ) 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 -- cgit v1.2.3