From cd0cd82eb7a018a9b7ec753f30887a2cc5ceb3b9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Sep 2019 08:55:53 -0700 Subject: [PATCH] add rewrites for #2575 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 85 ++++++++++++++++++++++++------- src/ast/rewriter/seq_rewriter.h | 2 +- src/ast/seq_decl_plugin.cpp | 8 +++ src/ast/seq_decl_plugin.h | 4 +- 4 files changed, 78 insertions(+), 21 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 30d43105c..6af16dd06 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -441,7 +441,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con st = mk_re_complement(args[0], result); break; case OP_RE_LOOP: - st = mk_re_loop(num_args, args, result); + st = mk_re_loop(f, num_args, args, result); break; case OP_RE_EMPTY_SET: return BR_FAILED; @@ -1682,27 +1682,41 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) { result = m_util.re.mk_concat(b, a); return BR_DONE; } - { - unsigned lo1, hi1, lo2, hi2; - if (m_util.re.is_loop(a, a1, lo1, hi1) && m_util.re.is_loop(b, b1, lo2, hi2) && a1 == b1) { - result = m_util.re.mk_loop(a1, lo1 + lo2, hi1 + hi2); - return BR_DONE; - } - if (m_util.re.is_loop(a, a1, lo1) && m_util.re.is_loop(b, b1, lo2) && a1 == b1) { + unsigned lo1, hi1, lo2, hi2; + + if (m_util.re.is_loop(a, a1, lo1, hi1) && m_util.re.is_loop(b, b1, lo2, hi2) && a1 == b1) { + SASSERT(lo1 <= hi1 && lo2 <= hi2); + result = m_util.re.mk_loop(a1, lo1 + lo2, hi1 + hi2); + return BR_DONE; + } + if (m_util.re.is_loop(a, a1, lo1) && m_util.re.is_loop(b, b1, lo2) && a1 == b1) { + result = m_util.re.mk_loop(a1, lo1 + lo2); + return BR_DONE; + } + for (unsigned i = 0; i < 2; ++i) { + // (loop a lo1) + (loop a lo2 hi2) = (loop a lo1 + lo2) + if (m_util.re.is_loop(a, a1, lo1) && m_util.re.is_loop(b, b1, lo2, hi2) && a1 == b1) { + SASSERT(lo2 <= hi2); result = m_util.re.mk_loop(a1, lo1 + lo2); return BR_DONE; } - } - { - expr* lo1, *hi1, *lo2, *hi2; - if (m_util.re.is_loop(a, a1, lo1, hi1) && m_util.re.is_loop(b, b1, lo2, hi2) && a1 == b1) { - result = m_util.re.mk_loop(a1, m_autil.mk_add(lo1, lo2), m_autil.mk_add(hi1, hi2)); + // (loop a lo1 hi1) + a* = (loop a lo1) + if (m_util.re.is_loop(a, a1, lo1, hi1) && m_util.re.is_star(b, b1) && a1 == b1) { + result = m_util.re.mk_loop(a1, lo1); return BR_DONE; } - if (m_util.re.is_loop(a, a1, lo1) && m_util.re.is_loop(b, b1, lo2) && a1 == b1) { - result = m_util.re.mk_loop(a1, m_autil.mk_add(lo1, lo2)); + // (loop a lo1) + a* = (loop a lo1) + if (m_util.re.is_loop(a, a1, lo1) && m_util.re.is_star(b, b1) && a1 == b1) { + result = a; return BR_DONE; } + // (loop a lo1 hi1) + a = (loop a lo1+1 hi1+1) + if (m_util.re.is_loop(a, a1, lo1, hi1) && a1 == b) { + SASSERT(lo1 <= hi1); + result = m_util.re.mk_loop(a1, lo1+1, hi1+1); + return BR_DONE; + } + std::swap(a, b); } return BR_FAILED; } @@ -1804,22 +1818,55 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { } -br_status seq_rewriter::mk_re_loop(unsigned num_args, expr* const* args, expr_ref& result) { +br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { rational n1, n2; + unsigned lo, hi; + expr* a = nullptr; switch (num_args) { case 1: + // (loop (loop a lo hi) lo2 hi2) = (loop lo*lo2 hi*hi2) + if (m_util.re.is_loop(args[0], a, lo, hi) && f->get_num_parameters() == 2) { + result = m_util.re.mk_loop(a, f->get_parameter(0).get_int() * lo, f->get_parameter(1).get_int() * hi); + return BR_REWRITE1; + } + // (loop (loop a lo hi) lo2) = (loop lo*lo2) + if (m_util.re.is_loop(args[0], a, lo, hi) && f->get_num_parameters() == 1) { + result = m_util.re.mk_loop(a, f->get_parameter(0).get_int() * lo); + return BR_REWRITE1; + } + // (loop (loop a lo) lo2 ..) = (loop lo*lo2) + if (m_util.re.is_loop(args[0], a, lo)) { + SASSERT(f->get_num_parameters() >= 1); + result = m_util.re.mk_loop(a, f->get_parameter(0).get_int() * lo); + return BR_REWRITE1; + } + // (loop a 0 0) = "" + if (f->get_num_parameters() == 2 && f->get_parameter(1).get_int() == 0) { + result = m_util.re.mk_to_re(m_util.str.mk_empty(m_util.re.to_seq(m().get_sort(args[0])))); + return BR_DONE; + } + // (loop a 1 1) = a + if (f->get_num_parameters() == 2 && f->get_parameter(0).get_int() == 1 && f->get_parameter(1).get_int() == 1) { + result = args[0]; + return BR_DONE; + } + // (loop a 0) = a* + if (f->get_num_parameters() == 1 && f->get_parameter(0).get_int() == 0) { + result = m_util.re.mk_star(args[0]); + return BR_DONE; + } break; case 2: if (m_autil.is_numeral(args[1], n1) && n1.is_unsigned()) { result = m_util.re.mk_loop(args[0], n1.get_unsigned()); - return BR_DONE; + return BR_REWRITE1; } break; case 3: if (m_autil.is_numeral(args[1], n1) && n1.is_unsigned() && - m_autil.is_numeral(args[2], n2) && n2.is_unsigned()) { + m_autil.is_numeral(args[2], n2) && n2.is_unsigned() && n1 <= n2) { result = m_util.re.mk_loop(args[0], n1.get_unsigned(), n2.get_unsigned()); - return BR_DONE; + return BR_REWRITE1; } break; default: diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 6e15a0b55..756ccb207 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -133,7 +133,7 @@ class seq_rewriter { 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); - br_status mk_re_loop(unsigned num_args, expr* const* args, expr_ref& result); + br_status mk_re_loop(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result); br_status mk_re_range(expr* lo, expr* hi, expr_ref& result); bool cannot_contain_prefix(expr* a, expr* b); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 105a498f9..5d2628c60 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -747,6 +747,9 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, if (num_parameters == 0 || num_parameters > 2 || !parameters[0].is_int() || (num_parameters == 2 && !parameters[1].is_int())) { m.raise_exception("Expecting two numeral parameters to function re-loop"); } + if (num_parameters == 2 && parameters[0].get_int() > parameters[1].get_int()) { + m.raise_exception("Lower bound cannot be higher than upper bound in loop specfication"); + } return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters)); case 2: if (m_re != domain[0] || !arith_util(m).is_int(domain[1])) { @@ -1083,6 +1086,11 @@ app* seq_util::str::mk_is_empty(expr* s) const { } +sort* seq_util::re::to_seq(sort* re) { + SASSERT(u.is_re(re)); + return to_sort(re->get_parameter(0).get_ast()); +} + app* seq_util::re::mk_loop(expr* r, unsigned lo) { parameter param(lo); return m.mk_app(m_fid, OP_RE_LOOP, 1, ¶m, 1, &r); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index c72252641..6b0a8047d 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -348,11 +348,13 @@ public: class re { ast_manager& m; + seq_util& u; family_id m_fid; public: - re(seq_util& u): m(u.m), m_fid(u.m_fid) {} + re(seq_util& u): u(u), m(u.m), m_fid(u.m_fid) {} sort* mk_re(sort* seq) { parameter param(seq); return m.mk_sort(m_fid, RE_SORT, 1, ¶m); } + sort* to_seq(sort* re); app* mk_to_re(expr* s) { return m.mk_app(m_fid, OP_SEQ_TO_RE, 1, &s); } app* mk_in_re(expr* s, expr* r) { return m.mk_app(m_fid, OP_SEQ_IN_RE, s, r); }