From 9a76bf0aa24185229e8d900d1025a130a25dbba1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Oct 2021 13:59:28 -0700 Subject: [PATCH] #5591 nth issue --- src/ast/rewriter/seq_rewriter.cpp | 26 ++++++++++++++++++-------- src/ast/seq_decl_plugin.h | 1 + 2 files changed, 19 insertions(+), 8 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index a956718dc..38fa1e1d1 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1603,23 +1603,33 @@ br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) { result = s; return BR_DONE; } - if (str().is_extract(a, s, p, len) && m_autil.is_numeral(p, pos1)) { + if (str().is_extract(a, s, p, len) && m_autil.is_numeral(p, pos1) && pos1 > 0) { expr_ref_vector lens(m()); rational pos2; + /* + * nth(s[k, |s| - k], b) = + * b < 0 -> nth_u(a, b) + * b + k < |s| -> nth(s, b + k) + * k >= |s| -> nth_u(empty, b) + * k < |s| <= b + k -> nth_u(a, b) + */ if (get_lengths(len, lens, pos2) && (pos1 == -pos2) && (lens.size() == 1) && (lens.get(0) == s)) { - expr_ref idx(m_autil.mk_int(pos1), m()); - idx = m_autil.mk_add(b, idx); - expr* es[2] = { s, idx }; - result = m().mk_app(m_util.get_family_id(), OP_SEQ_NTH, 2, es); + expr_ref k(m_autil.mk_int(pos1), m()); + expr_ref case1(str().mk_nth_i(s, m_autil.mk_add(b, k)), m()); + expr_ref case2(str().mk_nth_u(str().mk_empty(s->get_sort()), b), m()); + expr_ref case3(str().mk_nth_u(a, b), m()); + result = case3; + result = m().mk_ite(m_autil.mk_lt(m_autil.mk_add(k, b), str().mk_length(s)), case1, result); + result = m().mk_ite(m_autil.mk_ge(k, str().mk_length(s)), case2, result); + result = m().mk_ite(m_autil.mk_lt(b, zero()), case3, result); return BR_REWRITE_FULL; } } - expr* es[2] = { a, b}; expr* la = str().mk_length(a); result = m().mk_ite(m().mk_and(m_autil.mk_ge(b, zero()), m().mk_not(m_autil.mk_le(la, b))), - m().mk_app(m_util.get_family_id(), OP_SEQ_NTH_I, 2, es), - m().mk_app(m_util.get_family_id(), OP_SEQ_NTH_U, 2, es)); + str().mk_nth_i(a, b), + str().mk_nth_u(a, b)); return BR_REWRITE_FULL; } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 6bffbf62e..16edebee9 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -286,6 +286,7 @@ public: app* mk_at(expr* s, expr* i) const { expr* es[2] = { s, i }; return m.mk_app(m_fid, OP_SEQ_AT, 2, es); } app* mk_nth(expr* s, expr* i) const { expr* es[2] = { s, i }; return m.mk_app(m_fid, OP_SEQ_NTH, 2, es); } app* mk_nth_i(expr* s, expr* i) const { expr* es[2] = { s, i }; return m.mk_app(m_fid, OP_SEQ_NTH_I, 2, es); } + app* mk_nth_u(expr* s, expr* i) const { expr* es[2] = { s, i }; return m.mk_app(m_fid, OP_SEQ_NTH_U, 2, es); } app* mk_nth_c(expr* s, unsigned i) const; app* mk_substr(expr* a, expr* b, expr* c) const { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); }