mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

get_watch_level: prefer true literals at lower search index

Browse source
This commit is contained in:
Jakob Rath 2023-03-29 15:23:43 +02:00
parent 2a11be5c39
commit c516d6fe0c
1 changed files with 13 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/math/polysat/boolean.cpp
View file

@ -135,18 +135,22 @@ namespace polysat {
} }
/** /**
* A literal may be watched if there is no unwatched literal that has been assigned later, * Priority for watching literals:
* where true and unassigned literals are considered at infinite level. * 1. true literal, prefer lower search index to keep clause inactive for as long as possible.
* We prefer true literals to unassigned literals. * 2. unassigned literal
* 3. false literal, prefer higher search index (otherwise we might miss boolean propagations)
*/ */
uint64_t bool_var_manager::get_watch_level(sat::literal lit) const { uint64_t bool_var_manager::get_watch_level(sat::literal lit) const {
switch (value(lit)) { switch (value(lit)) {
case l_false: case l_true:
return s.m_search.get_bool_index(lit); // 0xFFFF'FFFF'****'****
case l_true: return 0xFFFF'FFFF'FFFF'FFFFull - s.m_search.get_bool_index(lit);
return std::numeric_limits<uint64_t>::max(); case l_undef:
case l_undef: // 0x0FFF'FFFF'FFFF'FFFF
return std::numeric_limits<uint64_t>::max() - 1; return 0x0FFF'FFFF'FFFF'FFFFull;
case l_false:
// 0x0000'0000'****'****
return s.m_search.get_bool_index(lit);
} }
UNREACHABLE(); UNREACHABLE();
return 0; return 0;