From 05c267b8d8ad4cf3c00e104453f2049ecd665a72 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Mar 2017 15:37:47 -0700 Subject: [PATCH] make seq.at operations generic Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index adb70c30c..26918261e 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -604,20 +604,21 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) { zstring c; rational r; - if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r)) { + if (m_autil.is_numeral(b, r)) { if (r.is_neg()) { - result = m_util.str.mk_string(symbol("")); + result = m_util.str.mk_empty(m().get_sort(a)); + return BR_DONE; + } + unsigned len = 0; + bool bounded = min_length(1, &a, len); + if (bounded && r >= rational(len)) { + result = m_util.str.mk_empty(m().get_sort(a)); return BR_DONE; - } else if (r.is_unsigned()) { - unsigned j = r.get_unsigned(); - if (j < c.length()) { - result = m_util.str.mk_string(c.extract(j, 1)); - return BR_DONE; - } else { - result = m_util.str.mk_string(symbol("")); - return BR_DONE; - } } + if (m_util.str.is_string(a, c) && r.is_unsigned() && r < rational(c.length())) { + result = m_util.str.mk_string(c.extract(r.get_unsigned(), 1)); + return BR_DONE; + } } return BR_FAILED; }