Adding APIs to mark cones. Creating test-bench for incremental solving &satoko -i.

4 files changed, 64 insertions, 4 deletions

diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
index e3134b77..8d55a81c 100644
--- a/src/sat/satoko/satoko.h
+++ b/src/sat/satoko/satoko.h
@@ -89,6 +89,8 @@ extern void satoko_assump_push(satoko_t *s, unsigned);
 extern void satoko_assump_pop(satoko_t *s);
 extern int  satoko_simplify(satoko_t *);
 extern int  satoko_solve(satoko_t *);
+extern void satoko_mark_cone(satoko_t *s, int * pvars, int nvars);
+extern void satoko_unmark_cone(satoko_t *s, int * pvars, int nvars);
 
 /* If problem is unsatisfiable under assumptions, this function is used to
  * obtain the final conflict clause expressed in the assumptions.
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index cdd3141e..2abc9833 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -190,14 +190,18 @@ static inline unsigned solver_decide(solver_t *s)
         if (heap_size(s->var_order) == 0) {
             next_var = UNDEF;
             return UNDEF;
-        } else
-            next_var = heap_remove_min(s->var_order);
+        }
+        next_var = heap_remove_min(s->var_order);
+        if (solver_has_marks(s) && !var_mark(s, next_var))
+            next_var = UNDEF;
     }
     return var2lit(next_var, vec_char_at(s->polarity, next_var));
 }
 
 static inline void solver_new_decision(solver_t *s, unsigned lit)
 {
+    if (solver_has_marks(s) && !var_mark(s, lit2var(lit)))
+        return;
     assert(var_value(s, lit2var(lit)) == VAR_UNASSING);
     vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail));
     solver_enqueue(s, lit, UNDEF);
@@ -538,6 +542,8 @@ unsigned solver_propagate(solver_t *s)
 
         n_propagations++;
         watch_list_foreach(s->bin_watches, i, p) {
+            if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker)))
+                continue;
             if (var_value(s, lit2var(i->blocker)) == VAR_UNASSING)
                 solver_enqueue(s, i->blocker, i->cref);
             else if (lit_value(s, i->blocker) == LIT_FALSE)
@@ -551,6 +557,12 @@ unsigned solver_propagate(solver_t *s)
             struct clause *clause;
             struct watcher w;
 
+            if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker)))
+            {
+                *j++ = *i++;
+                continue;
+            }
+
             if (lit_value(s, i->blocker) == LIT_TRUE) {
                 *j++ = *i++;
                 continue;
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h
index 849d738a..01912a6e 100644
--- a/src/sat/satoko/solver.h
+++ b/src/sat/satoko/solver.h
@@ -93,6 +93,9 @@ struct solver_t_ {
     vec_uint_t *stamps; /* Multipurpose stamp used to calculate LBD and
                  * clauses minimization with binary resolution */
 
+    /* Temporary data used for solving cones */
+    vec_char_t *marks;
+
     struct satoko_stats stats;
     struct satoko_opts opts;
 };
@@ -133,6 +136,18 @@ static inline unsigned var_reason(solver_t *s, unsigned var)
 {
     return vec_uint_at(s->reasons, var);
 }
+static inline int var_mark(solver_t *s, unsigned var)
+{
+    return (int)vec_char_at(s->marks, var);
+}
+static inline void var_set_mark(solver_t *s, unsigned var)
+{
+    vec_char_assign(s->marks, var, 1);
+}
+static inline void var_clean_mark(solver_t *s, unsigned var)
+{
+    vec_char_assign(s->marks, var, 0);
+}
 //===------------------------------------------------------------------------===
 // Inline lit functions
 //===------------------------------------------------------------------------===
@@ -185,6 +200,14 @@ static inline int solver_enqueue(solver_t *s, unsigned lit, unsigned reason)
     vec_uint_push_back(s->trail, lit);
     return SATOKO_OK;
 }
+static inline int solver_varnum(solver_t *s)
+{
+    return vec_char_size(s->assigns);
+}
+static inline int solver_has_marks(solver_t *s)
+{
+    return (int)(s->marks != NULL);
+}
 
 //===------------------------------------------------------------------------===
 // Inline clause functions
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index f3f3d781..b446fb05 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -145,11 +145,13 @@ void satoko_destroy(solver_t *s)
     vec_uint_free(s->stack);
     vec_uint_free(s->last_dlevel);
     vec_uint_free(s->stamps);
+    if (s->marks) vec_char_free(s->marks);
     satoko_free(s);
 }
 
 void satoko_default_opts(satoko_opts_t *opts)
 {
+    memset(opts, 0, sizeof(satoko_opts_t));
     opts->verbose = 0;
     /* Limits */
     opts->conf_limit = 0;
@@ -232,6 +234,7 @@ void satoko_add_variable(solver_t *s, char sign)
     vec_uint_push_back(s->stamps, 0);
     vec_char_push_back(s->seen, 0);
     heap_insert(s->var_order, var);
+    if (s->marks) vec_char_push_back(s->marks, 0);
 }
 
 int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size)
@@ -287,8 +290,8 @@ int satoko_solve(solver_t *s)
     char status = SATOKO_UNDEC;
 
     assert(s);
-    if (s->opts.verbose)
-        print_opts(s);
+    //if (s->opts.verbose)
+    //    print_opts(s);
 
     while (status == SATOKO_UNDEC) {
         status = solver_search(s);
@@ -317,4 +320,24 @@ satoko_stats_t satoko_stats(satoko_t *s)
     return s->stats;
 }
 
+void satoko_mark_cone(satoko_t *s, int * pvars, int nvars)
+{
+    int i;
+    if (!solver_has_marks(s))
+         s->marks = vec_char_init(solver_varnum(s), 0);
+    for (i = 0; i < nvars; i++)
+    {
+        var_set_mark(s, pvars[i]);
+        if (!heap_in_heap(s->var_order, pvars[i]))
+            heap_insert(s->var_order, pvars[i]);
+    }
+}
+void satoko_unmark_cone(satoko_t *s, int * pvars, int nvars)
+{
+    int i;
+    assert(solver_has_marks(s));
+    for (i = 0; i < nvars; i++)
+        var_clean_mark(s, pvars[i]);
+}
+
 ABC_NAMESPACE_IMPL_END