Implementing rollback in the updated solver.

1 files changed, 33 insertions, 1 deletions

diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 99a09081..17a9ba4a 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -160,6 +160,32 @@ void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the number of bytes used for each variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sat_Solver2GetVarMem( sat_solver2 * s )
+{
+    int Mem = 0;
+    Mem += (sizeof(s->activity[0]) == 4) ? sizeof(unsigned) : sizeof(double);  // activity
+    Mem += 2 * sizeof(veci); // wlists
+    Mem += sizeof(int);      // vi (variable info)
+    Mem += sizeof(int);      // trail
+    Mem += sizeof(int);      // orderpos
+    Mem += sizeof(int);      // reasons
+    Mem += sizeof(int);      // units
+    Mem += sizeof(int);      // order
+    Mem += sizeof(int);      // model
+    return Mem;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Writes the given clause in a file in DIMACS format.]
 
   Description []
@@ -177,7 +203,13 @@ 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        : %10d\n", veci_size(&s->clauses) );
+    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),
+        100.0 * (s->clauses.cap - s->clauses.size + 
+                 s->learnts.cap - s->learnts.size) / 
+                (s->clauses.cap + s->learnts.cap) );
 }
 
 /**Function*************************************************************