luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Changing default CNF generation in &bmc.

This commit is contained in:
Alan Mishchenko 2014-08-18 20:19:32 -07:00
parent 7c8136c82d
commit 65f9b73505
3 changed files with 9 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/aig/gia/giaUtil.c
View File

@ -1360,6 +1360,8 @@ void Gia_ManPrintCo_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
Gia_ManPrintCo_rec( p, Gia_ObjFanin0(pObj) );
Gia_ManPrintCo_rec( p, Gia_ObjFanin1(pObj) );
if ( Gia_ObjIsMux(p, pObj) )
Gia_ManPrintCo_rec( p, Gia_ObjFanin2(p, pObj) );
}
Gia_ObjPrint( p, pObj );
}
@ -1378,6 +1380,8 @@ void Gia_ManPrintCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNode
assert( Gia_ObjIsAnd(pObj) );
Gia_ManPrintCollect_rec( p, Gia_ObjFanin0(pObj), vNodes );
Gia_ManPrintCollect_rec( p, Gia_ObjFanin1(pObj), vNodes );
if ( Gia_ObjIsMux(p, pObj) )
Gia_ManPrintCollect_rec( p, Gia_ObjFanin2(p, pObj), vNodes );
Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
}
void Gia_ManPrintCone( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLeaves, int nLeaves, Vec_Int_t * vNodes )
@ -1400,6 +1404,8 @@ void Gia_ManPrintCollect2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNod
Gia_ManPrintCollect2_rec( p, Gia_ObjFanin0(pObj), vNodes );
if ( Gia_ObjIsAnd(pObj) )
Gia_ManPrintCollect2_rec( p, Gia_ObjFanin1(pObj), vNodes );
if ( Gia_ObjIsMux(p, pObj) )
Gia_ManPrintCollect2_rec( p, Gia_ObjFanin2(p, pObj), vNodes );
Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
}
void Gia_ManPrintCone2( Gia_Man_t * p, Gia_Obj_t * pObj )

2
src/base/abci/abc.c
View File

@ -34071,7 +34071,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fLoadCnf = 0; // dynamic CNF loading
pPars->fDumpFrames = 0; // dump unrolled timeframes
pPars->fUseSynth = 0; // use synthesis
pPars->fUseOldCnf = 0; // use old CNF construction
pPars->fUseOldCnf = 1; // use old CNF construction
pPars->fVerbose = 0; // verbose
pPars->fVeryVerbose = 0; // very verbose
pPars->fNotVerbose = 0; // skip line-by-line print-out

2
src/sat/bmc/bmcBmcAnd.c
View File

@ -985,6 +985,8 @@ 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, 6, 1, 0, 0 );
}
Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
// create clauses for constant node