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

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-06-07 22:03:16 -07:00
commit 24adae4166
3 changed files with 31 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/api/python/z3/z3.py
View file

@ -90,6 +90,9 @@ def _z3_assert(cond, msg):
if not cond:
raise Z3Exception(msg)
def _z3_check_cint_overflow(n, name):
_z3_assert(ctypes.c_int(n).value == n, name + " is too large")
def open_log(fname):
"""Log interaction to a file. This function must be invoked immediately after init(). """
Z3_open_log(fname)
@ -8132,6 +8135,7 @@ def _pb_args_coeffs(args, default_ctx = None):
_args, sz = _to_ast_array(args)
_coeffs = (ctypes.c_int * len(coeffs))()
for i in range(len(coeffs)):
_z3_check_cint_overflow(coeffs[i], "coefficient")
_coeffs[i] = coeffs[i]
return ctx, sz, _args, _coeffs
@ -8141,6 +8145,7 @@ def PbLe(args, k):
>>> a, b, c = Bools('a b c')
>>> f = PbLe(((a,1),(b,3),(c,2)), 3)
"""
_z3_check_cint_overflow(k, "k")
ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
@ -8150,6 +8155,7 @@ def PbGe(args, k):
>>> a, b, c = Bools('a b c')
>>> f = PbGe(((a,1),(b,3),(c,2)), 3)
"""
_z3_check_cint_overflow(k, "k")
ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
@ -8159,6 +8165,7 @@ def PbEq(args, k, ctx = None):
>>> a, b, c = Bools('a b c')
>>> f = PbEq(((a,1),(b,3),(c,2)), 3)
"""
_z3_check_cint_overflow(k, "k")
ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)

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;