diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-18 00:33:18 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-18 00:33:18 -0700 |
| commit | 84b3b9144754b738b163cee4d4c99e7b7206ddd1 (patch) | |
| tree | 2b0f949b93ea8e204123000efb498dfb23becbb0 /src/sat/bsat | |
| parent | 86e38c2a361cea9edbbabe25a821075d2d02cd8e (diff) | |
| download | abc-84b3b9144754b738b163cee4d4c99e7b7206ddd1.tar.gz abc-84b3b9144754b738b163cee4d4c99e7b7206ddd1.tar.bz2 abc-84b3b9144754b738b163cee4d4c99e7b7206ddd1.zip | |
SAT variable profiling (undo).
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satSolver.c | 14 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.h | 2 |
2 files changed, 0 insertions, 16 deletions
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; // |