Reporing memory usage by the SAT solver in 'bmc3'.

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

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 []

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

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