From 26c5a11e179c8b685f554d590a53d789d4b008c8 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Wed, 5 Aug 2026 13:27:00 -0700 Subject: [PATCH] Monadic refine (#10389) Co-authored-by: Nikolaj Bjorner Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9 --- src/ast/rewriter/seq_monadic.cpp | 36 +++++ src/ast/rewriter/seq_monadic.h | 12 ++ src/smt/seq_regex.cpp | 248 ++++++++++++++++++++++++++++--- src/smt/seq_regex.h | 85 +++++++++-- 4 files changed, 347 insertions(+), 34 deletions(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index c2fb368698..baa3d9a297 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -591,6 +591,42 @@ void seq_monadic::add(expr* term, expr* regex, void* d) { m_undo_trail.push(push_back_vector(m_memberships)); } +namespace { + // Restores a membership term on backtrack. The previous term is pinned by this trail + // object's own expr_ref and released in undo() (the trail region does not run + // destructors, mirroring obj_ref_trail). + class set_term_trail : public trail { + vector>& m_v; + unsigned m_idx; + expr_ref m_old; + public: + set_term_trail(vector>& v, unsigned idx, expr* old, ast_manager& m): + m_v(v), m_idx(idx), m_old(old, m) {} + void undo() override { + std::get<0>(m_v[m_idx]) = m_old; + m_old.reset(); + } + }; +} + +void seq_monadic::set_term(void* d, expr* term) { + for (unsigned i = 0; i < m_memberships.size(); ++i) { + if (std::get<2>(m_memberships[i]) != d) + continue; + expr_ref& t = std::get<0>(m_memberships[i]); + if (t.get() == term) + return; + m_undo_trail.push(set_term_trail(m_memberships, i, t, m)); + t = term; + return; + } +} + +bool seq_monadic::can_decide_term(expr* term) { + vector atoms; + return parse_term(term, atoms); +} + void seq_monadic::add_lo(expr* term, unsigned lo, void* d) { if (lo == 0) return; diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 136555f0a3..02c41a43e1 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -282,6 +282,18 @@ public: // Memberships remain asserted until the constructor-provided trail is popped. void add(expr* term, expr* regex, void* d); + // Replace the decided term of the membership carrying dependency `d` with `term` + // (trailed, so the previous term is restored on pop). Used to re-decide a membership + // over the current expansion of its term once theory_seq's equalities define it as a + // concatenation. No-op if no membership carries `d`. + void set_term(void* d, expr* term); + + // True if `term` is in the shape the solver can decide: a concatenation of string + // constants, epsilon, seq.unit of constant elements, and sequence variables. Callers + // that rewrite a term before add()/set_term() (e.g. by expanding it through equalities) + // can use this to avoid feeding a form that would only make check() bail. + bool can_decide_term(expr* term); + // Assert that `term` has at least `lo` elements. A zero lower bound is a no-op. void add_lo(expr* term, unsigned lo, void* d); diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 448bde4399..66c22ed87f 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -44,42 +44,203 @@ namespace smt { arith_util& seq_regex::a() { return th.m_autil; } void seq_regex::rewrite(expr_ref& e) { th.m_rewrite(e); } + expr_ref seq_regex::expand_shallow(expr* e, void*& deps, unsigned depth) { + expr* elem = nullptr; + if (depth > 40) + return expr_ref(e, m); // guard against pathological chains + if (str().is_concat(e)) { + expr_ref_vector args(m); + for (expr* arg : *to_app(e)) + args.push_back(expand_shallow(arg, deps, depth + 1)); + return expr_ref(str().mk_concat(args, e->get_sort()), m); + } + if (str().is_empty(e) || str().is_string(e)) + return expr_ref(e, m); // parseable constant leaf + if (str().is_unit(e, elem) && m.is_value(elem)) + return expr_ref(e, m); // seq.unit of a constant element + // A variable or a defined term: substitute through the solution map, but only keep + // the substitution if it stays monadic-decidable. A free variable whose only + // definition is its seq.unit(nth ..) length representation is thus kept atomic. + theory_seq::dependency* d = nullptr; + expr* r = th.m_rep.find(e, d); + if (r == e) + return expr_ref(e, m); // no defining equation: atomic leaf + void* sub = d; + expr_ref er = expand_shallow(r, sub, depth + 1); + if (m_monadic.can_decide_term(er)) { + deps = th.m_dm.mk_join(static_cast(deps), + static_cast(sub)); + return er; + } + return expr_ref(e, m); // keep atomic; drop the polluted expansion + } + + expr_ref seq_regex::compute_expansion(expr* s, void*& dep) { + dep = nullptr; + // Prefer full canonization: it collapses a variable defined by a word equation + // (and any variable pinned to a constant) down to constants/variables, which is + // what lets the monadic solver decide the real structure. If that yields a form + // the solver cannot decide -- typically because theory_seq has replaced a free + // variable by its seq.unit(nth ..) length representation -- fall back to a shallow + // expansion that keeps such variables atomic, and finally to the atomic term. + theory_seq::dependency* cdep = nullptr; + expr_ref full(m); + if (th.canonize(s, cdep, full) && full && m_monadic.can_decide_term(full)) { + dep = cdep; + return full; + } + void* sdep = nullptr; + expr_ref shallow = expand_shallow(s, sdep, 0); + if (shallow && m_monadic.can_decide_term(shallow)) { + dep = sdep; + return shallow; + } + dep = nullptr; + return expr_ref(s, m); + } + void seq_regex::add_monadic_membership(literal lit, expr* s, expr* r) { for (auto const& membership : m_monadic_memberships) if (membership.m_lit == lit) return; - m_monadic_memberships.push_back(monadic_membership(m, lit, s, r)); + // Decide the membership over the concatenation of variables/constants that define s + // (see compute_expansion) rather than over the atomic term s. Deciding s atomically + // yields witnesses that ignore s's defining word equation (e.g. x = x8 ++ "/" ++ s9), + // which then conflict on assume_eq and livelock. The equalities used are captured in + // `dep` and folded into any unsat core for soundness. + void* dep = nullptr; + expr_ref s_expanded = compute_expansion(s, dep); + unsigned idx = m_monadic_memberships.size(); + m_monadic_memberships.push_back(monadic_membership(m, lit, s, r, s_expanded, dep)); ctx.push_trail(push_back_vector(m_monadic_memberships)); - m_monadic.add(s, r, dep_of_literal(lit)); + m_monadic.add(s_expanded, r, dep_of_membership(idx)); ctx.push_trail(value_trail(m_monadic_generation)); ++m_monadic_generation; TRACE(seq_regex, tout << "monadic add " << lit << ": " - << mk_pp(s, m) << " in " << mk_pp(r, m) << "\n";); + << mk_pp(s_expanded, m) << " in " << mk_pp(r, m) << "\n";); } - void seq_regex::add_monadic_bounds() { + void seq_regex::refresh_expansions() { + for (unsigned idx = 0; idx < m_monadic_memberships.size(); ++idx) { + monadic_membership& mem = m_monadic_memberships[idx]; + void* dep = nullptr; + expr_ref s_expanded = compute_expansion(mem.m_s, dep); + // Always resync: m_s_expanded/m_dep are not trailed, so after a backtrack they + // may be stale while the monadic term (which IS trailed) was restored. + // set_term itself no-ops when the monadic term already matches. + mem.m_s_expanded = s_expanded; + mem.m_dep = dep; + m_monadic.set_term(dep_of_membership(idx), s_expanded); + TRACE(seq_regex, tout << "monadic expand " << mk_pp(mem.m_s, m) + << " -> " << mk_pp(s_expanded, m) << "\n";); + } + } + + void seq_regex::collect_vars(expr* s, ptr_vector& vars) { + // View s as a concatenation of string constants and variables (the same shape the + // monadic solver decomposes internally) and gather the distinct variables. + ptr_vector todo; + todo.push_back(s); + while (!todo.empty()) { + expr* t = todo.back(); + todo.pop_back(); + if (str().is_concat(t)) { + for (expr* arg : *to_app(t)) + todo.push_back(arg); + continue; + } + if (th.is_var(t) && !vars.contains(t)) + vars.push_back(t); + } + } + + void seq_regex::collect_candidate_bounds(vector& out) { // add_lo/add_hi/add_len build a length regex .{lo}.* / .{0,hi} / .{len}; keep the // bound small so the extra membership never itself blows past the monadic solver's // state cap (a too-large bound would only turn a solvable case into a give-up). const unsigned MAX_BOUND = 1000; - for (auto const& mem : m_monadic_memberships) { - expr* s = mem.m_s; - expr_ref len = th.mk_len(s); + // Record whatever arithmetic length bounds currently hold for term t as candidate + // length regexes for the monadic solver. + auto add_term = [&](expr* t) { + expr_ref len = th.mk_len(t); rational lo, hi; bool has_lo = th.lower_bound(len, lo) && lo.is_unsigned() && lo.get_unsigned() > 0; bool has_hi = th.upper_bound(len, hi) && hi.is_unsigned(); if (has_lo && has_hi && lo == hi) { if (lo.get_unsigned() <= MAX_BOUND) - record_bound(s, len, bound_constraint::LEN, lo.get_unsigned()); - continue; + out.push_back(candidate_bound(m, t, len, bound_constraint::LEN, lo.get_unsigned())); + return; } if (has_lo && lo.get_unsigned() <= MAX_BOUND) - record_bound(s, len, bound_constraint::LO, lo.get_unsigned()); + out.push_back(candidate_bound(m, t, len, bound_constraint::LO, lo.get_unsigned())); if (has_hi && hi.get_unsigned() <= MAX_BOUND) - record_bound(s, len, bound_constraint::HI, hi.get_unsigned()); + out.push_back(candidate_bound(m, t, len, bound_constraint::HI, hi.get_unsigned())); + }; + ptr_vector vars; + for (auto const& mem : m_monadic_memberships) { + // Use the expanded term: it is what the monadic solver actually decides, so its + // variables (and their lengths) are the ones a witness must respect. Bounding + // the original atomic term would reintroduce it as a fresh monadic variable. + expr* s = mem.m_s_expanded; + // The whole-term bound constrains the sum of the atom lengths. + add_term(s); + // Decompose s into constants and variables and bound each variable directly: + // per-variable bounds prune the monadic search for that variable's value, + // whereas the whole-term bound only constrains the total length. + vars.reset(); + collect_vars(s, vars); + for (expr* v : vars) + add_term(v); } } + bool seq_regex::model_len(expr* t, unsigned& len) { + obj_map const& model = m_monadic.get_model(); + ptr_vector todo; + todo.push_back(t); + len = 0; + while (!todo.empty()) { + expr* e = todo.back(); + todo.pop_back(); + expr* a = nullptr, *b = nullptr; + zstring s; + if (str().is_concat(e, a, b)) { + todo.push_back(a); + todo.push_back(b); + continue; + } + if (str().is_empty(e)) + continue; + if (str().is_unit(e)) { + ++len; + continue; + } + if (str().is_string(e, s)) { + len += s.length(); + continue; + } + expr* w = nullptr; + if (model.find(e, w) && w != e) { // variable: replace by its witness + todo.push_back(w); + continue; + } + return false; // unassigned variable / unsupported shape + } + return true; + } + + bool seq_regex::model_satisfies_bound(candidate_bound const& cb) { + unsigned len = 0; + if (!model_len(cb.m_term, len)) + return true; // cannot evaluate -> leave to arithmetic + switch (cb.m_kind) { + case bound_constraint::LO: return len >= cb.m_value; + case bound_constraint::HI: return len <= cb.m_value; + case bound_constraint::LEN: return len == cb.m_value; + } + return true; + } + void seq_regex::record_bound(expr* s, expr* len, bound_constraint::kind_t k, unsigned v) { for (auto const& b : m_monadic_bounds) if (b.m_len.get() == len && b.m_kind == k && b.m_value == v) @@ -102,10 +263,14 @@ namespace smt { return all_of(lits, [this](literal lit) { return l_true == ctx.get_assignment(lit); }); } - void seq_regex::add_core_literal(void* dep, literal_vector& lits) { + void seq_regex::add_core_literal(void* dep, literal_vector& lits, void*& deps) { size_t enc = reinterpret_cast(dep); - if ((enc & 1) == 0) { // even: monadic membership literal - lits.push_back(to_literal(static_cast(enc >> 1))); + if ((enc & 1) == 0) { // even: a monadic membership (by index) + monadic_membership const& mem = m_monadic_memberships[static_cast((enc >> 1) - 1)]; + lits.push_back(mem.m_lit); + if (mem.m_dep) // include the equalities used to expand its term + deps = th.m_dm.mk_join(static_cast(deps), + static_cast(mem.m_dep)); return; } // odd: a length bound; materialize its justifying arithmetic literal(s) now. @@ -176,19 +341,62 @@ namespace smt { return FC_DONE; } - ++th.m_stats.m_regex_monadic_checks; - add_monadic_bounds(); - lbool result = m_monadic.check(); + // Re-canonize membership terms now that theory_seq's solution map is populated: + // a variable defined by a word equation (x = x8 ++ "/" ++ s9) is decided over its + // expanded concatenation, so the monadic witness assigns the real subvariables + // consistently instead of inventing a value for the atomic term. + refresh_expansions(); + + // Lazy length-constraint enforcement: first decide the memberships WITHOUT any + // length regexes. If the resulting model already respects every candidate length + // bound, keep it; otherwise add exactly the violated bounds and re-solve. Each + // round enforces at least one new bound (finite set), so the loop terminates. + vector candidates; + collect_candidate_bounds(candidates); + lbool result = l_undef; + unsigned guard = candidates.size() + 1; + while (true) { + ++th.m_stats.m_regex_monadic_checks; + result = m_monadic.check(); + if (result != l_true) + break; + bool progressed = false; + for (auto const& cb : candidates) { + if (model_satisfies_bound(cb)) + continue; + record_bound(cb.m_term, cb.m_len, cb.m_kind, cb.m_value); + progressed = true; + } + if (!progressed || guard-- == 0) + break; + } + if (result == l_false) { ++th.m_stats.m_regex_monadic_unsat; literal_vector lits; + void* deps = nullptr; for (void* core_dep : m_monadic.core()) - add_core_literal(core_dep, lits); - if (all_true(lits)) - th.set_conflict(nullptr, lits); + add_core_literal(core_dep, lits, deps); + if (all_true(lits)) { + // Every core literal is assigned true, so the negated core (together with the + // equalities collected while canonizing membership terms, carried in deps) is a + // legitimate theory conflict. + th.set_conflict(static_cast(deps), lits); + } else { + // Some core literal is not currently assigned true, so this is not a legitimate + // theory conflict (see #10398): raising one would justify it with non-true + // literals. Assert the blocking clause instead -- the negation of the literals + // and canonization equalities that the monadic solver refuted. for (unsigned i = 0; i < lits.size(); ++i) lits[i] = ~lits[i]; + enode_pair_vector eqs; + literal_vector dep_lits; + th.linearize(static_cast(deps), eqs, dep_lits); + for (literal l : dep_lits) + lits.push_back(~l); + for (auto const& [a, b] : eqs) + lits.push_back(~th.mk_eq(a->get_expr(), b->get_expr(), false)); th.add_axiom(lits); } return FC_CONTINUE; diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index 5a01760093..eaa68dc781 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -111,11 +111,16 @@ namespace smt { struct monadic_membership { literal m_lit; - expr_ref m_s; + expr_ref m_s; // original membership term (used for the legacy fallback) expr_ref m_re; + expr_ref m_s_expanded; // term canonized through theory_seq's equalities; this is + // what the monadic solver decides so that a variable defined + // as a concatenation is seen with its structure, not atomically + void* m_dep; // theory_seq::dependency* (as void*) for the equalities used to + // expand m_s -> m_s_expanded; folded into an unsat core - monadic_membership(ast_manager& m, literal lit, expr* s, expr* re) : - m_lit(lit), m_s(s, m), m_re(re, m) {} + monadic_membership(ast_manager& m, literal lit, expr* s, expr* re, expr* s_expanded, void* dep) : + m_lit(lit), m_s(s, m), m_re(re, m), m_s_expanded(s_expanded, m), m_dep(dep) {} }; struct monadic_assumption { @@ -136,6 +141,20 @@ namespace smt { m_len(len, m), m_kind(k), m_value(v) {} }; + // A candidate length bound (for term m_term, with length term m_len) that MAY be + // enforced on the monadic solver. final_check adds these lazily: only bounds that + // the current monadic model actually violates are turned into length regexes via + // record_bound. This avoids eagerly loading loop regexes that the model already + // respects. + struct candidate_bound { + expr_ref m_term; + expr_ref m_len; + bound_constraint::kind_t m_kind; + unsigned m_value; + candidate_bound(ast_manager& m, expr* term, expr* len, bound_constraint::kind_t k, unsigned v): + m_term(term, m), m_len(len, m), m_kind(k), m_value(v) {} + }; + seq_monadic m_monadic; vector m_monadic_memberships; svector m_monadic_assumptions; @@ -233,22 +252,60 @@ namespace smt { bool block_if_empty(expr* r, literal lit); void add_monadic_membership(literal lit, expr* s, expr* r); - // Query current arithmetic length bounds of each monadic membership term and feed - // them to the monadic solver (via add_lo/add_hi/add_len) as extra length regexes, - // so proposed witnesses respect length constraints. Recorded in m_monadic_bounds. - void add_monadic_bounds(); + // Expand a term through theory_seq's solution map, but substitute a sub-term only + // when the substitution stays monadic-decidable. In particular a free variable is + // kept atomic even after theory_seq fixes its length and represents it as a + // concatenation of seq.unit(nth v i) skolems (which the monadic solver cannot + // decide). This exposes a term's defining word-equation structure (x = a ++ v ++ b) + // without the length representation that would otherwise force a bail. Equalities + // used are accumulated into `deps` (a theory_seq::dependency*). + expr_ref expand_shallow(expr* e, void*& deps, unsigned depth); + // Choose the term the monadic solver decides for membership term s: full + // canonization when decidable, else a shallow expansion (see expand_shallow) that + // keeps length-only variables atomic, else s itself. `dep` receives the equalities + // used (a theory_seq::dependency* held as void*). + expr_ref compute_expansion(expr* s, void*& dep); + // Re-canonize each monadic membership term through theory_seq's current equalities + // and, when the expansion changed, re-point the monadic solver at the expanded term. + // Called at final_check time because the solution map is only populated during + // solving (it is empty when propagate_in_re first registers the membership). + void refresh_expansions(); + // Compute the candidate arithmetic length bounds of each monadic membership term + // -- and, by decomposing the term into a concatenation of string constants and + // variables, of each variable occurring in it. These are NOT added to the monadic + // solver; final_check enforces (via record_bound) only the ones a proposed model + // violates. + void collect_candidate_bounds(vector& out); + // Length of term t under the monadic solver's current model (variables replaced by + // their witnesses). Returns false if some variable/atom is unassigned or the shape + // is unsupported, in which case the length cannot be evaluated. + bool model_len(expr* t, unsigned& len); + // True if the current monadic model satisfies candidate bound cb (or the bound + // cannot be evaluated against the model -- length regexes only prune, so an + // unevaluable bound is left to the arithmetic solver). + bool model_satisfies_bound(candidate_bound const& cb); + // Collect the distinct sequence variables of a term viewed as a concatenation of + // string constants and variables (mirrors seq_monadic's own term decomposition). + void collect_vars(expr* s, ptr_vector& vars); void record_bound(expr* s, expr* len, bound_constraint::kind_t k, unsigned v); - // Encode a monadic membership literal / bounds-constraint index as the void* - // dependency handed to the monadic solver: 2*lit.index() for literals (even), - // 2*bounds_index + 1 for bounds constraints (odd). add_core_literal decodes a - // dependency returned by m_monadic.core() into conflict literal(s). - static void* dep_of_literal(literal lit) { - return reinterpret_cast(static_cast(2 * lit.index())); + // Encode a monadic membership index / bounds-constraint index as the void* + // dependency handed to the monadic solver. seq_monadic OMITS null dependencies + // from its unsat core, so the encoding must never produce a null pointer (in + // particular 2*idx would map membership index 0 to null and silently drop it, + // yielding an empty -- i.e. spurious global -- conflict). We therefore use + // 2*(idx+1) for memberships (even, >= 2) -- from which add_core_literal recovers + // both the in_re literal and the canonization dependency -- and 2*idx+1 for bounds + // constraints (odd, >= 1). + static void* dep_of_membership(unsigned idx) { + return reinterpret_cast(static_cast(2 * (idx + 1))); } static void* dep_of_bound(unsigned idx) { return reinterpret_cast(static_cast(2 * idx + 1)); } - void add_core_literal(void* dep, literal_vector& lits); + // Decode a dependency returned by m_monadic.core() into conflict literal(s), also + // accumulating (into deps, a theory_seq::dependency* held as void*) the equalities + // used to canonize any participating membership term. + void add_core_literal(void* dep, literal_vector& lits, void*& deps); // Whether every literal is currently assigned true, i.e. whether the negated // clause is a legitimate theory conflict. bool all_true(literal_vector const& lits) const;