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

@@ -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 "?";
         };

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;

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;

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;
 

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.

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

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

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

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