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 | |
| parent | d65d8528b6aadbedc148fe97dd44eb9e7f71500a (diff) | |
| download | abc-e3f9ad3c9747bd9ad50406186828fefa59af4677.tar.gz abc-e3f9ad3c9747bd9ad50406186828fefa59af4677.tar.bz2 abc-e3f9ad3c9747bd9ad50406186828fefa59af4677.zip | |
New BMC engine.
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bmc/bmc.h | 1 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBmcAnd.c | 5 |
2 files changed, 4 insertions, 2 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index ef401e70..27e7d563 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -81,6 +81,7 @@ struct Bmc_AndPar_t_ int nFramesMax; // maximum number of timeframes int nFramesAdd; // the number of additional frames int nConfLimit; // maximum number of conflicts at a node + int nTimeOut; // timeout in seconds int fLoadCnf; // dynamic CNF loading int fDumpFrames; // dump unrolled timeframes int fUseSynth; // use synthesis 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 ) |