mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 15:53:41 +00:00
Code Activity

#5429 #5445

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-01 12:49:36 -07:00
parent 924ea6ab31
commit a4cc9e7895
3 changed files with 25 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/simplex/model_based_opt.cpp
View file

@ -1261,8 +1261,7 @@ namespace opt {
m_var2value[x] = eval(result); m_var2value[x] = eval(result);
TRACE("opt1", tout << "updated eval " << x << " := " << eval(x) << "\n";); TRACE("opt1", tout << "updated eval " << x << " := " << eval(x) << "\n";);
} }
else retire_row(row_id1);
retire_row(row_id1);
return result; return result;
} }

8
src/qe/mbp/mbp_arith.cpp
View file

@ -319,6 +319,14 @@ namespace mbp {
tids.insert(v, mbo.add_var(r, a.is_int(v))); tids.insert(v, mbo.add_var(r, a.is_int(v)));
} }
} }
// bail on variables in non-linear sub-terms
for (auto& kv : tids) {
expr* e = kv.m_key;
if (is_arith(e) && !var_mark.is_marked(e))
mark_rec(fmls_mark, e);
}
if (m_check_purified) { if (m_check_purified) {
for (expr* fml : fmls) for (expr* fml : fmls)
mark_rec(fmls_mark, fml); mark_rec(fmls_mark, fml);

26
src/sat/smt/euf_solver.cpp
View file

@ -288,8 +288,7 @@ namespace euf {
expr* e = m_bool_var2expr.get(l.var(), nullptr); expr* e = m_bool_var2expr.get(l.var(), nullptr);
TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";); TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";);
if (!e) if (!e)
return; return;
euf::enode* n = m_egraph.find(e); euf::enode* n = m_egraph.find(e);
if (!n) if (!n)
return; return;
@ -303,21 +302,28 @@ namespace euf {
SASSERT(l == get_literal(c)); SASSERT(l == get_literal(c));
if (n->value_conflict()) { if (n->value_conflict()) {
euf::enode* nb = sign ? mk_false() : mk_true(); euf::enode* nb = sign ? mk_false() : mk_true();
euf::enode* r = n->get_root();
euf::enode* rb = sign ? mk_true() : mk_false();
sat::literal rl(r->bool_var(), r->value() == l_false);
m_egraph.merge(n, nb, c); m_egraph.merge(n, nb, c);
m_egraph.merge(r, rb, to_ptr(rl));
SASSERT(m_egraph.inconsistent());
return; return;
} }
if (n->merge_tf()) { if (n->merge_tf()) {
euf::enode* nb = sign ? mk_false() : mk_true(); euf::enode* nb = sign ? mk_false() : mk_true();
m_egraph.merge(n, nb, c); m_egraph.merge(n, nb, c);
} }
if (!sign && n->is_equality()) { if (n->is_equality()) {
SASSERT(!m.is_iff(e)); if (sign)
euf::enode* na = n->get_arg(0); m_egraph.new_diseq(n);
euf::enode* nb = n->get_arg(1); else {
m_egraph.merge(na, nb, c); SASSERT(!m.is_iff(e));
} euf::enode* na = n->get_arg(0);
else if (sign && n->is_equality()) euf::enode* nb = n->get_arg(1);
m_egraph.new_diseq(n); m_egraph.merge(na, nb, c);
}
}
} }