Added memory reporting to &vta.

4 files changed, 33 insertions, 10 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 );
 }