diff options
-rw-r--r-- | src/aig/saig/saigBmc3.c | 14 | ||||
-rw-r--r-- | src/misc/vec/vecSet.h | 19 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.c | 35 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 1 |
4 files changed, 63 insertions, 6 deletions
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index fb19783a..a67f84f3 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1242,13 +1242,14 @@ clkOther += clock() - clk2; //ABC_PRT( "CNF generation runtime", clkOther ); if ( pPars->fVerbose ) { - printf( "%3d %s : ", f, fUnfinished ? "-" : "+" ); - printf( "Var =%8.0f. ", (double)p->nSatVars ); - printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses ); - printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts ); + printf( "%3d %s : ", f, fUnfinished ? "-" : "+" ); + printf( "Var =%8.0f. ", (double)p->nSatVars ); + printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses ); + printf( "Conf =%7.0f. ", (double)p->pSat->stats.conflicts ); printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); // ABC_PRT( "Time", clock() - clk ); - printf( "%9.2f sec", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); + printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); + printf( "%4.0f Mb", 1+(float)sat_solver_memory(p->pSat)/(1<<20) ); printf( "\n" ); // ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 ); // ABC_PRM( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); @@ -1309,7 +1310,8 @@ clkOther += clock() - clk2; printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts ); printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); // ABC_PRT( "Time", clock() - clk ); - printf( "%9.2f sec", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); + printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); + printf( "%4.0f Mb", 1+(float)sat_solver_memory(p->pSat)/(1<<20) ); printf( "\n" ); // ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 ); // ABC_PRM( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); diff --git a/src/misc/vec/vecSet.h b/src/misc/vec/vecSet.h index 5f8df449..df2a9a68 100644 --- a/src/misc/vec/vecSet.h +++ b/src/misc/vec/vecSet.h @@ -180,6 +180,25 @@ static inline void Vec_SetFree( Vec_Set_t * p ) /**Function************************************************************* + Synopsis [Returns memory in bytes occupied by the vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_ReportMemory( Vec_Set_t * p ) +{ + int Mem = sizeof(Vec_Set_t); + Mem += p->nPagesAlloc * sizeof(void *); + Mem += sizeof(word) * (1 << p->nPageSize) * (1 + p->iPage); + return Mem; +} + +/**Function************************************************************* + Synopsis [Appending entries to vector.] Description [] diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index cc5156d5..c48d277e 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1117,6 +1117,41 @@ void sat_solver_rollback( sat_solver* s ) s->stats.tot_literals = 0; } +// returns memory in bytes used by the SAT solver +int sat_solver_memory( sat_solver* s ) +{ + int i, Mem = sizeof(sat_solver); + for (i = 0; i < s->cap*2; i++) + Mem += s->wlists[i].cap * sizeof(int); + Mem += s->cap * sizeof(veci); // ABC_FREE(s->wlists ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->levels ); + Mem += s->cap * sizeof(char); // ABC_FREE(s->assigns ); + Mem += s->cap * sizeof(char); // ABC_FREE(s->polarity ); + Mem += s->cap * sizeof(char); // ABC_FREE(s->tags ); +#ifdef USE_FLOAT_ACTIVITY + Mem += s->cap * sizeof(double); // ABC_FREE(s->activity ); +#else + Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity ); +#endif + if ( s->factors ) + Mem += s->cap * sizeof(double); // ABC_FREE(s->factors ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->orderpos ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->reasons ); + Mem += s->cap * sizeof(lit); // ABC_FREE(s->trail ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->model ); + + Mem += s->order.cap * sizeof(int); + Mem += s->trail_lim.cap * sizeof(int); + Mem += s->tagged.cap * sizeof(int); + Mem += s->stack.cap * sizeof(int); + Mem += s->act_vars.cap * sizeof(int); + Mem += s->temp_clause.cap * sizeof(int); + Mem += s->conf_final.cap * sizeof(int); + Mem += Vec_ReportMemory( &s->Mem ); + return Mem; +} + + /* static void clause_remove(sat_solver* s, clause* c) { diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 25b756ef..42473a6e 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -52,6 +52,7 @@ extern void sat_solver_rollback( sat_solver* s ); extern int sat_solver_nvars(sat_solver* s); extern int sat_solver_nclauses(sat_solver* s); extern int sat_solver_nconflicts(sat_solver* s); +extern int sat_solver_memory(sat_solver* s); extern void sat_solver_setnvars(sat_solver* s,int n); extern int sat_solver_get_var_value(sat_solver* s, int v); |