Version abc50908

3 files changed, 33 insertions, 3 deletions

diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c
index d7f5b104..d7358749 100644
--- a/src/sat/asat/added.c
+++ b/src/sat/asat/added.c
@@ -119,6 +119,30 @@ void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement )
     fprintf( pFile, "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns a counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * solver_get_model( solver * p, int * pVars, int nVars )
+{
+    int * pModel;
+    int i;
+    pModel = ALLOC( int, nVars );
+    for ( i = 0; i < nVars; i++ )
+    {
+        assert( pVars[i] >= 0 && pVars[i] < p->size );
+        pModel[i] = (int)(p->model.ptr[pVars[i]] == (void *)l_True);
+    }
+    return pModel;    
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c
index c9dadcb4..98024a7f 100644
--- a/src/sat/asat/solver.c
+++ b/src/sat/asat/solver.c
@@ -22,6 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <stdio.h>
 #include <assert.h>
 #include <math.h>
+#include <time.h>
 
 #include "solver.h"
 
@@ -1055,13 +1056,14 @@ bool   solver_simplify(solver* s)
 }
 
 
-bool   solver_solve(solver* s, lit* begin, lit* end)
+int   solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
 {
     double  nof_conflicts = 100;
     double  nof_learnts   = solver_nclauses(s) / 3;
     lbool   status        = l_Undef;
     lbool*  values        = s->assigns;
     lit*    i;
+    int     timeStart     = clock();
 
     for (i = begin; i < end; i++)
         if ((lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]) == l_False || (assume(s,*i), solver_propagate(s) != 0)){
@@ -1096,12 +1098,15 @@ bool   solver_solve(solver* s, lit* begin, lit* end)
         status = solver_search(s,(int)nof_conflicts, (int)nof_learnts);
         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 )
+            break;
     }
     if (s->verbosity >= 1)
         printf("==============================================================================\n");
 
     solver_canceluntil(s,0);
-    return status != l_False;
+    return status;
 }
 
 
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index e04d5780..f328fad5 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -69,7 +69,8 @@ extern void    solver_delete(solver* s);
 
 extern bool    solver_addclause(solver* s, lit* begin, lit* end);
 extern bool    solver_simplify(solver* s);
-extern bool    solver_solve(solver* s, lit* begin, lit* end);
+extern int     solver_solve(solver* s, lit* begin, lit* end, int nSeconds);
+extern int *   solver_get_model( solver * p, int * pVars, int nVars );
 
 extern int     solver_nvars(solver* s);
 extern int     solver_nclauses(solver* s);