mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

z3str3: fix value cex in int.to.str model construction

Browse source
This commit is contained in:
Murphy Berzish 2020-02-28 20:30:09 -05:00 committed by Nikolaj Bjorner
parent 069a5fba16
commit 6ec9f9112c
1 changed files with 39 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

76
src/smt/theory_str_mc.cpp
View file

@ -712,43 +712,45 @@ namespace smt {
eqc_chars.push_back(base_chars.get(pos_value.get_unsigned()));
}
return true;
} else if (u.str.is_itos(term, arg0)) {
expr_ref i(arg0, m);
arith_value v(m);
v.init(&get_context());
rational iValue;
bool iValue_exists = v.get_value(i, iValue);
if (!iValue_exists) {
NOT_IMPLEMENTED_YET(); // TODO force assignment in arith solver
}
rational termLen;
bool termLen_exists = v.get_value(mk_strlen(term), termLen);
if(!termLen_exists) {
NOT_IMPLEMENTED_YET(); // TODO force assignment in arith solver
}
TRACE("str_fl", tout << "reduce int.to.str: n=" << iValue << std::endl;);
if (iValue.is_neg()) {
if (!termLen.is_zero()) {
// conflict
cex = expr_ref(m.mk_not(m.mk_and(m_autil.mk_le(arg0, mk_int(-1)), m.mk_not(mk_strlen(term)))), m);
return false;
}
// return the empty string
eqc_chars.reset();
return true;
} else {
if (termLen.get_unsigned() != iValue.to_string().length()) {
// conflict
cex = expr_ref(m.mk_not(m.mk_and(get_context().mk_eq_atom(mk_strlen(term), mk_int(termLen)), get_context().mk_eq_atom(arg0, mk_int(iValue)))), m);
return false;
}
// convert iValue to a constant
zstring iValue_str = zstring(iValue.to_string().c_str());
for (unsigned idx = 0; idx < iValue_str.length(); ++idx) {
expr_ref chTerm(bitvector_character_constants.get(iValue_str[idx]), sub_m);
eqc_chars.push_back(chTerm);
}
return true;
} else if (u.str.is_itos(term, arg0)) {
expr_ref i(arg0, m);
arith_value v(m);
v.init(&get_context());
rational iValue;
bool iValue_exists = v.get_value(i, iValue);
if (!iValue_exists) {
cex = expr_ref(m.mk_or(m_autil.mk_ge(arg0, mk_int(0)), m_autil.mk_le(arg0, mk_int(0))), m);
return false;
}
rational termLen;
bool termLen_exists = v.get_value(mk_strlen(term), termLen);
if(!termLen_exists) {
cex = expr_ref(m.mk_or(m_autil.mk_ge(mk_strlen(term), mk_int(0)), m_autil.mk_le(mk_strlen(term), mk_int(0))), m);
return false;
}
TRACE("str_fl", tout << "reduce int.to.str: n=" << iValue << std::endl;);
if (iValue.is_neg()) {
if (!termLen.is_zero()) {
// conflict
cex = expr_ref(m.mk_not(m.mk_and(m_autil.mk_le(arg0, mk_int(-1)), m.mk_not(mk_strlen(term)))), m);
return false;
}
// return the empty string
eqc_chars.reset();
return true;
} else {
if (termLen.get_unsigned() != iValue.to_string().length()) {
// conflict
cex = expr_ref(m.mk_not(m.mk_and(get_context().mk_eq_atom(mk_strlen(term), mk_int(termLen)), get_context().mk_eq_atom(arg0, mk_int(iValue)))), m);
return false;
}
// convert iValue to a constant
zstring iValue_str = zstring(iValue.to_string().c_str());
for (unsigned idx = 0; idx < iValue_str.length(); ++idx) {
expr_ref chTerm(bitvector_character_constants.get(iValue_str[idx]), sub_m);
eqc_chars.push_back(chTerm);
}
return true;
}
} else {
TRACE("str_fl", tout << "string term " << mk_pp(term, m) << " handled as uninterpreted function" << std::endl;);