From e83f31949e164d36a3e875003855bca8b7f7d8c6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 6 Mar 2021 12:35:15 -0800
Subject: [PATCH] fix #5074, add rewrite rules to simplify indexof special
cases
---
src/ast/rewriter/seq_axioms.cpp | 2 +-
src/ast/rewriter/seq_rewriter.cpp | 13 +++++++++++--
2 files changed, 12 insertions(+), 3 deletions(-)
diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index 2be078b9f..dd4b05eb3 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -420,7 +420,7 @@ namespace seq {
expr_ref cnt(seq.str.mk_contains(t, s), m);
expr_ref i_eq_m1 = mk_eq(i, minus_one);
expr_ref i_eq_0 = mk_eq(i, zero);
- expr_ref s_eq_empty = mk_eq_empty(s);
+ expr_ref s_eq_empty = mk_eq(s, seq.str.mk_empty(s->get_sort()));
expr_ref t_eq_empty = mk_eq_empty(t);
// |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index ce407e243..d36861ea8 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1578,6 +1578,7 @@ br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) {
indexof(s, b, c) -> -1 if c < 0
indexof(a, "", 0) -> if a = "" then 0 else -1
indexof("", b, r) -> if b = "" and r = 0 then 0 else -1
+ indexof(a, "", x) -> if 0 <= x <= len(a) then x else - 1
indexof(unit(x)+a, b, r+1) -> indexof(a, b, r)
indexof(unit(x)+a, unit(y)+b, 0) -> indexof(a,unit(y)+b, 0) if x != y
indexof(substr(x,y,len1), z, len2) -> -1 if len2 > len1
@@ -1591,11 +1592,11 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
if (isc1 && isc2 && m_autil.is_numeral(c, r) && r.is_unsigned()) {
int idx = s1.indexofu(s2, r.get_unsigned());
- result = m_autil.mk_numeral(rational(idx), true);
+ result = m_autil.mk_int(idx);
return BR_DONE;
}
if (m_autil.is_numeral(c, r) && r.is_neg()) {
- result = m_autil.mk_numeral(rational(-1), true);
+ result = m_autil.mk_int(-1);
return BR_DONE;
}
@@ -1604,6 +1605,14 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
return BR_DONE;
}
+ if (str().is_empty(b)) {
+ result = m().mk_ite(m().mk_and(m_autil.mk_le(m_autil.mk_int(0), c),
+ m_autil.mk_le(c, str().mk_length(a))),
+ c,
+ m_autil.mk_int(-1));
+ return BR_REWRITE2;
+ }
+
if (str().is_empty(a)) {
expr* emp = str().mk_is_empty(b);