diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-09 22:57:03 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-09 22:57:03 -0700 |
commit | 908d5e696c7e73f80abcef85ec796511f3bffb0f (patch) | |
tree | 6fb41dd27d8ae48d93f71cda4ed56526092c5302 /src/sat | |
parent | d46c49088d7b9f1725d4d8624717f7209022c632 (diff) | |
download | abc-908d5e696c7e73f80abcef85ec796511f3bffb0f.tar.gz abc-908d5e696c7e73f80abcef85ec796511f3bffb0f.tar.bz2 abc-908d5e696c7e73f80abcef85ec796511f3bffb0f.zip |
Replacing Mb/Gb to be MB/GB.
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/bsat/satInter.c | 2 | ||||
-rw-r--r-- | src/sat/bsat/satInterA.c | 2 | ||||
-rw-r--r-- | src/sat/bsat/satInterB.c | 2 | ||||
-rw-r--r-- | src/sat/bsat/satInterP.c | 2 | ||||
-rw-r--r-- | src/sat/bsat/satProof.c | 6 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 2 | ||||
-rw-r--r-- | src/sat/bsat/satUtil.c | 2 | ||||
-rw-r--r-- | src/sat/bsat/satVec.h | 2 | ||||
-rw-r--r-- | src/sat/proof/pr.c | 2 |
9 files changed, 11 insertions, 11 deletions
diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c index 6f564225..6bd07fb7 100644 --- a/src/sat/bsat/satInter.c +++ b/src/sat/bsat/satInter.c @@ -1057,7 +1057,7 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned if ( fVerbose ) { - printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", + printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n", p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c index 39385026..a4a06439 100644 --- a/src/sat/bsat/satInterA.c +++ b/src/sat/bsat/satInterA.c @@ -1009,7 +1009,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in if ( fVerbose ) { // ABC_PRT( "Interpo", clock() - clkTotal ); - printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", + printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n", p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); diff --git a/src/sat/bsat/satInterB.c b/src/sat/bsat/satInterB.c index 3f7cbf4c..07edf7a8 100644 --- a/src/sat/bsat/satInterB.c +++ b/src/sat/bsat/satInterB.c @@ -1045,7 +1045,7 @@ void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in if ( fVerbose ) { // ABC_PRT( "Interpo", clock() - clkTotal ); - printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", + printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n", p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); diff --git a/src/sat/bsat/satInterP.c b/src/sat/bsat/satInterP.c index ebcdc82f..404d5503 100644 --- a/src/sat/bsat/satInterP.c +++ b/src/sat/bsat/satInterP.c @@ -1022,7 +1022,7 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose ) if ( fVerbose ) { ABC_PRT( "Core", clock() - clkTotal ); - printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", + printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n", p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index ca8f3716..eaadf71d 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -354,7 +354,7 @@ void Sat_ProofReduce2( sat_solver2 * s ) if ( fVerbose ) { printf( "\n" ); - printf( "The proof was reduced from %6.2f Mb to %6.2f Mb (by %6.2f %%) ", + printf( "The proof was reduced from %6.2f MB to %6.2f MB (by %6.2f %%) ", 1.0 * Vec_SetMemory(vProof) / (1<<20), 1.0 * Vec_SetMemoryS(vProof) / (1<<20), 100.0 * (Vec_SetMemory(vProof) - Vec_SetMemoryS(vProof)) / Vec_SetMemory(vProof) ); TimeTotal += clock() - clk; @@ -423,7 +423,7 @@ void Sat_ProofReduce( sat_solver2 * s ) if ( fVerbose ) { printf( "\n" ); - printf( "The proof was reduced from %6.2f Mb to %6.2f Mb (by %6.2f %%) ", + printf( "The proof was reduced from %6.2f MB to %6.2f MB (by %6.2f %%) ", 1.0 * Vec_SetMemory(vProof) / (1<<20), 1.0 * Vec_SetMemoryS(vProof) / (1<<20), 100.0 * (Vec_SetMemory(vProof) - Vec_SetMemoryS(vProof)) / Vec_SetMemory(vProof) ); TimeTotal += clock() - clk; @@ -555,7 +555,7 @@ void Sat_ProofCheck( sat_solver2 * s ) // clean the proof Proof_CleanCollected( vProof, vUsed ); // compare the final clause - printf( "Used %6.2f Mb for resolvents.\n", 1.0 * Vec_SetMemory(vResolves) / (1<<20) ); + printf( "Used %6.2f MB for resolvents.\n", 1.0 * Vec_SetMemory(vResolves) / (1<<20) ); if ( pSet0->nEnts > 0 ) printf( "Derived clause with %d lits instead of the empty clause. ", pSet0->nEnts ); else diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index af03c70d..0e456f46 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1251,7 +1251,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_ReportMemory(&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); diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index 67f45b16..1694ae01 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -211,7 +211,7 @@ void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * s ) printf( "propagations : %10d\n", (int)s->stats.propagations ); // printf( "inspects : %10d\n", (int)s->stats.inspects ); // printf( "inspects2 : %10d\n", (int)s->stats.inspects2 ); - printf( "memory for variables %.1f Mb (free %6.2f %%) and clauses %.1f Mb (free %6.2f %%)\n", + printf( "memory for variables %.1f MB (free %6.2f %%) and clauses %.1f MB (free %6.2f %%)\n", 1.0 * Sat_Solver2GetVarMem(s) * s->size / (1<<20), 100.0 * (s->cap - s->size) / s->cap, 4.0 * (s->clauses.cap + s->learnts.cap) / (1<<20), diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h index 35cd3cb4..8a711007 100644 --- a/src/sat/bsat/satVec.h +++ b/src/sat/bsat/satVec.h @@ -58,7 +58,7 @@ static inline void veci_push (veci* v, int e) v->ptr = ABC_REALLOC( int, v->ptr, newsize ); if ( v->ptr == NULL ) { - printf( "Failed to realloc memory from %.1f Mb to %.1f Mb.\n", + printf( "Failed to realloc memory from %.1f MB to %.1f MB.\n", 1.0 * v->cap / (1<<20), 1.0 * newsize / (1<<20) ); fflush( stdout ); } diff --git a/src/sat/proof/pr.c b/src/sat/proof/pr.c index 7fbe3803..2727997a 100644 --- a/src/sat/proof/pr.c +++ b/src/sat/proof/pr.c @@ -1244,7 +1244,7 @@ p->timeRead = clock() - clk; 1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots), nUsed, 1.0*nUsed/(p->nClauses-p->nRoots) ); */ - printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", + printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n", p->nVars, p->nRoots, p->nClauses-p->nRoots, p->Counter, 1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots), 1.0*Pr_ManMemoryReport(p)/(1<<20) ); |