From 86dc9d3268df898ca1ed687ac75434d745a70e74 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Wed, 8 Apr 2026 18:24:11 +0200 Subject: [PATCH] We need to reset local conflicts --- src/smt/seq/seq_nielsen.cpp | 13 +++++++ src/smt/seq/seq_nielsen.h | 7 ++++ src/smt/seq/seq_nielsen_pp.cpp | 4 +-- src/smt/theory_nseq.cpp | 64 +++++++++++++++++++--------------- 4 files changed, 57 insertions(+), 31 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index c2e4bb899..d81b106e9 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1315,6 +1315,11 @@ namespace seq { SASSERT(depth <= cur_path.size()); m_stats.m_max_depth = std::max(m_stats.m_max_depth, depth); + if (node->is_general_conflict()) { + ++m_stats.m_num_simplify_conflict; + return search_result::unsat; + } + // check for external cancellation (timeout, user interrupt) if (!m.inc()) return search_result::unknown; @@ -1336,10 +1341,18 @@ namespace seq { return search_result::unknown; } node->set_eval_idx(m_run_idx); + SASSERT(!node->is_general_conflict()); + node->clear_local_conflict(); // clear local conflicts from previous runs + // we might need to tell the SAT solver about the new integer inequalities // that might have been added by an extension step assert_node_new_int_constraints(node); + if (node->is_currently_conflict()) { + ++m_stats.m_num_simplify_conflict; + return search_result::unsat; + } + // simplify constraints (idempotent after first call) const simplify_result sr = node->simplify_and_init(cur_path); diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 3f2c7356d..f98e8cd5e 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -611,6 +611,13 @@ namespace seq { (reason() != backtrack_reason::unevaluated && m_is_extended); } + void clear_local_conflict() { + SASSERT(!is_general_conflict()); + m_reason = backtrack_reason::unevaluated; + m_conflict_internal = nullptr; + m_conflict_external_literal = sat::null_literal; + } + backtrack_reason reason() const { return m_reason; } void set_child_conflict() { diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index f03b206cc..c2e436770 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -589,10 +589,10 @@ namespace seq { out << ", color=green"; else if (n->is_general_conflict()) out << ", color=darkred"; - else if (n->eval_idx() != m_run_idx) // inactive, not visited this run - out << ", color=blue"; else if (n->is_currently_conflict()) out << ", color=red"; + else if (n->eval_idx() != m_run_idx) // inactive, not visited this run + out << ", color=blue"; out << "];\n"; } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 5d67272f5..ee8ffa824 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -741,6 +741,36 @@ namespace smt { p.m_string_solver = "seq"; kernel kernel(m, p); + auto model_out = [&]() { + model_ref model; + kernel.get_model(model); + for (unsigned i = 0; i < model->get_num_constants(); i++) { + func_decl* f = model->get_constant(i); + expr_ref v(m); + VERIFY(model->eval(f, v)); + std::cout << f->get_name() << ": " << mk_pp(v, m) << std::endl; + } + for (unsigned i = 0; i < model->get_num_functions(); i++) { + func_decl* f = model->get_function(i); + func_interp* fi = model->get_func_interp(f); + auto entries = fi->get_entries(); + std::cout << f->get_name() << ":\n"; + for (unsigned j = 0; j < fi->num_entries(); j++) { + auto& e = entries[j]; + auto* args = e->get_args(); + std::cout << "\n("; + for (unsigned k = 0; k < fi->get_arity(); k++) { + if (k > 0) + std::cout << ", "; + std::cout << mk_pp(args[k], m); + } + std::cout << "): "; + expr* r = e->get_result(); + std::cout << mk_pp(r, m) << std::endl; + } + } + }; + for (seq::dep_source const& d : m_nielsen.conflict_sources()) { if (std::holds_alternative(d)) kernel.assert_expr( @@ -763,6 +793,7 @@ namespace smt { } auto dot = m_nielsen.to_dot(); std::cout << std::endl; + model_out(); kernel.reset(); auto& lits = ctx.assigned_literals(); for (literal l : lits) { @@ -772,44 +803,19 @@ namespace smt { th_rewriter th(m); expr_ref r(m); th(e, r); - std::cout << mk_pp(r, m) << std::endl; kernel.assert_expr(r); } auto res2 = kernel.check(); if (res2 == l_true) { // the algorithm is unsound std::cout << "Original input is SAT" << std::endl; - model_ref model; - kernel.get_model(model); - for (unsigned i = 0; i < model->get_num_constants(); i++) { - func_decl* f = model->get_constant(i); - expr_ref v(m); - VERIFY(model->eval(f, v)); - std::cout << f->get_name() << ": " << mk_pp(v, m) << std::endl; - } - for (unsigned i = 0; i < model->get_num_functions(); i++) { - func_decl* f = model->get_function(i); - func_interp* fi = model->get_func_interp(f); - auto entries = fi->get_entries(); - std::cout << f->get_name() << ":\n"; - for (unsigned j = 0; j < fi->num_entries(); j++) { - auto& e = entries[j]; - auto* args = e->get_args(); - std::cout << "\n("; - for (unsigned k = 0; k < fi->get_arity(); k++) { - if (k > 0) - std::cout << ", "; - std::cout << mk_pp(args[k], m); - } - std::cout << "): "; - expr* r = e->get_result(); - std::cout << mk_pp(r, m) << std::endl; - } - } + model_out(); } - else if (res == l_false) + else if (res2 == l_false) // the justification is too narrow std::cout << "Original input is UNSAT" << std::endl; + else + std::cout << "Original input is UNKNOWN" << std::endl; } VERIFY(res != l_true); }