mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
simplify code, issue #1028
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
7fab670719
commit
ceec81de0b
|
@ -440,20 +440,16 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
* (seq.unit (_ BitVector 8)) ==> String constant
|
||||
*/
|
||||
br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) {
|
||||
sort * s = m().get_sort(e);
|
||||
bv_util bvu(m());
|
||||
|
||||
if (is_sort_of(s, bvu.get_family_id(), BV_SORT)) {
|
||||
// specifically we want (_ BitVector 8)
|
||||
rational n_val;
|
||||
unsigned int n_size;
|
||||
if (bvu.is_numeral(e, n_val, n_size) && n_size == 8) {
|
||||
// convert to string constant
|
||||
zstring str(n_val.get_unsigned());
|
||||
TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;);
|
||||
result = m_util.str.mk_string(str);
|
||||
return BR_DONE;
|
||||
}
|
||||
rational n_val;
|
||||
unsigned int n_size;
|
||||
// specifically we want (_ BitVector 8)
|
||||
if (bvu.is_bv(e) && bvu.is_numeral(e, n_val, n_size) && n_size == 8) {
|
||||
// convert to string constant
|
||||
zstring str(n_val.get_unsigned());
|
||||
TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;);
|
||||
result = m_util.str.mk_string(str);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
|
|
Loading…
Reference in a new issue