mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
parent
c36355c1e5
commit
e902e1ef13
|
@ -61,13 +61,18 @@ namespace ba {
|
|||
|
||||
void pb::negate() {
|
||||
m_lit.neg();
|
||||
unsigned w = 0;
|
||||
unsigned w = 0, m = 0;
|
||||
for (unsigned i = 0; i < m_size; ++i) {
|
||||
m_wlits[i].second.neg();
|
||||
VERIFY(w + m_wlits[i].first >= w);
|
||||
w += m_wlits[i].first;
|
||||
m = std::max(m, m_wlits[i].first);
|
||||
}
|
||||
m_k = w - m_k + 1;
|
||||
if (m > m_k)
|
||||
for (unsigned i = 0; i < m_size; ++i)
|
||||
m_wlits[i].first = std::min(m_k, m_wlits[i].first);
|
||||
|
||||
VERIFY(w >= m_k && m_k > 0);
|
||||
}
|
||||
|
||||
|
@ -121,6 +126,7 @@ namespace ba {
|
|||
|
||||
// watch a prefix of literals, such that the slack of these is >= k
|
||||
bool pb::init_watch(solver_interface& s) {
|
||||
SASSERT(well_formed());
|
||||
auto& p = *this;
|
||||
clear_watch(s);
|
||||
if (lit() != sat::null_literal && s.value(p.lit()) == l_false) {
|
||||
|
@ -178,6 +184,7 @@ namespace ba {
|
|||
|
||||
TRACE("ba", display(tout << "init watch: ", s, true););
|
||||
|
||||
|
||||
// slack is tight:
|
||||
if (slack + slack1 == bound) {
|
||||
SASSERT(slack1 == 0);
|
||||
|
|
Loading…
Reference in a new issue