mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-29 03:48:51 +00:00
Code Activity

remove antimirov union and fix is_ground -> re().is_ground. There is ground and there is ground

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-25 22:20:06 -07:00
parent 2c5aef7d28
commit 92b349c669
4 changed files with 3 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/seq_derive.cpp
View file

@ -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)) {

8
src/ast/rewriter/seq_rewriter.cpp
View file

@ -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<bool> _block(m_in_bisim, true);
seq::regex_bisim bisim(*this);
switch (bisim.are_equivalent(l, r)) {

4
src/ast/seq_decl_plugin.cpp
View file

@ -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 ? "&#x22C3;" : "|");

4
src/ast/seq_decl_plugin.h
View file

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