Debugging

src/smt/seq/seq_nielsen.cpp

@@ -1328,7 +1328,7 @@ namespace seq {
         if (m_max_nodes > 0 && m_stats.m_num_dfs_nodes > m_max_nodes)
             return search_result::unknown;
 
-        // revisit detection: if already visited this run, return cached status.
+        // revisit detection: if already visited this run (e.g., iterative deepening), return cached status.
         // mirrors ZIPT's NielsenNode.GraphExpansion() evalIdx check.
         if (node->eval_idx() == m_run_idx) {
             if (node->is_satisfied()) {
@@ -3678,8 +3678,6 @@ namespace seq {
         // We enumerate all nodes rather than having a "todo"-list, as
         // hypothetically the graph could contain cycles in the future
         for (nielsen_node const* n : m_nodes) {
-            if (n->eval_idx() != m_run_idx)
-                continue;
             if (n->reason() == backtrack_reason::children_failed)
                 continue;
 
@@ -3687,6 +3685,7 @@ namespace seq {
             if (n->m_conflict_external_literal != sat::null_literal) {
                 // We know from the outer solver that this literal is assigned false
                 deps = m_dep_mgr.mk_join(deps, m_dep_mgr.mk_leaf(n->m_conflict_external_literal));
+                std::cout << "External literal: " << n->m_conflict_external_literal << std::endl;
                 if (n->m_conflict_internal)
                     deps = m_dep_mgr.mk_join(deps, n->m_conflict_internal);
                 continue;

src/smt/seq/seq_nielsen.h

@@ -244,7 +244,7 @@ Author:
 #include "ast/euf/euf_sgraph.h"
 #include <map>
 #include "model/model.h"
-
+#include "sat/smt/arith_solver.h"
 
 namespace smt {
     class enode;
@@ -575,6 +575,8 @@ namespace seq {
         vector<constraint> const& constraints() const { return m_constraints; }
         vector<constraint>& constraints() { return m_constraints; }
 
+        sat::literal get_external_conflict_literal() const { return m_conflict_external_literal; }
+
         // Query current bounds for a variable from the arithmetic subsolver.
         // Falls der Subsolver keinen Bound liefert, werden konservative Defaults
         // 0 / UINT_MAX verwendet.

src/smt/seq/seq_nielsen_pp.cpp

@@ -580,8 +580,10 @@ namespace seq {
                 << n->id() << ": ";
             n->to_html(out, names, next_id, m);
             // append conflict reason if this is a direct conflict
-            if (is_actual_conflict(n->reason()))
+            if (n->is_currently_conflict())
                 out << "<br/>" << reason_to_str(n->reason());
+            if (n->reason() == backtrack_reason::external)
+                out << "<br/>" << n->get_external_conflict_literal();
             out << ">";
 
             // colour

src/smt/theory_nseq.cpp

@@ -784,7 +784,7 @@ namespace smt {
             }
             auto res = kernel.check();
             if (res == l_true) {
-                std::cout << "Insufficient justification:\n";
+                std::cout << "Conflict is SAT - Insufficient justification:\n";
                 for (auto& lit : lits) {
                     std::cout << mk_pp(ctx.literal2expr(lit), m) << "\n-----------\n";
                 }
@@ -795,27 +795,43 @@ namespace smt {
                 std::cout << std::endl;
                 model_out();
                 kernel.reset();
-                auto& lits = ctx.assigned_literals();
+                for (auto& eq : m_nielsen.root()->str_eqs()) {
-                for (literal l : lits) {
+                    kernel.assert_expr(m.mk_eq(eq.m_lhs->get_expr(), eq.m_rhs->get_expr()));
-                    expr* e = ctx.literal2expr(l);
+                }
-                    if (!ctx.b_internalized(e) || !ctx.is_relevant(e))
+                for (auto& mem : m_nielsen.root()->str_mems()) {
-                         continue;
+                    kernel.assert_expr(m_seq.re.mk_in_re(mem.m_str->get_expr(), mem.m_regex->get_expr()));
-                    th_rewriter th(m);
-                    expr_ref r(m);
-                    th(e, r);
-                    kernel.assert_expr(r);
                 }
                 auto res2 = kernel.check();
                 if (res2 == l_true) {
-                    // the algorithm is unsound
+                    std::cout << "Nielsen input is SAT" << std::endl;
-                    std::cout << "Original input is SAT" << std::endl;
                     model_out();
+                    kernel.reset();
+                    auto& lits = ctx.assigned_literals();
+                    for (literal l : lits) {
+                        expr* e = ctx.literal2expr(l);
+                        if (!ctx.b_internalized(e) || !ctx.is_relevant(e))
+                            continue;
+                        th_rewriter th(m);
+                        expr_ref r(m);
+                        th(e, r);
+                        kernel.assert_expr(r);
+                    }
+                    auto res3 = kernel.check();
+                    if (res3 == l_true) {
+                        // the algorithm is unsound
+                        std::cout << "Complete input is SAT" << std::endl;
+                        model_out();
+                    }
+                    else if (res3 == l_false)
+                        // the justification is too narrow
+                        std::cout << "Complete input is UNSAT" << std::endl;
+                    else
+                        std::cout << "Complete input is UNKNOWN" << std::endl;
                 }
                 else if (res2 == l_false)
-                    // the justification is too narrow
+                    std::cout << "Nielsen input is UNSAT" << std::endl;
-                    std::cout << "Original input is UNSAT" << std::endl;
                 else
-                    std::cout << "Original input is UNKNOWN" << std::endl;
+                    std::cout << "Nielsen input is UNKNOWN" << std::endl;
             }
             VERIFY(res != l_true);
         }