Added memory reporting to &vta.

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);