From 8515044f8bec7d3daa30570dc6364c4a26db1cec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 27 Dec 2012 20:28:42 -0800 Subject: [PATCH] Add option bvnot2arith Signed-off-by: Leonardo de Moura --- src/ast/rewriter/bv_rewriter.cpp | 9 +++++++++ src/ast/rewriter/bv_rewriter.h | 1 + src/ast/rewriter/bv_rewriter_params.pyg | 4 +++- 3 files changed, 13 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index f8ff27337..44efe0199 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -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; } diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index ba5ac5580..a94fd18c1 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -67,6 +67,7 @@ class bv_rewriter : public poly_rewriter { bool m_mkbv2num; bool m_split_concat_eq; bool m_udiv2mul; + bool m_bvnot2arith; bool is_zero_bit(expr * x, unsigned idx); diff --git a/src/ast/rewriter/bv_rewriter_params.pyg b/src/ast/rewriter/bv_rewriter_params.pyg index 780d8e724..d9ee9f7a3 100644 --- a/src/ast/rewriter/bv_rewriter_params.pyg +++ b/src/ast/rewriter/bv_rewriter_params.pyg @@ -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)") + ))