mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
Merge pull request #938 from mtrberzi/str-at-semantics
alternate str.at semantics check in seq_rewriter
This commit is contained in:
commit
5cff42bbfa
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue