diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 588979534b1..cb7b778abde 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -552,9 +552,9 @@ 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_ANTIMOROV_UNION: + case _OP_RE_ANTIMIROV_UNION: SASSERT(num_args == 2); - // Rewrite Antimorov union to real union + // Rewrite antimirov union to real union result = re().mk_union(args[0], args[1]); st = BR_REWRITE1; break; @@ -2723,7 +2723,7 @@ expr_ref seq_rewriter::is_nullable_rec(expr* r) { 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_antimorov_union(r, r1, r2)) { + else if (re().is_union(r, r1, r2) || re().is_antimirov_union(r, r1, r2)) { m_br.mk_or(is_nullable(r1), is_nullable(r2), result); } else if (re().is_diff(r, r1, r2)) { @@ -2908,7 +2908,7 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) { Once the derivative is built, we return BR_REWRITE_FULL so that any remaining possible simplification is performed from the bottom up. - Rewriting also replaces _OP_RE_ANTIMOROV_UNION, which is produced + Rewriting also replaces _OP_RE_antimirov_UNION, which is produced by is_derivative, with real union. */ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) { @@ -2924,16 +2924,16 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) { When computing derivatives recursively, we preserve the following BDD normal form: - - At the top level, the derivative is a union of Antimorov derivatives + - At the top level, the derivative is a union of antimirov derivatives (Conceptually each element of the union is a different derivative). We currently express this derivative using an internal op code: - _OP_RE_ANTIMOROV_UNION - - An Antimorov derivative is a nested if-then-else term. + _OP_RE_antimirov_UNION + - An antimirov derivative is a nested if-then-else term. if-then-elses are pushed outwards and sorted by condition ID (cond->get_id()), from largest on the outside to smallest on the inside. Duplicate nested conditions are eliminated. - The leaves of the if-then-else BDD can have unions themselves, - but these are interpreted as Regex union, not as separate Antimorov + but these are interpreted as Regex union, not as separate antimirov derivatives. To debug the normal form, call Z3 with -dbg:seq_regex: @@ -2962,7 +2962,7 @@ bool seq_rewriter::check_deriv_normal_form(expr* r, int level) { unsigned lo = 0, hi = 0; STRACE("seq_verbose", tout << " (level " << level << ")";); int new_level = 0; - if (re().is_antimorov_union(r)) { + if (re().is_antimirov_union(r)) { SASSERT(level >= 2); new_level = 2; } @@ -2975,7 +2975,7 @@ bool seq_rewriter::check_deriv_normal_form(expr* r, int level) { SASSERT(!re().is_opt(r)); SASSERT(!re().is_plus(r)); - if (re().is_antimorov_union(r, r1, r2) || + if (re().is_antimirov_union(r, r1, r2) || re().is_concat(r, r1, r2) || re().is_union(r, r1, r2) || re().is_intersection(r, r1, r2) || @@ -3410,8 +3410,8 @@ expr_ref seq_rewriter::simplify_path(expr* path) { } -expr_ref seq_rewriter::mk_der_antimorov_union(expr* r1, expr* r2) { - return mk_der_op(_OP_RE_ANTIMOROV_UNION, r1, r2); +expr_ref seq_rewriter::mk_der_antimirov_union(expr* r1, expr* r2) { + return mk_der_op(_OP_RE_ANTIMIROV_UNION, r1, r2); } expr_ref seq_rewriter::mk_der_union(expr* r1, expr* r2) { @@ -3512,7 +3512,7 @@ bool seq_rewriter::ite_bdds_compatabile(expr* a, expr* b) { OP_RE_INTERSECT OP_RE_UNION OP_RE_CONCAT - _OP_RE_ANTIMOROV_UNION + _OP_RE_antimirov_UNION - a and b are in normal form (check_deriv_normal_form) Postcondition: @@ -3542,44 +3542,44 @@ expr_ref seq_rewriter::mk_der_op_rec(decl_kind k, expr* a, expr* b) { }; // Choose when to lift a union to the top level, by converting - // it to an Antimorov union - // This implements a restricted form of Antimorov derivatives + // it to an antimirov union + // This implements a restricted form of antimirov derivatives if (k == OP_RE_UNION) { - if (re().is_antimorov_union(a) || re().is_antimorov_union(b)) { - k = _OP_RE_ANTIMOROV_UNION; + if (re().is_antimirov_union(a) || re().is_antimirov_union(b)) { + k = _OP_RE_ANTIMIROV_UNION; } #if 0 - // Disabled: eager Antimorov lifting unless BDDs are compatible + // Disabled: eager antimirov lifting unless BDDs are compatible // Note: the check for BDD compatibility could be made more - // sophisticated: in an Antimorov union of n terms, we really + // sophisticated: in an antimirov union of n terms, we really // want to check if any pair of them is compatible. else if (m().is_ite(a) && m().is_ite(b) && !ite_bdds_compatabile(a, b)) { - k = _OP_RE_ANTIMOROV_UNION; + k = _OP_RE_ANTIMIROV_UNION; } #endif } - if (k == _OP_RE_ANTIMOROV_UNION) { - result = re().mk_antimorov_union(a, b); + if (k == _OP_RE_ANTIMIROV_UNION) { + result = re().mk_antimirov_union(a, b); return result; } - if (re().is_antimorov_union(a, a1, a2)) { + if (re().is_antimirov_union(a, a1, a2)) { expr_ref r1(m()), r2(m()); r1 = mk_der_op(k, a1, b); r2 = mk_der_op(k, a2, b); - result = re().mk_antimorov_union(r1, r2); + result = re().mk_antimirov_union(r1, r2); return result; } - if (re().is_antimorov_union(b, b1, b2)) { + if (re().is_antimirov_union(b, b1, b2)) { expr_ref r1(m()), r2(m()); r1 = mk_der_op(k, a, b1); r2 = mk_der_op(k, a, b2); - result = re().mk_antimorov_union(r1, r2); + result = re().mk_antimirov_union(r1, r2); return result; } // Remaining non-union case: combine two if-then-else BDDs - // (underneath top-level Antimorov unions) + // (underneath top-level antimirov unions) if (m().is_ite(a, ca, a1, a2)) { expr_ref r1(m()), r2(m()); expr_ref notca(m().mk_not(ca), m()); @@ -3688,9 +3688,9 @@ expr_ref seq_rewriter::mk_der_compl(expr* r) { expr_ref result(m_op_cache.find(OP_RE_COMPLEMENT, r, nullptr, nullptr), m()); if (!result) { expr* c = nullptr, * r1 = nullptr, * r2 = nullptr; - if (re().is_antimorov_union(r, r1, r2)) { + if (re().is_antimirov_union(r, r1, r2)) { // Convert union to intersection - // Result: Antimorov union at top level is lost, pushed inside ITEs + // Result: antimirov union at top level is lost, pushed inside ITEs expr_ref res1(m()), res2(m()); res1 = mk_der_compl(r1); res2 = mk_der_compl(r2); @@ -3796,11 +3796,11 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { return result; } else { - // Instead of mk_der_union here, we use mk_der_antimorov_union to + // Instead of mk_der_union here, we use mk_der_antimirov_union to // force the two cases to be considered separately and lifted to // the top level. This avoids blowup in cases where determinization // is expensive. - return mk_der_antimorov_union(result, mk_der_concat(is_n, dr2)); + return mk_der_antimirov_union(result, mk_der_concat(is_n, dr2)); } } else if (re().is_star(r, r1)) { diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 20978c2796f..5cba15fc856 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -200,7 +200,7 @@ class seq_rewriter { expr_ref mk_der_inter(expr* a, expr* b); expr_ref mk_der_compl(expr* a); expr_ref mk_der_cond(expr* cond, expr* ele, sort* seq_sort); - expr_ref mk_der_antimorov_union(expr* r1, expr* r2); + expr_ref mk_der_antimirov_union(expr* r1, expr* r2); bool ite_bdds_compatabile(expr* a, expr* b); /* if r has the form deriv(en..deriv(e1,to_re(s))..) returns 's = [e1..en]' else returns '() in r'*/ expr_ref is_nullable_symbolic_regex(expr* r, sort* seq_sort); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 0829aa09f61..8be046fd99b 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -243,7 +243,7 @@ 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_ANTIMOROV_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, 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); @@ -414,7 +414,7 @@ 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_ANTIMOROV_UNION: + case _OP_RE_ANTIMIROV_UNION: m_has_re = true; // fall-through case OP_SEQ_UNIT: @@ -1283,7 +1283,7 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const { print(out, r1); print(out, r2); } - else if (re.is_antimorov_union(e, r1, r2) || re.is_union(e, r1, r2)) { + else if (re.is_antimirov_union(e, r1, r2) || 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 09a10ee9a55..1db05b7221f 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -103,7 +103,7 @@ enum seq_op_kind { _OP_REGEXP_EMPTY, _OP_REGEXP_FULL_CHAR, _OP_RE_IS_NULLABLE, - _OP_RE_ANTIMOROV_UNION, // Lifted union for antimorov-style derivatives + _OP_RE_ANTIMIROV_UNION, // Lifted union for antimirov-style derivatives _OP_SEQ_SKOLEM, LAST_SEQ_OP }; @@ -525,7 +525,7 @@ class seq_util { 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_antimorov_union(expr* r1, expr* r2) { return m.mk_app(m_fid, _OP_RE_ANTIMOROV_UNION, r1, r2); } + 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); } @@ -557,7 +557,7 @@ class seq_util { 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_antimorov_union(expr const* n) const { return is_app_of(n, m_fid, _OP_RE_ANTIMOROV_UNION); } + 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); @@ -571,7 +571,7 @@ class seq_util { MATCH_UNARY(is_of_pred); MATCH_UNARY(is_reverse); MATCH_BINARY(is_derivative); - MATCH_BINARY(is_antimorov_union); + 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;