diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-02-12 02:16:36 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-02-12 02:16:36 -0800 |
| commit | d9edb7e549c2d4b77026d2fba71b1883d1ba378b (patch) | |
| tree | 04f1c97d3e322834aa5cfd70f33304b0104f3a24 /src/aig/gia | |
| parent | 862ebb214d2009edf70e54ff795fe97ccd967449 (diff) | |
| download | abc-d9edb7e549c2d4b77026d2fba71b1883d1ba378b.tar.gz abc-d9edb7e549c2d4b77026d2fba71b1883d1ba378b.tar.bz2 abc-d9edb7e549c2d4b77026d2fba71b1883d1ba378b.zip | |
Variable timeframe abstraction.
Diffstat (limited to 'src/aig/gia')
| -rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 21 |
2 files changed, 13 insertions, 9 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 1069f5d2..76f8d3ad 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -205,6 +205,7 @@ struct Gia_ParVta_t_ int nFramesStart; // starting frame int nFramesPast; // overlap frames int nConfLimit; // conflict limit + int nLearntMax; // max number of learned clauses int nTimeOut; // timeout in seconds int nRatioMin; // stop when less than this % of object is abstracted int fUseTermVars; // use terminal variables diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 764f5d30..0c33ed1f 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -145,15 +145,16 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame ); void Gia_VtaSetDefaultParams( Gia_ParVta_t * p ) { memset( p, 0, sizeof(Gia_ParVta_t) ); - p->nFramesMax = 0; // maximum frames - p->nFramesStart = 5; // starting frame - p->nFramesPast = 4; // overlap frames - p->nConfLimit = 0; // conflict limit - p->nTimeOut = 0; // timeout in seconds - p->nRatioMin = 10; // stop when less than this % of object is abstracted - p->fUseTermVars = 1; // use terminal variables - p->fVerbose = 0; // verbose flag - p->iFrame = -1; // the number of frames covered + p->nFramesMax = 0; // maximum frames + p->nFramesStart = 5; // starting frame + p->nFramesPast = 4; // overlap frames + p->nConfLimit = 0; // conflict limit + p->nLearntMax = 10000; // max number of learned clauses + p->nTimeOut = 0; // timeout in seconds + p->nRatioMin = 10; // stop when less than this % of object is abstracted + p->fUseTermVars = 1; // use terminal variables + p->fVerbose = 0; // verbose flag + p->iFrame = -1; // the number of frames covered } /**Function************************************************************* @@ -1401,6 +1402,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax ); // start the manager p = Vga_ManStart( pAig, pPars ); + sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax ); // set runtime limit if ( p->pPars->nTimeOut ) sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 ); @@ -1432,6 +1434,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) { // create bookmark to be used for rollback int nObjOld = p->nObjs; +// sat_solver2_reducedb( p->pSat ); sat_solver2_bookmark( p->pSat ); Vec_IntClear( p->vAddedNew ); // load the time frame |