diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-09 22:16:23 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-09 22:16:23 -0700 |
| commit | 291f1ee054b6a1746d7af208a0d6ff361a0fe71a (patch) | |
| tree | 267ce4a7dd393de7cefca1e83ee64a77d28081e6 | |
| parent | 637736827a770d32778c832802dd8c6ddee73073 (diff) | |
| download | abc-291f1ee054b6a1746d7af208a0d6ff361a0fe71a.tar.gz abc-291f1ee054b6a1746d7af208a0d6ff361a0fe71a.tar.bz2 abc-291f1ee054b6a1746d7af208a0d6ff361a0fe71a.zip | |
Performance bug fix in &gla.
| -rw-r--r-- | src/aig/gia/giaAbsGla.c | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 64ea44b0..017c9407 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -1760,7 +1760,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) Gla_Man_t * p; Vec_Int_t * vCore, * vPPis; Abc_Cex_t * pCex = NULL; - int f, i, iPrev, nConfls, Status, nCoreSize, fOneIsSent = 0, RetValue = -1; + int f, i, iPrev, nConfls, Status, nVarsOld, nCoreSize, fOneIsSent = 0, RetValue = -1; clock_t clk = clock(), clk2; // preconditions assert( Gia_ManPoNum(pAig) == 1 ); @@ -1827,6 +1827,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) sat_solver2_bookmark( p->pSat ); Vec_IntClear( p->vAddedNew ); p->nAbsOld = Vec_IntSize( p->vAbs ); + nVarsOld = p->nSatVars; // iterate as long as there are counter-examples for ( i = 0; ; i++ ) @@ -1904,6 +1905,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) // update storage Gla_ManRollBack( p ); Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses+1 ); + p->nSatVars = nVarsOld; // load this timeframe Gia_GlaAddToAbs( p, vCore, 0 ); Gia_GlaAddOneSlice( p, f, vCore ); |