Skip to content

A
abc
Commit d335ee09 by Alan Mishchenko
Options

Standardizing the use of new CNF generator. Adding CNF variable connectivity information.

parent 4e6978f2
Showing with 76 additions and 57 deletions
src/aig/gia/gia.h
...@@ -311,6 +311,7 @@ struct Jf_Par_t_ ...@@ -311,6 +311,7 @@ struct Jf_Par_t_
int fGenCnf; int fGenCnf;
int fCnfObjIds; int fCnfObjIds;
int fAddOrCla; int fAddOrCla;
int fCnfMapping;
int fPureAig; int fPureAig;
int fDoAverage; int fDoAverage;
int fCutHashing; int fCutHashing;
...@@ -1405,6 +1406,7 @@ extern int Gia_MmStepReadMemUsage( Gia_MmStep_t * p ); ...@@ -1405,6 +1406,7 @@ extern int Gia_MmStepReadMemUsage( Gia_MmStep_t * p );
/*=== giaMf.c ===========================================================*/ /*=== giaMf.c ===========================================================*/
extern void Mf_ManSetDefaultPars( Jf_Par_t * pPars ); extern void Mf_ManSetDefaultPars( Jf_Par_t * pPars );
extern Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, 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 ===========================================================*/ /*=== giaMini.c ===========================================================*/
extern Gia_Man_t * Gia_ManReadMiniAig( char * pFileName ); extern Gia_Man_t * Gia_ManReadMiniAig( char * pFileName );
extern void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName ); extern void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName );
......
src/aig/gia/giaMf.c
...@@ -388,6 +388,8 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) ...@@ -388,6 +388,8 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla )
Gia_ManForEachCoId( p->pGia, Id, i ) Gia_ManForEachCoId( p->pGia, Id, i )
pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[Id], 0); pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[Id], 0);
} }
if ( p->pPars->fCnfMapping )
pCnf->vMapping = Vec_IntStart( nVars );
// add clauses for the COs // add clauses for the COs
Gia_ManForEachCo( p->pGia, pObj, i ) Gia_ManForEachCo( p->pGia, pObj, i )
{ {
...@@ -401,6 +403,14 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) ...@@ -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[iCla++] = pCnf->pClauses[0] + iLit;
pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[Id], 1); pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[Id], 1);
pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[DriId], Gia_ObjFaninC0(pObj)); 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 // add clauses for the mapping
Gia_ManForEachAndReverseId( p->pGia, Id ) Gia_ManForEachAndReverseId( p->pGia, Id )
...@@ -427,6 +437,35 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) ...@@ -427,6 +437,35 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla )
if ( Mf_CubeLit(pCubes[c], k) ) if ( Mf_CubeLit(pCubes[c], k) )
pCnf->pClauses[0][iLit++] = Abc_Var2Lit( pFanins[k], Mf_CubeLit(pCubes[c], k) == 2 ); 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 // constant clause
pCnf->pClauses[iCla++] = pCnf->pClauses[0] + iLit; pCnf->pClauses[iCla++] = pCnf->pClauses[0] + iLit;
...@@ -1636,28 +1675,29 @@ Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) ...@@ -1636,28 +1675,29 @@ Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
SeeAlso [] 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; Gia_Man_t * pNew;
Jf_Par_t Pars, * pPars = &Pars; Jf_Par_t Pars, * pPars = &Pars;
assert( nLutSize >= 3 && nLutSize <= 8 ); assert( nLutSize >= 3 && nLutSize <= 8 );
Mf_ManSetDefaultPars( pPars ); Mf_ManSetDefaultPars( pPars );
pPars->fGenCnf = 1; pPars->fGenCnf = 1;
pPars->fCoarsen = !fCnfObjIds; pPars->fCoarsen = !fCnfObjIds;
pPars->nLutSize = nLutSize; pPars->nLutSize = nLutSize;
pPars->fCnfObjIds = fCnfObjIds; pPars->fCnfObjIds = fCnfObjIds;
pPars->fAddOrCla = fAddOrCla; pPars->fAddOrCla = fAddOrCla;
pPars->fVerbose = fVerbose; pPars->fCnfMapping = fMapping;
pPars->fVerbose = fVerbose;
pNew = Mf_ManPerformMapping( pGia, pPars ); pNew = Mf_ManPerformMapping( pGia, pPars );
Gia_ManStopP( &pNew ); Gia_ManStopP( &pNew );
// Cnf_DataPrint( (Cnf_Dat_t *)pGia->pData, 1 ); // 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 ) void Mf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose )
{ {
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
Cnf_Dat_t * pCnf; 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 ); Cnf_DataWriteIntoFile( pCnf, pFileName, 0, NULL, NULL );
// if ( fVerbose ) // if ( fVerbose )
{ {
......
src/aig/gia/giaQbf.c
...@@ -48,8 +48,6 @@ struct Qbf_Man_t_ ...@@ -48,8 +48,6 @@ struct Qbf_Man_t_
abctime clkSat; // SAT solver time 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 /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -192,7 +190,7 @@ int Gia_ManSatEnum( Gia_Man_t * pGia, int nConfLimit, int nTimeOut, int fVerbose ...@@ -192,7 +190,7 @@ int Gia_ManSatEnum( Gia_Man_t * pGia, int nConfLimit, int nTimeOut, int fVerbose
int i, iLit, iParVarBeg, Iter; int i, iLit, iParVarBeg, Iter;
int nSolutions = 0, RetValue = 0; int nSolutions = 0, RetValue = 0;
abctime clkStart = Abc_Clock(); 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 ); pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1; iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1;
Cnf_DataFree( pCnf ); Cnf_DataFree( pCnf );
...@@ -247,7 +245,7 @@ void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars ) ...@@ -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) // original problem: \exists p \forall x \exists y. M(p,x,y)
// negated problem: \forall p \exists 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; Vec_Int_t * vVarMap, * vForAlls, * vExists;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
char * pFileName; char * pFileName;
...@@ -291,7 +289,7 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose ) ...@@ -291,7 +289,7 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose )
Qbf_Man_t * p; Qbf_Man_t * p;
Cnf_Dat_t * pCnf; Cnf_Dat_t * pCnf;
Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) ); 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) ); Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) );
p = ABC_CALLOC( Qbf_Man_t, 1 ); p = ABC_CALLOC( Qbf_Man_t, 1 );
p->clkStart = Abc_Clock(); p->clkStart = Abc_Clock();
...@@ -426,7 +424,7 @@ Gia_Man_t * Gia_QbfCofactor( Gia_Man_t * p, int nPars, Vec_Int_t * vValues, Vec_ ...@@ -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 ) 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; int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof);// - 1;
pCnf->pMan = NULL; pCnf->pMan = NULL;
Cnf_DataLift( pCnf, sat_solver_nvars(p->pSatSyn) ); 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 ...@@ -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 ) 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 i, useold = 0;
int iFirstVar = useold ? sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) : pCnf->nVars - Gia_ManPiNum(pCof); //-1 int iFirstVar = useold ? sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) : pCnf->nVars - Gia_ManPiNum(pCof); //-1
pCnf->pMan = NULL; pCnf->pMan = NULL;
......
src/aig/gia/giaSatoko.c
...@@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START ...@@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -50,7 +48,7 @@ extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfOb ...@@ -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 * Gia_ManCreateSatoko( Gia_Man_t * p )
{ {
satoko_t * pSat = satoko_create(); 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; int i, status;
//sat_solver_setnvars( pSat, p->nVars ); //sat_solver_setnvars( pSat, p->nVars );
for ( i = 0; i < pCnf->nClauses; i++ ) for ( i = 0; i < pCnf->nClauses; i++ )
......
src/base/abci/abcCollapse.c
...@@ -537,8 +537,6 @@ extern Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose ); ...@@ -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 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 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************************************************************* /**Function*************************************************************
Synopsis [Derives GIA for the network.] 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 ...@@ -802,7 +800,7 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
if ( fCnfShared ) if ( fCnfShared )
{ {
vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); 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) ); vSopsRepr = Vec_PtrStart( Vec_IntSize(vReprs) );
pProgress = Extra_ProgressBarStart( stdout, Vec_IntSize(vReprs) ); pProgress = Extra_ProgressBarStart( stdout, Vec_IntSize(vReprs) );
......
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 ...@@ -901,8 +901,7 @@ Vec_Int_t * Abc_NtkFinCheckPair( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t
} }
else else
{ {
extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 );
Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL ) if ( pSat == NULL )
{ {
......
src/proof/cec/cecCec.c
...@@ -225,8 +225,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) ...@@ -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 ) 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 = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
Gia_Obj_t * pObj0, * pObj1; Gia_Obj_t * pObj0, * pObj1;
abctime clkStart = Abc_Clock(); abctime clkStart = Abc_Clock();
......
src/proof/pdr/pdrInv.c
...@@ -626,8 +626,6 @@ Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce ) ...@@ -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 ) #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 ) Vec_Int_t * Pdr_InvMap( Vec_Int_t * vCounts )
{ {
int i, k = 0, Count; 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 ...@@ -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 Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose )
{ {
int RetValue; 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 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
assert( sat_solver_nvars(pSat) == pCnf->nVars ); assert( sat_solver_nvars(pSat) == pCnf->nVars );
Cnf_DataFree( pCnf ); Cnf_DataFree( pCnf );
...@@ -796,7 +794,7 @@ Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) ...@@ -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; int n, i, k, status, nLits, fFailed = 0, fCannot = 0, nRemoved = 0;
Vec_Int_t * vRes = NULL; Vec_Int_t * vRes = NULL;
// create SAT solver // 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 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0]; int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0];
// create variables // create variables
...@@ -914,7 +912,7 @@ Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) ...@@ -914,7 +912,7 @@ Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose )
Vec_Int_t * vRes = NULL; Vec_Int_t * vRes = NULL;
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
int i, k, nLits = 0, * pCube, * pList = Vec_IntArray(vInv), nRemoved = 0; 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 * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); // sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
Pdr_ForEachCube( pList, pCube, i ) Pdr_ForEachCube( pList, pCube, i )
......
src/sat/bmc/bmcBmcAnd.c
...@@ -986,8 +986,7 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) ...@@ -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->pFrames = Jf_ManDeriveCnf( pTemp = p->pFrames, 1 ); Gia_ManStop( pTemp );
// p->pCnf = (Cnf_Dat_t *)p->pFrames->pData; p->pFrames->pData = NULL; // 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 = (Cnf_Dat_t *)Mf_ManGenerateCnf( p->pFrames, pPars->nLutSize, 1, 0, 0, pPars->fVerbose );
p->pCnf = Mf_ManGenerateCnf( p->pFrames, pPars->nLutSize, 1, 0, pPars->fVerbose );
} }
Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 ); Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
// create clauses for constant node // create clauses for constant node
......
src/sat/bmc/bmcChain.c
...@@ -185,10 +185,9 @@ Gia_Man_t * Gia_ManDupPosAndPropagateInit( Gia_Man_t * p ) ...@@ -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 ) 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; sat_solver * pSat;
Aig_Man_t * pAig = Gia_ManToAigSimple( p ); 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) ); Cnf_Dat_t * pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
// save SAT vars for the primary inputs // save SAT vars for the primary inputs
if ( vSatIds ) if ( vSatIds )
......
src/sat/bmc/bmcClp.c
...@@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START ...@@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -651,7 +649,7 @@ Vec_Str_t * Bmc_CollapseOneInt2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int ...@@ -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; int iOut = 0, iLit, iVar, status, n, Count, Start;
// create SAT solver // 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 * pSat[3] = {
(sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0),
(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 ...@@ -841,7 +839,7 @@ Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
{ {
int fVeryVerbose = fVerbose; int fVeryVerbose = fVerbose;
int nVars = Gia_ManCiNum(p); 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 * 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) }; 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; Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL;
...@@ -1173,7 +1171,7 @@ cleanup: ...@@ -1173,7 +1171,7 @@ cleanup:
} }
Vec_Str_t * Bmc_CollapseOne3( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) 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 * pSat0 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
sat_solver * pSat1 = (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); sat_solver * pSat2 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
...@@ -1507,7 +1505,7 @@ cleanup: ...@@ -1507,7 +1505,7 @@ cleanup:
} }
Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) 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); 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 ); Vec_Str_t * vSop = Bmc_CollapseOne_int( pSat, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
sat_solver_delete( pSat ); sat_solver_delete( pSat );
......
src/sat/bmc/bmcEnum.c
...@@ -29,8 +29,6 @@ ABC_NAMESPACE_IMPL_START ...@@ -29,8 +29,6 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -169,7 +167,7 @@ void Gia_ManDeriveOneTest( Gia_Man_t * p ) ...@@ -169,7 +167,7 @@ void Gia_ManDeriveOneTest( Gia_Man_t * p )
Gia_Man_t * pNew; Gia_Man_t * pNew;
Gia_Obj_t * pObj, * pRoot; Gia_Obj_t * pObj, * pRoot;
Vec_Int_t * vValues = Vec_IntStart( Gia_ManCiNum(p) ); 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); int i, iVar, nIter, iPoVarBeg = pCnf->nVars - Gia_ManCiNum(p);
sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
Vec_Int_t * vLits = Vec_IntAlloc( 100 ); Vec_Int_t * vLits = Vec_IntAlloc( 100 );
......
src/sat/bmc/bmcExpand.c
...@@ -33,8 +33,6 @@ ABC_NAMESPACE_IMPL_START ...@@ -33,8 +33,6 @@ ABC_NAMESPACE_IMPL_START
// iterator thought the cubes // iterator thought the cubes
#define Bmc_SopForEachCube( pSop, nVars, pCube ) for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 ) #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 /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -93,7 +91,7 @@ int Abc_ObjExpandCubes( Vec_Str_t * vSop, Gia_Man_t * p, int nVars ) ...@@ -93,7 +91,7 @@ int Abc_ObjExpandCubes( Vec_Str_t * vSop, Gia_Man_t * p, int nVars )
int fReverse = 0; int fReverse = 0;
Vec_Int_t * vVars = Vec_IntAlloc( nVars ); 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); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
int v, n, iLit, status, nCubesNew, iCiVarBeg = sat_solver_nvars(pSat) - nVars; int v, n, iLit, status, nCubesNew, iCiVarBeg = sat_solver_nvars(pSat) - nVars;
......
src/sat/bmc/bmcFault.c
...@@ -280,7 +280,7 @@ static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p ) ...@@ -280,7 +280,7 @@ static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
Aig_ManStop( pAig ); Aig_ManStop( pAig );
return pCnf; return pCnf;
// return Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); // return (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
} }
/**Function************************************************************* /**Function*************************************************************
......
src/sat/bmc/bmcFx.c
...@@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START ...@@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -598,7 +596,7 @@ int Bmc_FxCompute( Gia_Man_t * p ) ...@@ -598,7 +596,7 @@ int Bmc_FxCompute( Gia_Man_t * p )
extern Gia_Man_t * Gia_ManDupOnsetOffset( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOnsetOffset( Gia_Man_t * p );
Gia_Man_t * p2 = Gia_ManDupOnsetOffset( p ); Gia_Man_t * p2 = Gia_ManDupOnsetOffset( p );
// create SAT solver // 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 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
// compute parameters // compute parameters
int nOuts = Gia_ManCoNum(p); int nOuts = Gia_ManCoNum(p);
...@@ -674,7 +672,7 @@ int Bmc_FxComputeOne( Gia_Man_t * p, int nIterMax, int nDiv2Add ) ...@@ -674,7 +672,7 @@ int Bmc_FxComputeOne( Gia_Man_t * p, int nIterMax, int nDiv2Add )
{ {
int Extra = 1000; int Extra = 1000;
// create SAT solver // 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 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
// compute parameters // compute parameters
int nCiVars = Gia_ManCiNum(p); // PI count int nCiVars = Gia_ManCiNum(p); // PI count
......
src/sat/bmc/bmcGen.c
...@@ -29,8 +29,6 @@ ABC_NAMESPACE_IMPL_START ...@@ -29,8 +29,6 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -131,7 +129,7 @@ void Gia_ManMoFindSimulate( Gia_Man_t * p, int nWords ) ...@@ -131,7 +129,7 @@ void Gia_ManMoFindSimulate( Gia_Man_t * p, int nWords )
int Gia_ManTestSatEnum( Gia_Man_t * p ) int Gia_ManTestSatEnum( Gia_Man_t * p )
{ {
abctime clk = Abc_Clock(), clk2, clkTotal = 0; 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); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
int i, v, status, iLit, nWords = 1, iOutVar = 1, Count = 0; int i, v, status, iLit, nWords = 1, iOutVar = 1, Count = 0;
Vec_Int_t * vVars = Vec_IntAlloc( 1000 ); Vec_Int_t * vVars = Vec_IntAlloc( 1000 );
......
src/sat/bmc/bmcICheck.c
...@@ -392,11 +392,10 @@ int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fRev ...@@ -392,11 +392,10 @@ int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fRev
pCnf = Cnf_DeriveGiaRemapped( pMiter ); pCnf = Cnf_DeriveGiaRemapped( pMiter );
else 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 ); //pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
//Gia_ManStop( pTemp ); //Gia_ManStop( pTemp );
//pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL; //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 // collect positive literals
......
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