From 5c9d7538a03c0e18b1e99df863058e5218cf0022 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 13 Mar 2017 14:39:12 -0400 Subject: [PATCH] add alternate str.at semantics check in seq_rewriter this rewrites to empty string if the index is negative or beyond the length of the string, which is consistent with CVC4's semantics for this term --- src/ast/rewriter/seq_rewriter.cpp | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 26c3e23e4..adb70c30c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -598,14 +598,25 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } +/* + * (str.at s i), constants s/i, i < 0 or i >= |s| ==> (str.at s i) = "" + */ 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) && r.is_unsigned()) { - unsigned j = r.get_unsigned(); - if (j < c.length()) { - result = m_util.str.mk_string(c.extract(j, 1)); + if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r)) { + if (r.is_neg()) { + result = m_util.str.mk_string(symbol("")); 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; + } } } return BR_FAILED;