From 1e507cd11e21771c999b7f0180246c244efe04ab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Aug 2026 14:41:05 -0700 Subject: [PATCH] use definition of is_var from theory_seq Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_monadic.cpp | 15 ++++++--------- src/ast/rewriter/seq_monadic.h | 9 +++++++++ src/smt/seq_regex.cpp | 4 +++- 3 files changed, 18 insertions(+), 10 deletions(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 38c7abeb06..72332cf2de 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -273,16 +273,13 @@ bool seq_monadic::parse_term(expr* t, vector& atoms, expr*& the_var) { } 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)) { - atoms.push_back(atom(m, false, nullptr, elem)); - return true; - } - return false; // symbolic (non-constant) unit: unsupported + expr *elem = nullptr; + if (u().str.is_unit(t, elem) && m.is_value(elem)) { // seq.unit of a constant element + atoms.push_back(atom(m, false, nullptr, elem)); + return true; } - // uninterpreted 0-ary constant of sequence sort => a sequence variable - if (is_uninterp_const(t)) { + // uninterpreted constant of sequence sort => a sequence variable + if (is_var(t)) { the_var = t; // mark that at least one variable occurs atoms.push_back(atom(m, true, t, nullptr)); return true; diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 2f56c6a9e1..87b3a09a26 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -88,6 +88,7 @@ private: using membership_vec = vector>; membership_vec m_memberships; // asserted (term in regex, dep) for check() ptr_vector m_core; // dependencies of an unsat subset, filled by check() on l_false + std::function m_is_var; // predicate for whether a term is a sequence variable seq_util& u() const { return m_rw.u(); } seq_util::rex& re() const { return m_rw.u().re; } @@ -162,6 +163,10 @@ private: // deletion and collect the (non-null) dependencies of its members into m_core. void minimize_core(membership_vec const& memberships); + bool is_var(expr *term) const { + return m_is_var ? m_is_var(term) : is_uninterp(term); + } + public: seq_monadic(seq_rewriter& rw, trail_stack& undo_trail, transition_mode mode = transition_mode::light_antimirov) : @@ -191,6 +196,10 @@ public: // returns the dependencies of all asserted memberships (no deletion-based shrinking). void set_min_core(bool b) { m_min_core = b; } + void set_is_var(std::function const &is_var) { + m_is_var = is_var; + } + // Assert a membership (term in regex) to be decided jointly by the next check(). // `d` carries the dependency used for unsat-core tracking and may be nullptr. // Memberships remain asserted until the constructor-provided trail is popped. diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 0109279443..b7d839b802 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -32,7 +32,9 @@ namespace smt { m(th.get_manager()), m_monadic(seq_rw(), ctx.get_trail_stack()), m_state_to_expr(m), - m_state_graph(state_graph::state_pp(this, pp_state)) { } + m_state_graph(state_graph::state_pp(this, pp_state)) { + m_monadic.set_is_var([&th](expr *e) { return th.is_var(e); }); + } seq_util& seq_regex::u() { return th.m_util; } class seq_util::rex& seq_regex::re() { return th.m_util.re; }