Version abc51005

3 files changed, 22 insertions, 7 deletions

diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c
index d7358749..662fe1ff 100644
--- a/src/sat/asat/added.c
+++ b/src/sat/asat/added.c
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: added.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: added.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
 
 ***********************************************************************/
 
@@ -57,7 +57,7 @@ static void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement )
   SeeAlso     []
 
 ***********************************************************************/
-void Asat_SolverWriteDimacs( solver * p, char * pFileName )
+void Asat_SolverWriteDimacs( solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
 {
     FILE * pFile;
     void ** pClauses;
@@ -78,18 +78,31 @@ void Asat_SolverWriteDimacs( solver * p, char * pFileName )
     nClauses = p->clauses.size;
     pClauses = p->clauses.ptr;
     for ( i = 0; i < nClauses; i++ )
-        Asat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
+        Asat_ClauseWriteDimacs( pFile, pClauses[i], incrementVars );
 
     // write the learned clauses
     nClauses = p->learnts.size;
     pClauses = p->learnts.ptr;
     for ( i = 0; i < nClauses; i++ )
-        Asat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
+        Asat_ClauseWriteDimacs( pFile, pClauses[i], incrementVars );
 
     // write zero-level assertions
     for ( i = 0; i < p->size; i++ )
         if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
-            fprintf( pFile, "%s%d 0\n", (p->assigns[i] == l_False)? "-": "", i + 1 );
+            fprintf( pFile, "%s%d%s\n",
+                     (p->assigns[i] == l_False)? "-": "",
+                     i + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+
+    // write the assumptions
+    if (assumptionsBegin) {
+        for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) {
+            fprintf( pFile, "%s%d%s\n",
+                     lit_sign(*assumptionsBegin)? "-": "",
+                     lit_var(*assumptionsBegin) + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+        }
+    }
 
     fprintf( pFile, "\n" );
     fclose( pFile );
diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c
index d248b115..3927fac3 100644
--- a/src/sat/asat/solver.c
+++ b/src/sat/asat/solver.c
@@ -1099,7 +1099,7 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
         nof_conflicts *= 1.5;
         nof_learnts   *= 1.1;
         // if the runtime limit is exceeded, quit the restart loop
-        if ( clock() - timeStart >= nSeconds * CLOCKS_PER_SEC )
+        if ( (nSeconds >= 0) && (clock() - timeStart >= nSeconds * CLOCKS_PER_SEC) )
             break;
     }
     if (s->verbosity >= 1)
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index 9f80bc7e..b82601c4 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -73,7 +73,9 @@ extern int     solver_nvars(solver* s);
 extern int     solver_nclauses(solver* s);
 
 // additional procedures
-extern void    Asat_SolverWriteDimacs( solver * pSat, char * pFileName );
+extern void    Asat_SolverWriteDimacs( solver * pSat, char * pFileName,
+                                       lit* assumptionsBegin, lit* assumptionsEnd,
+                                       int incrementVars);
 
 struct stats_t
 {