[Satoko] Correcting bug found when integrating with pdr.

The head of the propagation queue was not begin properly reset.

Adding some debugging functions.

4 files changed, 102 insertions, 21 deletions

diff --git a/src/sat/satoko/cnf_reader.c b/src/sat/satoko/cnf_reader.c
index 8223affd..48a0b068 100644
--- a/src/sat/satoko/cnf_reader.c
+++ b/src/sat/satoko/cnf_reader.c
@@ -142,8 +142,9 @@ int satoko_parse_dimacs(char *fname, satoko_t **solver)
             }
             read_clause(&token, lits);
             if (!satoko_add_clause(p, (int*)vec_uint_data(lits), vec_uint_size(lits))) {
+                printf("Unable to add clause: ");
                 vec_uint_print(lits);
-                return 0;
+                return SATOKO_ERR;
             }
             }
     }
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index 51befd16..b35574ab 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -362,14 +362,16 @@ static inline void solver_handle_conflict(solver_t *s, unsigned confl_cref)
 
 static inline void solver_analyze_final(solver_t *s, unsigned lit)
 {
-    int i;
+    unsigned i;
 
+    // printf("[Satoko] Analize final..\n");
+    // printf("[Satoko] Conflicting lit: %d\n", lit);
     vec_uint_clear(s->final_conflict);
     vec_uint_push_back(s->final_conflict, lit);
     if (solver_dlevel(s) == 0)
         return;
     vec_char_assign(s->seen, lit2var(lit), 1);
-    for (i = (int) vec_uint_size(s->trail) - 1; i >= (int) vec_uint_at(s->trail_lim, 0); i--) {
+    for (i = vec_uint_size(s->trail); i --> vec_uint_at(s->trail_lim, 0);) {
         unsigned var = lit2var(vec_uint_at(s->trail, i));
 
         if (vec_char_at(s->seen, var)) {
@@ -385,10 +387,11 @@ static inline void solver_analyze_final(solver_t *s, unsigned lit)
                         vec_char_assign(s->seen, lit2var(clause->data[j].lit), 1);
                 }
             }
-        vec_char_assign(s->seen, var, 0);
+            vec_char_assign(s->seen, var, 0);
         }
     }
     vec_char_assign(s->seen, lit2var(lit), 0);
+    // solver_debug_check_unsat(s);
 }
 
 static inline void solver_garbage_collect(solver_t *s)
