From 8795bf06fb4cd0d6560bcc2807b104595edeb849 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 19 Mar 2026 10:42:18 -0700 Subject: [PATCH] theory_nseq: dispatch assign_eh on all seq predicate cases via m_axioms, add enqueue/dequeue_axiom with variant prop_item (#9040) * dispatch assign_eh cases via m_axioms: add prefix/suffix/contains true axioms Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * fix build: remove stale snode_label_html declaration from seq_nielsen.h Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * theory_nseq: add enqueue/dequeue_axiom + std::variant prop_item + relevant_eh Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/ast/rewriter/seq_axioms.cpp | 34 +++++++ src/ast/rewriter/seq_axioms.h | 3 + src/smt/seq/seq_nielsen.h | 2 - src/smt/theory_nseq.cpp | 168 ++++++++++++++++++++++++-------- src/smt/theory_nseq.h | 21 ++-- 5 files changed, 179 insertions(+), 49 deletions(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 9ed6863fc..b47b946a2 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -1274,6 +1274,40 @@ namespace seq { } + // prefix(s, t) => t = s ++ prefix_inv(s, t) + void axioms::prefix_true_axiom(expr* e) { + expr* _s = nullptr, *_t = nullptr; + VERIFY(seq.str.is_prefix(e, _s, _t)); + auto s = purify(_s); + auto t = purify(_t); + expr_ref inv = m_sk.mk_prefix_inv(s, t); + expr_ref lit(e, m); + add_clause(~lit, mk_seq_eq(t, mk_concat(s, inv))); + } + + // suffix(s, t) => t = suffix_inv(s, t) ++ s + void axioms::suffix_true_axiom(expr* e) { + expr* _s = nullptr, *_t = nullptr; + VERIFY(seq.str.is_suffix(e, _s, _t)); + auto s = purify(_s); + auto t = purify(_t); + expr_ref inv = m_sk.mk_suffix_inv(s, t); + expr_ref lit(e, m); + add_clause(~lit, mk_seq_eq(t, mk_concat(inv, s))); + } + + // contains(t, s) => t = contains_left(t, s) ++ s ++ contains_right(t, s) + void axioms::contains_true_axiom(expr* e) { + expr* _t = nullptr, *_s = nullptr; + VERIFY(seq.str.is_contains(e, _t, _s)); + auto t = purify(_t); + auto s = purify(_s); + expr_ref f1 = m_sk.mk_contains_left(t, s); + expr_ref f2 = m_sk.mk_contains_right(t, s); + expr_ref lit(e, m); + add_clause(~lit, mk_seq_eq(t, mk_concat(f1, s, f2))); + } + /** ~contains(a, b) => ~prefix(b, a) ~contains(a, b) => ~contains(tail(a), b) diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h index 48828a4e6..4a1b8b96e 100644 --- a/src/ast/rewriter/seq_axioms.h +++ b/src/ast/rewriter/seq_axioms.h @@ -84,6 +84,9 @@ namespace seq { void suffix_axiom(expr* n); void prefix_axiom(expr* n); + void prefix_true_axiom(expr* n); + void suffix_true_axiom(expr* n); + void contains_true_axiom(expr* n); void extract_axiom(expr* n); void indexof_axiom(expr* n); void last_indexof_axiom(expr* n); diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 84a92b7c3..e597db807 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -515,8 +515,6 @@ namespace seq { } }; - static std::string snode_label_html(euf::snode const* n, ast_manager& m); - // node in the Nielsen graph // mirrors ZIPT's NielsenNode class nielsen_node { diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 40c45e895..a1d17337a 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -172,7 +172,7 @@ namespace smt { unsigned idx = m_state.str_eqs().size(); m_state.add_str_eq(s1, s2, get_enode(v1), get_enode(v2)); ctx.push_trail(restore_vector(m_prop_queue)); - m_prop_queue.push_back({prop_item::eq_prop, idx}); + m_prop_queue.push_back(eq_item{idx}); } } @@ -196,39 +196,60 @@ namespace smt { void theory_nseq::assign_eh(bool_var v, bool is_true) { expr* e = ctx.bool_var2expr(v); - expr* s = nullptr; - expr* re = nullptr; - if (!m_seq.str.is_in_re(e, s, re)) { - // Track unhandled boolean string predicates (prefixof, contains, etc.) - if (is_app(e) && to_app(e)->get_family_id() == m_seq.get_family_id()) - push_unhandled_pred(); - return; + expr* s = nullptr, *re = nullptr; + TRACE(seq, tout << (is_true ? "" : "¬") << mk_bounded_pp(e, m, 3) << "\n";); + if (m_seq.str.is_in_re(e, s, re)) { + euf::snode* sn_str = get_snode(s); + euf::snode* sn_re = get_snode(re); + if (!sn_str || !sn_re) + return; + unsigned idx = m_state.str_mems().size(); + literal lit(v, !is_true); + if (is_true) { + m_state.add_str_mem(sn_str, sn_re, lit); + } + else { + // ¬(str ∈ R) ≡ str ∈ complement(R): store as a positive membership + // so the Nielsen graph sees it uniformly; the original negative literal + // is kept in mem_source for conflict reporting. + expr_ref re_compl(m_seq.re.mk_complement(re), m); + euf::snode* sn_re_compl = get_snode(re_compl.get()); + m_state.add_str_mem(sn_str, sn_re_compl, lit); + } + ctx.push_trail(restore_vector(m_prop_queue)); + m_prop_queue.push_back(mem_item{idx}); } - euf::snode* sn_str = get_snode(s); - euf::snode* sn_re = get_snode(re); - if (!sn_str || !sn_re) - return; - - unsigned idx = m_state.str_mems().size(); - literal lit(v, !is_true); - if (is_true) { - m_state.add_str_mem(sn_str, sn_re, lit); + else if (m_seq.str.is_prefix(e)) { + if (is_true) + m_axioms.prefix_true_axiom(e); + else + m_axioms.prefix_axiom(e); } - else { - // ¬(str ∈ R) ≡ str ∈ complement(R): store as a positive membership - // so the Nielsen graph sees it uniformly; the original negative literal - // is kept in mem_source for conflict reporting. - expr_ref re_compl(m_seq.re.mk_complement(re), m); - euf::snode* sn_re_compl = get_snode(re_compl.get()); - m_state.add_str_mem(sn_str, sn_re_compl, lit); + else if (m_seq.str.is_suffix(e)) { + if (is_true) + m_axioms.suffix_true_axiom(e); + else + m_axioms.suffix_axiom(e); } - ctx.push_trail(restore_vector(m_prop_queue)); - m_prop_queue.push_back({prop_item::pos_mem_prop, idx}); - - TRACE(seq, tout << "nseq assign_eh: " << (is_true ? "" : "¬") - << "str.in_re " - << mk_bounded_pp(s, m, 3) << " in " - << mk_bounded_pp(re, m, 3) << "\n";); + else if (m_seq.str.is_contains(e)) { + if (is_true) + m_axioms.contains_true_axiom(e); + else + m_axioms.unroll_not_contains(e); + } + else if (m_seq.str.is_lt(e) || m_seq.str.is_le(e)) { + // axioms added via relevant_eh → dequeue_axiom + } + else if (m_seq.is_skolem(e) || + m_seq.str.is_nth_i(e) || + m_seq.str.is_nth_u(e) || + m_seq.str.is_is_digit(e) || + m_seq.str.is_foldl(e) || + m_seq.str.is_foldli(e)) { + // no-op: handled by other mechanisms + } + else if (is_app(e) && to_app(e)->get_family_id() == m_seq.get_family_id()) + push_unhandled_pred(); } // ----------------------------------------------------------------------- @@ -266,15 +287,13 @@ namespace smt { return; ctx.push_trail(value_trail(m_prop_qhead)); while (m_prop_qhead < m_prop_queue.size() && !ctx.inconsistent()) { - auto [k, idx] = m_prop_queue[m_prop_qhead++]; - switch (k) { - case prop_item::eq_prop: - propagate_eq(idx); - break; - case prop_item::pos_mem_prop: - propagate_pos_mem(idx); - break; - } + auto const& item = m_prop_queue[m_prop_qhead++]; + if (std::holds_alternative(item)) + propagate_eq(std::get(item).idx); + else if (std::holds_alternative(item)) + propagate_pos_mem(std::get(item).idx); + else if (std::holds_alternative(item)) + dequeue_axiom(std::get(item).e); } } @@ -324,6 +343,75 @@ namespace smt { ctx.internalize(len, false); } + // ----------------------------------------------------------------------- + // Axiom enqueue / dequeue (follows theory_seq::enque_axiom / deque_axiom) + // ----------------------------------------------------------------------- + + void theory_nseq::enqueue_axiom(expr* e) { + if (m_axiom_set.contains(e)) + return; + m_axiom_set.insert(e); + ctx.push_trail(insert_obj_trail(m_axiom_set, e)); + ctx.push_trail(restore_vector(m_prop_queue)); + m_prop_queue.push_back(axiom_item{e}); + } + + void theory_nseq::dequeue_axiom(expr* n) { + TRACE(seq, tout << "dequeue_axiom: " << mk_bounded_pp(n, m, 2) << "\n";); + if (m_seq.str.is_length(n)) + m_axioms.length_axiom(n); + else if (m_seq.str.is_index(n)) + m_axioms.indexof_axiom(n); + else if (m_seq.str.is_last_index(n)) + m_axioms.last_indexof_axiom(n); + else if (m_seq.str.is_replace(n)) + m_axioms.replace_axiom(n); + else if (m_seq.str.is_replace_all(n)) + m_axioms.replace_all_axiom(n); + else if (m_seq.str.is_extract(n)) + m_axioms.extract_axiom(n); + else if (m_seq.str.is_at(n)) + m_axioms.at_axiom(n); + else if (m_seq.str.is_nth_i(n)) + m_axioms.nth_axiom(n); + else if (m_seq.str.is_itos(n)) + m_axioms.itos_axiom(n); + else if (m_seq.str.is_stoi(n)) + m_axioms.stoi_axiom(n); + else if (m_seq.str.is_lt(n)) + m_axioms.lt_axiom(n); + else if (m_seq.str.is_le(n)) + m_axioms.le_axiom(n); + else if (m_seq.str.is_unit(n)) + m_axioms.unit_axiom(n); + else if (m_seq.str.is_is_digit(n)) + m_axioms.is_digit_axiom(n); + else if (m_seq.str.is_from_code(n)) + m_axioms.str_from_code_axiom(n); + else if (m_seq.str.is_to_code(n)) + m_axioms.str_to_code_axiom(n); + } + + void theory_nseq::relevant_eh(app* n) { + if (m_seq.str.is_length(n) || + m_seq.str.is_index(n) || + m_seq.str.is_last_index(n) || + m_seq.str.is_replace(n) || + m_seq.str.is_replace_all(n)|| + m_seq.str.is_extract(n) || + m_seq.str.is_at(n) || + m_seq.str.is_nth_i(n) || + m_seq.str.is_itos(n) || + m_seq.str.is_stoi(n) || + m_seq.str.is_lt(n) || + m_seq.str.is_le(n) || + m_seq.str.is_unit(n) || + m_seq.str.is_is_digit(n) || + m_seq.str.is_from_code(n) || + m_seq.str.is_to_code(n)) + enqueue_axiom(n); + } + // ----------------------------------------------------------------------- // Final check: build Nielsen graph and search // ----------------------------------------------------------------------- diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 7c107de57..f9a40ea12 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -19,6 +19,7 @@ Author: --*/ #pragma once +#include #include "ast/seq_decl_plugin.h" #include "ast/rewriter/seq_rewriter.h" #include "ast/rewriter/seq_axioms.h" @@ -51,13 +52,16 @@ namespace smt { seq::seq_regex m_regex; // regex membership pre-processing seq_model m_model; // model construction helper - // propagation queue - struct prop_item { - enum kind_t { eq_prop, pos_mem_prop } m_kind; - unsigned m_idx; - }; - svector m_prop_queue; - unsigned m_prop_qhead = 0; + // propagation queue items (variant over the distinct propagation cases) + struct eq_item { unsigned idx; }; // string equality at index idx in str_eqs + struct mem_item { unsigned idx; }; // regex membership at index idx in str_mems + struct axiom_item { expr* e; }; // structural axiom for term e + + using prop_item = std::variant; + + vector m_prop_queue; + unsigned m_prop_qhead = 0; + obj_hashtable m_axiom_set; // dedup guard for axiom_item enqueues // statistics unsigned m_num_conflicts = 0; @@ -92,6 +96,7 @@ namespace smt { void propagate() override; void init() override; void assign_eh(bool_var v, bool is_true) override; + void relevant_eh(app* n) override; final_check_status final_check_eh(unsigned) override; void push_scope_eh() override; void pop_scope_eh(unsigned num_scopes) override; @@ -114,6 +119,8 @@ namespace smt { // propagation dispatch helpers void propagate_eq(unsigned idx); void propagate_pos_mem(unsigned idx); + void enqueue_axiom(expr* e); + void dequeue_axiom(expr* e); void ensure_length_var(expr* e); // higher-order term unfolding