diff options
| -rw-r--r-- | src/aig/gia/giaAbsGla.c | 4 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 6 | ||||
| -rw-r--r-- | src/base/abci/abcDar.c | 2 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 7 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.h | 2 |
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); |