mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix spelling

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-09 10:23:37 -08:00
parent b69ad786f2
commit 51fa40ece5
4 changed files with 39 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

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

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

2
src/ast/rewriter/seq_rewriter.h
View file

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

6
src/ast/seq_decl_plugin.cpp
View file

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

8
src/ast/seq_decl_plugin.h
View file

@ -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 @@ 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_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 @@ 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_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 @@ public:
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;