Version abc70123

1 files changed, 78 insertions, 1 deletions

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 1dd40155..6aafc187 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -477,6 +477,16 @@ static void sat_solver_record(sat_solver* s, veci* cls)
     clause* c     = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
     enqueue(s,*begin,c);
 
+    ///////////////////////////////////
+    // add clause to internal storage
+    if ( s->pStore )
+    {
+        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+        int RetValue = Sto_ManAddClause( s->pStore, begin, end );
+        assert( RetValue );
+    }
+    ///////////////////////////////////
+
     assert(veci_size(cls) > 0);
 
     if (c != 0) {
@@ -1022,6 +1032,7 @@ void sat_solver_delete(sat_solver* s)
         free(s->tags     );
     }
 
+    sat_solver_store_free(s);
     free(s);
 }
 
@@ -1046,6 +1057,7 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
         *j = l;
     }
     sat_solver_setnvars(s,maxvar+1);
+//    sat_solver_setnvars(s, lit_var(*(end-1))+1 );
 
     //printlits(begin,end); printf("\n");
     values = s->assigns;
@@ -1065,7 +1077,18 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
 
     if (j == begin)          // empty clause
         return false;
-    else if (j - begin == 1) // unit clause
+
+    ///////////////////////////////////
+    // add clause to internal storage
+    if ( s->pStore )
+    {
+        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+        int RetValue = Sto_ManAddClause( s->pStore, begin, j );
+        assert( RetValue );
+    }
+    ///////////////////////////////////
+
+    if (j - begin == 1) // unit clause
         return enqueue(s,*begin,(clause*)0);
 
     // create new clause
@@ -1198,6 +1221,15 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin
         printf("==============================================================================\n");
 
     sat_solver_canceluntil(s,0);
+
+    ////////////////////////////////////////////////
+    if ( status == l_Undef && s->pStore )
+    {
+        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+        int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL );
+        assert( RetValue );
+    }
+    ////////////////////////////////////////////////
     return status;
 }
 
@@ -1220,6 +1252,51 @@ int sat_solver_nconflicts(sat_solver* s)
 }
 
 //=================================================================================================
+// Clause storage functions:
+
+void sat_solver_store_alloc( sat_solver * s )
+{
+    extern void * Sto_ManAlloc();
+    assert( s->pStore == NULL );
+    s->pStore = Sto_ManAlloc();
+}
+
+void sat_solver_store_write( sat_solver * s, char * pFileName )
+{
+    extern void Sto_ManDumpClauses( void * p, char * pFileName );
+    Sto_ManDumpClauses( s->pStore, pFileName );
+}
+
+void sat_solver_store_free( sat_solver * s )
+{
+    extern void Sto_ManFree( void * p );
+    if ( s->pStore ) Sto_ManFree( s->pStore );
+    s->pStore = NULL;
+}
+
+void sat_solver_store_mark_roots( sat_solver * s )
+{
+    extern void Sto_ManMarkRoots( void * p );
+    if ( s->pStore ) Sto_ManMarkRoots( s->pStore );
+}
+
+void sat_solver_store_mark_clauses_a( sat_solver * s )
+{
+    extern void Sto_ManMarkClausesA( void * p );
+    if ( s->pStore ) Sto_ManMarkClausesA( s->pStore );
+}
+
+void * sat_solver_store_release( sat_solver * s )
+{
+    void * pTemp;
+    if ( s->pStore == NULL )
+        return NULL;
+    pTemp = s->pStore;
+    s->pStore = NULL;
+    return pTemp;
+}
+
+//=================================================================================================
 // Sorting functions (sigh):
 
 static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))