From 6b5401ef68d4cb95c937301032d0c3d166ab1c87 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 22 Mar 2026 12:05:24 -0700 Subject: [PATCH] Remove s_other from snode_kind; unify under s_var and is_var() (#9087) * remove s_other, use s_var and is_var() instead Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/d56594ed-7f7e-436a-a4b2-e6dc986b18a8 * fix build: add reset() override to test dummy solver stubs Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/d437376d-55d8-4087-baf1-e89451d2d597 --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/euf/euf_sgraph.cpp | 9 ++++----- src/ast/euf/euf_snode.h | 5 ++--- src/smt/seq/seq_nielsen.cpp | 2 +- src/smt/seq/seq_nielsen.h | 2 +- src/smt/seq/seq_regex.cpp | 4 ++-- src/test/nseq_basic.cpp | 1 + src/test/nseq_zipt.cpp | 2 ++ src/test/seq_nielsen.cpp | 2 ++ src/test/seq_parikh.cpp | 1 + 9 files changed, 16 insertions(+), 12 deletions(-) diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp index 1a22312d8..f7eba5694 100644 --- a/src/ast/euf/euf_sgraph.cpp +++ b/src/ast/euf/euf_sgraph.cpp @@ -46,7 +46,7 @@ namespace euf { snode_kind sgraph::classify(expr* e) const { if (!is_app(e)) - return snode_kind::s_other; + return snode_kind::s_var; if (m_seq.str.is_empty(e)) return snode_kind::s_empty; @@ -55,7 +55,7 @@ namespace euf { zstring s; if (m_seq.str.is_string(e, s) && s.empty()) return snode_kind::s_empty; - return snode_kind::s_other; + return snode_kind::s_var; } if (m_seq.str.is_concat(e) || m_seq.re.is_concat(e)) @@ -108,7 +108,7 @@ namespace euf { if (m_seq.is_seq(e->get_sort()) && (is_uninterp(e) || m_seq.is_skolem(e))) return snode_kind::s_var; - return snode_kind::s_other; + return snode_kind::s_var; } void sgraph::compute_metadata(snode* n) { @@ -376,7 +376,7 @@ namespace euf { // recursively register children // for seq/re children, create classified snodes - // for other children (e.g. integer exponents), create s_other snodes + // for other children, e.g. integer exponents, create s_var snodes snode_vector child_nodes; for (unsigned i = 0; i < arity; ++i) { expr* ch = a->get_arg(i); @@ -751,7 +751,6 @@ namespace euf { case snode_kind::s_range: return "range"; case snode_kind::s_to_re: return "to_re"; case snode_kind::s_in_re: return "in_re"; - case snode_kind::s_other: return "other"; } return "?"; }; diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h index cca7ccce8..6313d637e 100644 --- a/src/ast/euf/euf_snode.h +++ b/src/ast/euf/euf_snode.h @@ -53,12 +53,11 @@ namespace euf { s_range, // character range [lo,hi] (OP_RE_RANGE) s_to_re, // string to regex (OP_SEQ_TO_RE) s_in_re, // regex membership (OP_SEQ_IN_RE) - s_other, // other sequence expression not directly classified }; class snode { expr* m_expr = nullptr; - snode_kind m_kind = snode_kind::s_other; + snode_kind m_kind = snode_kind::s_var; unsigned m_id = UINT_MAX; unsigned m_num_args = 0; @@ -114,7 +113,7 @@ namespace euf { bool is_empty() const { return m_kind == snode_kind::s_empty; } bool is_char() const { return m_kind == snode_kind::s_char; } - bool is_var() const { return m_kind == snode_kind::s_var || m_kind == snode_kind::s_other; } + bool is_var() const { return m_kind == snode_kind::s_var; } bool is_unit() const { return m_kind == snode_kind::s_unit; } bool is_char_or_unit() const { return m_kind == snode_kind::s_char || m_kind == snode_kind::s_unit; diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index a26fe5342..a19b52117 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -2666,7 +2666,7 @@ namespace seq { // Variables and powers have symbolic/unknown length. if (tok->is_var() || tok->is_power()) return true; - // For s_other: check if it's a string literal (known constant length). + // For s_var string literals: check if it's a string literal (known constant length). if (tok->get_expr()) { seq_util& seq = m_sg.get_seq_util(); zstring s; diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index cf233df0a..927e39e1e 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -685,7 +685,7 @@ namespace seq { // true if all str_eqs are trivial and there are no str_mems bool is_satisfied() const; - // true if any constraint has opaque (s_other) terms that + // true if any constraint has opaque (s_var) terms that // the Nielsen graph cannot decompose bool has_opaque_terms() const; diff --git a/src/smt/seq/seq_regex.cpp b/src/smt/seq/seq_regex.cpp index 626e49311..0a8eca302 100644 --- a/src/smt/seq/seq_regex.cpp +++ b/src/smt/seq/seq_regex.cpp @@ -517,11 +517,11 @@ namespace seq { // Only handle ground regexes; non-ground can't be fully explored if (!re->is_ground()) return l_undef; - // s_other snodes (unrecognized regex kinds, e.g. re.+) cannot be + // s_var snodes (unrecognized regex kinds, e.g. re.+) cannot be // efficiently explored: the alphabet partition is trivially {∅} and // derivative computations may be slow. Report l_undef and let the // caller fall back to a more capable procedure. - if (re->kind() == euf::snode_kind::s_other) + if (re->is_var()) return l_undef; // BFS over the Brzozowski derivative automaton. diff --git a/src/test/nseq_basic.cpp b/src/test/nseq_basic.cpp index 4c7c95b81..6ebcdc018 100644 --- a/src/test/nseq_basic.cpp +++ b/src/test/nseq_basic.cpp @@ -27,6 +27,7 @@ public: void push() override {} void pop(unsigned) override {} void assert_expr(expr*) override {} + void reset() override {} lbool check() override { return l_true; } }; diff --git a/src/test/nseq_zipt.cpp b/src/test/nseq_zipt.cpp index b7be6317d..6a80b9e8c 100644 --- a/src/test/nseq_zipt.cpp +++ b/src/test/nseq_zipt.cpp @@ -35,6 +35,7 @@ public: void push() override {} void pop(unsigned) override {} void assert_expr(expr*) override {} + void reset() override {} lbool check() override { return l_true; } }; @@ -47,6 +48,7 @@ public: void push() override {} void pop(unsigned) override {} void assert_expr(expr*) override {} + void reset() override {} lbool check() override { return l_true; } }; diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp index 7e8fd786f..9db2a6c1e 100644 --- a/src/test/seq_nielsen.cpp +++ b/src/test/seq_nielsen.cpp @@ -28,6 +28,7 @@ public: void push() override {} void pop(unsigned n) override {} void assert_expr(expr *e) override {} + void reset() override {} lbool check() override { return l_true; } @@ -3269,6 +3270,7 @@ public: void push() override { ++push_count; } void pop(unsigned n) override { pop_count += n; } void assert_expr(expr* e) override { asserted.push_back(expr_ref(e, m)); } + void reset() override { reset_tracking(); } lbool check() override { return check_result; } void reset_tracking() { asserted.reset(); diff --git a/src/test/seq_parikh.cpp b/src/test/seq_parikh.cpp index 72f65a0aa..62af7535c 100644 --- a/src/test/seq_parikh.cpp +++ b/src/test/seq_parikh.cpp @@ -43,6 +43,7 @@ public: void push() override {} void pop(unsigned) override {} void assert_expr(expr*) override {} + void reset() override {} lbool check() override { return l_true; } };