mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

move modification to the front

Browse source
This commit is contained in:
Jakob Rath 2024-04-04 10:28:08 +02:00
parent 2b89767d1f
commit 3f3b052933
1 changed files with 12 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/sat/smt/polysat/viable.cpp
View file

@ -596,8 +596,20 @@ next:
*/
dependency_vector viable::explain() {
dependency_vector result;
// display_explain(verbose_stream()) << "\n";
// prune redundant intervals
remove_redundant_explanations();
explanation const last = m_explain.back();
// if there's more than one interval, we cannot have any full intervals
SASSERT(m_explain.size() <= 1 || all_of(m_explain, [](auto const& e) { return !e.e->interval.is_full(); }));
SASSERT(all_of(m_explain, [](auto const& e) { return !e.e->marked; }));
SASSERT(all_of(m_explain, [](auto const& e) { return !e.mark; }));
verbose_stream() << "\n\n\n\n\nviable::explain: " << m_explain_kind << " v" << m_var << "\n";
display_explain(verbose_stream()) << "\n";
@ -644,14 +656,6 @@ next:
SASSERT(m_explain_kind != explain_t::none);
// prune redundant intervals
remove_redundant_explanations();
// display_explain(verbose_stream()) << "\n";
SASSERT(all_of(m_explain, [](auto const& e) { return !e.e->marked; }));
SASSERT(all_of(m_explain, [](auto const& e) { return !e.mark; }));
explanation after = last;
for (unsigned i = m_explain.size() - 1; i-- > 0; ) {
explanation const& e = m_explain[i];