From f128c76f239001cd6ddb438388cce777fcb8aefe Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 2 Mar 2016 18:05:14 +0000 Subject: [PATCH] whitespace --- .../bit_blaster/bit_blaster_rewriter.cpp | 46 +++++++++---------- 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index 49c68fedf..022a2273a 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -30,7 +30,7 @@ struct blaster_cfg { bool_rewriter & m_rewriter; bv_util & m_util; blaster_cfg(bool_rewriter & r, bv_util & u):m_rewriter(r), m_util(u) {} - + ast_manager & m() const { return m_util.get_manager(); } 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); } @@ -59,7 +59,7 @@ struct blaster_cfg { mk_or(a, c, t2); mk_or(b, c, t3); 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_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_bindings.finalize(); } - + blaster_rewriter_cfg(ast_manager & m, blaster & b, params_ref const & p): m_manager(m), m_blaster(b), @@ -120,7 +120,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg { m_in2(m), m_out(m), m_bindings(m), - m_keys(m), + m_keys(m), m_values(m) { updt_params(p); } @@ -140,7 +140,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg { 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"); if (memory::get_allocation_size() > m_max_memory) 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_redor, mk_redor); MK_UNARY_REDUCE(reduce_redand, mk_redand); - + #define MK_BIN_REDUCE(OP, BB_OP) \ void OP(expr * arg1, expr * arg2, expr_ref & result) { \ 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) { m_in1.reset(); m_in2.reset(); - get_bits(arg2, m_in1); - get_bits(arg3, m_in2); + get_bits(arg2, m_in1); + get_bits(arg3, m_in2); m_out.reset(); 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) { @@ -342,7 +342,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); result = mk_mkbv(bits); result_pr = 0; } - + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { result_pr = 0; 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); return BR_DONE; } - + if (m().is_eq(f)) { SASSERT(num == 2); if (butil().is_bv(args[0])) { @@ -361,7 +361,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); } return BR_FAILED; } - + if (m().is_ite(f)) { SASSERT(num == 3); @@ -371,7 +371,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); } return BR_FAILED; } - + if (f->get_family_id() == butil().get_family_id()) { switch (f->get_decl_kind()) { case OP_BV_NUM: @@ -453,7 +453,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); case OP_BXOR: reduce_xor(num, args, result); return BR_DONE; - + case OP_CONCAT: reduce_concat(num, args, result); return BR_DONE; @@ -507,7 +507,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); SASSERT(num == 2); reduce_smul_no_underflow(args[0], args[1], result); return BR_DONE; - + case OP_BIT2BOOL: case OP_MKBV: 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); return BR_DONE; } - + return BR_FAILED; } @@ -570,18 +570,18 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); result_pr = 0; return true; } - + if (m_blast_full && butil().is_bv(t)) { blast_bv_term(t, result, result_pr); return true; } - + return false; } - bool reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, expr * const * new_no_patterns, expr_ref & result, proof_ref & result_pr) { @@ -627,8 +627,8 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl { blaster m_blaster; blaster_rewriter_cfg m_cfg; imp(ast_manager & m, params_ref const & p): - rewriter_tpl(m, - m.proofs_enabled(), + rewriter_tpl(m, + m.proofs_enabled(), m_cfg), m_blaster(m), m_cfg(m, m_blaster, p) {