From ba1ca336376341d4a3c86843cbb6df0cb22bb541 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 6 Jun 2020 12:54:44 -0700 Subject: [PATCH] normalization of union/intersection Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 89 ++++++++++++++++++++++++++++++- src/ast/rewriter/seq_rewriter.h | 1 + src/ast/rewriter/th_rewriter.cpp | 2 +- src/smt/seq_regex.cpp | 5 +- 4 files changed, 91 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 26021f9b6..9246cb390 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -416,6 +416,9 @@ br_status seq_rewriter::mk_bool_app(func_decl* f, unsigned n, expr* const* args, return mk_bool_app_helper(true, n, args, result); case OP_OR: return mk_bool_app_helper(false, n, args, result); + case OP_EQ: + SASSERT(n == 2); + // return mk_eq_helper(args[0], args[1], result); default: return BR_FAILED; } @@ -492,7 +495,27 @@ br_status seq_rewriter::mk_bool_app_helper(bool is_and, unsigned n, expr* const* } } - result = is_and ? m().mk_and(new_args.size(), new_args.c_ptr()) : m().mk_or(new_args.size(), new_args.c_ptr()); + result = is_and ? m().mk_and(new_args) : m().mk_or(new_args); + return BR_REWRITE_FULL; +} + +br_status seq_rewriter::mk_eq_helper(expr* a, expr* b, expr_ref& result) { + expr* sa = nullptr, *ra = nullptr, *sb = nullptr, *rb = nullptr; + if (str().is_in_re(b)) + std::swap(a, b); + if (!str().is_in_re(a, sa, ra)) + return BR_FAILED; + bool is_not = m().is_not(b, b); + if (!str().is_in_re(b, sb, rb)) + return BR_FAILED; + if (sa != sb) + return BR_FAILED; + // sa in ra = sb in rb; + // sa in (ra n rb) u (C(ra) n C(rb)) + if (is_not) + rb = re().mk_complement(rb); + expr* r = re().mk_union(re().mk_inter(ra, rb), re().mk_inter(re().mk_complement(ra), re().mk_complement(rb))); + result = re().mk_in_re(sa, r); return BR_REWRITE_FULL; } @@ -2870,6 +2893,35 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) { result = b; return BR_DONE; } + expr* ac = nullptr, *bc = nullptr; + expr* a1 = nullptr, *a2 = nullptr; + expr* b1 = nullptr, *b2 = nullptr; + // ensure union is right-associative + // and swap-sort entries + if (re().is_union(a, a1, a2)) { + result = re().mk_union(a1, re().mk_union(a2, b)); + return BR_REWRITE2; + } + auto mk_full = [&]() { return re().mk_full_seq(m().get_sort(a)); }; + auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); }; + if (re().is_union(b, b1, b2)) { + if (a == b1) { + result = b; + return BR_DONE; + } + if (re().is_complement(a, ac) && b1 == ac) { + result = mk_full(); + return BR_DONE; + } + if (re().is_complement(b1, bc) && a == bc) { + result = mk_full(); + return BR_DONE; + } + if (get_id(a) > get_id(b1)) { + result = re().mk_union(b1, re().mk_union(a, b2)); + return BR_REWRITE2; + } + } return BR_FAILED; } @@ -2891,6 +2943,10 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) { result = re().mk_empty(m().get_sort(a)); return BR_DONE; } + if (re().is_complement(a, e1)) { + result = e1; + return BR_DONE; + } return BR_FAILED; } @@ -2923,9 +2979,38 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { return BR_DONE; } expr* ac = nullptr, *bc = nullptr; + expr* a1 = nullptr, *a2 = nullptr; + expr* b1 = nullptr, *b2 = nullptr; + + // ensure intersection is right-associative + // and swap-sort entries + if (re().is_intersection(a, a1, a2)) { + result = re().mk_inter(a1, re().mk_inter(a2, b)); + return BR_REWRITE2; + } + auto mk_empty = [&]() { return re().mk_empty(m().get_sort(a)); }; + auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); }; + if (re().is_intersection(b, b1, b2)) { + if (a == b1) { + result = b; + return BR_DONE; + } + if (re().is_complement(a, ac) && b1 == ac) { + result = mk_empty(); + return BR_DONE; + } + if (re().is_complement(b1, bc) && a == bc) { + result = mk_empty(); + return BR_DONE; + } + if (get_id(a) > get_id(b1)) { + result = re().mk_inter(b1, re().mk_inter(a, b2)); + return BR_REWRITE2; + } + } if ((re().is_complement(a, ac) && ac == b) || (re().is_complement(b, bc) && bc == a)) { - result = re().mk_empty(m().get_sort(a)); + result = mk_empty(); return BR_DONE; } if (re().is_to_re(b)) diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 6b7b06653..8464b2fd4 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -238,6 +238,7 @@ class seq_rewriter { bool rewrite_contains_pattern(expr* a, expr* b, expr_ref& result); br_status mk_bool_app_helper(bool is_and, unsigned n, expr* const* args, expr_ref& result); + br_status mk_eq_helper(expr* a, expr* b, expr_ref& result); bool cannot_contain_prefix(expr* a, expr* b); bool cannot_contain_suffix(expr* a, expr* b); diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 6ba8bc481..340c76805 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -203,7 +203,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { if (st != BR_FAILED) return st; } - if ((k == OP_AND || k == OP_OR) && m_seq_rw.u().has_re()) { + if ((k == OP_AND || k == OP_OR /*|| k == OP_EQ*/) && m_seq_rw.u().has_re()) { st = m_seq_rw.mk_bool_app(f, num, args, result); if (st != BR_FAILED) return st; diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index c9dcb7181..b6c438546 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -304,11 +304,10 @@ namespace smt { literal_vector lits; for (unsigned i = 0; i < m_s_in_re.size(); ++i) { auto const& entry = m_s_in_re[i]; - std::cout << "CHECK " << i << " " << mk_pp(s, m) << " " << mk_pp(entry.m_s, m) << "\n"; - enode* n1 = th.ensure_enode(entry.m_s); - enode* n2 = th.ensure_enode(s); if (!entry.m_active) continue; + enode* n1 = th.ensure_enode(entry.m_s); + enode* n2 = th.ensure_enode(s); if (n1->get_root() != n2->get_root()) continue; if (entry.m_re == regex)