From 87ae5888ee603ec7e365700ac3eefcb98dc05938 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 12 Nov 2015 14:48:29 +0000 Subject: [PATCH] whitespace --- src/ast/rewriter/bool_rewriter.cpp | 88 +++++++++++++++--------------- 1 file changed, 44 insertions(+), 44 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 5b0c38616..6dec03307 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -84,7 +84,7 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg ptr_buffer buffer; expr_fast_mark1 neg_lits; expr_fast_mark2 pos_lits; - + for (unsigned i = 0; i < num_args; i++) { expr * arg = args[i]; if (m().is_true(arg)) { @@ -120,9 +120,9 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg } buffer.push_back(arg); } - + unsigned sz = buffer.size(); - + switch(sz) { case 0: result = m().mk_true(); @@ -208,9 +208,9 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args } buffer.push_back(arg); } - + unsigned sz = buffer.size(); - + switch(sz) { case 0: result = m().mk_false(); @@ -222,7 +222,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args if (m_local_ctx && m_local_ctx_cost <= m_local_ctx_limit) { neg_lits.reset(); pos_lits.reset(); - if (local_ctx_simp(sz, buffer.c_ptr(), result)) + if (local_ctx_simp(sz, buffer.c_ptr(), result)) return BR_DONE; } if (s) { @@ -273,11 +273,11 @@ expr * bool_rewriter::mk_or_app(unsigned num_args, expr * const * args) { /** \brief Auxiliary method for local_ctx_simp. - + Replace args[i] by true if marked in neg_lits. Replace args[i] by false if marked in pos_lits. */ -bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args, +bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, expr_ref & result) { ptr_buffer new_args; bool simp = false; @@ -307,13 +307,13 @@ bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args, } if (simp) { switch(new_args.size()) { - case 0: - result = m().mk_true(); + case 0: + result = m().mk_true(); return true; - case 1: - mk_not(new_args[0], result); + case 1: + mk_not(new_args[0], result); return true; - default: + default: result = m().mk_not(m().mk_or(new_args.size(), new_args.c_ptr())); return true; } @@ -358,7 +358,7 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul result = t; return; } - + if (m().is_false(c)) { result = e; return; @@ -368,7 +368,7 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul result = t; return; } - + if (m().is_bool(t)) { if (m().is_true(t)) { if (m().is_false(e)) { @@ -384,13 +384,13 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul return; } expr_ref tmp(m()); - mk_not(e, tmp); + mk_not(e, tmp); result = m().mk_not(m().mk_or(c, tmp)); return; } if (m().is_true(e)) { expr_ref tmp(m()); - mk_not(c, tmp); + mk_not(c, tmp); result = m().mk_or(tmp, t); return; } @@ -406,7 +406,7 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul result = m().mk_or(c, e); return; } - if (m().is_complement_core(t, e)) { // t = not(e) + if (m().is_complement_core(t, e)) { // t = not(e) mk_eq(c, t, result); return; } @@ -443,8 +443,8 @@ bool bool_rewriter::simp_nested_eq_ite(expr * t, expr_fast_mark1 & neg_lits, exp expr * new_e = simp_arg(to_app(t)->get_arg(2), neg_lits, pos_lits, modified); if (!modified) return false; - // It is not safe to invoke mk_ite here, since it can recursively call - // local_ctx_simp by + // It is not safe to invoke mk_ite here, since it can recursively call + // local_ctx_simp by // - transforming the ITE into an OR // - and invoked mk_or, that will invoke local_ctx_simp // mk_ite(new_c, new_t, new_e, result); @@ -522,7 +522,7 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_ PUSH_NEW_ARG(arg); \ } \ } - + m_local_ctx_cost += 2*num_args; #if 0 static unsigned counter = 0; @@ -567,9 +567,9 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_ /** \brief Apply simplification if ite is an if-then-else tree where every leaf is a value. - - This is an efficient way to - + + This is an efficient way to + */ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) { SASSERT(m().is_ite(ite)); @@ -585,7 +585,7 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) tout << t << " " << e << " " << val << "\n";); result = m().mk_false(); return BR_DONE; - } + } if (t == val && e == val) { result = m().mk_true(); @@ -598,7 +598,7 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) } SASSERT(e == val); - + mk_not(ite->get_arg(0), result); return BR_DONE; } @@ -642,14 +642,14 @@ static bool is_ite_value_tree_neq_value(ast_manager & m, app * ite, app * val) { return true; } -#endif +#endif br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { if (lhs == rhs) { result = m().mk_true(); return BR_DONE; } - + if (m().are_distinct(lhs, rhs)) { result = m().mk_false(); return BR_DONE; @@ -662,7 +662,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { // return BR_DONE; // } r = try_ite_value(to_app(lhs), to_app(rhs), result); - CTRACE("try_ite_value", r != BR_FAILED, + CTRACE("try_ite_value", r != BR_FAILED, tout << mk_ismt2_pp(lhs, m()) << "\n" << mk_ismt2_pp(rhs, m()) << "\n--->\n" << mk_ismt2_pp(result, m()) << "\n";); } else if (m().is_ite(rhs) && m().is_value(lhs)) { @@ -671,7 +671,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { // return BR_DONE; // } r = try_ite_value(to_app(rhs), to_app(lhs), result); - CTRACE("try_ite_value", r != BR_FAILED, + CTRACE("try_ite_value", r != BR_FAILED, tout << mk_ismt2_pp(lhs, m()) << "\n" << mk_ismt2_pp(rhs, m()) << "\n--->\n" << mk_ismt2_pp(result, m()) << "\n";); } if (r != BR_FAILED) @@ -756,13 +756,13 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args result = m().mk_and(new_diseqs.size(), new_diseqs.c_ptr()); return BR_REWRITE3; } - + return BR_FAILED; } br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result) { bool s = false; - + // (ite (not c) a b) ==> (ite c b a) if (m().is_not(c)) { c = to_app(c)->get_arg(0); @@ -788,7 +788,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re result = t; return BR_DONE; } - + if (m().is_false(c)) { result = e; return BR_DONE; @@ -814,18 +814,18 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re return BR_DONE; } expr_ref tmp(m()); - mk_not(c, tmp); + mk_not(c, tmp); mk_and(tmp, e, result); return BR_DONE; } if (m().is_true(e)) { expr_ref tmp(m()); - mk_not(c, tmp); + mk_not(c, tmp); mk_or(tmp, t, result); return BR_DONE; } if (m().is_false(e)) { - mk_and(c, t, result); + mk_and(c, t, result); return BR_DONE; } if (c == e) { @@ -833,10 +833,10 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re return BR_DONE; } if (c == t) { - mk_or(c, e, result); + mk_or(c, e, result); return BR_DONE; } - if (m().is_complement_core(t, e)) { // t = not(e) + if (m().is_complement_core(t, e)) { // t = not(e) mk_eq(c, t, result); return BR_DONE; } @@ -863,10 +863,10 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re result = m().mk_ite(new_c, to_app(t)->get_arg(1), e); return BR_REWRITE1; } - + if (m().is_ite(e)) { // (ite c1 (ite c2 t1 t2) (ite c3 t1 t2)) ==> (ite (or (and c1 c2) (and (not c1) c3)) t1 t2) - if (to_app(t)->get_arg(1) == to_app(e)->get_arg(1) && + if (to_app(t)->get_arg(1) == to_app(e)->get_arg(1) && to_app(t)->get_arg(2) == to_app(e)->get_arg(2)) { expr_ref and1(m()); expr_ref and2(m()); @@ -879,9 +879,9 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2)); return BR_REWRITE1; } - + // (ite c1 (ite c2 t1 t2) (ite c3 t2 t1)) ==> (ite (or (and c1 c2) (and (not c1) (not c3))) t1 t2) - if (to_app(t)->get_arg(1) == to_app(e)->get_arg(2) && + if (to_app(t)->get_arg(1) == to_app(e)->get_arg(2) && to_app(t)->get_arg(2) == to_app(e)->get_arg(1)) { expr_ref and1(m()); expr_ref and2(m()); @@ -922,10 +922,10 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re result = m().mk_ite(c, t, e); return BR_DONE; } - + return BR_FAILED; } - + br_status bool_rewriter::mk_not_core(expr * t, expr_ref & result) { if (m().is_not(t)) { result = to_app(t)->get_arg(0);