Variable timeframe abstraction.

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;