From 8493ebbabadea6852863a23f61900b235cfa6ceb Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 16 Mar 2023 16:51:18 +0100 Subject: [PATCH] nicer conditions --- src/math/polysat/solver.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 12d4b4606..dfae863ff 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -271,11 +271,11 @@ namespace polysat { } bool solver::can_repropagate_units() { - return !m_repropagate_units.empty(); + return !m_repropagate_units.empty() && !is_conflict(); } void solver::repropagate_units() { - while (!m_repropagate_units.empty() && !is_conflict()) { + while (can_repropagate_units()) { clause& cl = *m_repropagate_units.back(); m_repropagate_units.pop_back(); VERIFY_EQ(cl.size(), 1); @@ -300,7 +300,7 @@ namespace polysat { } bool solver::can_repropagate() { - return !m_repropagate_lits.empty(); + return !m_repropagate_lits.empty() && !is_conflict(); } // Repropagate: @@ -314,7 +314,7 @@ namespace polysat { // TODO: for assumptions this isn't implemented yet. But if we can bool-propagate an assumption from other literals, // it means that the external dependency on the assumed literal is unnecessary and a resulting unsat core may be smaller. void solver::repropagate() { - while (!m_repropagate_lits.empty() && !is_conflict()) { + while (can_repropagate() /* && !can_propagate() */) { sat::literal lit = m_repropagate_lits.back(); m_repropagate_lits.pop_back(); // check for missed lower boolean propagations