mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

fix boolean propagation

Browse source
This commit is contained in:
Jakob Rath 2023-02-20 09:39:44 +01:00
parent 2c44018a8a
commit 4501a372b1
1 changed files with 21 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/math/polysat/solver.cpp
View file

@ -331,6 +331,7 @@ namespace polysat {
* Return true if a new watch was found; or false to keep the existing one. * Return true if a new watch was found; or false to keep the existing one.
*/ */
bool solver::propagate(sat::literal lit, clause& cl) { bool solver::propagate(sat::literal lit, clause& cl) {
// scoped_set_log_enabled _enable(true);
#if 0 #if 0
LOG_H3("Propagate " << lit << " into " << cl); LOG_H3("Propagate " << lit << " into " << cl);
for (sat::literal l : cl) { for (sat::literal l : cl) {
@ -343,20 +344,34 @@ namespace polysat {
SASSERT(cl[1 - idx] == ~lit); SASSERT(cl[1 - idx] == ~lit);
if (m_bvars.is_true(cl[idx])) if (m_bvars.is_true(cl[idx]))
return false; return false;
unsigned i = 2; // Find a new watched literal:
for (; i < cl.size() && m_bvars.is_false(cl[i]); ++i); // - non-false literal (as usual)
if (i < cl.size()) { // - false literal, propagated at higher level than lit
// found non-false literal in cl; watch it instead // (may happen if a clause has been generated that propagated lit at a lower than current level)
unsigned i = cl.size();
uint64_t i_lvl = m_bvars.level(lit);
for (unsigned j = 2; j < cl.size(); ++j) {
uint64_t j_lvl = m_bvars.get_watch_level(cl[j]);
if (i_lvl < j_lvl) {
i = j;
i_lvl = j_lvl;
}
}
bool const updated_watch = i < cl.size();
if (updated_watch) {
// found better watch literal in cl; watch it instead
m_bvars.watch(cl[i]).push_back(&cl); m_bvars.watch(cl[i]).push_back(&cl);
// LOG("Found new watch: " << cl[i]);
std::swap(cl[1 - idx], cl[i]); std::swap(cl[1 - idx], cl[i]);
return true; if (!m_bvars.is_false(cl[1 - idx]))
return true;
} }
// all literals in cl are false, except possibly the other watch cl[idx] // all literals in cl are false, except possibly the other watch cl[idx]
if (m_bvars.is_false(cl[idx])) if (m_bvars.is_false(cl[idx]))
set_conflict(cl); set_conflict(cl);
else else
assign_propagate(cl[idx], cl); assign_propagate(cl[idx], cl);
return false; return updated_watch;
} }
void solver::linear_propagate() { void solver::linear_propagate() {