diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-18 00:34:37 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-18 00:34:37 -0700 |
commit | 66ff650f4865adff5aa41fd6c5675a4fe929b482 (patch) | |
tree | 8528190251f1c1ec67f1f338ac3a4211a248e1a2 /src | |
parent | 84b3b9144754b738b163cee4d4c99e7b7206ddd1 (diff) | |
download | abc-66ff650f4865adff5aa41fd6c5675a4fe929b482.tar.gz abc-66ff650f4865adff5aa41fd6c5675a4fe929b482.tar.bz2 abc-66ff650f4865adff5aa41fd6c5675a4fe929b482.zip |
SAT variable profiling.
Diffstat (limited to 'src')
-rw-r--r-- | src/sat/bmc/bmcBmc3.c | 3 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.c | 14 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 2 |
3 files changed, 19 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index b3a92950..d0249214 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1636,6 +1636,7 @@ 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 ); @@ -1657,6 +1658,8 @@ 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 8f3098d8..574bcd74 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -466,6 +466,10 @@ 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 @@ -957,6 +961,8 @@ 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); @@ -1077,6 +1083,14 @@ 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 acaceef9..8543b3fa 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -121,6 +121,8 @@ 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; // |