@@ -511,12 +514,12 @@ unsigned solver_clause_create(solver_t *s, vec_uint_t *lits, unsigned f_learnt)
 
 void solver_cancel_until(solver_t *s, unsigned level)
 {
-    int i;
+    unsigned i;
 
     if (solver_dlevel(s) <= level)
         return;
-    for (i = (int) vec_uint_size(s->trail) - 1; i >= (int) vec_uint_at(s->trail_lim, level); i--) {
-        unsigned var = lit2var(vec_uint_at(s->trail, (unsigned) i));
+    for (i = vec_uint_size(s->trail); i --> vec_uint_at(s->trail_lim, level);) {
+        unsigned var = lit2var(vec_uint_at(s->trail, i));
 
         vec_char_assign(s->polarity, var, vec_char_at(s->assigns, var));
         vec_char_assign(s->assigns, var, VAR_UNASSING);
@@ -636,6 +639,7 @@ char solver_search(solver_t *s)
                 b_queue_clean(s->bq_lbd);
             solver_handle_conflict(s, confl_cref);
         } else {
+            // solver_debug_check_clauses(s);
             /* No conflict */
             unsigned next_lit;
 
@@ -675,8 +679,10 @@ char solver_search(solver_t *s)
             if (next_lit == UNDEF) {
                 s->stats.n_decisions++;
                 next_lit = solver_decide(s);
-                if (next_lit == UNDEF)
+                if (next_lit == UNDEF) {
+                    // solver_debug_check(s, SATOKO_SAT);
                     return SATOKO_SAT;
+                }
             }
             solver_new_decision(s, next_lit);
         }
@@ -684,23 +690,66 @@ char solver_search(solver_t *s)
 }
 
 //===------------------------------------------------------------------------===
-// Debug procedure
+// Debug procedures
 //===------------------------------------------------------------------------===
-void solver_debug_check(solver_t *s, int result)
+void solver_debug_check_trail(solver_t *s)
 {
-    unsigned cref, i;
+    unsigned i;
     unsigned *array;
-
-    printf("Checking for trail(%u) inconsistencies...", vec_uint_size(s->trail));
-    array = vec_uint_data(s->trail);
-    for (i = 1; i < vec_uint_size(s->trail); i++)
+    vec_uint_t *trail_dup = vec_uint_alloc(0);
+    fprintf(stdout, "[Satoko] Checking for trail(%u) inconsistencies...\n", vec_uint_size(s->trail));
+    vec_uint_duplicate(trail_dup, s->trail);
+    vec_uint_sort(trail_dup, 1);
+    array = vec_uint_data(trail_dup);
+    for (i = 1; i < vec_uint_size(trail_dup); i++) {
         if (array[i - 1] == lit_compl(array[i])) {
-            printf("Inconsistent trail: %u %u\n", array[i - 1], array[i]);
+            fprintf(stdout, "[Satoko] Inconsistent trail: %u %u\n", array[i - 1], array[i]);
+            assert(0);
             return;
         }
-    printf(" TRAIL OK\n");
+    }
+    for (i = 0; i < vec_uint_size(trail_dup); i++) {
+        if (var_value(s, lit2var(array[i])) != lit_polarity(array[i])) {
+            fprintf(stdout, "[Satoko] Inconsistent trail assignment: %u, %u\n", vec_char_at(s->assigns, lit2var(array[i])), array[i]);
+            assert(0);
+            return;
+        }
+    }
+    fprintf(stdout, "[Satoko] Trail OK.\n");
+    vec_uint_print(trail_dup);
+    vec_uint_free(trail_dup);
 
-    printf("Checking clauses... \n");
+}
+
+void solver_debug_check_clauses(solver_t *s)
+{
+    unsigned cref, i;
+
+    fprintf(stdout, "[Satoko] Checking clauses (%d)...\n", vec_uint_size(s->originals));
+    vec_uint_foreach(s->originals, cref, i) {
+        unsigned j;
+        struct clause *clause = clause_fetch(s, cref);
+        for (j = 0; j < clause->size; j++) {
+            if (vec_uint_find(s->trail, lit_compl(clause->data[j].lit))) {
+                continue;
+            }
+            break;
+        }
+        if (j == clause->size) {
+            vec_uint_print(s->trail);
+            fprintf(stdout, "[Satoko] FOUND UNSAT CLAUSE]: (%d) ", i);
+            clause_print(clause);
+            assert(0);
+        }
+    }
+    fprintf(stdout, "[Satoko] All SAT - OK\n");
+}
+
+void solver_debug_check(solver_t *s, int result)
+{
+    unsigned cref, i;
+    solver_debug_check_trail(s);
+    fprintf(stdout, "[Satoko] Checking clauses (%d)... \n", vec_uint_size(s->originals));
     vec_uint_foreach(s->originals, cref, i) {
         unsigned j;
         struct clause *clause = clause_fetch(s, cref);
@@ -710,10 +759,12 @@ void solver_debug_check(solver_t *s, int result)
             }
         }
         if (result == SATOKO_SAT && j == clause->size) {
-            printf("FOUND UNSAT CLAUSE!!!!\n");
+            fprintf(stdout, "[Satoko] FOUND UNSAT CLAUSE: (%d) ", i);
             clause_print(clause);
+            assert(0);
         }
     }
+    fprintf(stdout, "[Satoko] All SAT - OK\n");
 }
 
 ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h
index d6f7d75e..ee7b84e2 100644
--- a/src/sat/satoko/solver.h
+++ b/src/sat/satoko/solver.h
@@ -99,6 +99,7 @@ struct solver_t_ {
     unsigned book_cdb;     /* Bookmark clause database size */
     unsigned book_vars;    /* Bookmark number of variables */
     unsigned book_trail;   /* Bookmark trail size */
+    // unsigned book_qhead;   /* Bookmark propagation queue head */
 
     /* Temporary data used for solving cones */
     vec_char_t *marks;
@@ -118,7 +119,11 @@ extern unsigned solver_clause_create(solver_t *, vec_uint_t *, unsigned);
 extern char solver_search(solver_t *);
 extern void solver_cancel_until(solver_t *, unsigned);
 extern unsigned solver_propagate(solver_t *);
+
+/* Debuging */
 extern void solver_debug_check(solver_t *, int);
+extern void solver_debug_check_trail(solver_t *);
+extern void solver_debug_check_clauses(solver_t *);
 
 //===------------------------------------------------------------------------===
 // Inline var/lit functions
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index 8784a761..d404992e 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -43,6 +43,11 @@ static inline int clause_is_satisfied(solver_t *s, struct clause *clause)
     return SATOKO_ERR;
 }
 
