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

use of mk_bool_val

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-06-24 09:11:45 -07:00
parent f72d9c25c6
commit 30cf0d19eb
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -252,7 +252,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
r2 = m_util.norm(r2, sz, is_signed);
if (is_num1 && is_num2) {
result = r1 <= r2 ? m().mk_true() : m().mk_false();
result = m().mk_bool_val(r1 <= r2);
return BR_DONE;
}
@ -1785,7 +1785,7 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
if (is_numeral(lhs)) {
SASSERT(is_numeral(rhs));
result = lhs == rhs ? m().mk_true() : m().mk_false();
result = m().mk_bool_val(lhs == rhs);
return BR_DONE;
}
@ -2134,7 +2134,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
st = cancel_monomials(lhs, rhs, false, new_lhs, new_rhs);
if (st != BR_FAILED) {
if (is_numeral(new_lhs) && is_numeral(new_rhs)) {
result = new_lhs == new_rhs ? m().mk_true() : m().mk_false();
result = m().mk_bool_val(new_lhs == new_rhs);
return BR_DONE;
}
}
@ -2213,7 +2213,7 @@ br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args,
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();
result = m().mk_bool_val(mr < lim);
return BR_DONE;
}
@ -2239,7 +2239,7 @@ br_status bv_rewriter::mk_bvumul_no_overflow(unsigned num, expr * const * args,
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();
result = m().mk_bool_val(mr < lim);
return BR_DONE;
}
@ -2270,7 +2270,7 @@ br_status bv_rewriter::mk_bvsmul_no_underflow(unsigned num, expr * const * args,
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();
result = m().mk_bool_val(mr >= neg_lim);
return BR_DONE;
}