Implemented rollback in the main SAT solver and updated PDR to use it (saves about 5% of runtime).

1 files changed, 27 insertions, 0 deletions

diff --git a/src/sat/bsat/satMem.c b/src/sat/bsat/satMem.c
index 30861993..e947cbf0 100644
--- a/src/sat/bsat/satMem.c
+++ b/src/sat/bsat/satMem.c
@@ -239,6 +239,9 @@ void Sat_MmFixedRestart( Sat_MmFixed_t * p )
 {
     int i;
     char * pTemp;
+    if ( p->nChunks == 0 )
+        return;
+    assert( p->nChunks > 0 );
 
     // deallocate all chunks except the first one
     for ( i = 1; i < p->nChunks; i++ )
@@ -482,6 +485,30 @@ void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose )
 
 /**Function*************************************************************
 
+  Synopsis    [Stops the memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_MmStepRestart( Sat_MmStep_t * p )
+{
+    int i;
+    if ( p->nChunksAlloc )
+    {
+        for ( i = 0; i < p->nChunks; i++ )
+            ABC_FREE( p->pChunks[i] );
+        p->nChunks = 0;
+    }
+    for ( i = 0; i < p->nMems; i++ )
+        Sat_MmFixedRestart( p->pMems[i] );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates the entry.]
 
   Description []