Monadic refine (#10389)

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9

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<std::tuple<expr_ref, expr_ref, void*>>& m_v;
+        unsigned m_idx;
+        expr_ref m_old;
+    public:
+        set_term_trail(vector<std::tuple<expr_ref, expr_ref, void*>>& 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<atom> atoms;
+    return parse_term(term, atoms);
+}
+
 void seq_monadic::add_lo(expr* term, unsigned lo, void* d) {
     if (lo == 0)
         return;

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);
 

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<theory_seq::dependency*>(deps),
+                                   static_cast<theory_seq::dependency*>(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<unsigned>(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<expr>& 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<expr> 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<candidate_bound>& 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<expr> 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<expr, expr*> const& model = m_monadic.get_model();
+        ptr_vector<expr> 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<size_t>(dep);
-        if ((enc & 1) == 0) {                     // even: monadic membership literal
-            lits.push_back(to_literal(static_cast<int>(enc >> 1)));
+        if ((enc & 1) == 0) {                     // even: a monadic membership (by index)
+            monadic_membership const& mem = m_monadic_memberships[static_cast<unsigned>((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<theory_seq::dependency*>(deps),
+                                       static_cast<theory_seq::dependency*>(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<candidate_bound> 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<theory_seq::dependency*>(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<theory_seq::dependency*>(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;

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<monadic_membership>         m_monadic_memberships;
         svector<monadic_assumption>        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<candidate_bound>& 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<expr>& 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<void*>(static_cast<size_t>(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<void*>(static_cast<size_t>(2 * (idx + 1)));
         }
         static void* dep_of_bound(unsigned idx) {
             return reinterpret_cast<void*>(static_cast<size_t>(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;