mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 04:15:51 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Leonardo de Moura 2012-12-28 09:13:26 -08:00
commit d0d48c7ce2
3 changed files with 13 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/rewriter/bv_rewriter.cpp
View file

@ -63,6 +63,7 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
m_blast_eq_value = p.blast_eq_value();
m_split_concat_eq = p.split_concat_eq();
m_udiv2mul = p.udiv2mul();
m_bvnot2arith = p.bvnot2arith();
m_mkbv2num = _p.get_bool("mkbv2num", false);
}
@ -1527,6 +1528,14 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) {
}
#endif
if (m_bvnot2arith) {
// (bvnot x) --> (bvsub -1 x)
bv_size = get_bv_size(arg);
rational minus_one = (rational::power_of_two(bv_size) - numeral(1));
result = m_util.mk_bv_sub(m_util.mk_numeral(minus_one, bv_size), arg);
return BR_REWRITE1;
}
return BR_FAILED;
}

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

@ -67,6 +67,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
bool m_mkbv2num;
bool m_split_concat_eq;
bool m_udiv2mul;
bool m_bvnot2arith;
bool is_zero_bit(expr * x, unsigned idx);

4
src/ast/rewriter/bv_rewriter_params.pyg
View file

@ -7,4 +7,6 @@ def_module_params(module_name='rewriter',
("blast_eq_value", BOOL, False, "blast (some) Bit-vector equalities into bits"),
("elim_sign_ext", BOOL, True, "expand sign-ext operator using concat and extract"),
("hi_div0", BOOL, True, "use the 'hardware interpretation' for division by zero (for bit-vector terms)"),
("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation")))
("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"),
("bvnot2arith", BOOL, False, "replace (bvnot x) with (bvsub -1 x)")
))