diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-30 11:31:26 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-30 11:31:26 -0700 |
| commit | ed564664f1ab86611cc05245745a22501f8414c2 (patch) | |
| tree | bb9c5d150a72ae5f4112006619debea8ef7f4ab8 /src/aig/gia/giaAbsGla.c | |
| parent | cd39fd6b0585659922908d172b0d058a5cb02dbb (diff) | |
| download | abc-ed564664f1ab86611cc05245745a22501f8414c2.tar.gz abc-ed564664f1ab86611cc05245745a22501f8414c2.tar.bz2 abc-ed564664f1ab86611cc05245745a22501f8414c2.zip | |
Disabling learned clause removal when incremental proof-logging is running (tends to generate smaller abstarctions).
Diffstat (limited to 'src/aig/gia/giaAbsGla.c')
| -rw-r--r-- | src/aig/gia/giaAbsGla.c | 33 |
1 files changed, 18 insertions, 15 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index a76e291e..27f40523 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -74,9 +74,9 @@ struct Gla_Man_t_ unsigned * pObj2Obj; // mapping of GIA obj into GLA obj int nObjs; // the number of objects int nAbsOld; // previous abstraction - int nAbsNew; // previous abstraction - int nLrnOld; // the number of bytes - int nLrnNew; // the number of bytes +// int nAbsNew; // previous abstraction +// int nLrnOld; // the number of bytes +// int nLrnNew; // the number of bytes // other data int nCexes; // the number of counter-examples int nObjAdded; // total number of objects added @@ -1929,16 +1929,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) // load timeframe Gia_GlaAddTimeFrame( p, f ); - // create bookmark to be used for rollback - sat_solver2_bookmark( p->pSat ); - Vec_IntClear( p->vAddedNew ); - p->nAbsOld = Vec_IntSize( p->vAbs ); - nVarsOld = p->nSatVars; - p->nLrnOld = sat_solver2_nlearnts( p->pSat ); - // iterate as long as there are counter-examples - p->nAbsNew = 0; - p->nLrnNew = 0; for ( i = 0; ; i++ ) { clk2 = clock(); @@ -1990,6 +1981,16 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) // start proof logging if ( i == 0 ) { + // create bookmark to be used for rollback + sat_solver2_bookmark( p->pSat ); + Vec_IntClear( p->vAddedNew ); + p->nAbsOld = Vec_IntSize( p->vAbs ); + nVarsOld = p->nSatVars; +// p->nLrnOld = sat_solver2_nlearnts( p->pSat ); +// p->nAbsNew = 0; +// p->nLrnNew = 0; + + // start incremental proof manager assert( p->pSat->pPrf2 == NULL ); p->pSat->pPrf2 = Prf_ManAlloc(); if ( p->pSat->pPrf2 ) @@ -2003,7 +2004,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) { // resize the proof logger if ( p->pSat->pPrf2 ) - Prf_ManGrow( p->pSat->pPrf2, Vec_IntSize(p->vAbs) - p->nAbsOld + Vec_IntSize(vPPis) ); + Prf_ManGrow( p->pSat->pPrf2, p->nProofIds + Vec_IntSize(vPPis) ); } Gia_GlaAddToAbs( p, vPPis, 1 ); @@ -2033,8 +2034,8 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) else { p->pPars->nFramesNoChange = 0; - p->nAbsNew = Vec_IntSize( p->vAbs ) - p->nAbsOld; - p->nLrnNew = Abc_AbsInt( sat_solver2_nlearnts( p->pSat ) - p->nLrnOld ); +// p->nAbsNew = Vec_IntSize( p->vAbs ) - p->nAbsOld; +// p->nLrnNew = Abc_AbsInt( sat_solver2_nlearnts( p->pSat ) - p->nLrnOld ); // update the SAT solver sat_solver2_rollback( p->pSat ); // update storage @@ -2124,6 +2125,8 @@ finish: } else { + if ( p->pPars->fVerbose ) + printf( "\n" ); ABC_FREE( pAig->pCexSeq ); pAig->pCexSeq = pCex; if ( !Gia_ManVerifyCex( pAig, pCex, 0 ) ) |