mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

z3str3: reduce int-to-string in bitvector model construction

Browse source
This commit is contained in:
Murphy Berzish 2020-02-28 18:14:25 -05:00 • committed by Nikolaj Bjorner
parent ba79700096
commit 8881084449
1 changed files with 22 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/theory_str_mc.cpp
View file

@ -712,6 +712,28 @@ namespace smt {
eqc_chars.push_back(base_chars.get(pos_value.get_unsigned())); eqc_chars.push_back(base_chars.get(pos_value.get_unsigned()));
} }
return true; 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
}
TRACE("str_fl", tout << "reduce int.to.str: n=" << iValue << std::endl;);
if (iValue.is_neg()) {
// return the empty string
eqc_chars.reset();
} else {
// 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 { } else {
TRACE("str_fl", tout << "string term " << mk_pp(term, m) << " handled as uninterpreted function" << std::endl;); TRACE("str_fl", tout << "string term " << mk_pp(term, m) << " handled as uninterpreted function" << std::endl;);
if (!uninterpreted_to_char_subterm_map.contains(term)) { if (!uninterpreted_to_char_subterm_map.contains(term)) {