SAT variable profiling (undo).

3 files changed, 0 insertions, 19 deletions

diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index d0249214..b3a92950 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1636,7 +1636,6 @@ nTimeUndec += clock() - clk2;
             }
             printf( "%4d %s : ", f, fUnfinished ? "-" : "+" );
             printf( "Var =%8.0f. ", (double)p->nSatVars );
-            printf( "Var2 =%8.0f. ", (double)p->pSat->nVarUsed );
             printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
             printf( "Cnf =%7.0f. ",(double)p->pSat->stats.conflicts );
 //            printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
@@ -1658,8 +1657,6 @@ nTimeUndec += clock() - clk2;
 //            printf( "Dups = %6d. ", p->nDupNum );
             printf( "\n" );
             fflush( stdout );
-            memset( p->pSat->pFreqs, 0, sizeof(int) * p->pSat->size );
-            p->pSat->nVarUsed = 0;
         }
     }
     // consider the next timeframe
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 574bcd74..8f3098d8 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -466,10 +466,6 @@ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
 static inline int sat_solver_enqueue(sat_solver* s, lit l, int from)
 {
     int v  = lit_var(l);
-
-    if ( s->pFreqs[v]++ == 0 )
-        s->nVarUsed++;
-
 #ifdef VERBOSEDEBUG
     printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
 #endif
@@ -961,8 +957,6 @@ sat_solver* sat_solver_new(void)
     s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT;  // ratio of learned clause limit
     s->nLearntMax   = s->nLearntStart;
 
-    s->pFreqs  = ABC_CALLOC( int, 10000000 );
-
     // initialize vectors
     veci_new(&s->order);
     veci_new(&s->trail_lim);
@@ -1083,14 +1077,6 @@ void sat_solver_setnvars(sat_solver* s,int n)
 
 void sat_solver_delete(sat_solver* s)
 {
-    int i, nVars = 0;
-    // count non-zero entries
-    for ( i = 0; i < s->size; i++ )
-        nVars += (s->pFreqs[i] > 0);
-    printf( "Assigned = %d.  Total = %d.  (%6.2f %%)\n", nVars, s->size, 100.0 * nVars/s->size );
-    ABC_FREE( s->pFreqs );
-
-
 //    Vec_SetFree_( &s->Mem );
     Sat_MemFree_( &s->Mem );
 
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 8543b3fa..acaceef9 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -121,8 +121,6 @@ struct sat_solver_t
     unsigned*   activity;      // A heuristic measurement of the activity of a variable.
     unsigned*   activity2;     // backup variable activity
 #endif
-    int *       pFreqs;
-    int         nVarUsed;
 
 //    varinfo *   vi;            // variable information
     int*        levels;        //