Updating memory print-out of &vta and &gla.

5 files changed, 11 insertions, 10 deletions

diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 9576ea38..7a509f7f 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -1633,7 +1633,7 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl
     Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); 
     Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 ); 
     Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
-    Abc_Print( 1, "%5.1f Gb", sat_solver2_memory_proof( p->pSat ) / (1<<30) );
+    Abc_Print( 1, "%5.1f Gb", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
     Abc_Print( 1, "%s", nCoreSize > 0 ? "\n" : "\r" );
     fflush( stdout );
 }
@@ -1643,7 +1643,7 @@ void Gla_ManReportMemory( Gla_Man_t * p )
     int i;
     double memTot = 0;
     double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
-    double memSat = sat_solver2_memory( p->pSat );
+    double memSat = sat_solver2_memory( p->pSat, 1 );
     double memPro = sat_solver2_memory_proof( p->pSat );
     double memMap = p->nObjs * sizeof(Gla_Obj_t) + Gia_ManObjNum(p->pGia) * sizeof(int);
     double memRef = Gia_ManObjNum(p->pGia) * sizeof(Vec_Int_t);
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 50692670..2fdf484c 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1247,7 +1247,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
         for ( k = 0; k < 7; k++ )
             Abc_Print( 1, "     " );
         Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
-        Abc_Print( 1, "%5.1f Gb", sat_solver2_memory_proof( p->pSat ) / (1<<30) );
+        Abc_Print( 1, "%5.1f Gb", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
         Abc_Print( 1, "\r" );
     }
     else
@@ -1269,7 +1269,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
                 Abc_Print( 1, "     " );
         }
         Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
-        Abc_Print( 1, "%5.1f Gb", sat_solver2_memory_proof( p->pSat ) / (1<<30) );
+        Abc_Print( 1, "%5.1f Gb", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
         Abc_Print( 1, "\n" );
     }
     fflush( stdout );
@@ -1511,7 +1511,7 @@ void Gia_VtaPrintMemory( Vta_Man_t * p )
 {
     double memTot = 0;
     double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
-    double memSat = sat_solver2_memory( p->pSat );
+    double memSat = sat_solver2_memory( p->pSat, 1 );
     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);
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 4fd80eef..75df783f 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -3203,7 +3203,7 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize,
 {
     Aig_Man_t * pMan;
     int status, RetValue = -1;
-    clock_t clk = clock();
+//    clock_t clk = clock();
     if ( Abc_NtkGetChoiceNum(pNtk) )
     {
         Abc_Print( 1, "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 573c1d35..c6eedeb5 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1621,12 +1621,13 @@ void sat_solver2_rollback( sat_solver2* s )
 }
 
 // returns memory in bytes used by the SAT solver
-double sat_solver2_memory( sat_solver2* s )
+double sat_solver2_memory( sat_solver2* s, int fAll )
 {
     int i;
     double Mem = sizeof(sat_solver2);
-    for (i = 0; i < s->cap*2; i++)
-        Mem += s->wlists[i].cap * sizeof(int);
+    if ( fAll )
+        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);
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index d1179422..5f847f68 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -49,7 +49,7 @@ 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( sat_solver2* s, int fAll );
 extern double       sat_solver2_memory_proof( sat_solver2* s );
 
 extern void         sat_solver2_setnvars(sat_solver2* s,int n);