+static inline void solver_clean_stats(solver_t *s)
+{
+    memset(&(s->stats), 0, sizeof(struct satoko_stats));
+}
+
 static inline void print_opts(solver_t *s)
 {
     printf( "+-[ BLACK MAGIC - PARAMETERS ]-+\n");
@@ -282,12 +287,15 @@ int satoko_add_clause(solver_t *s, int *lits, int size)
 
 void satoko_assump_push(solver_t *s, int lit)
 {
+    assert(lit2var(lit) < solver_varnum(s));
+    // printf("[Satoko] Push assumption: %d\n", lit);
     vec_uint_push_back(s->assumptions, lit);
 }
 
 void satoko_assump_pop(solver_t *s)
 {
     assert(vec_uint_size(s->assumptions) > 0);
+    // printf("[Satoko] Pop assumption: %d\n", vec_uint_pop_back(s->assumptions));
     vec_uint_pop_back(s->assumptions);
     solver_cancel_until(s, vec_uint_size(s->assumptions));
 }
@@ -297,6 +305,7 @@ int satoko_solve(solver_t *s)
     int status = SATOKO_UNDEC;
 
     assert(s);
+    solver_clean_stats(s);
     //if (s->opts.verbose)
     //    print_opts(s);
     if (s->status == SATOKO_ERR) {
@@ -327,6 +336,12 @@ int satoko_solve(solver_t *s)
 int satoko_solve_assumptions(solver_t *s, int * plits, int nlits)
 {
     int i, status;
+    // printf("\n[Satoko] Solve with assumptions.. (%d)\n", vec_uint_size(s->assumptions));
+    // printf("[Satoko]   + Variables: %d\n", solver_varnum(s));
+    // printf("[Satoko]   + Clauses: %d\n", solver_clausenum(s));
+    // printf("[Satoko]   + Trail size: %d\n", vec_uint_size(s->trail));
+    // printf("[Satoko]   + Queue head: %d\n", s->i_qhead);
+    // solver_debug_check_trail(s);
     for ( i = 0; i < nlits; i++ )
         satoko_assump_push( s, plits[i] );
     status = satoko_solve( s );
@@ -357,28 +372,33 @@ satoko_stats_t satoko_stats(satoko_t *s)
 
 void satoko_bookmark(satoko_t *s)
 {
+    // printf("[Satoko] Bookmark.\n");
     assert(s->status == SATOKO_OK);
     assert(solver_dlevel(s) == 0);
     s->book_cl_orig = vec_uint_size(s->originals);
     s->book_cl_lrnt = vec_uint_size(s->learnts);
     s->book_vars = vec_char_size(s->assigns);
     s->book_trail = vec_uint_size(s->trail);
+    // s->book_qhead = s->i_qhead;
     s->opts.no_simplify = 1;
 }
 
 void satoko_unbookmark(satoko_t *s)
 {
+    // printf("[Satoko] Unbookmark.\n");
     assert(s->status == SATOKO_OK);
     s->book_cl_orig = 0;
     s->book_cl_lrnt = 0;
     s->book_cdb = 0;
     s->book_vars = 0;
     s->book_trail = 0;
+    // s->book_qhead = 0;
     s->opts.no_simplify = 0;
 }
 
 void satoko_reset(satoko_t *s)
 {
+    // printf("[Satoko] Reset.\n");
     vec_uint_clear(s->assumptions);
     vec_uint_clear(s->final_conflict);
     cdb_clear(s->all_clauses);
@@ -412,6 +432,7 @@ void satoko_reset(satoko_t *s)
     s->book_cdb = 0;
     s->book_vars = 0;
     s->book_trail = 0;
+    s->i_qhead = 0;
 }
 
 void satoko_rollback(satoko_t *s)
@@ -421,13 +442,13 @@ void satoko_rollback(satoko_t *s)
     unsigned n_learnts = vec_uint_size(s->learnts) - s->book_cl_lrnt;
     struct clause **cl_to_remove;
 
+    // printf("[Satoko] rollback.\n");
     assert(s->status == SATOKO_OK);
     assert(solver_dlevel(s) == 0);
     if (!s->book_vars) {
         satoko_reset(s);
         return;
     }
-
     cl_to_remove = satoko_alloc(struct clause *, n_originals + n_learnts);
     /* Mark clauses */
     vec_uint_foreach_start(s->originals, cref, i, s->book_cl_orig)
@@ -446,6 +467,7 @@ void satoko_rollback(satoko_t *s)
         vec_wl_at(s->watches, i)->size = 0;
         vec_wl_at(s->watches, i)->n_bin = 0;
     }
+    // s->i_qhead = s->book_qhead;
     s->watches->size = s->book_vars;
     vec_act_shrink(s->activity, s->book_vars);
     vec_uint_shrink(s->levels, s->book_vars);
@@ -464,6 +486,7 @@ void satoko_rollback(satoko_t *s)
     s->book_cl_lrnt = 0;
     s->book_vars = 0;
     s->book_trail = 0;
+    // s->book_qhead = 0;
 }
 
 void satoko_mark_cone(satoko_t *s, int * pvars, int n_vars)
@@ -510,7 +533,7 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
     fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig);
     for (i = 0; i < vec_char_size(s->assigns); i++)
         if ( var_value(s, i) != VAR_UNASSING )
-            fprintf(file, "%d\n", var_value(s, i) == LIT_FALSE ? -(int)(i + !zero_var) : i + !zero_var);
+            fprintf(file, "%d %d\n", var_value(s, i) == LIT_FALSE ? -(int)(i + !zero_var) : i + !zero_var, zero_var ? : 0);
     
     array = vec_uint_data(s->originals);
     for (i = 0; i < vec_uint_size(s->originals); i++)
@@ -521,6 +544,7 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
         for (i = 0; i < n_lrnts; i++)
             clause_dump(file, clause_fetch(s, array[i]), !zero_var);
     }
+    fclose(file);
 
 }