summaryrefslogtreecommitdiffstats
path: root/src/sat/satoko/solver.h
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-08-13 13:37:36 +0700
committerAlan Mishchenko <alanmi@berkeley.edu>2017-08-13 13:37:36 +0700
commitb39b55e885fd72750ad087abbb6558b0a4dcf2ac (patch)
tree1eba93caaa7ee00ff6a20ec9429ed63627c03481 /src/sat/satoko/solver.h
parentcf427690a5df7decdfb6dd21d076e68415b82f46 (diff)
downloadabc-b39b55e885fd72750ad087abbb6558b0a4dcf2ac.tar.gz
abc-b39b55e885fd72750ad087abbb6558b0a4dcf2ac.tar.bz2
abc-b39b55e885fd72750ad087abbb6558b0a4dcf2ac.zip
Adding a callback feature to Satoko.
Diffstat (limited to 'src/sat/satoko/solver.h')
-rw-r--r--src/sat/satoko/solver.h11
1 files changed, 11 insertions, 0 deletions
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