From 73d73e6c953dd0d63d76c1dca7f88bc04ccf4565 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Mar 2020 13:29:36 -0700 Subject: [PATCH] enhance rewriting for indexof based on #3516 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 14d5d4dfc..2cf1f0814 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1138,6 +1138,23 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result result = c; return BR_DONE; } + + if (a == b) { + if (m_autil.is_numeral(c, r)) { + if (r.is_zero()) { + result = m_autil.mk_int(0); + } + else { + result = m_autil.mk_int(-1); + } + return BR_DONE; + } + else { + result = m().mk_ite(m().mk_eq(m_autil.mk_int(0), c), m_autil.mk_int(0), m_autil.mk_int(-1)); + return BR_REWRITE2; + } + } + // Enhancement: walk segments of a, determine which segments must overlap, must not overlap, may overlap. return BR_FAILED; }