mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-03-02 18:05:14 +00:00
parent 1e86175c03
commit f128c76f23
1 changed files with 23 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -30,7 +30,7 @@ struct blaster_cfg {
bool_rewriter & m_rewriter; bool_rewriter & m_rewriter;
bv_util & m_util; bv_util & m_util;
blaster_cfg(bool_rewriter & r, bv_util & u):m_rewriter(r), m_util(u) {} blaster_cfg(bool_rewriter & r, bv_util & u):m_rewriter(r), m_util(u) {}
ast_manager & m() const { return m_util.get_manager(); } ast_manager & m() const { return m_util.get_manager(); }
numeral power(unsigned n) const { return rational::power_of_two(n); } numeral power(unsigned n) const { return rational::power_of_two(n); }
void mk_xor(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_xor(a, b, r); } void mk_xor(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_xor(a, b, r); }
@ -59,7 +59,7 @@ struct blaster_cfg {
mk_or(a, c, t2); mk_or(a, c, t2);
mk_or(b, c, t3); mk_or(b, c, t3);
mk_and(t1, t2, t3, r); mk_and(t1, t2, t3, r);
#endif #endif
} }
void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { m_rewriter.mk_ite(c, t, e, r); } void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { m_rewriter.mk_ite(c, t, e, r); }
void mk_nand(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_nand(a, b, r); } void mk_nand(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_nand(a, b, r); }
@ -112,7 +112,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
m_out.finalize(); m_out.finalize();
m_bindings.finalize(); m_bindings.finalize();
} }
blaster_rewriter_cfg(ast_manager & m, blaster & b, params_ref const & p): blaster_rewriter_cfg(ast_manager & m, blaster & b, params_ref const & p):
m_manager(m), m_manager(m),
m_blaster(b), m_blaster(b),
@ -120,7 +120,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
m_in2(m), m_in2(m),
m_out(m), m_out(m),
m_bindings(m), m_bindings(m),
m_keys(m), m_keys(m),
m_values(m) { m_values(m) {
updt_params(p); updt_params(p);
} }
@ -140,7 +140,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
bool rewrite_patterns() const { return true; } bool rewrite_patterns() const { return true; }
bool max_steps_exceeded(unsigned num_steps) const { bool max_steps_exceeded(unsigned num_steps) const {
cooperate("bit blaster"); cooperate("bit blaster");
if (memory::get_allocation_size() > m_max_memory) if (memory::get_allocation_size() > m_max_memory)
throw rewriter_exception(Z3_MAX_MEMORY_MSG); throw rewriter_exception(Z3_MAX_MEMORY_MSG);
@ -219,7 +219,7 @@ void OP(expr * arg, expr_ref & result) { \
MK_UNARY_REDUCE(reduce_not, mk_not); MK_UNARY_REDUCE(reduce_not, mk_not);
MK_UNARY_REDUCE(reduce_redor, mk_redor); MK_UNARY_REDUCE(reduce_redor, mk_redor);
MK_UNARY_REDUCE(reduce_redand, mk_redand); MK_UNARY_REDUCE(reduce_redand, mk_redand);
#define MK_BIN_REDUCE(OP, BB_OP) \ #define MK_BIN_REDUCE(OP, BB_OP) \
void OP(expr * arg1, expr * arg2, expr_ref & result) { \ void OP(expr * arg1, expr * arg2, expr_ref & result) { \
m_in1.reset(); m_in2.reset(); \ m_in1.reset(); m_in2.reset(); \
@ -289,11 +289,11 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
void reduce_ite(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { void reduce_ite(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
m_in1.reset(); m_in1.reset();
m_in2.reset(); m_in2.reset();
get_bits(arg2, m_in1); get_bits(arg2, m_in1);
get_bits(arg3, m_in2); get_bits(arg3, m_in2);
m_out.reset(); m_out.reset();
m_blaster.mk_multiplexer(arg1, m_in1.size(), m_in1.c_ptr(), m_in2.c_ptr(), m_out); m_blaster.mk_multiplexer(arg1, m_in1.size(), m_in1.c_ptr(), m_in2.c_ptr(), m_out);
result = mk_mkbv(m_out); result = mk_mkbv(m_out);
} }
void reduce_concat(unsigned num_args, expr * const * args, expr_ref & result) { void reduce_concat(unsigned num_args, expr * const * args, expr_ref & result) {
@ -342,7 +342,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
result = mk_mkbv(bits); result = mk_mkbv(bits);
result_pr = 0; result_pr = 0;
} }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0; result_pr = 0;
TRACE("bit_blaster", tout << f->get_name() << " "; TRACE("bit_blaster", tout << f->get_name() << " ";
@ -352,7 +352,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
mk_const(f, result); mk_const(f, result);
return BR_DONE; return BR_DONE;
} }
if (m().is_eq(f)) { if (m().is_eq(f)) {
SASSERT(num == 2); SASSERT(num == 2);
if (butil().is_bv(args[0])) { if (butil().is_bv(args[0])) {
@ -361,7 +361,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
} }
return BR_FAILED; return BR_FAILED;
} }
if (m().is_ite(f)) { if (m().is_ite(f)) {
SASSERT(num == 3); SASSERT(num == 3);
@ -371,7 +371,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
} }
return BR_FAILED; return BR_FAILED;
} }
if (f->get_family_id() == butil().get_family_id()) { if (f->get_family_id() == butil().get_family_id()) {
switch (f->get_decl_kind()) { switch (f->get_decl_kind()) {
case OP_BV_NUM: case OP_BV_NUM:
@ -453,7 +453,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
case OP_BXOR: case OP_BXOR:
reduce_xor(num, args, result); reduce_xor(num, args, result);
return BR_DONE; return BR_DONE;
case OP_CONCAT: case OP_CONCAT:
reduce_concat(num, args, result); reduce_concat(num, args, result);
return BR_DONE; return BR_DONE;
@ -507,7 +507,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
SASSERT(num == 2); SASSERT(num == 2);
reduce_smul_no_underflow(args[0], args[1], result); reduce_smul_no_underflow(args[0], args[1], result);
return BR_DONE; return BR_DONE;
case OP_BIT2BOOL: case OP_BIT2BOOL:
case OP_MKBV: case OP_MKBV:
case OP_INT2BV: case OP_INT2BV:
@ -524,7 +524,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
blast_bv_term(m().mk_app(f, num, args), result, result_pr); blast_bv_term(m().mk_app(f, num, args), result, result_pr);
return BR_DONE; return BR_DONE;
} }
return BR_FAILED; return BR_FAILED;
} }
@ -570,18 +570,18 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
result_pr = 0; result_pr = 0;
return true; return true;
} }
if (m_blast_full && butil().is_bv(t)) { if (m_blast_full && butil().is_bv(t)) {
blast_bv_term(t, result, result_pr); blast_bv_term(t, result, result_pr);
return true; return true;
} }
return false; return false;
} }
bool reduce_quantifier(quantifier * old_q, bool reduce_quantifier(quantifier * old_q,
expr * new_body, expr * new_body,
expr * const * new_patterns, expr * const * new_patterns,
expr * const * new_no_patterns, expr * const * new_no_patterns,
expr_ref & result, expr_ref & result,
proof_ref & result_pr) { proof_ref & result_pr) {
@ -627,8 +627,8 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl<blaster_rewriter_cfg> {
blaster m_blaster; blaster m_blaster;
blaster_rewriter_cfg m_cfg; blaster_rewriter_cfg m_cfg;
imp(ast_manager & m, params_ref const & p): imp(ast_manager & m, params_ref const & p):
rewriter_tpl<blaster_rewriter_cfg>(m, rewriter_tpl<blaster_rewriter_cfg>(m,
m.proofs_enabled(), m.proofs_enabled(),
m_cfg), m_cfg),
m_blaster(m), m_blaster(m),
m_cfg(m, m_blaster, p) { m_cfg(m, m_blaster, p) {