mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

merge with update to bv rewriter

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-06-24 09:08:01 -07:00
commit f72d9c25c6
3 changed files with 93 additions and 99 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/bit_blaster/bit_blaster.h
View file

@ -20,8 +20,8 @@ Revision History:
#define BIT_BLASTER_H_
#include"bool_rewriter.h"
#include"bit_blaster/bit_blaster_params.h"
#include"bit_blaster/bit_blaster_tpl.h"
#include"bit_blaster_params.h"
#include"bit_blaster_tpl.h"
#include"bv_decl_plugin.h"
#include"rational.h"

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

@ -20,7 +20,6 @@ Notes:
#include"bv_rewriter_params.hpp"
#include"poly_rewriter_def.h"
#include"ast_smt2_pp.h"
#include"bit_blaster/bit_blaster.h"
void bv_rewriter::updt_local_params(params_ref const & _p) {
@ -190,15 +189,12 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
return mk_bv_comp(args[0], args[1], result);
case OP_MKBV:
return mk_mkbv(num_args, args, result);
case OP_BUMUL_NO_OVFL:
SASSERT(num_args == 2);
return mk_bv_umul_no_ovfl(args[0], args[1], result);
case OP_BSMUL_NO_OVFL:
SASSERT(num_args == 2);
return mk_bv_smul_no_ovfl(args[0], args[1], result);
case OP_BSMUL_NO_UDFL:
SASSERT(num_args == 2);
return mk_bv_smul_no_udfl(args[0], args[1], result);
return mk_bvsmul_no_overflow(num_args, args, result);
case OP_BUMUL_NO_OVFL:
return mk_bvumul_no_overflow(num_args, args, result);
case OP_BSMUL_NO_UDFL:
return mk_bvsmul_no_underflow(num_args, args, result);
default:
return BR_FAILED;
}
@ -1110,90 +1106,6 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
return BR_DONE;
}
br_status bv_rewriter::mk_bv_umul_no_ovfl(expr * arg1, expr * arg2, expr_ref& result) {
rational val1, val2;
unsigned bv_size;
bool is_num1 = is_numeral(arg1, val1, bv_size);
bool is_num2 = is_numeral(arg2, val2, bv_size);
if (is_num1 && (val1.is_zero() || val1.is_one())) {
result = m().mk_true();
return BR_DONE;
}
if (is_num2 && (val2.is_zero() || val2.is_one())) {
result = m().mk_true();
return BR_DONE;
}
if (is_num1 && is_num2) {
SASSERT(!val1.is_neg());
SASSERT(!val2.is_neg());
rational r = val1 * val2;
result = m().mk_bool_val(r < rational(2).expt(bv_size));
return BR_DONE;
}
return BR_FAILED;
}
br_status bv_rewriter::mk_bv_smul_no_ovfl(expr * arg1, expr * arg2, expr_ref& result) {
rational val1, val2;
unsigned bv_size;
bool is_num1 = is_numeral(arg1, val1, bv_size);
bool is_num2 = is_numeral(arg2, val2, bv_size);
if (is_num1 && (val1.is_zero() || val1.is_one())) {
result = m().mk_true();
return BR_DONE;
}
if (is_num2 && (val2.is_zero() || val2.is_one())) {
result = m().mk_true();
return BR_DONE;
}
if (is_num1 && is_num2) {
bit_blaster_params params;
bit_blaster blaster(m(), params);
SASSERT(!val1.is_neg());
SASSERT(!val2.is_neg());
expr_ref_vector bits1(m()), bits2(m());
for (unsigned i = 0; i < bv_size; ++i) {
bits1.push_back(m().mk_bool_val(!val1.is_even()));
bits2.push_back(m().mk_bool_val(!val2.is_even()));
val1 = div(val1, rational(2));
val2 = div(val2, rational(2));
}
blaster.mk_smul_no_overflow(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), result);
return BR_DONE;
}
return BR_FAILED;
}
br_status bv_rewriter::mk_bv_smul_no_udfl(expr * arg1, expr * arg2, expr_ref& result) {
rational val1, val2;
unsigned bv_size;
bool is_num1 = is_numeral(arg1, val1, bv_size);
bool is_num2 = is_numeral(arg2, val2, bv_size);
if (is_num1 && (val1.is_zero() || val1.is_one())) {
result = m().mk_true();
return BR_DONE;
}
if (is_num2 && (val2.is_zero() || val2.is_one())) {
result = m().mk_true();
return BR_DONE;
}
if (is_num1 && is_num2) {
bit_blaster_params params;
bit_blaster blaster(m(), params);
SASSERT(!val1.is_neg());
SASSERT(!val2.is_neg());
expr_ref_vector bits1(m()), bits2(m());
for (unsigned i = 0; i < bv_size; ++i) {
bits1.push_back(m().mk_bool_val(!val1.is_even()));
bits2.push_back(m().mk_bool_val(!val2.is_even()));
val1 = div(val1, rational(2));
val2 = div(val2, rational(2));
}
blaster.mk_smul_no_underflow(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), result);
return BR_DONE;
}
return BR_FAILED;
}
br_status bv_rewriter::mk_zero_extend(unsigned n, expr * arg, expr_ref & result) {
@ -2282,6 +2194,88 @@ br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & res
return BR_FAILED;
}
br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
unsigned bv_sz;
rational a0_val, a1_val;
bool is_num1 = is_numeral(args[0], a0_val, bv_sz);
bool is_num2 = is_numeral(args[1], a1_val, bv_sz);
if (is_num1 && (a0_val.is_zero() || a0_val.is_one())) {
result = m().mk_true();
return BR_DONE;
}
if (is_num2 && (a1_val.is_zero() || a1_val.is_one())) {
result = m().mk_true();
return BR_DONE;
}
if (is_num1 && is_num2) {
rational mr = a0_val * a1_val;
rational lim = rational::power_of_two(bv_sz-1);
result = (mr < lim) ? m().mk_true() : m().mk_false();
return BR_DONE;
}
return BR_FAILED;
}
br_status bv_rewriter::mk_bvumul_no_overflow(unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
unsigned bv_sz;
rational a0_val, a1_val;
bool is_num1 = is_numeral(args[0], a0_val, bv_sz);
bool is_num2 = is_numeral(args[1], a1_val, bv_sz);
if (is_num1 && (a0_val.is_zero() || a0_val.is_one())) {
result = m().mk_true();
return BR_DONE;
}
if (is_num2 && (a1_val.is_zero() || a1_val.is_one())) {
result = m().mk_true();
return BR_DONE;
}
if (is_num1 && is_num2) {
rational mr = a0_val * a1_val;
rational lim = rational::power_of_two(bv_sz);
result = (mr < lim) ? m().mk_true() : m().mk_false();
return BR_DONE;
}
return BR_FAILED;
}
br_status bv_rewriter::mk_bvsmul_no_underflow(unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
unsigned bv_sz;
rational a0_val, a1_val;
bool is_num1 = is_numeral(args[0], a0_val, bv_sz);
bool is_num2 = is_numeral(args[1], a1_val, bv_sz);
if (is_num1 && (a0_val.is_zero() || a0_val.is_one())) {
result = m().mk_true();
return BR_DONE;
}
if (is_num2 && (a1_val.is_zero() || a1_val.is_one())) {
result = m().mk_true();
return BR_DONE;
}
if (is_num1 && is_num2) {
rational ul = rational::power_of_two(bv_sz);
rational lim = rational::power_of_two(bv_sz-1);
if (a0_val >= lim) a0_val -= ul;
if (a1_val >= lim) a1_val -= ul;
rational mr = a0_val * a1_val;
rational neg_lim = -lim;
TRACE("bv_rewriter_bvsmul_no_underflow", tout << "a0:" << a0_val << " a1:" << a1_val << " mr:" << mr << " neg_lim:" << neg_lim << std::endl;);
result = (mr >= neg_lim) ? m().mk_true() : m().mk_false();
return BR_DONE;
}
return BR_FAILED;
}
template class poly_rewriter<bv_rewriter_core>;

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

