mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

experimental rewrite of bitvector unit sequences to string constants

Browse source
This commit is contained in:
Murphy Berzish 2017-03-06 13:58:03 -05:00
parent 51e03c2371
commit 577cb19745
2 changed files with 35 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -322,7 +322,13 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
switch(f->get_decl_kind()) {
case OP_SEQ_UNIT:
return BR_FAILED;
// TODO configuration param
if (true) {
SASSERT(num_args == 1);
return mk_seq_unit(args[0], result);
} else {
return BR_FAILED;
}
case OP_SEQ_EMPTY:
return BR_FAILED;
case OP_RE_PLUS:
@ -427,6 +433,33 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
return BR_FAILED;
}
/*
* (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)) {
if (n_size == 8) {
// convert to string constant
char ch = (char)n_val.get_int32();
TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << ch << "\"" << std::endl;);
char s_tmp[2] = {ch, '\0'};
symbol s(s_tmp);
result = m_util.str.mk_string(s);
return BR_DONE;
}
}
}
return BR_FAILED;
}
/*
string + string = string
a + (b + c) = (a + b) + c

1
src/ast/rewriter/seq_rewriter.h
View file

@ -98,6 +98,7 @@ class seq_rewriter {
re2automaton m_re2aut;
expr_ref_vector m_es, m_lhs, m_rhs;
br_status mk_seq_unit(expr* e, expr_ref& result);
br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
br_status mk_seq_length(expr* a, expr_ref& result);
br_status mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result);