From b39b55e885fd72750ad087abbb6558b0a4dcf2ac Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 13 Aug 2017 13:37:36 +0700
Subject: Adding a callback feature to Satoko.

---
 src/sat/satoko/solver.c     |  2 +-
 src/sat/satoko/solver.h     | 11 +++++++++++
 src/sat/satoko/solver_api.c |  2 +-
 3 files changed, 13 insertions(+), 2 deletions(-)

(limited to 'src/sat/satoko')

diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index a72e39f7..f7cfb011 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -639,7 +639,7 @@ char solver_search(solver_t *s)
             /* No conflict */
             unsigned next_lit;
 
-            if (solver_rst(s) || solver_check_limits(s) == 0) {
+            if (solver_rst(s) || solver_check_limits(s) == 0 || solver_stop(s)) {
                 b_queue_clean(s->bq_lbd);
                 solver_cancel_until(s, 0);
                 return SATOKO_UNDEC;
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h
index 94035d6e..26de91ad 100644
--- a/src/sat/satoko/solver.h
+++ b/src/sat/satoko/solver.h
@@ -102,6 +102,9 @@ struct solver_t_ {
 
     /* Temporary data used for solving cones */
     vec_char_t *marks;
+    
+    /* Callback to stop the solver */
+    int * pstop;
 
     struct satoko_stats stats;
     struct satoko_opts opts;
@@ -223,6 +226,14 @@ static inline int solver_has_marks(solver_t *s)
 {
     return (int)(s->marks != NULL);
 }
+static inline int solver_stop(solver_t *s)
+{
+    return s->pstop && *s->pstop;
+}
+static inline void solver_set_stop(solver_t *s, int * pstop)
+{
+    s->pstop = pstop;
+}
 
 //===------------------------------------------------------------------------===
 // Inline clause functions
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index dfd996ca..f30ee12d 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -303,7 +303,7 @@ int satoko_solve(solver_t *s)
 
     while (status == SATOKO_UNDEC) {
         status = solver_search(s);
-        if (solver_check_limits(s) == 0)
+        if (solver_check_limits(s) == 0 || solver_stop(s))
             break;
     }
     if (s->opts.verbose)
-- 
cgit v1.2.3