move seq_derive and fix include paths, remove antimirov code

src/ast/rewriter/CMakeLists.txt

@@ -40,6 +40,7 @@ z3_add_component(rewriter
     seq_axioms.cpp
     seq_eq_solver.cpp
     seq_subset.cpp
+    seq_derive.cpp
     seq_rewriter.cpp
     seq_regex_bisim.cpp
     seq_skolem.cpp

src/ast/rewriter/seq_derive.cpp

@@ -0,0 +1,679 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    seq_derive.cpp
+
+Abstract:
+
+    Symbolic derivative computation for regular expressions.
+    Produces an ITE-tree (transition regex) representation following
+    the approach of RE# (Varatalu, Veanes, Ernits - POPL 2025).
+
+    The symbolic derivative δ(r) maps each character to the resulting
+    derivative state via an ITE-tree. The free variable (:var 0) represents
+    the input character.
+
+Authors:
+
+    Nikolaj Bjorner (nbjorner) 2025-06-03
+
+--*/
+
+#include "ast/rewriter/seq_derive.h"
+#include "ast/ast_pp.h"
+#include "ast/array_decl_plugin.h"
+#include "ast/rewriter/bool_rewriter.h"
+#include <algorithm>
+
+namespace seq {
+
+    derive::derive(ast_manager& m) :
+        m(m),
+        m_util(m),
+        m_autil(m),
+        m_br(m),
+        m_trail(m),
+        m_ele(m) {
+        m_br.set_flat_and_or(false);
+    }
+
+    void derive::reset() {
+        m_cache.reset();
+        m_trail.reset();
+    }
+
+    expr_ref derive::operator()(expr* ele, expr* r) {
+        SASSERT(m_util.is_re(r));
+        m_ele = ele;
+        m_depth = 0;
+        expr_ref result = derive_rec(r);
+        m_ele = nullptr;
+        return result;
+    }
+
+    expr_ref derive::operator()(expr* r) {
+        SASSERT(m_util.is_re(r));
+        sort* seq_sort = nullptr, * ele_sort = nullptr;
+        VERIFY(m_util.is_re(r, seq_sort));
+        VERIFY(m_util.is_seq(seq_sort, ele_sort));
+        expr_ref v(m.mk_var(0, ele_sort), m);
+        return (*this)(v, r);
+    }
+
+    // -------------------------------------------------------
+    // Core derivative computation
+    // -------------------------------------------------------
+
+    expr_ref derive::derive_rec(expr* r) {
+        SASSERT(m_util.is_re(r));
+
+        // Check cache
+        expr* cached = nullptr;
+        if (m_cache.find(r, cached))
+            return expr_ref(cached, m);
+
+        // Depth check
+        if (m_depth >= m_max_depth) {
+            // Return stuck derivative (the derivative operator applied symbolically)
+            return expr_ref(re().mk_derivative(m_ele, r), m);
+        }
+
+        ++m_depth;
+        expr_ref result = derive_core(r);
+        --m_depth;
+
+        // Cache the result
+        m_cache.insert(r, result);
+        m_trail.push_back(r);
+        m_trail.push_back(result);
+        return result;
+    }
+
+    // Forward declaration helper
+    expr_ref derive::derive_core(expr* r) {
+        sort* s = nullptr;
+        VERIFY(m_util.is_re(r, s));
+
+        auto nothing = [&]() { return expr_ref(re().mk_empty(r->get_sort()), m); };
+        auto epsilon = [&]() { return expr_ref(re().mk_to_re(u().str.mk_empty(s)), m); };
+        auto dotstar = [&]() { return expr_ref(re().mk_full_seq(r->get_sort()), m); };
+
+        expr* r1 = nullptr;
+        expr* r2 = nullptr;
+        expr* cond = nullptr;
+        unsigned lo = 0, hi = 0;
+
+        // δ(∅) = ∅, δ(ε) = ∅
+        if (re().is_empty(r) || re().is_epsilon(r))
+            return nothing();
+
+        // δ(Σ*) = Σ*, δ(.+) = Σ*
+        if (re().is_full_seq(r) || re().is_dot_plus(r))
+            return dotstar();
+
+        // δ(.) = ε (full char accepts any single character)
+        if (re().is_full_char(r))
+            return epsilon();
+
+        // δ(str.to_re(s)) - derivative of a literal string
+        if (re().is_to_re(r, r1))
+            return derive_to_re(r1, s);
+
+        // δ(re.range(lo, hi)) - character range
+        if (re().is_range(r, r1, r2))
+            return derive_range(r1, r2, s);
+
+        // δ(re.of_pred(p)) - predicate-based regex
+        if (re().is_of_pred(r, r1))
+            return derive_of_pred(r1, s);
+
+        // δ(r1 · r2) = δ(r1) · r2 ∪ (if nullable(r1) then δ(r2) else ∅)
+        if (re().is_concat(r, r1, r2)) {
+            expr_ref d1 = derive_rec(r1);
+            expr_ref d1_r2 = mk_deriv_concat(d1, r2);
+            expr_ref nullable_r1 = is_nullable(r1);
+            if (m.is_true(nullable_r1))
+                return mk_union(d1_r2, derive_rec(r2));
+            if (m.is_false(nullable_r1))
+                return d1_r2;
+            // Conditional: nullable is a Boolean expression
+            expr_ref d2 = derive_rec(r2);
+            expr_ref guarded = mk_ite(nullable_r1, d2, nothing());
+            return mk_union(d1_r2, guarded);
+        }
+
+        // δ(r1 ∪ r2) = δ(r1) ∪ δ(r2)
+        if (re().is_union(r, r1, r2)) {
+            expr_ref d1 = derive_rec(r1);
+            expr_ref d2 = derive_rec(r2);
+            return mk_union(d1, d2);
+        }
+
+        // δ(r1 ∩ r2) = δ(r1) ∩ δ(r2)
+        if (re().is_intersection(r, r1, r2)) {
+            expr_ref d1 = derive_rec(r1);
+            expr_ref d2 = derive_rec(r2);
+            return mk_inter(d1, d2);
+        }
+
+        // δ(~r1) = ~δ(r1)
+        if (re().is_complement(r, r1)) {
+            expr_ref d1 = derive_rec(r1);
+            return mk_complement(d1);
+        }
+
+        // δ(r1*) = δ(r1) · r1*
+        if (re().is_star(r, r1)) {
+            expr_ref d1 = derive_rec(r1);
+            expr_ref star_r1(re().mk_star(r1), m);
+            return mk_deriv_concat(d1, star_r1);
+        }
+
+        // δ(r1+) = δ(r1) · r1*
+        if (re().is_plus(r, r1)) {
+            expr_ref d1 = derive_rec(r1);
+            expr_ref star_r1(re().mk_star(r1), m);
+            return mk_deriv_concat(d1, star_r1);
+        }
+
+        // δ(r1?) = δ(r1)
+        if (re().is_opt(r, r1))
+            return derive_rec(r1);
+
+        // δ(r1{lo,hi})
+        if (re().is_loop(r, r1, lo, hi)) {
+            if (hi == 0 || hi < lo)
+                return nothing();
+            expr_ref d1 = derive_rec(r1);
+            expr_ref tail(re().mk_loop_proper(r1, (lo == 0 ? 0 : lo - 1), hi - 1), m);
+            return mk_deriv_concat(d1, tail);
+        }
+
+        // δ(r1{lo,}) - unbounded loop
+        if (re().is_loop(r, r1, lo)) {
+            expr_ref d1 = derive_rec(r1);
+            expr_ref tail(re().mk_loop(r1, (lo == 0 ? 0 : lo - 1)), m);
+            return mk_deriv_concat(d1, tail);
+        }
+
+        // δ(r1 \ r2) = δ(r1) ∩ ~δ(r2)
+        if (re().is_diff(r, r1, r2)) {
+            expr_ref d1 = derive_rec(r1);
+            expr_ref d2 = derive_rec(r2);
+            expr_ref neg_d2 = mk_complement(d2);
+            return mk_inter(d1, neg_d2);
+        }
+
+        // δ(ite(c, r1, r2)) = ite(c, δ(r1), δ(r2))
+        if (m.is_ite(r, cond, r1, r2)) {
+            expr_ref d1 = derive_rec(r1);
+            expr_ref d2 = derive_rec(r2);
+            return mk_ite(cond, d1, d2);
+        }
+
+        // δ(reverse(r1)) - stuck: return symbolic derivative
+        if (re().is_reverse(r, r1))
+            return expr_ref(re().mk_derivative(m_ele, r), m);
+
+        // Stuck/uninterpreted case
+        return expr_ref(re().mk_derivative(m_ele, r), m);
+    }
+
+    // -------------------------------------------------------
+    // Derivative of specific regex constructs
+    // -------------------------------------------------------
+
+    expr_ref derive::derive_to_re(expr* s, sort* seq_sort) {
+        sort* re_sort = re().mk_re(seq_sort);
+        // δ(to_re("")) = ∅
+        if (u().str.is_empty(s))
+            return expr_ref(re().mk_empty(re_sort), m);
+
+        // δ(to_re("c₁c₂...cₙ")) = ite(ele = c₁, to_re("c₂...cₙ"), ∅)
+        zstring zs;
+        if (u().str.is_string(s, zs)) {
+            if (zs.length() == 0)
+                return expr_ref(re().mk_empty(re_sort), m);
+            // First character
+            expr_ref head(m_util.mk_char(zs[0]), m);
+            expr_ref cond(m.mk_eq(m_ele, head), m);
+            // Tail string
+            expr_ref tail_str(u().str.mk_string(zs.extract(1, zs.length() - 1)), m);
+            expr_ref tail_re(re().mk_to_re(tail_str), m);
+            expr_ref empty(re().mk_empty(re_sort), m);
+            return mk_ite(cond, tail_re, empty);
+        }
+
+        // Non-ground sequence: δ(to_re(s)) = ite(s ≠ "" ∧ ele = s[0], to_re(s[1:]), ∅)
+        expr_ref empty_seq(u().str.mk_empty(seq_sort), m);
+        expr_ref is_non_empty(m.mk_not(m.mk_eq(s, empty_seq)), m);
+        expr_ref zero(m_autil.mk_int(0), m);
+        expr_ref first(u().str.mk_nth_i(s, zero), m);
+        expr_ref eq_first(m.mk_eq(m_ele, first), m);
+        expr_ref guard(m.mk_and(is_non_empty, eq_first), m);
+        expr_ref one(m_autil.mk_int(1), m);
+        expr_ref len(u().str.mk_length(s), m);
+        expr_ref rest_len(m_autil.mk_sub(len, one), m);
+        expr_ref rest(u().str.mk_substr(s, one, rest_len), m);
+        expr_ref rest_re(re().mk_to_re(rest), m);
+        expr_ref empty(re().mk_empty(re_sort), m);
+        return mk_ite(guard, rest_re, empty);
+    }
+
+    expr_ref derive::derive_range(expr* lo, expr* hi, sort* seq_sort) {
+        sort* re_sort = re().mk_re(seq_sort);
+        expr_ref empty(re().mk_empty(re_sort), m);
+        expr_ref eps(re().mk_to_re(u().str.mk_empty(seq_sort)), m);
+
+        // Extract character values from unit strings
+        expr_ref c_lo(m), c_hi(m);
+        if (u().str.is_unit_string(lo, c_lo) && u().str.is_unit_string(hi, c_hi)) {
+            // ite(lo <= ele && ele <= hi, ε, ∅)
+            expr_ref ge_lo(m_util.mk_le(c_lo, m_ele), m);
+            expr_ref le_hi(m_util.mk_le(m_ele, c_hi), m);
+            expr_ref in_range(m.mk_and(ge_lo, le_hi), m);
+            return mk_ite(in_range, eps, empty);
+        }
+
+        // Fallback: stuck derivative
+        return expr_ref(re().mk_derivative(m_ele, re().mk_range(lo, hi)), m);
+    }
+
+    expr_ref derive::derive_of_pred(expr* pred, sort* seq_sort) {
+        sort* re_sort = re().mk_re(seq_sort);
+        expr_ref empty(re().mk_empty(re_sort), m);
+        expr_ref eps(re().mk_to_re(u().str.mk_empty(seq_sort)), m);
+
+        // Apply predicate to the element
+        array_util autil(m);
+        expr* args[2] = { pred, m_ele };
+        expr_ref cond(autil.mk_select(2, args), m);
+        return mk_ite(cond, eps, empty);
+    }
+
+    // -------------------------------------------------------
+    // Nullability - uses info class from seq_decl_plugin.h
+    // -------------------------------------------------------
+
+    expr_ref derive::is_nullable(expr* r) {
+        // First, try the static info which handles ground/interpreted regex
+        lbool nb = re().get_info(r).nullable;
+        if (nb == l_true)
+            return expr_ref(m.mk_true(), m);
+        if (nb == l_false)
+            return expr_ref(m.mk_false(), m);
+        // info is undetermined (l_undef) — fall back to recursive computation
+        return is_nullable_rec(r);
+    }
+
+    expr_ref derive::is_nullable_rec(expr* r) {
+        expr* r1 = nullptr, * r2 = nullptr, * cond = nullptr;
+        sort* s = nullptr;
+        unsigned lo = 0, hi = 0;
+
+        if (re().is_concat(r, r1, r2) || re().is_intersection(r, r1, r2)) {
+            expr_ref n1 = is_nullable(r1);
+            expr_ref n2 = is_nullable(r2);
+            expr_ref result(m);
+            m_br.mk_and(n1, n2, result);
+            return result;
+        }
+        if (re().is_union(r, r1, r2)) {
+            expr_ref n1 = is_nullable(r1);
+            expr_ref n2 = is_nullable(r2);
+            expr_ref result(m);
+            m_br.mk_or(n1, n2, result);
+            return result;
+        }
+        if (re().is_complement(r, r1)) {
+            expr_ref n1 = is_nullable(r1);
+            expr_ref result(m);
+            m_br.mk_not(n1, result);
+            return result;
+        }
+        if (re().is_diff(r, r1, r2)) {
+            expr_ref n1 = is_nullable(r1);
+            expr_ref n2 = is_nullable(r2);
+            expr_ref not_n2(m);
+            m_br.mk_not(n2, not_n2);
+            expr_ref result(m);
+            m_br.mk_and(n1, not_n2, result);
+            return result;
+        }
+        if (re().is_to_re(r, r1)) {
+            if (u().str.is_empty(r1))
+                return expr_ref(m.mk_true(), m);
+            zstring zs;
+            if (u().str.is_string(r1, zs))
+                return expr_ref(m.mk_bool_val(zs.length() == 0), m);
+            return expr_ref(m.mk_eq(r1, u().str.mk_empty(r1->get_sort())), m);
+        }
+        if (m.is_ite(r, cond, r1, r2)) {
+            expr_ref n1 = is_nullable(r1);
+            expr_ref n2 = is_nullable(r2);
+            expr_ref result(m);
+            m_br.mk_ite(cond, n1, n2, result);
+            return result;
+        }
+        // Unknown: use membership test
+        if (m_util.is_re(r, s))
+            return expr_ref(re().mk_in_re(u().str.mk_empty(s), r), m);
+
+        return expr_ref(m.mk_true(), m);
+    }
+
+    // -------------------------------------------------------
+    // Smart constructors with simplification
+    // -------------------------------------------------------
+
+    expr_ref derive::mk_union(expr* a, expr* b) {
+        // Identity / annihilator
+        if (a == b) return expr_ref(a, m);
+        if (re().is_empty(a)) return expr_ref(b, m);
+        if (re().is_empty(b)) return expr_ref(a, m);
+        if (re().is_full_seq(a)) return expr_ref(a, m);
+        if (re().is_full_seq(b)) return expr_ref(b, m);
+
+        // Complement absorption: r ∪ ~r = Σ*
+        expr* c = nullptr;
+        if (re().is_complement(a, c) && c == b)
+            return expr_ref(re().mk_full_seq(a->get_sort()), m);
+        if (re().is_complement(b, c) && c == a)
+            return expr_ref(re().mk_full_seq(a->get_sort()), m);
+
+        // ITE combination: if both are ITE with same condition, merge
+        expr *c1, *t1, *e1, *c2, *t2, *e2;
+        if (m.is_ite(a, c1, t1, e1) && m.is_ite(b, c2, t2, e2) && c1 == c2) {
+            expr_ref then_br = mk_union(t1, t2);
+            expr_ref else_br = mk_union(e1, e2);
+            return mk_ite(c1, then_br, else_br);
+        }
+
+        // ACI: flatten, sort, deduplicate
+        expr_ref_vector args(m);
+        flatten_union(a, args);
+        flatten_union(b, args);
+
+        // Sort by expr id for canonical form
+        std::stable_sort(args.data(), args.data() + args.size(),
+            [](expr* x, expr* y) { return x->get_id() < y->get_id(); });
+
+        // Deduplicate
+        unsigned j = 0;
+        for (unsigned i = 0; i < args.size(); ++i) {
+            if (j > 0 && args.get(i) == args.get(j - 1))
+                continue; // skip duplicate
+            if (re().is_empty(args.get(i)))
+                continue; // skip empty
+            if (re().is_full_seq(args.get(i)))
+                return expr_ref(args.get(i), m); // universal absorbs
+            args.set(j++, args.get(i));
+        }
+        args.shrink(j);
+
+        if (args.empty())
+            return expr_ref(re().mk_empty(a->get_sort()), m);
+
+        return mk_union_from_sorted(args);
+    }
+
+    expr_ref derive::mk_inter(expr* a, expr* b) {
+        // Identity / annihilator
+        if (a == b) return expr_ref(a, m);
+        if (re().is_empty(a)) return expr_ref(a, m);
+        if (re().is_empty(b)) return expr_ref(b, m);
+        if (re().is_full_seq(a)) return expr_ref(b, m);
+        if (re().is_full_seq(b)) return expr_ref(a, m);
+
+        // Complement absorption: r ∩ ~r = ∅
+        expr* c = nullptr;
+        if (re().is_complement(a, c) && c == b)
+            return expr_ref(re().mk_empty(a->get_sort()), m);
+        if (re().is_complement(b, c) && c == a)
+            return expr_ref(re().mk_empty(a->get_sort()), m);
+
+        // ITE combination: if both are ITE with same condition, merge
+        expr *c1, *t1, *e1, *c2, *t2, *e2;
+        if (m.is_ite(a, c1, t1, e1) && m.is_ite(b, c2, t2, e2) && c1 == c2) {
+            expr_ref then_br = mk_inter(t1, t2);
+            expr_ref else_br = mk_inter(e1, e2);
+            return mk_ite(c1, then_br, else_br);
+        }
+
+        // ACI: flatten, sort, deduplicate
+        expr_ref_vector args(m);
+        flatten_inter(a, args);
+        flatten_inter(b, args);
+
+        std::stable_sort(args.data(), args.data() + args.size(),
+            [](expr* x, expr* y) { return x->get_id() < y->get_id(); });
+
+        unsigned j = 0;
+        for (unsigned i = 0; i < args.size(); ++i) {
+            if (j > 0 && args.get(i) == args.get(j - 1))
+                continue;
+            if (re().is_full_seq(args.get(i)))
+                continue; // skip universal
+            if (re().is_empty(args.get(i)))
+                return expr_ref(args.get(i), m); // empty absorbs
+            args.set(j++, args.get(i));
+        }
+        args.shrink(j);
+
+        if (args.empty())
+            return expr_ref(re().mk_full_seq(a->get_sort()), m);
+
+        return mk_inter_from_sorted(args);
+    }
+
+    expr_ref derive::mk_concat(expr* a, expr* b) {
+        if (re().is_empty(a)) return expr_ref(a, m);
+        if (re().is_empty(b)) return expr_ref(b, m);
+        if (re().is_epsilon(a)) return expr_ref(b, m);
+        if (re().is_epsilon(b)) return expr_ref(a, m);
+
+        // to_re(s1) · to_re(s2) → to_re(s1 ++ s2)
+        expr* s1 = nullptr, * s2 = nullptr;
+        if (re().is_to_re(a, s1) && re().is_to_re(b, s2))
+            return expr_ref(re().mk_to_re(u().str.mk_concat(s1, s2)), m);
+
+        // r* · r* → r*
+        expr* a1 = nullptr, * b1 = nullptr;
+        if (re().is_star(a, a1) && re().is_star(b, b1) && a1 == b1)
+            return expr_ref(a, m);
+
+        // Right-associate: (a · b) · c → a · (b · c)
+        if (re().is_concat(a, a1, b1)) {
+            expr_ref tail = mk_concat(b1, b);
+            return expr_ref(re().mk_concat(a1, tail), m);
+        }
+
+        return expr_ref(re().mk_concat(a, b), m);
+    }
+
+    expr_ref derive::mk_complement(expr* a) {
+        // ~~r → r
+        expr* r = nullptr;
+        if (re().is_complement(a, r))
+            return expr_ref(r, m);
+        // ~∅ → Σ*
+        if (re().is_empty(a))
+            return expr_ref(re().mk_full_seq(a->get_sort()), m);
+        // ~Σ* → ∅
+        if (re().is_full_seq(a))
+            return expr_ref(re().mk_empty(a->get_sort()), m);
+
+        // Push through ITE: ~(ite(c, t, e)) → ite(c, ~t, ~e)
+        expr* c, * t, * e;
+        if (m.is_ite(a, c, t, e)) {
+            expr_ref ct = mk_complement(t);
+            expr_ref ce = mk_complement(e);
+            return mk_ite(c, ct, ce);
+        }
+
+        return expr_ref(re().mk_complement(a), m);
+    }
+
+    expr_ref derive::mk_ite(expr* c, expr* t, expr* e) {
+        if (m.is_true(c) || t == e)
+            return expr_ref(t, m);
+        if (m.is_false(c))
+            return expr_ref(e, m);
+        return expr_ref(m.mk_ite(c, t, e), m);
+    }
+
+    // -------------------------------------------------------
+    // ACI normalization helpers
+    // -------------------------------------------------------
+
+    void derive::flatten_union(expr* r, expr_ref_vector& args) {
+        expr* a = nullptr, * b = nullptr;
+        if (re().is_union(r, a, b)) {
+            flatten_union(a, args);
+            flatten_union(b, args);
+        }
+        else {
+            args.push_back(r);
+        }
+    }
+
+    void derive::flatten_inter(expr* r, expr_ref_vector& args) {
+        expr* a = nullptr, * b = nullptr;
+        if (re().is_intersection(r, a, b)) {
+            flatten_inter(a, args);
+            flatten_inter(b, args);
+        }
+        else {
+            args.push_back(r);
+        }
+    }
+
+    expr_ref derive::mk_union_from_sorted(expr_ref_vector& args) {
+        if (args.empty()) {
+            // All elements were identity/absorbed - should not happen in practice
+            // but handle gracefully
+            UNREACHABLE();
+            return expr_ref(m.mk_true(), m);
+        }
+        if (args.size() == 1)
+            return expr_ref(args.get(0), m);
+        // Build right-associated union
+        expr_ref result(args.back(), m);
+        for (unsigned i = args.size() - 1; i > 0; ) {
+            --i;
+            result = expr_ref(re().mk_union(args.get(i), result), m);
+        }
+        return result;
+    }
+
+    expr_ref derive::mk_inter_from_sorted(expr_ref_vector& args) {
+        if (args.empty()) {
+            UNREACHABLE();
+            return expr_ref(m.mk_true(), m);
+        }
+        if (args.size() == 1)
+            return expr_ref(args.get(0), m);
+        // Build right-associated intersection
+        expr_ref result(args.back(), m);
+        for (unsigned i = args.size() - 1; i > 0; ) {
+            --i;
+            result = expr_ref(re().mk_inter(args.get(i), result), m);
+        }
+        return result;
+    }
+
+    // -------------------------------------------------------
+    // ITE-tree combinators (analogous to REsharp mk_binary/mk_unary)
+    // -------------------------------------------------------
+
+    expr_ref derive::ite_combine_binary(expr* d1, expr* d2,
+        std::function<expr_ref(expr*, expr*)> const& op) {
+        expr *c1, *t1, *e1, *c2, *t2, *e2;
+
+        // Both are leaves (non-ITE)
+        if (!m.is_ite(d1, c1, t1, e1) && !m.is_ite(d2, c2, t2, e2))
+            return op(d1, d2);
+
+        // d1 is ITE, d2 is not
+        if (m.is_ite(d1, c1, t1, e1) && !m.is_ite(d2, c2, t2, e2)) {
+            expr_ref then_r = ite_combine_binary(t1, d2, op);
+            expr_ref else_r = ite_combine_binary(e1, d2, op);
+            return mk_ite(c1, then_r, else_r);
+        }
+
+        // d2 is ITE, d1 is not
+        if (!m.is_ite(d1, c1, t1, e1) && m.is_ite(d2, c2, t2, e2)) {
+            expr_ref then_r = ite_combine_binary(d1, t2, op);
+            expr_ref else_r = ite_combine_binary(d1, e2, op);
+            return mk_ite(c2, then_r, else_r);
+        }
+
+        // Both are ITE
+        VERIFY(m.is_ite(d1, c1, t1, e1));
+        VERIFY(m.is_ite(d2, c2, t2, e2));
+
+        if (c1 == c2) {
+            // Same condition: combine pairwise
+            expr_ref then_r = ite_combine_binary(t1, t2, op);
+            expr_ref else_r = ite_combine_binary(e1, e2, op);
+            return mk_ite(c1, then_r, else_r);
+        }
+
+        // Order by condition id (larger id on outside for canonical form)
+        if (c1->get_id() > c2->get_id()) {
+            expr_ref then_r = ite_combine_binary(t1, d2, op);
+            expr_ref else_r = ite_combine_binary(e1, d2, op);
+            return mk_ite(c1, then_r, else_r);
+        }
+        else {
+            expr_ref then_r = ite_combine_binary(d1, t2, op);
+            expr_ref else_r = ite_combine_binary(d1, e2, op);
+            return mk_ite(c2, then_r, else_r);
+        }
+    }
+
+    expr_ref derive::ite_combine_unary(expr* d,
+        std::function<expr_ref(expr*)> const& op) {
+        expr* c, * t, * e;
+        if (m.is_ite(d, c, t, e)) {
+            expr_ref then_r = ite_combine_unary(t, op);
+            expr_ref else_r = ite_combine_unary(e, op);
+            return mk_ite(c, then_r, else_r);
+        }
+        return op(d);
+    }
+
+    // -------------------------------------------------------
+    // Distribute concat through ITE/union structure of derivative
+    // -------------------------------------------------------
+
+    expr_ref derive::mk_deriv_concat(expr* d, expr* tail) {
+        expr_ref _d(d, m), _tail(tail, m);
+        expr* c, * t, * e;
+
+        if (re().is_empty(d))
+            return expr_ref(d, m);
+        if (re().is_epsilon(d))
+            return expr_ref(tail, m);
+
+        if (m.is_ite(d, c, t, e)) {
+            expr_ref then_r = mk_deriv_concat(t, tail);
+            expr_ref else_r = mk_deriv_concat(e, tail);
+            return mk_ite(c, then_r, else_r);
+        }
+
+        if (re().is_union(d, t, e)) {
+            expr_ref left = mk_deriv_concat(t, tail);
+            expr_ref right = mk_deriv_concat(e, tail);
+            return mk_union(left, right);
+        }
+
+        return mk_concat(d, tail);
+    }
+
+}
+
+
+

src/ast/rewriter/seq_derive.h

@@ -0,0 +1,130 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    seq_derive.h
+
+Abstract:
+
+    Symbolic derivative computation for regular expressions.
+    Produces an ITE-tree (transition regex) representation where
+    the free variable is de Bruijn index 0 representing the input character.
+
+    Based on the theory of symbolic derivatives and transition regexes:
+    - Veanes et al., "On Symbolic Derivatives and Transition Regexes" (LPAR 2024)
+    - Varatalu, Veanes, Ernits, "RE#" (POPL 2025)
+    - Stanford, Veanes, Bjørner, "Symbolic Boolean Derivatives" (PLDI 2021)
+
+Authors:
+
+    Nikolaj Bjorner (nbjorner) 2025-06-03
+
+--*/
+
+#pragma once
+
+#include "ast/seq_decl_plugin.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/array_decl_plugin.h"
+#include "ast/rewriter/bool_rewriter.h"
+
+namespace seq {
+
+    /**
+     * Symbolic derivative engine for regular expressions.
+     *
+     * Given a regex r, operator()(r) computes a symbolic derivative δ(r)
+     * represented as an ITE-tree over character predicates (using de Bruijn
+     * variable 0 for the character). Evaluating the ITE-tree for a concrete
+     * character 'a' yields the classical Brzozowski derivative δ_a(r).
+     *
+     * The ITE-tree structure implicitly defines minterms (equivalence classes
+     * of characters indistinguishable by the regex).
+     *
+     * Key properties:
+     * - Results are memoized for termination on cyclic derivative graphs
+     * - Union/intersection operands are sorted for ACI canonicalization
+     * - Depth-bounded to prevent stack overflow
+     */
+    class derive {
+        ast_manager&    m;
+        seq_util        m_util;
+        arith_util      m_autil;
+        bool_rewriter   m_br;
+
+        // Cache: maps regex expr to its symbolic derivative
+        obj_map<expr, expr*> m_cache;
+        expr_ref_vector      m_trail;    // pin cached results
+
+        // Depth limiting
+        unsigned m_depth { 0 };
+        static const unsigned m_max_depth = 512;
+
+        seq_util::rex& re() { return m_util.re; }
+        seq_util& u() { return m_util; }
+
+        // The element (character) for the current derivative computation
+        expr_ref m_ele;
+
+        // Core derivative computation
+        expr_ref derive_rec(expr* r);
+        expr_ref derive_core(expr* r);
+
+        // Helpers for specific regex constructs
+        expr_ref derive_to_re(expr* s, sort* seq_sort);
+        expr_ref derive_range(expr* lo, expr* hi, sort* seq_sort);
+        expr_ref derive_of_pred(expr* pred, sort* seq_sort);
+
+        // Nullable check: returns a Boolean expression
+        expr_ref is_nullable(expr* r);
+        expr_ref is_nullable_rec(expr* r);
+
+        // Smart constructors with simplification and ACI canonicalization
+        expr_ref mk_union(expr* a, expr* b);
+        expr_ref mk_inter(expr* a, expr* b);
+        expr_ref mk_concat(expr* a, expr* b);
+        expr_ref mk_complement(expr* a);
+        expr_ref mk_ite(expr* c, expr* t, expr* e);
+
+        // Flatten and sort for ACI normal form
+        void flatten_union(expr* r, expr_ref_vector& args);
+        void flatten_inter(expr* r, expr_ref_vector& args);
+        expr_ref mk_union_from_sorted(expr_ref_vector& args);
+        expr_ref mk_inter_from_sorted(expr_ref_vector& args);
+
+        // ITE-tree binary combinator (analogous to REsharp mk_binary)
+        // Combines two ITE-tree derivatives with a binary regex operation
+        expr_ref ite_combine_binary(expr* d1, expr* d2,
+            std::function<expr_ref(expr*, expr*)> const& op);
+
+        // ITE-tree unary combinator (analogous to REsharp mk_unary)
+        expr_ref ite_combine_unary(expr* d, std::function<expr_ref(expr*)> const& op);
+
+        // Distribute concatenation through ITE/union in derivative
+        expr_ref mk_deriv_concat(expr* d, expr* tail);
+
+        sort* re_sort(expr* r) { return r->get_sort(); }
+        sort* seq_sort(expr* r) { sort* s = nullptr; m_util.is_re(r, s); return s; }
+        sort* ele_sort(expr* r) { sort* s = seq_sort(r); sort* e = nullptr; m_util.is_seq(s, e); return e; }
+
+    public:
+        derive(ast_manager& m);
+
+        /**
+         * Compute the derivative of regex r with respect to element ele.
+         * When ele is a de Bruijn variable, produces a symbolic ITE-tree.
+         * When ele is a concrete character, produces the concrete derivative.
+         */
+        expr_ref operator()(expr* ele, expr* r);
+
+        /**
+         * Convenience: symbolic derivative using de Bruijn var 0.
+         */
+        expr_ref operator()(expr* r);
+
+        void reset();
+    };
+
+}
+

src/ast/rewriter/seq_rewriter.cpp

@@ -2962,394 +2962,6 @@ expr_ref seq_rewriter::mk_derivative(expr* ele, expr* r) {
     return m_derive(ele, r);
 }
 
-expr_ref seq_rewriter::mk_antimirov_deriv(expr* e, expr* r, expr* path) {
-    // Ensure references are owned
-    expr_ref _e(e, m()), _path(path, m()), _r(r, m());
-    expr_ref result(m_op_cache.find(OP_RE_DERIVATIVE, e, r, path), m());
-    if (!result) {
-        mk_antimirov_deriv_rec(e, r, path, result);
-        m_op_cache.insert(OP_RE_DERIVATIVE, e, r, path, result);
-        STRACE(seq_regex, tout << "D(" << mk_pp(e, m()) << "," << mk_pp(r, m()) << "," << mk_pp(path, m()) << ")" << std::endl;);
-        STRACE(seq_regex, tout << "= " << mk_pp(result, m()) << std::endl;);
-    }
-    return result;
-}
-
-void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref& result) {
-    sort* seq_sort = nullptr, * ele_sort = nullptr;
-    expr_ref _r(r, m()), _path(path, m());
-    VERIFY(m_util.is_re(r, seq_sort));
-    VERIFY(m_util.is_seq(seq_sort, ele_sort));
-    SASSERT(ele_sort == e->get_sort());
-    expr* r1 = nullptr, * r2 = nullptr, * c = nullptr;
-    expr_ref c1(m());
-    expr_ref c2(m());
-    auto nothing = [&]() { return expr_ref(re().mk_empty(r->get_sort()), m()); };
-    auto epsilon = [&]() { return expr_ref(re().mk_epsilon(seq_sort), m()); };
-    auto dotstar = [&]() { return expr_ref(re().mk_full_seq(r->get_sort()), m()); };
-    unsigned lo = 0, hi = 0;
-    if (re().is_empty(r) || re().is_epsilon(r))
-        // D(e,[]) = D(e,()) = []
-        result = nothing();
-    else if (re().is_full_seq(r) || re().is_dot_plus(r))
-        // D(e,.*) = D(e,.+) = .*
-        result = dotstar();
-    else if (re().is_full_char(r))
-        // D(e,.) = ()
-        result = epsilon();
-    else if (re().is_to_re(r, r1)) {
-        expr_ref h(m());
-        expr_ref t(m());
-        // here r1 is a sequence
-        if (get_head_tail(r1, h, t)) {
-            if (eq_char(e, h))
-                result = re().mk_to_re(t);
-            else if (neq_char(e, h))
-                result = nothing();
-            else
-                result = re().mk_ite_simplify(m().mk_eq(e, h), re().mk_to_re(t), nothing());
-        }
-        else {
-            // observe that the precondition |r1|>0 is is implied by c1 for use of mk_seq_first
-            {
-                auto is_non_empty = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort)));
-                auto eq_first = m().mk_eq(mk_seq_first(r1), e);
-                m_br.mk_and(is_non_empty, eq_first, c1);
-            }
-            m_br.mk_and(path, c1, c2);
-            if (m().is_false(c2))
-                result = nothing();
-            else
-                // observe that the precondition |r1|>0 is implied by c1 for use of mk_seq_rest
-                result = m().mk_ite(c1, re().mk_to_re(mk_seq_rest(r1)), nothing());
-        }
-    }
-    else if (re().is_reverse(r, r2))
-        if (re().is_to_re(r2, r1)) {
-            // here r1 is a sequence
-            // observe that the precondition |r1|>0 of mk_seq_last is implied by c1
-            {
-                auto is_non_empty = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort)));
-                auto eq_last = m().mk_eq(mk_seq_last(r1), e);
-                m_br.mk_and(is_non_empty, eq_last, c1);
-            }
-            m_br.mk_and(path, c1, c2);
-            if (m().is_false(c2))
-                result = nothing();
-            else
-                // observe that the precondition |r1|>0 of mk_seq_rest is implied by c1
-                result = re().mk_ite_simplify(c1, re().mk_reverse(re().mk_to_re(mk_seq_butlast(r1))), nothing());
-        }
-        else {
-            result = mk_regex_reverse(r2);
-            if (result.get() == r)
-                //r2 is an uninterpreted regex that is stuck
-                //for example if r = (re.reverse R) where R is a regex variable then
-                //here result.get() == r
-                result = re().mk_derivative(e, result);
-            else
-                result = mk_antimirov_deriv(e, result, path);
-        }
-    else if (re().is_concat(r, r1, r2)) {
-        expr_ref r1nullable(is_nullable(r1), m());
-        c1 = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), r2);
-        expr_ref r1nullable_and_path(m());
-        m_br.mk_and(r1nullable, path, r1nullable_and_path);
-        if (m().is_false(r1nullable_and_path))
-            // D(e,r1)r2
-            result = c1;
-        else
-            // D(e,r1)r2|(ite (r1nullable) (D(e,r2)) [])
-            // observe that (mk_ite_simplify(true, D(e,r2), []) = D(e,r2)
-            result = mk_antimirov_deriv_union(c1, re().mk_ite_simplify(r1nullable, mk_antimirov_deriv(e, r2, path), nothing()));
-    }
-    else if (m().is_ite(r, c, r1, r2)) {
-        {
-            auto cp = m().mk_and(c, path);
-            c1 = simplify_path(e, cp);
-        }
-        {
-            auto notc = m().mk_not(c);
-            auto np = m().mk_and(notc, path);
-            c2 = simplify_path(e, np);
-        }
-        if (m().is_false(c1))
-            result = mk_antimirov_deriv(e, r2, c2);
-        else if (m().is_false(c2))
-            result = mk_antimirov_deriv(e, r1, c1);
-        else
-            result = re().mk_ite_simplify(c, mk_antimirov_deriv(e, r1, c1), mk_antimirov_deriv(e, r2, c2));
-    }
-    else if (re().is_range(r, r1, r2)) {
-        expr_ref range(m());
-        expr_ref psi(m().mk_false(), m());
-        if (str().is_unit_string(r1, c1) && str().is_unit_string(r2, c2)) {
-            // SASSERT(u().is_char(c1));
-            // SASSERT(u().is_char(c2));
-            // case: c1 <= e <= c2
-            // deterministic evaluation for range bounds
-            auto a_le = u().mk_le(c1, e);
-            auto b_le = u().mk_le(e, c2);
-            auto rng_cond = m().mk_and(a_le, b_le);
-            range = simplify_path(e, rng_cond);
-            psi = simplify_path(e, m().mk_and(path, range));
-        }
-        else if (!str().is_string(r1) && str().is_unit_string(r2, c2)) {
-            SASSERT(u().is_char(c2));
-            // r1 nonground: |r1|=1 & r1[0] <= e <= c2
-            expr_ref one(m_autil.mk_int(1), m());
-            expr_ref zero(m_autil.mk_int(0), m());
-            expr_ref r1_length_eq_one(m().mk_eq(str().mk_length(r1), one), m());
-            expr_ref r1_0(str().mk_nth_i(r1, zero), m());
-            range = simplify_path(e, m().mk_and(r1_length_eq_one, m().mk_and(u().mk_le(r1_0, e), u().mk_le(e, c2))));
-            psi = simplify_path(e, m().mk_and(path, range));
-        }
-        else if (!str().is_string(r2) && str().is_unit_string(r1, c1)) {
-            SASSERT(u().is_char(c1));
-            // r2 nonground: |r2|=1 & c1 <= e <= r2_0
-            expr_ref one(m_autil.mk_int(1), m());
-            expr_ref zero(m_autil.mk_int(0), m());
-            expr_ref r2_length_eq_one(m().mk_eq(str().mk_length(r2), one), m());
-            expr_ref r2_0(str().mk_nth_i(r2, zero), m());
-            range = simplify_path(e, m().mk_and(r2_length_eq_one, m().mk_and(u().mk_le(c1, e), u().mk_le(e, r2_0))));
-            psi = simplify_path(e, m().mk_and(path, range));
-        }
-        else if (!str().is_string(r1) && !str().is_string(r2)) {
-            // both r1 and r2 nonground: |r1|=1 & |r2|=1 & r1[0] <= e <= r2[0]
-            expr_ref one(m_autil.mk_int(1), m());
-            expr_ref zero(m_autil.mk_int(0), m());
-            expr_ref r1_length_eq_one(m().mk_eq(str().mk_length(r1), one), m());
-            expr_ref r1_0(str().mk_nth_i(r1, zero), m());
-            expr_ref r2_length_eq_one(m().mk_eq(str().mk_length(r2), one), m());
-            expr_ref r2_0(str().mk_nth_i(r2, zero), m());
-            range = simplify_path(e, m().mk_and(r1_length_eq_one, m().mk_and(r2_length_eq_one, m().mk_and(u().mk_le(r1_0, e), u().mk_le(e, r2_0)))));
-            psi = simplify_path(e, m().mk_and(path, range));
-        }
-        if (m().is_false(psi))
-            result = nothing();
-        else
-            result = re().mk_ite_simplify(range, epsilon(), nothing());
-    }
-    else if (re().is_union(r, r1, r2))
-        result = mk_antimirov_deriv_union(mk_antimirov_deriv(e, r1, path), mk_antimirov_deriv(e, r2, path));
-    else if (re().is_intersection(r, r1, r2))
-        result = mk_antimirov_deriv_intersection(e, 
-            mk_antimirov_deriv(e, r1, path),
-            mk_antimirov_deriv(e, r2, path), m().mk_true());
-    else if (re().is_star(r, r1) || re().is_plus(r, r1) || (re().is_loop(r, r1, lo) && 0 <= lo && lo <= 1))
-        result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_star(r1));
-    else if (re().is_loop(r, r1, lo))
-        result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop(r1, lo - 1));
-    else if (re().is_loop(r, r1, lo, hi)) {
-        if ((lo == 0 && hi == 0) || hi < lo)
-            result = nothing();
-        else {
-            expr_ref t(re().mk_loop_proper(r1, (lo == 0 ? 0 : lo - 1), hi - 1), m());
-            result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), t);
-        }
-    }
-    else if (re().is_opt(r, r1))
-        result = mk_antimirov_deriv(e, r1, path);
-    else if (re().is_complement(r, r1))
-        // D(e,~r1) = ~D(e,r1)
-        result = mk_antimirov_deriv_negate(e, mk_antimirov_deriv(e, r1, path));
-    else if (re().is_diff(r, r1, r2))
-        result = mk_antimirov_deriv_intersection(e, 
-            mk_antimirov_deriv(e, r1, path),
-            mk_antimirov_deriv_negate(e, mk_antimirov_deriv(e, r2, path)), m().mk_true());
-    else if (re().is_xor(r, r1, r2))
-        // D(e, r1 XOR r2) = D(e, r1) XOR D(e, r2)
-        result = mk_der_xor(mk_antimirov_deriv(e, r1, path),
-                            mk_antimirov_deriv(e, r2, path));
-    else if (re().is_of_pred(r, r1)) {
-        array_util array(m());
-        expr* args[2] = { r1, e };
-        result = array.mk_select(2, args);
-        // Use mk_der_cond to normalize
-        result = mk_der_cond(result, e, seq_sort);
-    }
-    else
-        // stuck cases
-        result = re().mk_derivative(e, r);
-}
-
-expr_ref seq_rewriter::mk_antimirov_deriv_intersection(expr* e, expr* d1, expr* d2, expr* path) {
-    sort* seq_sort = nullptr, * ele_sort = nullptr;
-    VERIFY(m_util.is_re(d1, seq_sort));
-    VERIFY(m_util.is_seq(seq_sort, ele_sort));
-    expr_ref result(m());
-    expr* c, * a, * b;
-    if (m_re_deriv_depth >= m_max_re_deriv_depth) {
-        // Depth limit reached: construct intersection without further decomposition
-        result = mk_regex_inter_normalize(d1, d2);
-    }
-    else if (re().is_empty(d1))
-        result = d1;
-    else if (re().is_empty(d2))
-        result = d2;
-    else if (m().is_ite(d1, c, a, b)) {
-        expr_ref path_and_c(simplify_path(e, m().mk_and(path, c)), m());
-        expr_ref path_and_notc(simplify_path(e, m().mk_and(path, m().mk_not(c))), m());
-        ++m_re_deriv_depth;
-        if (m().is_false(path_and_c))
-            result = mk_antimirov_deriv_intersection(e, b, d2, path);
-        else if (m().is_false(path_and_notc))
-            result = mk_antimirov_deriv_intersection(e, a, d2, path);
-        else
-            result = m().mk_ite(c, mk_antimirov_deriv_intersection(e, a, d2, path_and_c),
-                mk_antimirov_deriv_intersection(e, b, d2, path_and_notc));
-        --m_re_deriv_depth;
-    }
-    else if (m().is_ite(d2)) {
-        // swap d1 and d2
-        ++m_re_deriv_depth;
-        result = mk_antimirov_deriv_intersection(e, d2, d1, path);
-        --m_re_deriv_depth;
-    }
-    else if (d1 == d2 || re().is_full_seq(d2))
-        result = mk_antimirov_deriv_restrict(e, d1, path);
-    else if (re().is_full_seq(d1))
-        result = mk_antimirov_deriv_restrict(e, d2, path);
-    else if (re().is_union(d1, a, b)) {
-        // distribute intersection over the union in d1
-        ++m_re_deriv_depth;
-        result = mk_antimirov_deriv_union(mk_antimirov_deriv_intersection(e, a, d2, path),
-            mk_antimirov_deriv_intersection(e, b, d2, path));
-        --m_re_deriv_depth;
-    }
-    else if (re().is_union(d2, a, b)) {
-        // distribute intersection over the union in d2
-        ++m_re_deriv_depth;
-        result = mk_antimirov_deriv_union(mk_antimirov_deriv_intersection(e, d1, a, path),
-            mk_antimirov_deriv_intersection(e, d1, b, path));
-        --m_re_deriv_depth;
-    }
-    else
-        result = mk_regex_inter_normalize(d1, d2);
-    return result;
-}
-
-expr_ref seq_rewriter::mk_antimirov_deriv_concat(expr* d, expr* r) {
-    expr_ref result(m());
-    expr_ref _r(r, m()), _d(d, m());
-    expr* c, * t, * e;
-    if (m_re_deriv_depth >= m_max_re_deriv_depth) {
-        // Depth limit reached: construct concat without further decomposition
-        result = mk_re_append(d, r);
-    }
-    else if (m().is_ite(d, c, t, e)) {
-        ++m_re_deriv_depth;
-        auto r2 = mk_antimirov_deriv_concat(e, r);
-        auto r1 = mk_antimirov_deriv_concat(t, r);
-        --m_re_deriv_depth;
-        result = m().mk_ite(c, r1, r2);
-    }
-    else if (re().is_union(d, t, e)) {
-        ++m_re_deriv_depth;
-        result = mk_antimirov_deriv_union(mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r));
-        --m_re_deriv_depth;
-    }
-    else
-        result = mk_re_append(d, r);
-    SASSERT(result.get());
-    return result;
-}
-
-expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* elem, expr* d) {
-    sort* seq_sort = nullptr;
-    VERIFY(m_util.is_re(d, seq_sort));
-    auto nothing = [&]() { return expr_ref(re().mk_empty(d->get_sort()), m()); };
-    auto epsilon = [&]() { return expr_ref(re().mk_epsilon(seq_sort), m()); };
-    auto dotstar = [&]() { return expr_ref(re().mk_full_seq(d->get_sort()), m()); };
-    auto dotplus = [&]() { return expr_ref(re().mk_plus(re().mk_full_char(d->get_sort())), m()); };
-    expr_ref result(m());
-    expr* c, * t, * e;
-    if (m_re_deriv_depth >= m_max_re_deriv_depth) {
-        // Depth limit reached: construct complement without further decomposition
-        result = re().mk_complement(d);
-    }
-    else if (re().is_empty(d))
-        result = dotstar();
-    else if (re().is_epsilon(d))
-        result = dotplus();
-    else if (re().is_full_seq(d))
-        result = nothing();
-    else if (re().is_dot_plus(d))
-        result = epsilon();
-    else if (m().is_ite(d, c, t, e)) {
-        ++m_re_deriv_depth;
-        result = m().mk_ite(c, mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e));
-        --m_re_deriv_depth;
-    }
-    else if (re().is_union(d, t, e)) {
-        ++m_re_deriv_depth;
-        result = mk_antimirov_deriv_intersection(elem, mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e), m().mk_true());
-        --m_re_deriv_depth;
-    }
-    else if (re().is_intersection(d, t, e)) {
-        ++m_re_deriv_depth;
-        result = mk_antimirov_deriv_union(mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e));
-        --m_re_deriv_depth;
-    }
-    else if (re().is_complement(d, t))
-        result = t;
-    else
-        result = re().mk_complement(d);
-    return result;
-}
-
-expr_ref seq_rewriter::mk_antimirov_deriv_union(expr* d1, expr* d2) {
-    sort* seq_sort = nullptr, * ele_sort = nullptr;
-    VERIFY(m_util.is_re(d1, seq_sort));
-    VERIFY(m_util.is_seq(seq_sort, ele_sort));
-    expr_ref result(m());
-    expr* c1, * t1, * e1, * c2, * t2, * e2;
-    if (m().is_ite(d1, c1, t1, e1) && m().is_ite(d2, c2, t2, e2)  && c1 == c2)
-        // eliminate duplicate branching on exactly the same condition
-        result = m().mk_ite(c1, mk_antimirov_deriv_union(t1, t2), mk_antimirov_deriv_union(e1, e2));
-    else
-        result = mk_regex_union_normalize(d1, d2);
-    return result;
-}
-
-// restrict the guards of all conditionals id d and simplify the resulting derivative
-// restrict(if(c, a, b), cond) = if(c, restrict(a, cond & c), restrict(b, cond & ~c))
-// restrict(a U b, cond) = restrict(a, cond) U restrict(b, cond)
-//     where {} U X = X, X U X = X
-// restrict(R, cond) = R 
-// 
-// restrict(d, false) = []
-// 
-// it is already assumed that the restriction takes place within a branch
-// so the condition is not added explicitly but propagated down in order to eliminate 
-// infeasible cases
-expr_ref seq_rewriter::mk_antimirov_deriv_restrict(expr* e, expr* d, expr* cond) {
-    expr_ref result(d, m());
-    expr_ref _cond(cond, m());
-    expr* c, * a, * b;
-    if (m().is_false(cond))
-        result = re().mk_empty(d->get_sort());
-    else if (re().is_empty(d) || m().is_true(cond))
-        result = d;
-    else if (m_re_deriv_depth >= m_max_re_deriv_depth)
-        result = d;
-    else if (m().is_ite(d, c, a, b)) {
-        expr_ref path_and_c(simplify_path(e, m().mk_and(cond, c)), m());
-        expr_ref path_and_notc(simplify_path(e, m().mk_and(cond, m().mk_not(c))), m());
-        ++m_re_deriv_depth;
-        result = re().mk_ite_simplify(c, mk_antimirov_deriv_restrict(e, a, path_and_c),
-            mk_antimirov_deriv_restrict(e, b, path_and_notc));
-        --m_re_deriv_depth;
-    }
-    else if (re().is_union(d, a, b)) {
-        ++m_re_deriv_depth;
-        expr_ref a1(mk_antimirov_deriv_restrict(e, a, cond), m());
-        expr_ref b1(mk_antimirov_deriv_restrict(e, b, cond), m());
-        --m_re_deriv_depth;
-        result = mk_antimirov_deriv_union(a1, b1);
-    }
-    return result;
-}
 
 expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) {
     expr_ref _r1(r1, m()), _r2(r2, m());
@@ -3601,29 +3213,6 @@ expr_ref seq_rewriter::mk_regex_concat(expr* r, expr* s) {
     return result;
 }
 
-expr_ref seq_rewriter::mk_in_antimirov(expr* s, expr* d){
-    expr_ref result(mk_in_antimirov_rec(s, d), m());
-    return result;
-}
-
-expr_ref seq_rewriter::mk_in_antimirov_rec(expr* s, expr* d) {
-    expr* c, * d1, * d2;
-    expr_ref result(m());
-    if (re().is_full_seq(d) || (str().min_length(s) > 0 && re().is_dot_plus(d)))
-        // s in .* <==> true, also: s in .+ <==> true when |s|>0
-        result = m().mk_true();
-    else if (re().is_empty(d) || (str().min_length(s) > 0 && re().is_epsilon(d)))
-        // s in [] <==> false, also: s in () <==> false when |s|>0
-        result = m().mk_false();
-    else if (m().is_ite(d, c, d1, d2))
-        result = re().mk_ite_simplify(c, mk_in_antimirov_rec(s, d1), mk_in_antimirov_rec(s, d2));
-    else if (re().is_union(d, d1, d2))
-        m_br.mk_or(mk_in_antimirov_rec(s, d1), mk_in_antimirov_rec(s, d2), result);
-    else
-        result = re().mk_in_re(s, d);
-    return result;
-}
-
 /*
 * calls elim_condition
 */

src/ast/rewriter/seq_rewriter.h

@@ -19,7 +19,7 @@ Notes:
 #pragma once
 
 #include "ast/seq_decl_plugin.h"
-#include "ast/seq_derive.h"
+#include "ast/rewriter/seq_derive.h"
 #include "ast/ast_pp.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/rewriter/rewriter_types.h"
@@ -199,17 +199,6 @@ class seq_rewriter {
     bool check_deriv_normal_form(expr* r, int level = 3);
     #endif
 
-    void mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref& result);
-
-    expr_ref mk_antimirov_deriv(expr* e, expr* r, expr* path);
-    expr_ref mk_in_antimirov_rec(expr* s, expr* d);
-    expr_ref mk_in_antimirov(expr* s, expr* d);
-
-    expr_ref mk_antimirov_deriv_intersection(expr* elem, expr* d1, expr* d2, expr* path);
-    expr_ref mk_antimirov_deriv_concat(expr* d, expr* r);
-    expr_ref mk_antimirov_deriv_negate(expr* elem, expr* d);
-    expr_ref mk_antimirov_deriv_union(expr* d1, expr* d2);
-    expr_ref mk_antimirov_deriv_restrict(expr* elem, expr* d1, expr* cond);
     expr_ref mk_regex_reverse(expr* r);
     expr_ref mk_regex_concat(expr* r1, expr* r2);