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

2 files changed, 20 insertions, 3 deletions

diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index beed07bb..129375d2 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -156,6 +156,7 @@ extern void            Cnf_DataFlipLastLiteral( Cnf_Dat_t * p );
 extern void            Cnf_DataPrint( Cnf_Dat_t * p, int fReadable );
 extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
 extern void *          Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
+extern void *          Cnf_DataWriteIntoSolverInt( void * pSat, Cnf_Dat_t * p, int nFrames, int fInit );
 extern int             Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
 extern int             Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf );
 extern void            Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos );
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 85311229..07c52b05 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -334,12 +334,12 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
   SeeAlso     []
 
 ***********************************************************************/
-void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
+void * Cnf_DataWriteIntoSolverInt( sat_solver * pSat, Cnf_Dat_t * p, int nFrames, int fInit )
 {
-    sat_solver * pSat;
     int i, f, status;
     assert( nFrames > 0 );
-    pSat = sat_solver_new();
+    assert( pSat );
+//    pSat = sat_solver_new();
     sat_solver_setnvars( pSat, p->nVars * nFrames );
     for ( i = 0; i < p->nClauses; i++ )
     {
@@ -426,6 +426,22 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
   SeeAlso     []
 
 ***********************************************************************/
+void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
+{
+    return Cnf_DataWriteIntoSolverInt( sat_solver_new(), p, nFrames, fInit );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes CNF into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit )
 {
     sat_solver2 * pSat;