Refine sequence membership length pruning

Port the reverted PR #10389 length abstraction into the dedicated length-constraint plugin. Propagate lower bounds through concatenations and repeated variables before comparing against regex maximum lengths, and preserve all participating dependencies in the unsat core.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot-Session: 50bd7da9-7958-4348-8d12-e3be026b4d3f

src/ast/rewriter/seq_membership_length_constraints.cpp

@@ -16,17 +16,113 @@ Abstract:
 
 namespace seq {
 
+bool membership_length_constraints::is_var(expr* term) const {
+    return m_is_var ? m_is_var(term) : is_uninterp(term);
+}
+
+bool membership_length_constraints::length_interval(expr* regex, unsigned& lo, unsigned& hi) const {
+    auto& re = m_rw.u().re;
+    expr* body = nullptr, *head = nullptr, *tail = nullptr;
+    unsigned lower = 0, upper = 0;
+    if (re.is_full_char(regex)) {
+        lo = hi = 1;
+        return true;
+    }
+    if (re.is_epsilon(regex)) {
+        lo = hi = 0;
+        return true;
+    }
+    if (re.is_loop(regex, body, lower, upper) && re.is_full_char(body)) {
+        lo = lower;
+        hi = upper;
+        return true;
+    }
+    if (!re.is_concat(regex, head, tail) || !re.is_full_seq(tail))
+        return false;
+    if (re.is_full_char(head)) {
+        lo = 1;
+        hi = UINT_MAX;
+        return true;
+    }
+    if (re.is_loop(head, body, lower, upper) && re.is_full_char(body) && lower == upper) {
+        lo = lower;
+        hi = UINT_MAX;
+        return true;
+    }
+    return false;
+}
+
 lbool membership_length_constraints::check(constraint_vector const& constraints) {
     m_core.reset();
+    obj_map<expr, unsigned> lo_bounds;
+    obj_map<expr, void*> lo_dependencies;
+    for (auto const& [term, regex, dependency] : constraints) {
+        unsigned lo = 0, hi = 0, current = 0;
+        if (length_interval(regex, lo, hi) && lo > 0 &&
+            (!lo_bounds.find(term.get(), current) || lo > current)) {
+            lo_bounds.insert(term.get(), lo);
+            lo_dependencies.insert(term.get(), dependency);
+        }
+    }
+
+    auto add_dependency = [&](void* dependency) {
+        if (!dependency)
+            return;
+        for (void* existing : m_core)
+            if (existing == dependency)
+                return;
+        m_core.push_back(dependency);
+    };
+
+    std::function<bool(expr*, unsigned&)> min_length = [&](expr* term, unsigned& result) {
+        auto& str = m_rw.u().str;
+        if (str.is_concat(term)) {
+            result = 0;
+            for (expr* arg : *to_app(term)) {
+                unsigned arg_length = 0;
+                if (!min_length(arg, arg_length))
+                    return false;
+                result = add_truncate(result, arg_length);
+            }
+            return true;
+        }
+        if (str.is_empty(term)) {
+            result = 0;
+            return true;
+        }
+        zstring value;
+        if (str.is_string(term, value)) {
+            result = value.length();
+            return true;
+        }
+        expr* element = nullptr;
+        if (str.is_unit(term, element) && m_rw.m().is_value(element)) {
+            result = 1;
+            return true;
+        }
+        if (!is_var(term))
+            return false;
+        result = 0;
+        if (lo_bounds.find(term, result) && result > 0) {
+            void* dependency = nullptr;
+            if (lo_dependencies.find(term, dependency))
+                add_dependency(dependency);
+        }
+        return true;
+    };
+
     for (auto const& [term, regex, dependency] : constraints) {
-        unsigned min_length = m_rw.u().str.min_length(term);
         unsigned max_length = m_rw.u().re.max_length(regex);
-        if (min_length <= max_length)
+        if (max_length == UINT_MAX)
             continue;
-        if (dependency)
-            m_core.push_back(dependency);
+        m_core.reset();
+        unsigned lower = 0;
+        if (!min_length(term, lower) || lower <= max_length)
+            continue;
+        add_dependency(dependency);
         return l_false;
     }
+    m_core.reset();
     return l_true;
 }
 

src/ast/rewriter/seq_membership_length_constraints.h

@@ -15,6 +15,7 @@ Abstract:
 #include "ast/ast.h"
 #include "util/lbool.h"
 #include "util/vector.h"
+#include <functional>
 #include <tuple>
 
 class seq_rewriter;
@@ -29,10 +30,16 @@ public:
 private:
     seq_rewriter& m_rw;
     ptr_vector<void> m_core;
+    std::function<bool(expr*)> m_is_var;
+
+    bool is_var(expr* term) const;
+    bool length_interval(expr* regex, unsigned& lo, unsigned& hi) const;
 
 public:
     explicit membership_length_constraints(seq_rewriter& rw) : m_rw(rw) {}
 
+    void set_is_var(std::function<bool(expr*)> const& is_var) { m_is_var = is_var; }
+
     // Return l_false when the constraints are inconsistent and populate core().
     // Return l_true when no contradiction was found.
     lbool check(constraint_vector const& constraints);

src/ast/rewriter/seq_monadic.h

@@ -288,6 +288,7 @@ public:
 
     void set_is_var(std::function<bool(expr *)> const &is_var) {
         m_is_var = is_var;
+        m_length_constraints.set_is_var(is_var);
     }
 
     // Assert a membership  (term in regex)  to be decided jointly by the next check().

src/test/seq_monadic.cpp

@@ -783,19 +783,20 @@ public:
             ms.push_back(std::make_pair((expr*)x.get(), (expr*)aP.get()));        // 2: x in a+
             check_core("z in a* (& x in b* & x in a+)", ms, std::set<unsigned>{1, 2});
         }
-        // The term's syntactic minimum length exceeds the regex's finite maximum.
+        // Lower bounds on repeated variables refine the compound term's minimum length.
         {
             m_trail.push_scope();
-            m_mon.add(sword("aa"), word("a"), m_dm.mk_leaf(0));
-            m_mon.add(y, dotstar(), m_dm.mk_leaf(1));
+            m_mon.add_lo(x, 3, m_dm.mk_leaf(0));
+            m_mon.add_hi(t_xax, 5, m_dm.mk_leaf(1));
+            m_mon.add(y, dotstar(), m_dm.mk_leaf(2));
             lbool got = m_mon.check();
             std::set<unsigned> ids;
             core_ids(ids);
             m_trail.pop_scope(1);
-            bool ok = got == l_false && ids == std::set<unsigned>{0};
+            bool ok = got == l_false && ids == std::set<unsigned>{0, 1};
             if (!ok) ++m_fail;
             std::cout << (ok ? "  OK   " : "  FAIL ")
-                      << "minimum sequence length exceeds maximum regex length\n";
+                      << "refined minimum sequence length exceeds maximum regex length\n";
         }
 
         std::cout << "=== seq_monadic: " << (m_fail == 0 ? "ALL PASS" : "FAILURES") << " ("