mirror of
https://github.com/Z3Prover/z3
synced 2025-08-01 17:03:18 +00:00
get_watch_level
This commit is contained in:
parent
5a45f81d44
commit
2c44018a8a
4 changed files with 32 additions and 14 deletions
|
@ -129,4 +129,22 @@ namespace polysat {
|
||||||
out << " by " << show_deref(reason(lit));
|
out << " by " << show_deref(reason(lit));
|
||||||
return out;
|
return out;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* A literal may be watched if there is no unwatched literal at higher level,
|
||||||
|
* where true and unassigned literals are considered at infinite level.
|
||||||
|
* We prefer true literals to unassigned literals.
|
||||||
|
*/
|
||||||
|
uint64_t bool_var_manager::get_watch_level(sat::literal lit) const {
|
||||||
|
switch (value(lit)) {
|
||||||
|
case l_false:
|
||||||
|
return level(lit);
|
||||||
|
case l_true:
|
||||||
|
return std::numeric_limits<uint64_t>::max();
|
||||||
|
case l_undef:
|
||||||
|
return std::numeric_limits<uint64_t>::max() - 1;
|
||||||
|
}
|
||||||
|
UNREACHABLE();
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -63,6 +63,7 @@ namespace polysat {
|
||||||
lbool value(sat::literal lit) const { return m_value[lit.index()]; }
|
lbool value(sat::literal lit) const { return m_value[lit.index()]; }
|
||||||
bool is_true(sat::literal lit) const { return value(lit) == l_true; }
|
bool is_true(sat::literal lit) const { return value(lit) == l_true; }
|
||||||
bool is_false(sat::literal lit) const { return value(lit) == l_false; }
|
bool is_false(sat::literal lit) const { return value(lit) == l_false; }
|
||||||
|
bool is_undef(sat::literal lit) const { return value(lit) == l_undef; }
|
||||||
unsigned level(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_level[var]; }
|
unsigned level(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_level[var]; }
|
||||||
unsigned level(sat::literal lit) const { return level(lit.var()); }
|
unsigned level(sat::literal lit) const { return level(lit.var()); }
|
||||||
clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); SASSERT(is_bool_propagation(var) == !!m_reason[var]); return m_reason[var]; }
|
clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); SASSERT(is_bool_propagation(var) == !!m_reason[var]); return m_reason[var]; }
|
||||||
|
@ -95,6 +96,8 @@ namespace polysat {
|
||||||
UNREACHABLE();
|
UNREACHABLE();
|
||||||
return out;
|
return out;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
uint64_t get_watch_level(sat::literal lit) const;
|
||||||
};
|
};
|
||||||
|
|
||||||
struct bool_justification_pp {
|
struct bool_justification_pp {
|
||||||
|
|
|
@ -96,21 +96,12 @@ namespace polysat {
|
||||||
// A literal may be watched if there is no unwatched literal at higher level,
|
// A literal may be watched if there is no unwatched literal at higher level,
|
||||||
// where true and unassigned literals are considered at infinite level.
|
// where true and unassigned literals are considered at infinite level.
|
||||||
// We prefer true literals to unassigned literals.
|
// We prefer true literals to unassigned literals.
|
||||||
auto get_watch_level = [&](sat::literal lit) -> unsigned {
|
auto get_watch_level = [&](sat::literal lit) -> uint64_t {
|
||||||
switch (s.m_bvars.value(lit)) {
|
return s.m_bvars.get_watch_level(lit);
|
||||||
case l_false:
|
|
||||||
return s.m_bvars.level(lit);
|
|
||||||
case l_true:
|
|
||||||
return UINT_MAX;
|
|
||||||
case l_undef:
|
|
||||||
return UINT_MAX - 1;
|
|
||||||
}
|
|
||||||
UNREACHABLE();
|
|
||||||
return 0;
|
|
||||||
};
|
};
|
||||||
|
|
||||||
unsigned lvl0 = get_watch_level(cl[0]);
|
uint64_t lvl0 = get_watch_level(cl[0]);
|
||||||
unsigned lvl1 = get_watch_level(cl[1]);
|
uint64_t lvl1 = get_watch_level(cl[1]);
|
||||||
if (lvl0 < lvl1) {
|
if (lvl0 < lvl1) {
|
||||||
std::swap(lvl0, lvl1);
|
std::swap(lvl0, lvl1);
|
||||||
std::swap(cl[0], cl[1]);
|
std::swap(cl[0], cl[1]);
|
||||||
|
@ -118,7 +109,7 @@ namespace polysat {
|
||||||
SASSERT(lvl0 >= lvl1);
|
SASSERT(lvl0 >= lvl1);
|
||||||
for (unsigned i = 2; i < cl.size(); ++i) {
|
for (unsigned i = 2; i < cl.size(); ++i) {
|
||||||
sat::literal const lit = cl[i];
|
sat::literal const lit = cl[i];
|
||||||
unsigned const lvl = get_watch_level(lit);
|
uint64_t const lvl = get_watch_level(lit);
|
||||||
if (lvl > lvl0) {
|
if (lvl > lvl0) {
|
||||||
cl[i] = cl[1];
|
cl[i] = cl[1];
|
||||||
cl[1] = cl[0];
|
cl[1] = cl[0];
|
||||||
|
|
|
@ -331,6 +331,12 @@ 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) {
|
||||||
|
#if 0
|
||||||
|
LOG_H3("Propagate " << lit << " into " << cl);
|
||||||
|
for (sat::literal l : cl) {
|
||||||
|
LOG(" " << lit_pp(*this, l));
|
||||||
|
}
|
||||||
|
#endif
|
||||||
SASSERT(m_bvars.is_true(lit));
|
SASSERT(m_bvars.is_true(lit));
|
||||||
SASSERT(cl.size() >= 2);
|
SASSERT(cl.size() >= 2);
|
||||||
unsigned idx = (cl[0] == ~lit) ? 1 : 0;
|
unsigned idx = (cl[0] == ~lit) ? 1 : 0;
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue