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

implement explain()

Browse source
This commit is contained in:
Lev Nachmanson 2024-11-01 18:48:23 -07:00 committed by Lev Nachmanson
parent b30272feed
commit 58e57352c2
1 changed files with 2 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/math/lp/dioph_eq.cpp
View file

@ -970,7 +970,7 @@ public:
SASSERT(ex.empty()); SASSERT(ex.empty());
TRACE("dioph_eq", tout << "conflict:"; print_eprime_entry(m_conflict_index, tout, true) << std::endl;); TRACE("dioph_eq", tout << "conflict:"; print_eprime_entry(m_conflict_index, tout, true) << std::endl;);
auto & ep = m_eprime[m_conflict_index]; auto & ep = m_eprime[m_conflict_index];
for (auto ci: lra.flatten(eq_deps(ep.m_l))) { for (auto ci: lra.flatten(explain_fixed_in_meta_term(ep.m_l))) {
ex.push_back(ci); ex.push_back(ci);
} }
TRACE("dioph_eq", lra.print_expl(tout, ex);); TRACE("dioph_eq", lra.print_expl(tout, ex););
@ -981,11 +981,7 @@ public:
} }
bool can_substitute(unsigned k) { bool can_substitute(unsigned k) {
return k < m_k2s.size() && m_k2s[k] != UINT_MAX; return k < m_k2s.size() && m_k2s[k] != UINT_MAX;
} }
u_dependency * eq_deps(const lar_term& t) {
NOT_IMPLEMENTED_YET();
return nullptr;
}
}; };
// Constructor definition // Constructor definition
dioph_eq::dioph_eq(int_solver& lia) { dioph_eq::dioph_eq(int_solver& lia) {