diff options
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 1 | ||||
| -rw-r--r-- | src/aig/saig/saigGlaPba2.c | 2 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 8 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.h | 8 |
4 files changed, 9 insertions, 10 deletions
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index b373fd27..9c50ae52 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1402,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 ); + p->pSat->fVerbose = p->pPars->fVerbose; sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax ); // set runtime limit if ( p->pPars->nTimeOut ) diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c index 55aa0a3d..4fa0012d 100644 --- a/src/aig/saig/saigGlaPba2.c +++ b/src/aig/saig/saigGlaPba2.c @@ -516,7 +516,7 @@ Vec_Int_t * Aig_Gla3ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in Aig_Gla3ManStop( p ); return NULL; } - sat_solver2_set_random( p->pSat, fSkipRand ); + p->pSat->fNotUseRandom = fSkipRand; p->timePre += clock() - clk; // set runtime limit diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index e603d866..e4d713d1 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1153,7 +1153,8 @@ sat_solver2* sat_solver2_new(void) #endif s->fSkipSimplify = 1; s->fNotUseRandom = 0; - s->nLearntMax = 0; + s->nLearntMax = 0; + s->fVerbose = 0; // prealloc clause assert( !s->clauses.ptr ); @@ -1220,7 +1221,6 @@ void sat_solver2_setnvars(sat_solver2* s,int n) *((int*)s->vi + var) = 0; //s->vi[var].val = varX; s->levels [var] = 0; s->assigns [var] = varX; - s->orderpos[var] = veci_size(&s->order); s->reasons [var] = 0; if ( s->fProofLogging ) s->units [var] = 0; @@ -1232,6 +1232,7 @@ void sat_solver2_setnvars(sat_solver2* s,int n) s->model [var] = 0; // does not hold because variables enqueued at top level will not be reinserted in the heap // assert(veci_size(&s->order) == var); + s->orderpos[var] = veci_size(&s->order); veci_push(&s->order,var); order_update(s, var); } @@ -1420,6 +1421,7 @@ void sat_solver2_reducedb(sat_solver2* s) c->mark = 1; } // report the results + if ( s->fVerbose ) printf( "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ", veci_size(&s->learnt_live), s->stats.learnts, 100.0 * veci_size(&s->learnt_live) / s->stats.learnts ); @@ -1488,6 +1490,7 @@ void sat_solver2_reducedb(sat_solver2* s) Sat_ProofReduce( s ); TimeTotal += clock() - clk; + if ( s->fVerbose ) Abc_PrintTime( 1, "Time", TimeTotal ); } @@ -1548,6 +1551,7 @@ void sat_solver2_rollback( sat_solver2* s ) // reset watcher lists for ( i = 2*s->iVarPivot; i < 2*s->size; i++ ) s->wlists[i].size = 0; + // clean the room for ( i = s->iVarPivot; i < s->size; i++ ) { *((int*)s->vi + i) = 0; diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 4d01427a..4b1eec61 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -106,6 +106,7 @@ struct sat_solver2_t int fNotUseRandom; // do not allow random decisions with a fixed probability int fSkipSimplify; // set to one to skip simplification of the clause database int fProofLogging; // enable proof-logging + int fVerbose; // clauses veci clauses; // clause memory @@ -240,13 +241,6 @@ static inline int sat_solver2_set_runtime_limit(sat_solver2* s, int Limit) return temp; } -static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom) -{ - int temp = s->fNotUseRandom; - s->fNotUseRandom = fNotUseRandom; - return temp; -} - static inline int sat_solver2_set_learntmax(sat_solver2* s, int nLearntMax) { int temp = s->nLearntMax; |