mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix bugs exposed by Nuno's PB example

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-07 21:43:37 -07:00
parent 9e916edcb0
commit 29c2672407
2 changed files with 24 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/sat/ba_solver.cpp
View file

@ -166,10 +166,11 @@ namespace sat {
unsigned w = 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_k = w - m_k + 1;
SASSERT(w >= m_k && m_k > 0);
VERIFY(w >= m_k && m_k > 0);
}
bool ba_solver::pb::is_watching(literal l) const {
@ -526,11 +527,13 @@ namespace sat {
bool ba_solver::init_watch(pb& p) {
clear_watch(p);
if (p.lit() != null_literal && value(p.lit()) == l_false) {
//IF_VERBOSE(0, verbose_stream() << "negate: " << p.k() << "\n");
p.negate();
}
VERIFY(p.lit() == null_literal || value(p.lit()) == l_true);
unsigned sz = p.size(), bound = p.k();
//IF_VERBOSE(0, verbose_stream() << "bound: " << p.k() << "\n");
// put the non-false literals into the head.
unsigned slack = 0, slack1 = 0, num_watch = 0, j = 0;
@ -833,9 +836,19 @@ namespace sat {
remove_constraint(p, "recompiled to cardinality");
return;
}
else {
p.set_size(sz);
p.update_max_sum();
if (p.max_sum() < k) {
if (p.lit() == null_literal) {
s().set_conflict(justification());
}
else {
s().assign(~p.lit(), justification());
}
remove_constraint(p, "recompiled to false");
return;
}
p.set_k(k);
SASSERT(p.well_formed());
@ -3210,6 +3223,7 @@ namespace sat {
if (is_marked(l) && m_weights[l.index()] <= p2.get_coeff(i)) {
++num_sub;
}
if (p1.size() + i > p2.size() + num_sub) return false;
}
return num_sub == p1.size();
}
@ -3364,8 +3378,9 @@ namespace sat {
m_weights.setx(l.second.index(), l.first, 0);
mark_visited(l.second);
}
for (unsigned i = 0; i < p1.num_watch(); ++i) {
subsumes(p1, p1[i].second);
for (unsigned i = 0; i < std::min(10u, p1.num_watch()); ++i) {
unsigned j = s().m_rand() % p1.num_watch();
subsumes(p1, p1[j].second);
}
for (wliteral l : p1) {
m_weights[l.second.index()] = 0;

8
src/sat/ba_solver.h
View file

@ -124,8 +124,8 @@ namespace sat {
protected:
unsigned m_k;
public:
pb_base(tag_t t, unsigned id, literal l, unsigned sz, size_t osz, unsigned k): constraint(t, id, l, sz, osz), m_k(k) {}
virtual void set_k(unsigned k) { m_k = k; }
pb_base(tag_t t, unsigned id, literal l, unsigned sz, size_t osz, unsigned k): constraint(t, id, l, sz, osz), m_k(k) { VERIFY(k < 4000000000); }
virtual void set_k(unsigned k) { VERIFY(k < 4000000000); m_k = k; }
virtual unsigned get_coeff(unsigned i) const { UNREACHABLE(); return 0; }
unsigned k() const { return m_k; }
virtual bool well_formed() const;
@ -157,7 +157,6 @@ namespace sat {
unsigned m_num_watch;
unsigned m_max_sum;
wliteral m_wlits[0];
void update_max_sum();
public:
static size_t get_obj_size(unsigned num_lits) { return sizeof(pb) + num_lits * sizeof(wliteral); }
pb(unsigned id, literal lit, svector<wliteral> const& wlits, unsigned k);
@ -171,10 +170,11 @@ namespace sat {
void set_slack(unsigned s) { m_slack = s; }
unsigned num_watch() const { return m_num_watch; }
unsigned max_sum() const { return m_max_sum; }
void update_max_sum();
void set_num_watch(unsigned s) { m_num_watch = s; }
bool is_cardinality() const;
virtual void negate();
virtual void set_k(unsigned k) { m_k = k; update_max_sum(); }
virtual void set_k(unsigned k) { m_k = k; VERIFY(k < 4000000000); update_max_sum(); }
virtual void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); }
virtual literal_vector literals() const { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; }
virtual bool is_watching(literal l) const;