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

simplify code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-22 13:19:03 -07:00
parent d0f2b00f96
commit e64bab4bb8
1 changed files with 14 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -268,18 +268,6 @@ namespace euf {
} }
} }
m_egraph.end_explain(); m_egraph.end_explain();
unsigned nv = s().num_vars();
expr_ref_vector eqs(m);
if (create_hint) {
// add negated equalities to hint.
for (auto const& [a,b] : m_hint_eqs) {
eqs.push_back(m.mk_eq(a->get_expr(), b->get_expr()));
set_tmp_bool_var(nv, eqs.back());
m_hint_lits.push_back(literal(nv, false));
++nv;
}
hint = mk_hint(m_euf, l);
}
CTRACE("euf", probing, tout << "explain " << l << " <- " << r << "\n"); CTRACE("euf", probing, tout << "explain " << l << " <- " << r << "\n");
unsigned j = 0; unsigned j = 0;
@ -289,10 +277,21 @@ namespace euf {
CTRACE("euf", create_hint, tout << "explain " << l << " <- " << m_hint_lits << "\n"); CTRACE("euf", create_hint, tout << "explain " << l << " <- " << m_hint_lits << "\n");
DEBUG_CODE(for (auto lit : r) SASSERT(s().value(lit) == l_true);); DEBUG_CODE(for (auto lit : r) SASSERT(s().value(lit) == l_true););
if (!probing) if (create_hint) {
unsigned nv = s().num_vars();
expr_ref_vector eqs(m);
// add equalities to hint.
for (auto const& [a,b] : m_hint_eqs) {
eqs.push_back(m.mk_eq(a->get_expr(), b->get_expr()));
set_tmp_bool_var(nv, eqs.back());
m_hint_lits.push_back(literal(nv, false));
++nv;
}
hint = mk_hint(m_euf, l);
log_antecedents(l, r, hint); log_antecedents(l, r, hint);
for (unsigned v = s().num_vars(); v < nv; ++v) for (unsigned v = s().num_vars(); v < nv; ++v)
set_tmp_bool_var(v, nullptr); set_tmp_bool_var(v, nullptr);
}
} }
void solver::get_th_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing) { void solver::get_th_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing) {