luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

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

This commit is contained in:
Alan Mishchenko 2012-07-08 14:01:28 -07:00
parent d533f18219
commit ff0ec52d4d
5 changed files with 11 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/aig/gia/giaAbsGla.c
View File

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

6
src/aig/gia/giaAbsVta.c
View File

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

2
src/base/abci/abcDar.c
View File

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

7
src/sat/bsat/satSolver2.c
View File

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

2
src/sat/bsat/satSolver2.h
View File

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