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

Merge remote-tracking branch 'upstream/master'

Browse source
This commit is contained in:
Lev Nachmanson 2017-05-16 12:04:20 -07:00
commit e78a799b53
1 changed files with 9 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -440,25 +440,17 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
* (seq.unit (_ BitVector 8)) ==> String constant * (seq.unit (_ BitVector 8)) ==> String constant
*/ */
br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) { br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) {
sort * s = m().get_sort(e);
bv_util bvu(m()); bv_util bvu(m());
if (is_sort_of(s, bvu.get_family_id(), BV_SORT)) {
// specifically we want (_ BitVector 8)
rational n_val; rational n_val;
unsigned int n_size; unsigned int n_size;
if (bvu.is_numeral(e, n_val, n_size)) { // specifically we want (_ BitVector 8)
if (n_size == 8) { if (bvu.is_bv(e) && bvu.is_numeral(e, n_val, n_size) && n_size == 8) {
// convert to string constant // convert to string constant
char ch = (char)n_val.get_int32(); zstring str(n_val.get_unsigned());
TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << ch << "\"" << std::endl;); TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;);
char s_tmp[2] = {ch, '\0'}; result = m_util.str.mk_string(str);
symbol s(s_tmp);
result = m_util.str.mk_string(s);
return BR_DONE; return BR_DONE;
} }
}
}
return BR_FAILED; return BR_FAILED;
} }