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

fix regression crash

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-11-15 11:20:12 -08:00
parent 9845c33236
commit 255414f4a9
1 changed files with 13 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -647,11 +647,13 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
SASSERT(m().is_value(val)); SASSERT(m().is_value(val));
if (m().are_distinct(val, e)) { if (m().are_distinct(val, e)) {
result = m().mk_and(mk_eq(t, val), cond); mk_eq(t, val, result);
result = m().mk_and(result, cond);
return BR_REWRITE2; return BR_REWRITE2;
} }
if (m().are_distinct(val, t)) { if (m().are_distinct(val, t)) {
result = m().mk_and(mk_eq(e, val), m().mk_not(cond)); mk_eq(e, val, result);
result = m().mk_and(result, m().mk_not(cond));
return BR_REWRITE2; return BR_REWRITE2;
} }
if (m().are_equal(val, t)) { if (m().are_equal(val, t)) {
@ -660,12 +662,14 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
return BR_DONE; return BR_DONE;
} }
else { else {
result = m().mk_or(mk_eq(e, val), cond); mk_eq(e, val, result);
result = m().mk_or(result, cond);
} }
return BR_REWRITE2; return BR_REWRITE2;
} }
if (m().are_equal(val, e)) { if (m().are_equal(val, e)) {
result = m().mk_or(mk_eq(t, val), m().mk_not(cond)); mk_eq(t, val, result);
result = m().mk_or(result, m().mk_not(cond));
return BR_REWRITE2; return BR_REWRITE2;
} }
@ -686,10 +690,6 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
app* bool_rewriter::mk_eq(expr* lhs, expr* rhs) { app* bool_rewriter::mk_eq(expr* lhs, expr* rhs) {
if (m().are_distinct(lhs, rhs))
return m().mk_false();
if (lhs == rhs)
return m().mk_true();
// degrades simplification // degrades simplification
// if (lhs->get_id() > rhs->get_id()) std::swap(lhs, rhs); // if (lhs->get_id() > rhs->get_id()) std::swap(lhs, rhs);
return m().mk_eq(lhs, rhs); return m().mk_eq(lhs, rhs);
@ -761,7 +761,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
} }
if (unfolded) { if (unfolded) {
result = mk_eq(lhs, rhs); result = m().mk_eq(lhs, rhs);
return BR_REWRITE1; return BR_REWRITE1;
} }
@ -789,7 +789,8 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
if (num_args == 2) { if (num_args == 2) {
expr_ref tmp(m()); expr_ref tmp(m());
result = mk_not(mk_eq(args[0], args[1])); mk_eq(args[0], args[1], tmp);
mk_not(tmp, result);
return BR_REWRITE2; // mk_eq may be dispatched to other rewriters. return BR_REWRITE2; // mk_eq may be dispatched to other rewriters.
} }
@ -828,10 +829,10 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
} }
if (m_blast_distinct && num_args < m_blast_distinct_threshold) { if (m_blast_distinct && num_args < m_blast_distinct_threshold) {
ptr_buffer<expr> new_diseqs; expr_ref_vector new_diseqs(m());
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
for (unsigned j = i + 1; j < num_args; j++) for (unsigned j = i + 1; j < num_args; j++)
new_diseqs.push_back(mk_not(mk_eq(args[i], args[j]))); new_diseqs.push_back(m().mk_not(m().mk_eq(args[i], args[j])));
} }
result = m().mk_and(new_diseqs); result = m().mk_and(new_diseqs);
return BR_REWRITE3; return BR_REWRITE3;