mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

remove incorrect assertions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-06 17:40:30 -08:00
parent 200f47369d
commit ff6b3304f8
3 changed files with 16 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/smt/asserted_formulas.cpp
View file

@ -357,25 +357,35 @@ void asserted_formulas::flatten_clauses() {
if (m.proofs_enabled()) return; if (m.proofs_enabled()) return;
bool change = true; bool change = true;
vector<justified_expr> new_fmls; vector<justified_expr> new_fmls;
auto mk_not = [this](expr* e) { return m.is_not(e, e) ? e : m.mk_not(e); };
auto is_literal = [this](expr *e) { m.is_not(e, e); return !is_app(e) || to_app(e)->get_num_args() == 0; };
expr *a = nullptr, *b = nullptr, *c = nullptr;
while (change) { while (change) {
change = false; change = false;
new_fmls.reset(); new_fmls.reset();
unsigned sz = m_formulas.size(); unsigned sz = m_formulas.size();
for (unsigned i = m_qhead; i < sz; ++i) { for (unsigned i = m_qhead; i < sz; ++i) {
auto const& j = m_formulas.get(i); auto const& j = m_formulas.get(i);
expr* f = j.get_fml(), *a = nullptr, *b = nullptr; expr* f = j.get_fml();
bool decomposed = false; bool decomposed = false;
if (m.is_or(f, a, b) && m.is_not(b, b) && m.is_or(b) && b->get_ref_count() == 1) { if (m.is_or(f, a, b) && m.is_not(b, b) && m.is_or(b) && (b->get_ref_count() == 1 || is_literal(a))) {
decomposed = true; decomposed = true;
} }
else if (m.is_or(f, b, a) && m.is_not(b, b) && m.is_or(b) && b->get_ref_count() == 1) { else if (m.is_or(f, b, a) && m.is_not(b, b) && m.is_or(b) && (b->get_ref_count() == 1 || is_literal(a))) {
decomposed = true; decomposed = true;
} }
if (decomposed) { if (decomposed) {
for (expr* arg : *to_app(b)) { for (expr* arg : *to_app(b)) {
justified_expr j1(m, m.mk_or(a, m.is_not(arg, arg) ? arg : m.mk_not(arg)), nullptr); justified_expr j1(m, m.mk_or(a, mk_not(arg)), nullptr);
new_fmls.push_back(j1); new_fmls.push_back(j1);
} }
change = true;
continue;
}
if (m.is_ite(f, a, b, c)) {
new_fmls.push_back(justified_expr(m, m.mk_or(mk_not(a), b), nullptr));
new_fmls.push_back(justified_expr(m, m.mk_or(a, c), nullptr));
change = true;
continue; continue;
} }
new_fmls.push_back(j); new_fmls.push_back(j);

2
src/smt/smt_context_inv.cpp
View file

@ -34,7 +34,7 @@ namespace smt {
SASSERT(is_watching_clause(~cls->get_literal(1), cls)); SASSERT(is_watching_clause(~cls->get_literal(1), cls));
for (literal l : *cls) { for (literal l : *cls) {
// holds, TBD re-enable when ready to re-check // holds, TBD re-enable when ready to re-check
// SASSERT(m_lit_occs[l.index()] > 0); // SASSERT(!track_occs() || m_lit_occs[l.index()] > 0);
} }
return true; return true;
} }

2
src/smt/theory_lra.cpp
View file

@ -1922,7 +1922,6 @@ public:
theory_var v1 = mk_var(p); theory_var v1 = mk_var(p);
lp::impq r1 = get_ivalue(v1); lp::impq r1 = get_ivalue(v1);
SASSERT(r1.y.is_zero()); SASSERT(r1.y.is_zero());
SASSERT(r1.x.is_int());
rational r2; rational r2;
if (!r1.x.is_int() || r1.x.is_neg()) { if (!r1.x.is_int() || r1.x.is_neg()) {
@ -1942,7 +1941,6 @@ public:
} }
lp::impq val_v = get_ivalue(v); lp::impq val_v = get_ivalue(v);
SASSERT(val_v.y.is_zero()); SASSERT(val_v.y.is_zero());
SASSERT(val_v.x.is_int());
if (val_v.x == div(r1.x, r2)) continue; if (val_v.x == div(r1.x, r2)) continue;
TRACE("arith", tout << get_value(v) << " != " << r1 << " div " << r2 << "\n";); TRACE("arith", tout << get_value(v) << " != " << r1 << " div " << r2 << "\n";);