From 4fb6b906309a435ffde8bab7ce96cc5a8a6b1403 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Aug 2026 10:16:55 -0700 Subject: [PATCH] Use expr refs for seq monadic atoms Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 1a1a0632-f993-4bee-b4f8-a87f960836a1 --- src/ast/rewriter/seq_monadic.cpp | 21 +++++++++------------ src/ast/rewriter/seq_monadic.h | 13 ++++++++++--- 2 files changed, 19 insertions(+), 15 deletions(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 95fd2e5f19..42fa1376f7 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -24,7 +24,6 @@ TODOs: - create a validation harness: expose certificates for correctness that can be checked. - extend with lower and upper bound constraints - consider using expr_ref as alternative to pinned expressions - - change type of atom to use expr_ref and avoid pin. svector -> vector. - revisit parse_term and "the_var" condition. A sequence of units should be allowed. - support units of non-values (element variables). Model construction would assign values to the elements. @@ -262,7 +261,7 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w return l_false; } -bool seq_monadic::parse_term(expr* t, svector& atoms, expr*& the_var) { +bool seq_monadic::parse_term(expr* t, vector& atoms, expr*& the_var) { if (u().str.is_concat(t)) return all_of(*to_app(t), [&](expr* arg) { return parse_term(arg, atoms, the_var); }); if (u().str.is_empty(t)) @@ -271,16 +270,14 @@ bool seq_monadic::parse_term(expr* t, svector& atoms, expr*& the_var) { if (u().str.is_string(t, s)) { for (unsigned i = 0; i < s.length(); ++i) { expr* elem = u().str.mk_char(s, i); - m_pin.push_back(elem); - atoms.push_back(atom{ false, nullptr, elem }); + atoms.push_back(atom(m, false, nullptr, elem)); } return true; } if (u().str.is_unit(t)) { // seq.unit of a constant element expr* elem = to_app(t)->get_arg(0); if (m.is_value(elem)) { - m_pin.push_back(elem); - atoms.push_back(atom{ false, nullptr, elem }); + atoms.push_back(atom(m, false, nullptr, elem)); return true; } return false; // symbolic (non-constant) unit: unsupported @@ -288,13 +285,13 @@ bool seq_monadic::parse_term(expr* t, svector& atoms, expr*& the_var) { // uninterpreted 0-ary constant of sequence sort => a sequence variable if (is_uninterp_const(t)) { the_var = t; // mark that at least one variable occurs - atoms.push_back(atom{ true, t, nullptr }); + atoms.push_back(atom(m, true, t, nullptr)); return true; } return false; } -bool seq_monadic::decompose(svector const& atoms, unsigned i, expr* R, +bool seq_monadic::decompose(vector const& atoms, unsigned i, expr* R, vector& out) { if (m_giveup) return false; @@ -309,12 +306,12 @@ bool seq_monadic::decompose(svector const& atoms, unsigned i, expr* R, } atom const& a = atoms[i]; if (!a.is_var) { - expr_ref d = der_elem(R, a.elem); + expr_ref d = der_elem(R, a.elem.get()); return decompose(atoms, i + 1, d, out); } if (i + 1 == atoms.size()) { // last atom: membership component a.var in R disjunct D; - D.push_back(component{ a.var, R, nullptr }); + D.push_back(component{ a.var.get(), R, nullptr }); out.push_back(D); return true; } @@ -331,7 +328,7 @@ bool seq_monadic::decompose(svector const& atoms, unsigned i, expr* R, if (out.size() > DISJUNCT_CAP || m_budget == 0) { m_giveup = true; return false; } --m_budget; disjunct D(sd); - D.push_back(component{ a.var, R, q }); // reach component: a.var drives R -> q + D.push_back(component{ a.var.get(), R, q }); // reach component: a.var drives R -> q out.push_back(D); } } @@ -376,7 +373,7 @@ bool seq_monadic::build_membership_dnf(expr* term, expr* R, vector& dn return false; if (!u().is_seq(m_seq_sort, m_elem_sort)) return false; - svector atoms; + vector atoms; expr* the_var = nullptr; if (!parse_term(term, atoms, the_var)) return false; diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 610c6687c3..d7ce921e6e 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -92,7 +92,14 @@ private: seq_util::rex& re() const { return m_rw.u().re; } // A term atom: a sequence variable or a constant element (a value of the element sort). - struct atom { bool is_var; expr* var; expr* elem; }; + struct atom { + bool is_var; + expr_ref var; + expr_ref elem; + + atom(ast_manager& m, bool is_var, expr* var, expr* elem) : + is_var(is_var), var(var, m), elem(elem, m) {} + }; // A component of one variable's constraint. As the variable's value w is read, // the current state is derived from `state`; the component accepts when @@ -126,11 +133,11 @@ private: lbool product_nonempty(svector const& comps, expr_ref* witness_word = nullptr); // Flatten a str.++ term into atoms; false on an unsupported shape (non-constant unit). - bool parse_term(expr* term, svector& atoms, expr*& the_var); + bool parse_term(expr* term, vector& atoms, expr*& the_var); // Monadic decomposition: append to `out` the DNF disjuncts for atoms[i..] in R, // threading the current derivative state R. Returns false on give-up. - bool decompose(svector const& atoms, unsigned i, expr* R, + bool decompose(vector const& atoms, unsigned i, expr* R, vector& out); // Drop disjuncts with a syntactically-empty component and dedup identical disjuncts.