From 069068ce5e27f9e214157da45811cfc123aefe89 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Tue, 9 Jun 2026 15:40:28 +0200 Subject: [PATCH] Don't use enodes for justifying disequality conflicts --- src/smt/seq/seq_nielsen.cpp | 88 ++++++++++++++++--------------------- src/smt/seq/seq_nielsen.h | 6 +-- src/smt/seq/seq_state.h | 10 ++--- src/smt/theory_nseq.cpp | 28 +++++++----- src/smt/theory_nseq.h | 4 +- 5 files changed, 65 insertions(+), 71 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 31e8841a9..bff2362b2 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -35,6 +35,7 @@ NSB review: #include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/seq_skolem.h" #include "ast/rewriter/var_subst.h" +#include "smt/smt_enode.h" #include "util/statistics.h" #include #include @@ -442,18 +443,10 @@ namespace seq { // nielsen_graph // ----------------------------------------------- - nielsen_graph::nielsen_graph(euf::sgraph &sg, sub_solver_i &solver, context_solver_i& ctx_solver): - m(sg.get_manager()), - a(sg.get_manager()), - m_seq(sg.get_seq_util()), - m_sg(sg), - m_rw(m), - m_sk(m, m_rw), - m_length_solver(solver), - m_context_solver(ctx_solver), - m_partial_dfa_pin(sg.get_manager()), - m_parikh(alloc(seq_parikh, sg)), - m_seq_regex(alloc(seq::seq_regex, sg)) { + nielsen_graph::nielsen_graph(euf::sgraph &sg, sub_solver_i &solver, context_solver_i &ctx_solver) + : m(sg.get_manager()), a(sg.get_manager()), m_seq(sg.get_seq_util()), m_sg(sg), m_rw(m), m_sk(m, m_rw), + m_length_solver(solver), m_context_solver(ctx_solver), m_partial_dfa_pin(sg.get_manager()), + m_parikh(alloc(seq_parikh, sg)), m_seq_regex(alloc(seq::seq_regex, sg)) { // Answer projection-state membership queries during projection-aware // derivatives (the sgraph cannot reach the partial DFA otherwise). m_sg.set_projection_oracle(this); @@ -466,14 +459,14 @@ namespace seq { reset(); } - bool nielsen_graph::projection_state_in_Q(expr* state, unsigned nu) { + bool nielsen_graph::projection_state_in_Q(expr *state, unsigned nu) { if (!state || nu == 0) return false; const unsigned sid = state->get_id(); // r ∈ Q_nu iff r is incident to a partial-DFA edge whose extraction // index lies in [1, nu] (the "edges marked ≤ ν" subautomaton of the // implementation-aspects section of the paper). - auto incident = [&](std::unordered_map const& adj) { + auto incident = [&](std::unordered_map const &adj) { auto it = adj.find(sid); if (it == adj.end()) return false; @@ -489,68 +482,58 @@ namespace seq { return incident(m_partial_dfa_out) || incident(m_partial_dfa_in); } - euf::snode* nielsen_graph::mk_projection_term(euf::snode* root_re, unsigned nu) { - SASSERT(root_re && root_re->get_expr()); - // π_{Q_nu, {root}}(root): current state == accepting state == root. - expr_ref proj = m_sg.mk_re_proj(root_re->get_expr(), root_re->get_expr(), nu); - return m_sg.mk(proj); - } - - nielsen_node* nielsen_graph::mk_node() { + nielsen_node *nielsen_graph::mk_node() { const unsigned id = m_nodes.size(); - nielsen_node* n = alloc(nielsen_node, *this, id); + nielsen_node *n = alloc(nielsen_node, *this, id); m_nodes.push_back(n); SASSERT(n->id() == m_nodes.size() - 1); return n; } - nielsen_node* nielsen_graph::mk_child(nielsen_node* parent) { - nielsen_node* child = mk_node(); + nielsen_node *nielsen_graph::mk_child(nielsen_node *parent) { + nielsen_node *child = mk_node(); child->clone_from(*parent); child->m_parent_ic_count = parent->constraints().size(); return child; } - nielsen_edge* nielsen_graph::mk_edge(nielsen_node *src, nielsen_node *tgt, const char *rule, + nielsen_edge *nielsen_graph::mk_edge(nielsen_node *src, nielsen_node *tgt, const char *rule, const bool is_progress) { SASSERT(src != nullptr); SASSERT(tgt != nullptr); - nielsen_edge* e = alloc(nielsen_edge, src, tgt, rule, is_progress); + nielsen_edge *e = alloc(nielsen_edge, src, tgt, rule, is_progress); m_edges.push_back(e); src->add_outgoing(e); return e; } - void nielsen_graph::add_str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r) { + void nielsen_graph::add_str_eq(euf::snode *lhs, euf::snode *rhs, smt::enode *l, smt::enode *r) const { const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r)); str_eq eq(lhs, rhs, dep); eq.sort(); // check if root node contains this equation already - if (std::ranges::any_of(m_root->str_eqs(), [&](const str_eq& e) { - return e.m_lhs == eq.m_lhs && e.m_rhs == eq.m_rhs; - })) + if (std::ranges::any_of(m_root->str_eqs(), + [&](const str_eq &e) { return e.m_lhs == eq.m_lhs && e.m_rhs == eq.m_rhs; })) // already present, no need to add again return; m_root->add_str_eq(eq); } - void nielsen_graph::add_str_deq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r) { - const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r)); + void nielsen_graph::add_str_deq(euf::snode *lhs, euf::snode *rhs, sat::literal l) const { + const dep_tracker dep = m_dep_mgr.mk_leaf(l); str_deq deq(lhs, rhs, dep); // check if root node contains this equation already - if (std::ranges::any_of(m_root->str_deqs(), [&](const str_deq& e) { - return e.m_lhs == deq.m_lhs && e.m_rhs == deq.m_rhs; - })) + if (std::ranges::any_of(m_root->str_deqs(), + [&](const str_deq &e) { return e.m_lhs == deq.m_lhs && e.m_rhs == deq.m_rhs; })) // already present, no need to add again return; m_root->add_str_deq(deq); } - void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l) { + void nielsen_graph::add_str_mem(euf::snode *str, euf::snode *regex, sat::literal l) const { // check if root node contains this membership constraint already - if (std::ranges::any_of(m_root->str_mems(), [&](const str_mem& e) { - return e.m_regex == regex && e.m_str == str; - })) + if (std::ranges::any_of(m_root->str_mems(), + [&](const str_mem &e) { return e.m_regex == regex && e.m_str == str; })) // already present, no need to add again return; const dep_tracker dep = m_dep_mgr.mk_leaf(l); @@ -558,29 +541,29 @@ namespace seq { } // test-friendly overloads (no external dependency tracking) - void nielsen_graph::add_str_eq(euf::snode* lhs, euf::snode* rhs) { + void nielsen_graph::add_str_eq(euf::snode *lhs, euf::snode *rhs) { const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr)); str_eq eq(lhs, rhs, dep); eq.sort(); m_root->add_str_eq(eq); } - void nielsen_graph::add_str_deq(euf::snode* lhs, euf::snode* rhs) { + void nielsen_graph::add_str_deq(euf::snode *lhs, euf::snode *rhs) { const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr)); str_deq deq(lhs, rhs, dep); m_root->add_str_deq(deq); } - void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex) { + void nielsen_graph::add_str_mem(euf::snode *str, euf::snode *regex) { const dep_tracker dep = nullptr; m_root->add_str_mem(str_mem(str, regex, dep)); } void nielsen_graph::reset() { - for (nielsen_node* n : m_nodes) { + for (nielsen_node *n : m_nodes) { dealloc(n); } - for (nielsen_edge* e : m_edges) { + for (nielsen_edge *e : m_edges) { dealloc(e); } m_nodes.reset(); @@ -591,15 +574,15 @@ namespace seq { m_depth_bound = 0; m_fresh_cnt = 0; m_root_constraints_asserted = false; - //m_mod_cnt.reset(); + // m_mod_cnt.reset(); m_partial_dfa_edges.reset(); m_partial_dfa_out.clear(); m_partial_dfa_in.clear(); m_partial_dfa_edge_index.clear(); m_partial_dfa_pin.reset(); m_projection_extract_idx = 0; - //m_length_trail.reset(); - //m_length_info.reset(); + // m_length_trail.reset(); + // m_length_info.reset(); m_dep_mgr.reset(); m_length_solver.reset(); SASSERT(m_nodes.empty()); @@ -608,7 +591,7 @@ namespace seq { SASSERT(m_sat_node == nullptr); } - void nielsen_graph::add_le_dependency(const dep_tracker dep, nielsen_node* n, expr* lhs, expr* rhs) const { + void nielsen_graph::add_le_dependency(const dep_tracker dep, nielsen_node *n, expr *lhs, expr *rhs) const { SASSERT(lhs); SASSERT(rhs); const expr_ref le(a.mk_le(lhs, rhs), m); @@ -618,6 +601,13 @@ namespace seq { n->add_constraint(constraint(le, dep, m)); } + euf::snode *nielsen_graph::mk_projection_term(euf::snode *root_re, unsigned nu) { + SASSERT(root_re && root_re->get_expr()); + // π_{Q_nu, {root}}(root): current state == accepting state == root. + expr_ref proj = m_sg.mk_re_proj(root_re->get_expr(), root_re->get_expr(), nu); + return m_sg.mk(proj); + } + // ----------------------------------------------------------------------- // nielsen_node: simplify_and_init // ----------------------------------------------------------------------- diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index f5afa54dd..76d568b85 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -1060,9 +1060,9 @@ namespace seq { ptr_vector const& sat_path() const { return m_sat_path; } // add constraints to the root node from external solver - void add_str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r); - void add_str_deq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r); - void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l); + void add_str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r) const; + void add_str_deq(euf::snode* lhs, euf::snode* rhs, sat::literal l) const; + void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l) const; // test-friendly overloads (no external dependency tracking) void add_str_eq(euf::snode* lhs, euf::snode* rhs); diff --git a/src/smt/seq/seq_state.h b/src/smt/seq/seq_state.h index 263f994ba..6831e1591 100644 --- a/src/smt/seq/seq_state.h +++ b/src/smt/seq/seq_state.h @@ -29,19 +29,19 @@ namespace smt { struct tracked_str_eq : seq::str_eq { enode *m_l, *m_r; - tracked_str_eq(euf::snode *lhs, euf::snode *rhs, smt::enode *l, smt::enode *r, seq::dep_tracker const &dep) + tracked_str_eq(euf::snode *lhs, euf::snode *rhs, enode *l, enode *r, seq::dep_tracker const &dep) : str_eq(lhs, rhs, dep), m_l(l), m_r(r) {} }; struct tracked_str_deq : seq::str_deq { - enode *m_l, *m_r; - tracked_str_deq(euf::snode *lhs, euf::snode *rhs, smt::enode *l, smt::enode *r, seq::dep_tracker const &dep) - : str_deq(lhs, rhs, dep), m_l(l), m_r(r) {} + sat::literal lit; + tracked_str_deq(euf::snode *lhs, euf::snode *rhs, const sat::literal lit, seq::dep_tracker const &dep) + : str_deq(lhs, rhs, dep), lit(lit) {} }; struct tracked_str_mem : seq::str_mem { sat::literal lit; - tracked_str_mem(euf::snode *str, euf::snode *regex, sat::literal lit, seq::dep_tracker const &dep) + tracked_str_mem(euf::snode *str, euf::snode *regex, const sat::literal lit, seq::dep_tracker const &dep) : str_mem(str, regex, dep), lit(lit) {} }; diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 3aa83a69f..1b86662c5 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -267,9 +267,10 @@ namespace smt { else { euf::snode *s1 = get_snode(e1); euf::snode *s2 = get_snode(e2); - seq::dep_tracker dep = nullptr; + const seq::dep_tracker dep = nullptr; ctx.push_trail(restore_vector(m_prop_queue)); - m_prop_queue.push_back(deq_item(s1, s2, get_enode(v1), get_enode(v2), dep)); + expr_ref eq_expr(m.mk_not(m.mk_eq(e1, e2)), m); + m_prop_queue.push_back(deq_item(s1, s2, ctx.get_literal(eq_expr), dep)); m_last_constraint_added = ctx.get_scope_level(); m_can_hot_restart = false; } @@ -437,16 +438,16 @@ namespace smt { } } - void theory_nseq::propagate_eq(tracked_str_eq const& eq) { + void theory_nseq::propagate_eq(tracked_str_eq const &eq) const { // When s1 = s2 is learned, ensure len(s1) and len(s2) are // internalized so congruence closure propagates len(s1) = len(s2). ensure_length_var(eq.m_l->get_expr()); ensure_length_var(eq.m_r->get_expr()); } - void theory_nseq::propagate_deq(tracked_str_deq const& eq) { - ensure_length_var(eq.m_l->get_expr()); - ensure_length_var(eq.m_r->get_expr()); + void theory_nseq::propagate_deq(tracked_str_deq const& eq) const { + ensure_length_var(eq.m_lhs->get_expr()); + ensure_length_var(eq.m_rhs->get_expr()); } void theory_nseq::propagate_pos_mem(tracked_str_mem const& mem) { @@ -706,8 +707,8 @@ namespace smt { } if (std::holds_alternative(item)) { SASSERT(!get_fparams().m_nseq_axiomatize_diseq); - auto const& eq = std::get(item); - m_nielsen.add_str_deq(eq.m_lhs, eq.m_rhs, eq.m_l, eq.m_r); + auto const& deq = std::get(item); + m_nielsen.add_str_deq(deq.m_lhs, deq.m_rhs, deq.lit); ++num_deqs; } else if (std::holds_alternative(item)) { @@ -917,9 +918,6 @@ namespace smt { << (m_nielsen.sat_node() ? "set" : "null") << "\n"); // Nielsen found a consistent assignment for positive constraints. SASSERT(has_eq_or_diseq_or_mem); // we should have axiomatized them - - bool all_sat = add_nielsen_assumptions(); - if (!check_length_coherence()) return FC_CONTINUE; @@ -927,6 +925,9 @@ namespace smt { return FC_CONTINUE; CTRACE(seq, !has_unhandled_preds(), display(tout << "done\n")); + + bool all_sat = add_nielsen_assumptions(); + if (!all_sat) return FC_CONTINUE; @@ -1149,7 +1150,10 @@ namespace smt { for (auto [a, b] : eqs) tout << enode_pp(a, ctx) << " == " << enode_pp(b, ctx) << "\n"; ); - SASSERT(all_of(eqs, [&](auto eq) { return eq.first->get_root() == eq.second->get_root(); })); + for (auto& eq : eqs) { + std::cout << mk_pp(eq.first->get_expr(), m) << " == " << mk_pp(eq.second->get_expr(), m) << std::endl; + SASSERT(eq.first->get_root() == eq.second->get_root()); + }; bool all_true = all_of(lits, [&](auto lit) { return ctx.get_assignment(lit) == l_true; }); diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 132470d98..355f1cb33 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -150,8 +150,8 @@ namespace smt { euf::snode* get_snode(expr* e); // propagation dispatch helpers - void propagate_eq(tracked_str_eq const& eq); - void propagate_deq(tracked_str_deq const& deq); + void propagate_eq(tracked_str_eq const& eq) const; + void propagate_deq(tracked_str_deq const& deq) const; void propagate_pos_mem(tracked_str_mem const& mem); void enqueue_axiom(expr* e); void dequeue_axiom(expr* e);