diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index c65f51144..c9745a46b 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -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 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 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 diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 2860f11a0..83dd8f653 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -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); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 3215840bc..58355eb0e 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -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); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 4739af84b..4100fe6cc 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -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);