summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bsat/satInter.c2
-rw-r--r--src/sat/bsat/satInterA.c2
-rw-r--r--src/sat/bsat/satInterB.c2
-rw-r--r--src/sat/bsat/satInterP.c2
-rw-r--r--src/sat/bsat/satProof.c6
-rw-r--r--src/sat/bsat/satSolver2.c2
-rw-r--r--src/sat/bsat/satUtil.c2
-rw-r--r--src/sat/bsat/satVec.h2
-rw-r--r--src/sat/proof/pr.c2
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) );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 20:05:22 +0000