1 files changed, 17 insertions, 0 deletions
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