mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

make seq.at operations generic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-14 15:37:47 -07:00
parent 0668ba5f6c
commit 05c267b8d8
1 changed files with 12 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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;
}