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

Add option bvnot2arith

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-27 20:28:42 -08:00
parent 1a09523c99
commit 8515044f8b
3 changed files with 13 additions and 1 deletions
Show stats 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_blast_eq_value = p.blast_eq_value();
m_split_concat_eq = p.split_concat_eq(); m_split_concat_eq = p.split_concat_eq();
m_udiv2mul = p.udiv2mul(); m_udiv2mul = p.udiv2mul();
m_bvnot2arith = p.bvnot2arith();
m_mkbv2num = _p.get_bool("mkbv2num", false); m_mkbv2num = _p.get_bool("mkbv2num", false);
} }
@ -1527,6 +1528,14 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) {
} }
#endif #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; 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_mkbv2num;
bool m_split_concat_eq; bool m_split_concat_eq;
bool m_udiv2mul; bool m_udiv2mul;
bool m_bvnot2arith;
bool is_zero_bit(expr * x, unsigned idx); 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"), ("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"), ("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)"), ("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)")
))