diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-27 22:55:23 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-27 22:55:23 -0700 |
commit | e3f9ad3c9747bd9ad50406186828fefa59af4677 (patch) | |
tree | 3e530d5d04063d9cbdef72b4f5c1f0349dd98907 /src/sat/bmc/bmcBmcAnd.c | |
parent | d65d8528b6aadbedc148fe97dd44eb9e7f71500a (diff) | |
download | abc-e3f9ad3c9747bd9ad50406186828fefa59af4677.tar.gz abc-e3f9ad3c9747bd9ad50406186828fefa59af4677.tar.bz2 abc-e3f9ad3c9747bd9ad50406186828fefa59af4677.zip |
New BMC engine.
Diffstat (limited to 'src/sat/bmc/bmcBmcAnd.c')
-rw-r--r-- | src/sat/bmc/bmcBmcAnd.c | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c index 649453ee..d69c05ae 100644 --- a/src/sat/bmc/bmcBmcAnd.c +++ b/src/sat/bmc/bmcBmcAnd.c @@ -868,14 +868,14 @@ int Gia_ManBmcPerform_old_cnf( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) void Gia_ManBmcAddCnfNew_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj ) { int iObj = Gia_ObjId( p->pFrames, pObj ); - if ( Vec_IntEntry(p->vId2Var, iObj) > 0 ) - return; if ( Gia_ObjIsAnd(pObj) && p->pCnf->pObj2Count[iObj] == -1 ) { Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin0(pObj) ); Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin1(pObj) ); return; } + if ( Vec_IntEntry(p->vId2Var, iObj) > 0 ) + return; Vec_IntWriteEntry(p->vId2Var, iObj, p->nSatVars++); if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsPo(p->pFrames, pObj) ) { @@ -960,6 +960,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) int nFramesMax, f, i=0, Lit = 1, status, RetValue = -2; abctime clk = Abc_Clock(); p = Bmc_MnaAlloc(); + sat_solver_set_runtime_limit( p->pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap ); nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia); if ( pPars->fVerbose ) |