@ -114,9 +114,6 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
br_status mk_bv_srem_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_srem_core(arg1, arg2, true, result); }
br_status mk_bv_urem_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_urem_core(arg1, arg2, true, result); }
br_status mk_bv_smod_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_smod_core(arg1, arg2, true, result); }
br_status mk_bv_umul_no_ovfl(expr * arg1, expr * arg2, expr_ref& result);
br_status mk_bv_smul_no_ovfl(expr * arg1, expr * arg2, expr_ref& result);
br_status mk_bv_smul_no_udfl(expr * arg1, expr * arg2, expr_ref& result);
br_status mk_int2bv(unsigned bv_size, expr * arg, expr_ref & result);
br_status mk_bv2int(expr * arg, expr_ref & result);
br_status mk_bv_redor(expr * arg, expr_ref & result);
@ -126,6 +123,9 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
br_status mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & result);
br_status mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result);
br_status mk_mkbv(unsigned num, expr * const * args, expr_ref & result);
br_status mk_bvsmul_no_overflow(unsigned num, expr * const * args, expr_ref & result);
br_status mk_bvumul_no_overflow(unsigned num, expr * const * args, expr_ref & result);
br_status mk_bvsmul_no_underflow(unsigned num, expr * const * args, expr_ref & result);
bool is_minus_one_times_t(expr * arg);
void mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & result);