mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
add partial support for complementation of regular expressions. Handles case of complementing character ranges
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
9dbb8057ca
commit
94453033b6
|
@ -83,7 +83,7 @@ eautomaton* re2automaton::operator()(expr* e) {
|
|||
|
||||
eautomaton* re2automaton::re2aut(expr* e) {
|
||||
SASSERT(u.is_re(e));
|
||||
expr* e1, *e2;
|
||||
expr *e0, *e1, *e2;
|
||||
scoped_ptr<eautomaton> a, b;
|
||||
unsigned lo, hi;
|
||||
zstring s1, s2;
|
||||
|
@ -98,8 +98,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
|
|||
}
|
||||
else if (u.re.is_star(e, e1) && (a = re2aut(e1))) {
|
||||
a->add_final_to_init_moves();
|
||||
a->add_init_to_final_states();
|
||||
|
||||
a->add_init_to_final_states();
|
||||
return a.detach();
|
||||
}
|
||||
else if (u.re.is_plus(e, e1) && (a = re2aut(e1))) {
|
||||
|
@ -116,8 +115,6 @@ eautomaton* re2automaton::re2aut(expr* e) {
|
|||
unsigned start = s1[0];
|
||||
unsigned stop = s2[0];
|
||||
unsigned nb = s1.num_bits();
|
||||
sort_ref s(bv.mk_sort(nb), m);
|
||||
expr_ref v(m.mk_var(0, s), m);
|
||||
expr_ref _start(bv.mk_numeral(start, nb), m);
|
||||
expr_ref _stop(bv.mk_numeral(stop, nb), m);
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop));
|
||||
|
@ -127,6 +124,39 @@ eautomaton* re2automaton::re2aut(expr* e) {
|
|||
TRACE("seq", tout << "Range expression is not handled: " << mk_pp(e, m) << "\n";);
|
||||
}
|
||||
}
|
||||
else if (u.re.is_complement(e, e0)) {
|
||||
if (u.re.is_range(e0, e1, e2) && u.str.is_string(e1, s1) && u.str.is_string(e2, s2) &&
|
||||
s1.length() == 1 && s2.length() == 1) {
|
||||
unsigned start = s1[0];
|
||||
unsigned stop = s2[0];
|
||||
unsigned nb = s1.num_bits();
|
||||
sort_ref s(bv.mk_sort(nb), m);
|
||||
expr_ref v(m.mk_var(0, s), m);
|
||||
expr_ref _start(bv.mk_numeral(start, nb), m);
|
||||
expr_ref _stop(bv.mk_numeral(stop, nb), m);
|
||||
expr_ref _pred(m.mk_not(m.mk_and(bv.mk_ule(_start, v), bv.mk_ule(v, _stop))), m);
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
|
||||
return a.detach();
|
||||
}
|
||||
else if (u.re.is_to_re(e0, e1) && u.str.is_string(e1, s1) && s1.length() == 1) {
|
||||
unsigned nb = s1.num_bits();
|
||||
sort_ref s(bv.mk_sort(nb), m);
|
||||
expr_ref v(m.mk_var(0, s), m);
|
||||
expr_ref _ch(bv.mk_numeral(s1[0], nb), m);
|
||||
expr_ref _pred(m.mk_not(m.mk_eq(v, _ch)), m);
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
|
||||
return a.detach();
|
||||
}
|
||||
else if (u.re.is_to_re(e0, e1) && u.str.is_unit(e1, e2)) {
|
||||
expr_ref v(m.mk_var(0, m.get_sort(e2)), m);
|
||||
expr_ref _pred(m.mk_not(m.mk_eq(v, e2)), m);
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
|
||||
return a.detach();
|
||||
}
|
||||
else {
|
||||
TRACE("seq", tout << "Complement expression is not handled: " << mk_pp(e, m) << "\n";);
|
||||
}
|
||||
}
|
||||
else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) {
|
||||
scoped_ptr<eautomaton> eps = eautomaton::mk_epsilon(sm);
|
||||
b = eautomaton::mk_epsilon(sm);
|
||||
|
@ -225,6 +255,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
case OP_RE_INTERSECT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_re_inter(args[0], args[1], result);
|
||||
case OP_RE_COMPLEMENT:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_re_complement(args[0], result);
|
||||
case OP_RE_LOOP:
|
||||
return mk_re_loop(num_args, args, result);
|
||||
case OP_RE_EMPTY_SET:
|
||||
|
@ -967,6 +1000,26 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
|
|||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
|
||||
expr* e1, *e2;
|
||||
if (m_util.re.is_intersection(a, e1, e2)) {
|
||||
result = m_util.re.mk_union(m_util.re.mk_complement(e1), m_util.re.mk_complement(e2));
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
if (m_util.re.is_union(a, e1, e2)) {
|
||||
result = m_util.re.mk_inter(m_util.re.mk_complement(e1), m_util.re.mk_complement(e2));
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
if (m_util.re.is_empty(a)) {
|
||||
result = m_util.re.mk_full(m().get_sort(a));
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_full(a)) {
|
||||
result = m_util.re.mk_empty(m().get_sort(a));
|
||||
return BR_DONE;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
/**
|
||||
(emp n r) = emp
|
||||
|
|
|
@ -96,6 +96,7 @@ class seq_rewriter {
|
|||
br_status mk_re_concat(expr* a, expr* b, expr_ref& result);
|
||||
br_status mk_re_union(expr* a, expr* b, expr_ref& result);
|
||||
br_status mk_re_inter(expr* a, expr* b, expr_ref& result);
|
||||
br_status mk_re_complement(expr* a, expr_ref& result);
|
||||
br_status mk_re_star(expr* a, expr_ref& result);
|
||||
br_status mk_re_plus(expr* a, expr_ref& result);
|
||||
br_status mk_re_opt(expr* a, expr_ref& result);
|
||||
|
|
|
@ -456,6 +456,7 @@ void seq_decl_plugin::init() {
|
|||
m_sigs[OP_RE_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, reA);
|
||||
m_sigs[OP_RE_INTERSECT] = alloc(psig, m, "re.inter", 1, 2, reAreA, reA);
|
||||
m_sigs[OP_RE_LOOP] = alloc(psig, m, "re.loop", 1, 1, &reA, reA);
|
||||
m_sigs[OP_RE_COMPLEMENT] = alloc(psig, m, "re.complement", 1, 1, &reA, reA);
|
||||
m_sigs[OP_RE_EMPTY_SET] = alloc(psig, m, "re.empty", 1, 0, 0, reA);
|
||||
m_sigs[OP_RE_FULL_SET] = alloc(psig, m, "re.all", 1, 0, 0, reA);
|
||||
m_sigs[OP_RE_OF_PRED] = alloc(psig, m, "re.of.pred", 1, 1, &predA, reA);
|
||||
|
@ -574,7 +575,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
case OP_RE_STAR:
|
||||
case OP_RE_OPTION:
|
||||
case OP_RE_RANGE:
|
||||
case OP_RE_EMPTY_SET:
|
||||
case OP_RE_OF_PRED:
|
||||
case OP_STRING_ITOS:
|
||||
case OP_STRING_STOI:
|
||||
|
@ -587,6 +587,15 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
}
|
||||
match(*m_sigs[k], arity, domain, range, rng);
|
||||
return m.mk_func_decl(symbol("re.allchar"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_FULL_SET));
|
||||
case OP_RE_FULL_SET:
|
||||
if (!range) range = m_re;
|
||||
if (range == m_re) {
|
||||
match(*m_sigs[k], arity, domain, range, rng);
|
||||
return m.mk_func_decl(symbol("re.allchar"), arity, domain, rng, func_decl_info(m_family_id, k));
|
||||
}
|
||||
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
|
||||
|
||||
|
||||
case _OP_REGEXP_EMPTY:
|
||||
if (!range) {
|
||||
range = m_re;
|
||||
|
@ -594,6 +603,14 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
match(*m_sigs[k], arity, domain, range, rng);
|
||||
return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_EMPTY_SET));
|
||||
|
||||
case OP_RE_EMPTY_SET:
|
||||
if (!range) range = m_re;
|
||||
if (range == m_re) {
|
||||
match(*m_sigs[k], arity, domain, range, rng);
|
||||
return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, k));
|
||||
}
|
||||
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
|
||||
|
||||
case OP_RE_LOOP:
|
||||
switch (arity) {
|
||||
case 1:
|
||||
|
@ -624,6 +641,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
return m.mk_const_decl(m_stringc_sym, m_string,
|
||||
func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters));
|
||||
|
||||
case OP_RE_COMPLEMENT:
|
||||
case OP_RE_UNION:
|
||||
case OP_RE_CONCAT:
|
||||
case OP_RE_INTERSECT:
|
||||
|
@ -825,6 +843,15 @@ app* seq_util::re::mk_loop(expr* r, unsigned lo, unsigned hi) {
|
|||
return m.mk_app(m_fid, OP_RE_LOOP, 2, params, 1, &r);
|
||||
}
|
||||
|
||||
app* seq_util::re::mk_full(sort* s) {
|
||||
return m.mk_app(m_fid, OP_RE_FULL_SET, 0, 0, 0, 0, s);
|
||||
}
|
||||
|
||||
app* seq_util::re::mk_empty(sort* s) {
|
||||
return m.mk_app(m_fid, OP_RE_EMPTY_SET, 0, 0, 0, 0, s);
|
||||
}
|
||||
|
||||
|
||||
bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) {
|
||||
if (is_loop(n)) {
|
||||
app const* a = to_app(n);
|
||||
|
|
|
@ -54,6 +54,7 @@ enum seq_op_kind {
|
|||
OP_RE_UNION,
|
||||
OP_RE_INTERSECT,
|
||||
OP_RE_LOOP,
|
||||
OP_RE_COMPLEMENT,
|
||||
OP_RE_EMPTY_SET,
|
||||
OP_RE_FULL_SET,
|
||||
OP_RE_OF_PRED,
|
||||
|
@ -299,16 +300,20 @@ public:
|
|||
app* mk_concat(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_CONCAT, r1, r2); }
|
||||
app* mk_union(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_UNION, r1, r2); }
|
||||
app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); }
|
||||
app* mk_complement(expr* r) { return m.mk_app(m_fid, OP_RE_COMPLEMENT, r); }
|
||||
app* mk_star(expr* r) { return m.mk_app(m_fid, OP_RE_STAR, r); }
|
||||
app* mk_plus(expr* r) { return m.mk_app(m_fid, OP_RE_PLUS, r); }
|
||||
app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); }
|
||||
app* mk_loop(expr* r, unsigned lo);
|
||||
app* mk_loop(expr* r, unsigned lo, unsigned hi);
|
||||
app* mk_full(sort* s);
|
||||
app* mk_empty(sort* s);
|
||||
|
||||
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); }
|
||||
bool is_union(expr const* n) const { return is_app_of(n, m_fid, OP_RE_UNION); }
|
||||
bool is_intersection(expr const* n) const { return is_app_of(n, m_fid, OP_RE_INTERSECT); }
|
||||
bool is_complement(expr const* n) const { return is_app_of(n, m_fid, OP_RE_COMPLEMENT); }
|
||||
bool is_star(expr const* n) const { return is_app_of(n, m_fid, OP_RE_STAR); }
|
||||
bool is_plus(expr const* n) const { return is_app_of(n, m_fid, OP_RE_PLUS); }
|
||||
bool is_opt(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OPTION); }
|
||||
|
@ -321,6 +326,7 @@ public:
|
|||
MATCH_BINARY(is_union);
|
||||
MATCH_BINARY(is_intersection);
|
||||
MATCH_BINARY(is_range);
|
||||
MATCH_UNARY(is_complement);
|
||||
MATCH_UNARY(is_star);
|
||||
MATCH_UNARY(is_plus);
|
||||
MATCH_UNARY(is_opt);
|
||||
|
|
Loading…
Reference in a new issue