From 735a831e13684334d55b422993a80d94d356f180 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 22 Jun 2012 10:30:22 -0700 Subject: Added memory reporting to &vta. --- src/sat/bsat/satSolver2.c | 52 ++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 51 insertions(+), 1 deletion(-) (limited to 'src/sat/bsat/satSolver2.c') diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index f014b6fc..2e0a5f4a 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1250,7 +1250,7 @@ void sat_solver2_delete(sat_solver2* s) } // report statistics - Abc_Print(1, "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 1.0 * Vec_SetMemory(&s->Proofs) / (1<<20), s->nUnits ); +// Abc_Print(1, "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 1.0 * Vec_ReportMemory(&s->Proofs) / (1<<20), s->nUnits ); // delete vectors veci_delete(&s->order); @@ -1618,6 +1618,56 @@ void sat_solver2_rollback( sat_solver2* s ) } } +// returns memory in bytes used by the SAT solver +double sat_solver2_memory( sat_solver2* s ) +{ + int i; + double Mem = sizeof(sat_solver2); + 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->clauses.cap * sizeof(int); + Mem += s->learnts.cap * sizeof(int); + Mem += s->claActs.cap * sizeof(int); + Mem += s->claProofs.cap * sizeof(int); +// Mem += s->cap * sizeof(char); // ABC_FREE(s->polarity ); +// Mem += s->cap * sizeof(char); // ABC_FREE(s->tags ); + Mem += s->cap * sizeof(varinfo2); // ABC_FREE(s->vi ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->levels ); + Mem += s->cap * sizeof(char); // ABC_FREE(s->assigns ); +#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(lit); // ABC_FREE(s->trail ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->orderpos ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->reasons ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->units ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->model ); + + Mem += s->tagged.cap * sizeof(int); + Mem += s->stack.cap * sizeof(int); + Mem += s->order.cap * sizeof(int); + Mem += s->trail_lim.cap * sizeof(int); + Mem += s->temp_clause.cap * sizeof(int); + Mem += s->conf_final.cap * sizeof(int); + Mem += s->mark_levels.cap * sizeof(int); + Mem += s->min_lit_order.cap * sizeof(int); + Mem += s->min_step_order.cap * sizeof(int); + Mem += s->learnt_live.cap * sizeof(int); + Mem += s->temp_proof.cap * sizeof(int); +// Mem += Vec_ReportMemory( &s->Mem ); + return Mem; +} +double sat_solver2_memory_proof( sat_solver2* s ) +{ + return Vec_ReportMemory( &s->Proofs ); +} + + // find the clause in the watcher lists int sat_solver2_find_clause( sat_solver2* s, int Hand, int fVerbose ) { -- cgit v1.2.3