mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
7caae3f5d2
commit
e1027790ae
|
@ -676,8 +676,7 @@ bool seq_rewriter::is_suffix(expr* s, expr* offset, expr* len) {
|
|||
(a.neg(), m_autil.is_numeral(offset, b) &&
|
||||
b.is_pos() &&
|
||||
a == b &&
|
||||
lens.size() == 1 &&
|
||||
lens[0] == s);
|
||||
lens.contains(s));
|
||||
}
|
||||
|
||||
bool seq_rewriter::sign_is_determined(expr* e, sign& s) {
|
||||
|
@ -696,18 +695,6 @@ bool seq_rewriter::sign_is_determined(expr* e, sign& s) {
|
|||
}
|
||||
return true;
|
||||
}
|
||||
if (m_util.str.is_length(e)) {
|
||||
s = sign_pos;
|
||||
return true;
|
||||
}
|
||||
rational pos;
|
||||
if (m_autil.is_numeral(e, pos)) {
|
||||
if (pos.is_pos())
|
||||
s = sign_pos;
|
||||
else if (pos.is_neg())
|
||||
s = sign_neg;
|
||||
return true;
|
||||
}
|
||||
if (m_autil.is_mul(e)) {
|
||||
for (expr* arg : *to_app(e)) {
|
||||
sign s1;
|
||||
|
@ -726,7 +713,19 @@ bool seq_rewriter::sign_is_determined(expr* e, sign& s) {
|
|||
}
|
||||
return true;
|
||||
}
|
||||
return true;
|
||||
if (m_util.str.is_length(e)) {
|
||||
s = sign_pos;
|
||||
return true;
|
||||
}
|
||||
rational r;
|
||||
if (m_autil.is_numeral(e, r)) {
|
||||
if (r.is_pos())
|
||||
s = sign_pos;
|
||||
else if (r.is_neg())
|
||||
s = sign_neg;
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result) {
|
||||
|
|
Loading…
Reference in a new issue