3 files changed, 33 insertions, 0 deletions
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
index 6634e68e..2095a650 100644
--- a/src/sat/satoko/satoko.h
+++ b/src/sat/satoko/satoko.h
@@ -92,6 +92,7 @@ extern void satoko_assump_push(satoko_t *s, int);
 extern void satoko_assump_pop(satoko_t *s);
 extern int  satoko_simplify(satoko_t *);
 extern int  satoko_solve(satoko_t *);
+extern int  satoko_solve_with_assumptions(satoko_t *s, int * plits, int nlits);
 extern void satoko_mark_cone(satoko_t *, int *, int);
 extern void satoko_unmark_cone(satoko_t *, int *, int);
 
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h
index cfb7d538..4abf9979 100644
--- a/src/sat/satoko/solver.h
+++ b/src/sat/satoko/solver.h
@@ -222,6 +222,19 @@ static inline int solver_varnum(solver_t *s)
 {
     return vec_char_size(s->assigns);
 }
+static inline int solver_clausenum(solver_t *s)
+{
+    return vec_uint_size(s->originals);
+}
+static inline int solver_learntnum(solver_t *s)
+{
+    return vec_uint_size(s->learnts);
+}
+static inline int solver_conflictnum(solver_t *s)
+{
+    return satoko_stats(s).n_conflicts;
+}
+
 static inline int solver_has_marks(solver_t *s)
 {
     return (int)(s->marks != NULL);
@@ -234,6 +247,10 @@ static inline void solver_set_stop(solver_t *s, int * pstop)
 {
     s->pstop = pstop;
 }
+static inline int solver_read_cex_varvalue(solver_t *s, int ivar)
+{
+    return var_polarity(s, ivar) == LIT_TRUE;
+}
 
 //===------------------------------------------------------------------------===
 // Inline clause functions
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index 62749e88..54987007 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -313,6 +313,21 @@ int satoko_solve(solver_t *s)
     return status;
 }
 
+int satoko_solve_with_assumptions(solver_t *s, int * plits, int nlits)
+{
+    int i, status;
+    for ( i = 0; i < nlits; i++ )
+        satoko_assump_push( s, plits[i] );
+    status = satoko_solve( s );
+    for ( i = 0; i < nlits; i++ )
+        satoko_assump_pop( s );
+    if ( status == SATOKO_UNSAT )
+        return 1;
+    if ( status == SATOKO_SAT )
+        return 0;
+    return -1;
+}
+
 int satoko_final_conflict(solver_t *s, unsigned *out)
 {
     if (vec_uint_size(s->final_conflict) == 0)