diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-06-22 10:30:22 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-06-22 10:30:22 -0700 |
commit | 735a831e13684334d55b422993a80d94d356f180 (patch) | |
tree | 0bf12906593cf6f6010c107cb9cb8f57fb335b79 /src/sat | |
parent | 072c264f761268838e2613d0e6735d1a721e0ae9 (diff) | |
download | abc-735a831e13684334d55b422993a80d94d356f180.tar.gz abc-735a831e13684334d55b422993a80d94d356f180.tar.bz2 abc-735a831e13684334d55b422993a80d94d356f180.zip |
Added memory reporting to &vta.
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/bsat/satSolver.c | 5 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 2 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 52 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.h | 2 |
4 files changed, 57 insertions, 4 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index c48d277e..2d41e2fe 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1118,9 +1118,10 @@ void sat_solver_rollback( sat_solver* s ) } // returns memory in bytes used by the SAT solver -int sat_solver_memory( sat_solver* s ) +double sat_solver_memory( sat_solver* s ) { - int i, Mem = sizeof(sat_solver); + int i; + double 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 ); diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 42473a6e..40f637ee 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -52,7 +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 double 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); 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 ) { diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 07a03c9f..79eb64ed 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -49,6 +49,8 @@ extern int sat_solver2_simplify(sat_solver2* s); extern int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); extern void sat_solver2_rollback(sat_solver2* s); extern void sat_solver2_reducedb(sat_solver2* s); +extern double sat_solver2_memory( sat_solver2* s ); +extern double sat_solver2_memory_proof( sat_solver2* s ); extern void sat_solver2_setnvars(sat_solver2* s,int n); |