mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

Simplify boolean propagation level

Browse source
This commit is contained in:
Jakob Rath 2022-11-09 16:59:51 +01:00
parent 27d65df70b
commit abc4cc5295
3 changed files with 2 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/polysat/constraint.cpp
View file

@ -77,16 +77,6 @@ namespace polysat {
return out.str(); return out.str();
} }
unsigned constraint::level(solver& s) const {
if (s.m_bvars.value(sat::literal(bvar())) != l_undef)
return s.m_bvars.level(bvar());
unsigned level = s.base_level();
for (auto v : vars())
if (s.is_assigned(v))
level = std::max(level, s.get_level(v));
return level;
}
lbool signed_constraint::bvalue(solver& s) const { lbool signed_constraint::bvalue(solver& s) const {
return get()->has_bvar() ? s.m_bvars.value(blit()) : l_undef; return get()->has_bvar() ? s.m_bvars.value(blit()) : l_undef;
} }

2
src/math/polysat/constraint.h
View file

@ -108,7 +108,6 @@ namespace polysat {
bool contains_var(pvar v) const { return m_vars.contains(v); } bool contains_var(pvar v) const { return m_vars.contains(v); }
sat::bool_var bvar() const { SASSERT(has_bvar()); return m_bvar; } sat::bool_var bvar() const { SASSERT(has_bvar()); return m_bvar; }
std::string bvar2string() const; std::string bvar2string() const;
unsigned level(solver& s) const;
void set_external(bool sign) { m_external_sign = to_lbool(sign); } void set_external(bool sign) { m_external_sign = to_lbool(sign); }
void unset_external() { m_external_sign = l_undef; } void unset_external() { m_external_sign = l_undef; }
@ -159,7 +158,6 @@ namespace polysat {
bool is_currently_false(solver& s, assignment_t const& sub) const { return get()->is_currently_false(s, sub, is_positive()); } bool is_currently_false(solver& s, assignment_t const& sub) const { return get()->is_currently_false(s, sub, is_positive()); }
bool is_currently_true(solver& s, assignment_t const& sub) const { return get()->is_currently_false(s, sub, is_negative()); } bool is_currently_true(solver& s, assignment_t const& sub) const { return get()->is_currently_false(s, sub, is_negative()); }
lbool bvalue(solver& s) const; lbool bvalue(solver& s) const;
unsigned level(solver& s) const { return get()->level(s); }
void narrow(solver& s, bool first) { get()->narrow(s, is_positive(), first); } void narrow(solver& s, bool first) { get()->narrow(s, is_positive(), first); }
inequality as_inequality() const { return get()->as_inequality(is_positive()); } inequality as_inequality() const { return get()->as_inequality(is_positive()); }

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

@ -936,9 +936,8 @@ namespace polysat {
for (auto lit : cl) { for (auto lit : cl) {
if (lit == lit0) if (lit == lit0)
continue; continue;
auto c = lit2cnstr(lit); SASSERT(m_bvars.is_false(lit));
if (m_bvars.is_false(lit) || c.is_currently_false(*this)) lvl = std::max(lvl, m_bvars.level(lit));
lvl = std::max(lvl, c.level(*this));
} }
return lvl; return lvl;
} }