mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

Merge branch 'str-extract-semantics' into develop

Browse source
This commit is contained in:
Murphy Berzish 2017-03-14 14:14:53 -04:00
commit 9659f08322
1 changed files with 30 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/ast/rewriter/seq_rewriter.cpp
View file

@ -543,15 +543,40 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result) { br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result) {
zstring s; zstring s;
rational pos, len; rational pos, len;
if (m_util.str.is_string(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) &&
pos.is_unsigned() && len.is_unsigned() && pos.get_unsigned() + len.get_unsigned() <= s.length()) { bool constantBase = m_util.str.is_string(a, s);
unsigned _pos = pos.get_unsigned(); bool constantPos = m_autil.is_numeral(b, pos);
unsigned _len = len.get_unsigned(); bool constantLen = m_autil.is_numeral(c, len);
result = m_util.str.mk_string(s.extract(_pos, _len));
// case 1: pos<0 or len<0
// rewrite to ""
if ( (constantPos && pos.is_neg()) || (constantLen && len.is_neg()) ) {
result = m_util.str.mk_string(symbol(""));
return BR_DONE; return BR_DONE;
} }
// case 1.1: pos >= length(base)
// rewrite to ""
if (constantBase && constantPos && pos.get_unsigned() >= s.length()) {
result = m_util.str.mk_string(symbol(""));
return BR_DONE;
}
if (constantBase && constantPos && constantLen) {
if (pos.get_unsigned() + len.get_unsigned() >= s.length()) {
// case 2: pos+len goes past the end of the string
unsigned _len = s.length() - pos.get_unsigned() + 1;
result = m_util.str.mk_string(s.extract(pos.get_unsigned(), _len));
return BR_DONE;
} else {
// case 3: pos+len still within string
result = m_util.str.mk_string(s.extract(pos.get_unsigned(), len.get_unsigned()));
return BR_DONE;
}
}
return BR_FAILED; return BR_FAILED;
} }
br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
zstring c, d; zstring c, d;
if (m_util.str.is_string(a, c) && m_util.str.is_string(b, d)) { if (m_util.str.is_string(a, c) && m_util.str.is_string(b, d)) {