summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satUtil.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-07-11 12:45:46 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-07-11 12:45:46 -0700
commitb9ee5d8564025acfbeb632cf3c28ecb8d61a7aa4 (patch)
tree9e5e3e6aebf36d28cf3c7726ac7f5f7bcdd8a843 /src/sat/bsat/satUtil.c
parent5f3ba152e5729824f78fd03e3d164de81a452d22 (diff)
downloadabc-b9ee5d8564025acfbeb632cf3c28ecb8d61a7aa4.tar.gz
abc-b9ee5d8564025acfbeb632cf3c28ecb8d61a7aa4.tar.bz2
abc-b9ee5d8564025acfbeb632cf3c28ecb8d61a7aa4.zip
Improvements in the proof-logging SAT solver.
Diffstat (limited to 'src/sat/bsat/satUtil.c')
-rw-r--r--src/sat/bsat/satUtil.c2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 1694ae01..05b9403d 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -211,6 +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",
1.0 * Sat_Solver2GetVarMem(s) * s->size / (1<<20),
100.0 * (s->cap - s->size) / s->cap,
@@ -218,6 +219,7 @@ void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * s )
100.0 * (s->clauses.cap - s->clauses.size +
s->learnts.cap - s->learnts.size) /
(s->clauses.cap + s->learnts.cap) );
+*/
}
/**Function*************************************************************