mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
propagate has-length over map/mapi
This commit is contained in:
parent
8900db527f
commit
7d0c789af0
|
@ -2783,30 +2783,29 @@ bool theory_seq::get_length(expr* e, rational& val) {
|
|||
todo.push_back(e1);
|
||||
todo.push_back(e2);
|
||||
}
|
||||
else if (m_util.str.is_unit(c)) {
|
||||
else if (m_util.str.is_unit(c))
|
||||
val += rational(1);
|
||||
}
|
||||
else if (m_util.str.is_empty(c)) {
|
||||
else if (m_util.str.is_empty(c))
|
||||
continue;
|
||||
}
|
||||
else if (m_util.str.is_string(c, s)) {
|
||||
else if (m_util.str.is_map(c, e1, e2))
|
||||
todo.push_back(e2);
|
||||
else if (m_util.str.is_mapi(c, e1, e2, c))
|
||||
todo.push_back(c);
|
||||
else if (m_util.str.is_string(c, s))
|
||||
val += rational(s.length());
|
||||
}
|
||||
else if (!has_length(c)) {
|
||||
len = mk_len(c);
|
||||
else
|
||||
continue;
|
||||
len = mk_len(c);
|
||||
if (!has_length(c)) {
|
||||
add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(0))));
|
||||
TRACE("seq", tout << "literal has no length " << mk_pp(c, m) << "\n";);
|
||||
return false;
|
||||
}
|
||||
else {
|
||||
len = mk_len(c);
|
||||
if (m_arith_value.get_value(len, val1) && !val1.is_neg()) {
|
||||
val += val1;
|
||||
}
|
||||
else {
|
||||
TRACE("seq", tout << "length has not been internalized " << mk_pp(c, m) << "\n";);
|
||||
return false;
|
||||
}
|
||||
else if (m_arith_value.get_value(len, val1) && !val1.is_neg())
|
||||
val += val1;
|
||||
else {
|
||||
TRACE("seq", tout << "length has not been internalized " << mk_pp(c, m) << "\n";);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
CTRACE("seq", !val.is_int(), tout << "length is not an integer\n";);
|
||||
|
|
Loading…
Reference in a new issue