Added memory reporting to &vta.

17 files changed, 237 insertions, 32 deletions

diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 6bc5bd4f..d4ff109f 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -983,7 +983,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p->pGia        = pGia;
     p->pPars       = pPars;
     // internal data
-    p->nObjsAlloc  = (1 << 20);
+    p->nObjsAlloc  = (1 << 18);
     p->pObjs       = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc );
     p->nObjs       = 1;
     p->nBins       = Abc_PrimeCudd( 2*p->nObjsAlloc );
@@ -1656,11 +1656,34 @@ finish:
     Abc_PrintTime( 1, "Time", clock() - clk );
 
     p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
-    ABC_PRTP( "Solver UNSAT", p->timeUnsat,  clock() - clk );
-    ABC_PRTP( "Solver SAT  ", p->timeSat,    clock() - clk );
-    ABC_PRTP( "Refinement  ", p->timeCex,    clock() - clk );
-    ABC_PRTP( "Other       ", p->timeOther,  clock() - clk );
-    ABC_PRTP( "TOTAL       ", clock() - clk, clock() - clk );
+    ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat,  clock() - clk );
+    ABC_PRTP( "Runtime: Solver SAT  ", p->timeSat,    clock() - clk );
+    ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    clock() - clk );
+    ABC_PRTP( "Runtime: Other       ", p->timeOther,  clock() - clk );
+    ABC_PRTP( "Runtime: TOTAL       ", clock() - clk, clock() - clk );
+
+    
+    { // memory report
+    double memTot = 0;
+    double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
+    double memSat = sat_solver2_memory( p->pSat );
+    double memPro = sat_solver2_memory_proof( p->pSat );
+    double memMap = p->nObjsAlloc * sizeof(Vta_Obj_t) + p->nBins * sizeof(int);
+    double memOth = sizeof(Vta_Man_t);
+    memOth += Vec_IntCap(p->vOrder) * sizeof(int);
+    memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vFrames );
+    memOth += Vec_BitCap(p->vSeenGla) * sizeof(int);
+    memOth += Vec_IntCap(p->vCla2Var) * sizeof(int);
+    memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCores );
+    memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
+    memTot = memAig + memSat + memPro + memMap + memOth;
+    ABC_PRMP( "Memory: AIG  ", memAig, memTot );
+    ABC_PRMP( "Memory: SAT  ", memSat, memTot );
+    ABC_PRMP( "Memory: Proof", memPro, memTot );
+    ABC_PRMP( "Memory: Map  ", memMap, memTot );
+    ABC_PRMP( "Memory: Other", memOth, memTot );
+    ABC_PRMP( "Memory: TOTAL", memTot, memTot );
+    }
 
     Vga_ManStop( p );
     fflush( stdout );
diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c
index 49142683..cf8ecf00 100644
--- a/src/aig/gia/giaCof.c
+++ b/src/aig/gia/giaCof.c
@@ -682,7 +682,7 @@ void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes )
     Gia_ManHashStart( pGia );
     Cof_ManPrintHighFanout( p, nNodes );
     Gia_ManHashStop( pGia );
-ABC_PRM( "Memory for logic network", 4*p->nObjData );
+ABC_PRMn( "Memory for logic network", 4*p->nObjData );
 ABC_PRT( "Time", clock() - clk );
     Cof_ManStop( p );
 }
diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c
index 0dfee293..fc4d2736 100644
--- a/src/aig/gia/giaGlitch.c
+++ b/src/aig/gia/giaGlitch.c
@@ -772,7 +772,7 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb
     if ( fVerbose )
     {
         printf( "\nSimulated %d patterns.  ", nPatterns );
-        ABC_PRM( "Memory", 4*p->nObjData );
+        ABC_PRMn( "Memory", 4*p->nObjData );
         ABC_PRT( "Time", clock() - clk );
     }
 }
diff --git a/src/aig/gia/giaSat.c b/src/aig/gia/giaSat.c
index cb410dd7..138eedd5 100644
--- a/src/aig/gia/giaSat.c
+++ b/src/aig/gia/giaSat.c
@@ -411,8 +411,8 @@ void Gia_ManSatExperiment( Gia_Man_t * p )
     Gia_ManSatStop( pMan );
     for ( i = 0; i < 2*GIA_LIMIT+2; i++ )
         printf( "%2d=%6d  %7.2f %%  %7.2f %%\n", i, nCount[i], 100.0*nCount[i]/nCountAll, 100.0*i*nCount[i]/Gia_ManAndNum(p) );
