From 92b349c6690f8a46afc11b028327561e5cbaebbe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 25 Jun 2026 22:20:06 -0700 Subject: [PATCH] remove antimirov union and fix is_ground -> re().is_ground. There is ground and there is ground Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_derive.cpp | 2 +- src/ast/rewriter/seq_rewriter.cpp | 8 +------- src/ast/seq_decl_plugin.cpp | 4 +--- src/ast/seq_decl_plugin.h | 4 ---- 4 files changed, 3 insertions(+), 15 deletions(-) diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index f99abb382f..8b89c97546 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -536,7 +536,7 @@ namespace seq { re().is_intersection(r, r1, r2)) { m_br.mk_and(is_nullable(r1), is_nullable(r2), result); } - else if (re().is_union(r, r1, r2) || re().is_antimirov_union(r, r1, r2)) { + else if (re().is_union(r, r1, r2)) { m_br.mk_or(is_nullable(r1), is_nullable(r2), result); } else if (re().is_diff(r, r1, r2)) { diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 0acea0955c..9e4a6ca72c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -241,12 +241,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con st = mk_re_concat(args[0], args[1], result); } break; - case _OP_RE_ANTIMIROV_UNION: - SASSERT(num_args == 2); - // Rewrite antimirov union to real union - result = re().mk_union(args[0], args[1]); - st = BR_REWRITE1; - break; case OP_RE_UNION: if (num_args == 1) { result = args[0]; @@ -4424,7 +4418,7 @@ br_status seq_rewriter::reduce_re_eq(expr* l, expr* r, expr_ref& result) { * indirectly. On l_undef the rewriter falls through to the existing * axiomatisation path. */ - if (!m_in_bisim && is_ground(l) && is_ground(r)) { + if (!m_in_bisim && re().is_ground(l) && re().is_ground(r)) { flet _block(m_in_bisim, true); seq::regex_bisim bisim(*this); switch (bisim.are_equivalent(l, r)) { diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index da3a2085be..75949316a0 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -240,7 +240,6 @@ void seq_decl_plugin::init() { m_sigs[OP_RE_OF_PRED] = alloc(psig, m, "re.of.pred", 1, 1, &predA, reA); m_sigs[OP_RE_REVERSE] = alloc(psig, m, "re.reverse", 1, 1, &reA, reA); m_sigs[OP_RE_DERIVATIVE] = alloc(psig, m, "re.derivative", 1, 2, AreA, reA); - m_sigs[_OP_RE_ANTIMIROV_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, reA); m_sigs[OP_SEQ_TO_RE] = alloc(psig, m, "seq.to.re", 1, 1, &seqA, reA); m_sigs[OP_SEQ_IN_RE] = alloc(psig, m, "seq.in.re", 1, 2, seqAreA, boolT); m_sigs[OP_SEQ_REPLACE_RE_ALL] = alloc(psig, m, "str.replace_re_all", 1, 3, seqAreAseqA, seqA); @@ -412,7 +411,6 @@ func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p case OP_RE_COMPLEMENT: case OP_RE_REVERSE: case OP_RE_DERIVATIVE: - case _OP_RE_ANTIMIROV_UNION: m_has_re = true; Z3_fallthrough; case OP_SEQ_UNIT: @@ -1447,7 +1445,7 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const { print(out, r1); print(out, r2); } - else if (re.is_antimirov_union(e, r1, r2) || re.is_union(e, r1, r2)) { + else if (re.is_union(e, r1, r2)) { out << "("; print(out, r1); out << (html_encode ? "⋃" : "|"); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index c643d8356b..9de2c01525 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -108,7 +108,6 @@ enum seq_op_kind { _OP_REGEXP_EMPTY, _OP_REGEXP_FULL_CHAR, _OP_RE_IS_NULLABLE, - _OP_RE_ANTIMIROV_UNION, // Lifted union for antimirov-style derivatives _OP_SEQ_SKOLEM, LAST_SEQ_OP }; @@ -544,7 +543,6 @@ public: app* mk_of_pred(expr* p); app* mk_reverse(expr* r) { return m.mk_app(m_fid, OP_RE_REVERSE, r); } app* mk_derivative(expr* ele, expr* r) { return m.mk_app(m_fid, OP_RE_DERIVATIVE, ele, r); } - app* mk_antimirov_union(expr* r1, expr* r2) { return m.mk_app(m_fid, _OP_RE_ANTIMIROV_UNION, r1, r2); } bool is_to_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); } bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_RE_CONCAT); } @@ -578,7 +576,6 @@ public: bool is_of_pred(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OF_PRED); } bool is_reverse(expr const* n) const { return is_app_of(n, m_fid, OP_RE_REVERSE); } bool is_derivative(expr const* n) const { return is_app_of(n, m_fid, OP_RE_DERIVATIVE); } - bool is_antimirov_union(expr const* n) const { return is_app_of(n, m_fid, _OP_RE_ANTIMIROV_UNION); } MATCH_UNARY(is_to_re); MATCH_BINARY(is_concat); MATCH_BINARY(is_union); @@ -593,7 +590,6 @@ public: MATCH_UNARY(is_of_pred); MATCH_UNARY(is_reverse); MATCH_BINARY(is_derivative); - MATCH_BINARY(is_antimirov_union); bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) const; bool is_loop(expr const* n, expr*& body, unsigned& lo) const; bool is_loop(expr const* n, expr*& body, expr*& lo, expr*& hi) const;