diff options
| -rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 24 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 2 |
3 files changed, 19 insertions, 8 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index a784ab92..3a0fb150 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -203,6 +203,7 @@ struct Gia_ParVta_t_ { int nFramesStart; // starting frame int nFramesMax; // maximum frames + int nFramesOver; // overlap frames int nConfLimit; // conflict limit int nTimeOut; // timeout in seconds int fUseTermVars; // use terminal variables diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 52101dc0..6f87f348 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -129,12 +129,14 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame ); ***********************************************************************/ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p ) { + int size = sizeof(Gia_ParVta_t); memset( p, 0, sizeof(Gia_ParVta_t) ); - p->nFramesStart = 10; - p->nFramesMax = 0; - p->nConfLimit = 0; - p->nTimeOut = 60; - p->fVerbose = 1; + p->nFramesStart = 10; // the number of starting frames + p->nFramesMax = 0; // the max number of frames +// p->nFramesOver = 4; // the number of overlapping frames + p->nConfLimit = 0; // conflict limit + p->nTimeOut = 60; // timeout in seconds + p->fVerbose = 1; // verbosity flag } /**Function************************************************************* @@ -601,7 +603,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) pThis->Prio = 0; // set highest priority continue; } - // collect useful terminals + // collect terminals assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) ); if ( !pThis->fAdded ) { @@ -683,6 +685,8 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) assert( pThis0 ); pThis->Prio = pThis0->Prio; } + else + pThis->Prio = 0; } } @@ -764,13 +768,19 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) // verify Vta_ManForEachObjVec( p->vOrder, p, pThis, i ) - pThis->Value = VTA_VARX; + if ( !pThis->fAdded ) + pThis->Value = VTA_VARX; Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i ) + { + assert( !pThis->fAdded ); pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0; + } // simulate Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i ) { assert( pThis->fVisit == 0 ); + if ( !pThis->fAdded ) + continue; if ( Gia_ObjIsAnd(pObj) ) { pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5fc9bfad..5d8d06f5 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -26404,7 +26404,7 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Gia_ParVta_t Pars, * pPars = &Pars; + Gia_ParVta_t Pars, Pars2, * pPars = &Pars; int c; Gia_VtaSetDefaultParams( pPars ); Extra_UtilGetoptReset(); |