mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-11-12 14:48:29 +00:00
parent be2d215fac
commit 87ae5888ee
1 changed files with 44 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

88
src/ast/rewriter/bool_rewriter.cpp
View file

@ -84,7 +84,7 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg
ptr_buffer<expr> buffer; ptr_buffer<expr> buffer;
expr_fast_mark1 neg_lits; expr_fast_mark1 neg_lits;
expr_fast_mark2 pos_lits; expr_fast_mark2 pos_lits;
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
expr * arg = args[i]; expr * arg = args[i];
if (m().is_true(arg)) { 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); buffer.push_back(arg);
} }
unsigned sz = buffer.size(); unsigned sz = buffer.size();
switch(sz) { switch(sz) {
case 0: case 0:
result = m().mk_true(); 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); buffer.push_back(arg);
} }
unsigned sz = buffer.size(); unsigned sz = buffer.size();
switch(sz) { switch(sz) {
case 0: case 0:
result = m().mk_false(); 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) { if (m_local_ctx && m_local_ctx_cost <= m_local_ctx_limit) {
neg_lits.reset(); neg_lits.reset();
pos_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; return BR_DONE;
} }
if (s) { 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. \brief Auxiliary method for local_ctx_simp.
Replace args[i] by true if marked in neg_lits. Replace args[i] by true if marked in neg_lits.
Replace args[i] by false if marked in pos_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) { expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, expr_ref & result) {
ptr_buffer<expr> new_args; ptr_buffer<expr> new_args;
bool simp = false; bool simp = false;
@ -307,13 +307,13 @@ bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args,
} }
if (simp) { if (simp) {
switch(new_args.size()) { switch(new_args.size()) {
case 0: case 0:
result = m().mk_true(); result = m().mk_true();
return true; return true;
case 1: case 1:
mk_not(new_args[0], result); mk_not(new_args[0], result);
return true; return true;
default: default:
result = m().mk_not(m().mk_or(new_args.size(), new_args.c_ptr())); result = m().mk_not(m().mk_or(new_args.size(), new_args.c_ptr()));
return true; return true;
} }
@ -358,7 +358,7 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul
result = t; result = t;
return; return;
} }
if (m().is_false(c)) { if (m().is_false(c)) {
result = e; result = e;
return; return;
@ -368,7 +368,7 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul
result = t; result = t;
return; return;
} }
if (m().is_bool(t)) { if (m().is_bool(t)) {
if (m().is_true(t)) { if (m().is_true(t)) {
if (m().is_false(e)) { 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; return;
} }
expr_ref tmp(m()); expr_ref tmp(m());
mk_not(e, tmp); mk_not(e, tmp);
result = m().mk_not(m().mk_or(c, tmp)); result = m().mk_not(m().mk_or(c, tmp));
return; return;
} }
if (m().is_true(e)) { if (m().is_true(e)) {
expr_ref tmp(m()); expr_ref tmp(m());
mk_not(c, tmp); mk_not(c, tmp);
result = m().mk_or(tmp, t); result = m().mk_or(tmp, t);
return; 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); result = m().mk_or(c, e);
return; 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); mk_eq(c, t, result);
return; 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); expr * new_e = simp_arg(to_app(t)->get_arg(2), neg_lits, pos_lits, modified);
if (!modified) if (!modified)
return false; return false;
// It is not safe to invoke mk_ite here, since it can recursively call // It is not safe to invoke mk_ite here, since it can recursively call
// local_ctx_simp by // local_ctx_simp by
// - transforming the ITE into an OR // - transforming the ITE into an OR
// - and invoked mk_or, that will invoke local_ctx_simp // - and invoked mk_or, that will invoke local_ctx_simp
// mk_ite(new_c, new_t, new_e, result); // 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); \ PUSH_NEW_ARG(arg); \
} \ } \
} }
m_local_ctx_cost += 2*num_args; m_local_ctx_cost += 2*num_args;
#if 0 #if 0
static unsigned counter = 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. \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) { br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) {
SASSERT(m().is_ite(ite)); 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";); tout << t << " " << e << " " << val << "\n";);
result = m().mk_false(); result = m().mk_false();
return BR_DONE; return BR_DONE;
} }
if (t == val && e == val) { if (t == val && e == val) {
result = m().mk_true(); 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); SASSERT(e == val);
mk_not(ite->get_arg(0), result); mk_not(ite->get_arg(0), result);
return BR_DONE; return BR_DONE;
} }
@ -642,14 +642,14 @@ static bool is_ite_value_tree_neq_value(ast_manager & m, app * ite, app * val) {
return true; return true;
} }
#endif #endif
br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
if (lhs == rhs) { if (lhs == rhs) {
result = m().mk_true(); result = m().mk_true();
return BR_DONE; return BR_DONE;
} }
if (m().are_distinct(lhs, rhs)) { if (m().are_distinct(lhs, rhs)) {
result = m().mk_false(); result = m().mk_false();
return BR_DONE; return BR_DONE;
@ -662,7 +662,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
// return BR_DONE; // return BR_DONE;
// } // }
r = try_ite_value(to_app(lhs), to_app(rhs), result); 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";); 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)) { 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; // return BR_DONE;
// } // }
r = try_ite_value(to_app(rhs), to_app(lhs), result); 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";); tout << mk_ismt2_pp(lhs, m()) << "\n" << mk_ismt2_pp(rhs, m()) << "\n--->\n" << mk_ismt2_pp(result, m()) << "\n";);
} }
if (r != BR_FAILED) 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()); result = m().mk_and(new_diseqs.size(), new_diseqs.c_ptr());
return BR_REWRITE3; return BR_REWRITE3;
} }
return BR_FAILED; return BR_FAILED;
} }
br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result) { br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result) {
bool s = false; bool s = false;
// (ite (not c) a b) ==> (ite c b a) // (ite (not c) a b) ==> (ite c b a)
if (m().is_not(c)) { if (m().is_not(c)) {
c = to_app(c)->get_arg(0); 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; result = t;
return BR_DONE; return BR_DONE;
} }
if (m().is_false(c)) { if (m().is_false(c)) {
result = e; result = e;
return BR_DONE; 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; return BR_DONE;
} }
expr_ref tmp(m()); expr_ref tmp(m());
mk_not(c, tmp); mk_not(c, tmp);
mk_and(tmp, e, result); mk_and(tmp, e, result);
return BR_DONE; return BR_DONE;
} }
if (m().is_true(e)) { if (m().is_true(e)) {
expr_ref tmp(m()); expr_ref tmp(m());
mk_not(c, tmp); mk_not(c, tmp);
mk_or(tmp, t, result); mk_or(tmp, t, result);
return BR_DONE; return BR_DONE;
} }
if (m().is_false(e)) { if (m().is_false(e)) {
mk_and(c, t, result); mk_and(c, t, result);
return BR_DONE; return BR_DONE;
} }
if (c == e) { 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; return BR_DONE;
} }
if (c == t) { if (c == t) {
mk_or(c, e, result); mk_or(c, e, result);
return BR_DONE; 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); mk_eq(c, t, result);
return BR_DONE; 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); result = m().mk_ite(new_c, to_app(t)->get_arg(1), e);
return BR_REWRITE1; return BR_REWRITE1;
} }
if (m().is_ite(e)) { 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) // (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)) { to_app(t)->get_arg(2) == to_app(e)->get_arg(2)) {
expr_ref and1(m()); expr_ref and1(m());
expr_ref and2(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)); result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2));
return BR_REWRITE1; 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) // (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)) { to_app(t)->get_arg(2) == to_app(e)->get_arg(1)) {
expr_ref and1(m()); expr_ref and1(m());
expr_ref and2(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); result = m().mk_ite(c, t, e);
return BR_DONE; return BR_DONE;
} }
return BR_FAILED; return BR_FAILED;
} }
br_status bool_rewriter::mk_not_core(expr * t, expr_ref & result) { br_status bool_rewriter::mk_not_core(expr * t, expr_ref & result) {
if (m().is_not(t)) { if (m().is_not(t)) {
result = to_app(t)->get_arg(0); result = to_app(t)->get_arg(0);