-    ABC_PRM( "MemoryEst", 4*nWords );
-    ABC_PRM( "MemoryReal", 4*nWords2 );
+    ABC_PRMn( "MemoryEst", 4*nWords );
+    ABC_PRMn( "MemoryReal", 4*nWords2 );
     printf( "%5.2f bpn  ", 4.0*nWords2/Gia_ManObjNum(p) );
     ABC_PRT( "Time", clock() - clk );
 }
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index a67f84f3..cf19947a 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -1248,11 +1248,11 @@ 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( "%4.0f Mb",      1+(float)sat_solver_memory(p->pSat)/(1<<20) );
+                        printf( "%9.2f sec ",   (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
+                        printf( "%5.0f Mb",      1.0+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 );
+//                        ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
+//                        ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
 //                        printf( "Simples = %6d. ", p->nBufNum );
 //                        printf( "Dups = %6d. ", p->nDupNum );
 //                        printf( "\n" );
@@ -1310,11 +1310,11 @@ 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( "%4.0f Mb",     1+(float)sat_solver_memory(p->pSat)/(1<<20) );
+            printf( "%9.2f sec ",  (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
+            printf( "%5.0f Mb",     1.0+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 );
+//            ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
+//            ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
 //            printf( "Simples = %6d. ", p->nBufNum );
 //            printf( "Dups = %6d. ", p->nDupNum );
 //            printf( "\n" );
@@ -1329,8 +1329,8 @@ clkOther += clock() - clk2;
 //ABC_PRT( "CNF generation runtime", clkOther );
     if ( pPars->fVerbose )
     {
-//    ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 );
-//    ABC_PRM( "SAT", 48 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
+//    ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
+//    ABC_PRMn( "SAT", 48 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
 //    printf( "Simples = %6d. ", p->nBufNum );
 //    printf( "Dups = %6d. ", p->nDupNum );
 //    printf( "\n" );
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index 5f0e1232..9524c505 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -205,12 +205,14 @@ typedef ABC_UINT64_T word;
 
 #define ABC_SWAP(Type, a, b)  { Type t = a; a = b; b = t; }
 
-#define ABC_PRT(a,t)    (Abc_Print(1, "%s = ", (a)), Abc_Print(1, "%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)))
-#define ABC_PRTr(a,t)   (Abc_Print(1, "%s = ", (a)), Abc_Print(1, "%7.2f sec\r", (float)(t)/(float)(CLOCKS_PER_SEC)))
-#define ABC_PRTn(a,t)   (Abc_Print(1, "%s = ", (a)), Abc_Print(1, "%6.2f sec  ", (float)(t)/(float)(CLOCKS_PER_SEC)))
-#define ABC_PRTP(a,t,T) (Abc_Print(1, "%s = ", (a)), Abc_Print(1, "%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0))
-#define ABC_PRM(a,f)    (Abc_Print(1, "%s = ", (a)), Abc_Print(1, "%7.3f Mb  ",    1.0*(f)/(1<<20)))
-#define ABC_PRMP(a,f,F) (Abc_Print(1, "%s = ", (a)), Abc_Print(1, "%7.3f Mb (%6.2f %%)  ",  (1.0*(f)/(1<<20)), ((F)? 100.0*(f)/(F) : 0.0) ) )
+#define ABC_PRT(a,t)    (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%9.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)))
+#define ABC_PRTr(a,t)   (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%9.2f sec\r", (float)(t)/(float)(CLOCKS_PER_SEC)))
+#define ABC_PRTn(a,t)   (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%9.2f sec  ", (float)(t)/(float)(CLOCKS_PER_SEC)))
+#define ABC_PRTP(a,t,T) (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%9.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0))
+#define ABC_PRM(a,f)    (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%10.3f Mb\n",    1.0*(f)/(1<<20)))
+#define ABC_PRMr(a,f)   (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%10.3f Mb\r",    1.0*(f)/(1<<20)))
+#define ABC_PRMn(a,f)   (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%10.3f Mb  ",    1.0*(f)/(1<<20)))
+#define ABC_PRMP(a,f,F) (Abc_Print(1, "%s =", (a)), Abc_Print(1, "%10.3f Mb (%6.2f %%)\n",  (1.0*(f)/(1<<20)), ((F)? 100.0*(f)/(F) : 0.0) ) )
 
 #define ABC_ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
 #define ABC_CALLOC(type, num)    ((type *) calloc((num), sizeof(type)))
diff --git a/src/misc/vec/vecBit.h b/src/misc/vec/vecBit.h
index 7f0d7409..4024d0ee 100644
--- a/src/misc/vec/vecBit.h
+++ b/src/misc/vec/vecBit.h
@@ -252,6 +252,22 @@ static inline int Vec_BitSize( Vec_Bit_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Vec_BitCap( Vec_Bit_t * p )
+{
+    return p->nCap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline int Vec_BitEntry( Vec_Bit_t * p, int i )
 {
     assert( i >= 0 && i < p->nSize );
diff --git a/src/misc/vec/vecFlt.h b/src/misc/vec/vecFlt.h
index 0ad6da27..19423ae0 100644
--- a/src/misc/vec/vecFlt.h
+++ b/src/misc/vec/vecFlt.h
@@ -295,6 +295,22 @@ static inline int Vec_FltSize( Vec_Flt_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Vec_FltCap( Vec_Flt_t * p )
+{
+    return p->nCap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline float Vec_FltEntry( Vec_Flt_t * p, int i )
 {
     assert( i >= 0 && i < p->nSize );
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index afad09d1..1d60ec50 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -298,6 +298,22 @@ static inline int Vec_PtrSize( Vec_Ptr_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Vec_PtrCap( Vec_Ptr_t * p )
+{
+    return p->nCap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline int Vec_PtrCountZero( Vec_Ptr_t * p ) 
 {
     int i, Counter = 0;
diff --git a/src/misc/vec/vecSet.h b/src/misc/vec/vecSet.h
index df2a9a68..72358ea1 100644
--- a/src/misc/vec/vecSet.h
+++ b/src/misc/vec/vecSet.h
@@ -189,9 +189,9 @@ static inline void Vec_SetFree( Vec_Set_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Vec_ReportMemory( Vec_Set_t * p )
+static inline double Vec_ReportMemory( Vec_Set_t * p )
 {
-    int Mem = sizeof(Vec_Set_t);
+    double Mem = sizeof(Vec_Set_t);
     Mem += p->nPagesAlloc * sizeof(void *);
     Mem += sizeof(word) * (1 << p->nPageSize) * (1 + p->iPage);
     return Mem;
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index c794dc2f..cefa0ea9 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -289,6 +289,22 @@ static inline int Vec_StrSize( Vec_Str_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Vec_StrCap( Vec_Str_t * p )
+{
+    return p->nCap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline char Vec_StrEntry( Vec_Str_t * p, int i )
 {
     assert( i >= 0 && i < p->nSize );
diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h
index 8bed4574..6d309dc4 100644
--- a/src/misc/vec/vecVec.h
+++ b/src/misc/vec/vecVec.h
@@ -247,6 +247,22 @@ static inline int Vec_VecSize( Vec_Vec_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Vec_VecCap( Vec_Vec_t * p )
+{
+    return p->nCap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline int Vec_VecLevelSize( Vec_Vec_t * p, int i )
 {
     return Vec_PtrSize( (Vec_Ptr_t *)p->pArray[i] );
@@ -673,6 +689,37 @@ static inline void Vec_VecPrintInt( Vec_Vec_t * p, int fSkipSingles )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns memory, in bytes, used by the vector.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline double Vec_VecMemory( Vec_Vec_t * p )
+{
+    int i;
+    Vec_Ptr_t * vVec;
+    double Mem = sizeof(Vec_Vec_t);
+    Mem += Vec_VecCap(p) * sizeof(void *);
+    Vec_VecForEachLevel( p, vVec, i )
+        Mem += sizeof(Vec_Ptr_t) + Vec_PtrCap(vVec) * sizeof(void *);
+    return Mem;
+}
+static inline double Vec_VecMemoryInt( Vec_Vec_t * p )
+{
+    int i;
+    Vec_Int_t * vVec;
+    double Mem = sizeof(Vec_Vec_t);
+    Mem += Vec_VecCap(p) * sizeof(void *);
+    Vec_VecForEachLevelInt( p, vVec, i )
+        Mem += sizeof(Vec_Int_t) + Vec_IntCap(vVec) * sizeof(int);
+    return Mem;
+}
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h
index 11414ff7..97296401 100644
--- a/src/misc/vec/vecWrd.h
+++ b/src/misc/vec/vecWrd.h
@@ -345,6 +345,22 @@ static inline int Vec_WrdSize( Vec_Wrd_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Vec_WrdCap( Vec_Wrd_t * p )
+{
+    return p->nCap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline word Vec_WrdEntry( Vec_Wrd_t * p, int i )
 {
     assert( i >= 0 && i < p->nSize );
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);