From 50f27471363e6bc01d186a7db75f1fe05ae7d640 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Aug 2026 10:27:32 -0700 Subject: [PATCH] Add sequence length constraints to seq monadic Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 1a1a0632-f993-4bee-b4f8-a87f960836a1 --- src/ast/rewriter/seq_monadic.cpp | 27 ++++++++++++++++++-- src/ast/rewriter/seq_monadic.h | 9 +++++++ src/test/seq_monadic.cpp | 44 ++++++++++++++++++++++++++++++++ 3 files changed, 78 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 42fa1376f7..2dc028e97f 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -30,8 +30,6 @@ TODOs: - encapsulate within general interface: create: undo_trail x dependency_manager x ast_manager -> regex_membership add_constraint : expr* x expr* x dependency* -> void -add_lo: expr* x unsigned * dependency* -> void -add_hi: expr* x unsigned * dependency* ->void check: void -> lbool explain: void -> dependency* model: void -> (expr* x expr*) vector or value: expr* -> expr* @@ -426,6 +424,31 @@ void seq_monadic::add(expr* term, expr* regex, u_dependency* d) { m_undo_trail.push(push_back_vector(m_memberships)); } +void seq_monadic::add_lo(expr* term, unsigned lo, u_dependency* d) { + if (lo == 0) + return; + sort* re_sort = re().mk_re(term->get_sort()); + expr_ref all_char(re().mk_full_char(re_sort), m); + expr_ref prefix(re().mk_loop_proper(all_char, lo, lo), m); + expr_ref all(re().mk_full_seq(re_sort), m); + expr_ref regex(re().mk_concat(prefix, all), m); + add(term, regex, d); +} + +void seq_monadic::add_hi(expr* term, unsigned hi, u_dependency* d) { + sort* re_sort = re().mk_re(term->get_sort()); + expr_ref all_char(re().mk_full_char(re_sort), m); + expr_ref regex(re().mk_loop_proper(all_char, 0, hi), m); + add(term, regex, d); +} + +void seq_monadic::add_len(expr* term, unsigned len, u_dependency* d) { + sort* re_sort = re().mk_re(term->get_sort()); + expr_ref all_char(re().mk_full_char(re_sort), m); + expr_ref regex(re().mk_loop_proper(all_char, len, len), m); + add(term, regex, d); +} + lbool seq_monadic::decide(vector> const& memberships) { m_model.reset(); if (memberships.empty()) diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index d7ce921e6e..4b0855de2a 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -195,6 +195,15 @@ public: // Memberships remain asserted until the constructor-provided trail is popped. void add(expr* term, expr* regex, u_dependency* d); + // Assert that `term` has at least `lo` elements. A zero lower bound is a no-op. + void add_lo(expr* term, unsigned lo, u_dependency* d); + + // Assert that `term` has at most `hi` elements. + void add_hi(expr* term, unsigned hi, u_dependency* d); + + // Assert that `term` has exactly `len` elements. + void add_len(expr* term, unsigned len, u_dependency* d); + // Decide the CONJUNCTION of all memberships asserted via add() jointly: a variable // shared across memberships is constrained consistently (the DNFs are multiplied and // each variable's constraints intersected). This is the natural extension of single- diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index 612a95dc7e..36457cb023 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -445,6 +445,50 @@ public: std::cout << (trail_ok ? " OK " : " FAIL ") << "check preserves assertions and pop removes them\n"; + std::cout << "=== seq_monadic: length bounds ===\n"; + auto check_bound = [&](char const* name, expr* regex, unsigned bound, bool is_lo, + lbool expected) { + m_trail.push_scope(); + m_mon.add(x, regex, nullptr); + if (is_lo) + m_mon.add_lo(x, bound, nullptr); + else + m_mon.add_hi(x, bound, nullptr); + lbool got = m_mon.check(); + m_trail.pop_scope(1); + bool ok = got == expected; + if (!ok) ++m_fail; + std::cout << (ok ? " OK " : " FAIL ") << name + << " got=" << s(got) << " expected=" << s(expected) << "\n"; + }; + check_bound("x in a, |x| >= 1", word("a"), 1, true, l_true); + check_bound("x in a, |x| >= 2", word("a"), 2, true, l_false); + check_bound("x in aa, |x| <= 2", word("aa"), 2, false, l_true); + check_bound("x in aa, |x| <= 1", word("aa"), 1, false, l_false); + check_bound("x in epsilon, |x| <= 0", word(""), 0, false, l_true); + auto check_len = [&](char const* name, expr* regex, unsigned len, lbool expected) { + m_trail.push_scope(); + m_mon.add(x, regex, nullptr); + m_mon.add_len(x, len, nullptr); + lbool got = m_mon.check(); + m_trail.pop_scope(1); + bool ok = got == expected; + if (!ok) ++m_fail; + std::cout << (ok ? " OK " : " FAIL ") << name + << " got=" << s(got) << " expected=" << s(expected) << "\n"; + }; + check_len("x in aa, |x| = 2", word("aa"), 2, l_true); + check_len("x in aa, |x| = 1", word("aa"), 1, l_false); + check_len("x in epsilon, |x| = 0", word(""), 0, l_true); + m_trail.push_scope(); + unsigned trail_size = m_trail.size(); + m_mon.add_lo(x, 0, m_dm.mk_leaf(0)); + bool zero_lo_ok = m_trail.size() == trail_size && m_mon.check() == l_true; + m_trail.pop_scope(1); + if (!zero_lo_ok) ++m_fail; + std::cout << (zero_lo_ok ? " OK " : " FAIL ") + << "|x| >= 0 is a no-op\n"; + // ---- unsat cores: the extracted core must contain only constraints that // ---- participate in the contradiction, not independent ones. std::cout << "=== seq_monadic: unsat cores ===\n";