From 7e452254c385f76d0cd18af3ba72657cbf09a364 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Nov 2019 11:24:18 -0800 Subject: [PATCH] distribute string and regex concatenation on literals, scenario exposed by #2668 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 258d920e7..90e3c85f0 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1581,6 +1581,11 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { result = m().mk_true(); return BR_DONE; } + expr* b1 = nullptr; + if (m_util.re.is_to_re(b, b1)) { + result = m().mk_eq(a, b1); + return BR_REWRITE1; + } scoped_ptr aut; expr_ref_vector seq(m()); if (!(aut = m_re2aut(b))) { @@ -1694,6 +1699,10 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) { return BR_DONE; } expr* a1 = nullptr, *b1 = nullptr; + if (m_util.re.is_to_re(a, a1) && m_util.re.is_to_re(b, b1)) { + result = m_util.re.mk_to_re(m_util.str.mk_concat(a1, b1)); + return BR_REWRITE2; + } if (m_util.re.is_star(a, a1) && m_util.re.is_star(b, b1) && a1 == b1) { result = a; return BR_DONE;