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<expr> 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<expr> 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);