mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fix #2081

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-13 01:18:03 -08:00
parent dc5e4ca1c5
commit 4b35ef29c9
6 changed files with 78 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/pb_rewriter.cpp
View file

@ -323,7 +323,7 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
break;
}
}
TRACE("pb",
TRACE("pb_verbose",
expr_ref tmp(m);
tmp = m.mk_app(f, num_args, args);
tout << tmp << "\n";

2
src/opt/opt_context.cpp
View file

@ -437,7 +437,7 @@ namespace opt {
for (unsigned i = 0; r == l_true && i < sz; ++i) {
objective const& o = m_objectives[i];
bool is_last = i + 1 == sz;
r = execute(o, i + 1 < sz, sc && !is_last && o.m_type != O_MAXSMT);
r = execute(o, i + 1 < sz, sc && !is_last);
if (r == l_true && o.m_type == O_MINIMIZE && !get_lower_as_num(i).is_finite()) {
return r;
}

4
src/opt/wmax.cpp
View file

@ -75,11 +75,9 @@ namespace opt {
trace_bounds("wmax");
TRACE("opt",
s().display(tout); tout << "\n";
s().display(tout)<< "\n";
tout << "lower: " << m_lower << " upper: " << m_upper << "\n";);
while (!m.canceled() && m_lower < m_upper) {
//mk_assumptions(asms);
//is_sat = s().preferred_sat(asms, cores);
is_sat = s().check_sat(0, nullptr);
if (m.canceled()) {
is_sat = l_undef;

95
src/smt/theory_pb.cpp
View file

@ -467,7 +467,6 @@ namespace smt {
context& ctx = get_context();
ast_manager& m = get_manager();
TRACE("pb", tout << mk_pp(atom, m) << "\n";);
if (ctx.b_internalized(atom)) {
return true;
}
@ -494,17 +493,25 @@ namespace smt {
ctx.set_var_theory(abv, get_id());
literal lit(abv);
if (pb.is_eq(atom)) {
expr_ref_vector args(m);
expr_ref_vector args(m), nargs(m);
vector<rational> coeffs;
unsigned n = atom->get_num_args();
for (unsigned i = 0; i < n; ++i) {
rational sum(0);
for (unsigned i = 0; i < num_args; ++i) {
args.push_back(atom->get_arg(i));
coeffs.push_back(pb.get_coeff(atom, i));
nargs.push_back(::mk_not(m, atom->get_arg(i)));
rational c = pb.get_coeff(atom, i);
coeffs.push_back(c);
sum += c;
}
expr_ref le(pb.mk_le(n, coeffs.c_ptr(), args.c_ptr(), pb.get_k(atom)), m);
expr_ref ge(pb.mk_ge(n, coeffs.c_ptr(), args.c_ptr(), pb.get_k(atom)), m);
rational k = pb.get_k(atom);
// ax + by + cz <= k
// <=>
// -ax - by - cz >= -k
// <=>
// a(1-x) + b(1-y) + c(1-z) >= a + b + c - k
expr_ref le(pb.mk_ge(num_args, coeffs.c_ptr(), nargs.c_ptr(), sum - k), m);
expr_ref ge(pb.mk_ge(num_args, coeffs.c_ptr(), args.c_ptr(), k), m);
ctx.internalize(le, false);
ctx.internalize(ge, false);
literal le_lit = ctx.get_literal(le);
@ -540,23 +547,24 @@ namespace smt {
}
}
if (pb.is_at_most_k(atom) || pb.is_le(atom)) {
// turn W <= k into -W >= -k
for (unsigned i = 0; i < args.size(); ++i) {
args[i].second = -args[i].second;
}
IF_VERBOSE(0, verbose_stream() << "***le\n");
k = -k;
for (auto& a : args) {
a.first.neg();
k += a.second;
}
}
else {
SASSERT(pb.is_at_least_k(atom) || pb.is_ge(atom) || pb.is_eq(atom));
}
TRACE("pb", display(tout, *c, true););
TRACE("pb", display(tout << "inconsistent: " << ctx.inconsistent() << " ", *c, true););
c->unique();
lbool is_true = c->normalize();
c->prune();
c->post_prune();
TRACE("pb", display(tout, *c); tout << " := " << lit << "\n";);
TRACE("pb", display(tout, *c); tout << " := " << lit << " " << is_true << "\n";);
switch (is_true) {
case l_false:
lit = ~lit;
@ -584,8 +592,8 @@ namespace smt {
// maximal coefficient:
scoped_mpz& max_watch = c->m_max_watch;
max_watch.reset();
for (unsigned i = 0; i < args.size(); ++i) {
mpz const& num = args[i].second.to_mpq().numerator();
for (auto const& a : args) {
mpz const& num = a.second.to_mpq().numerator();
if (m_mpz_mgr.lt(max_watch, num)) {
max_watch = num;
}
@ -1046,12 +1054,8 @@ namespace smt {
}
ineq* c = m_var_infos[v].m_ineq;
if (c != nullptr) {
if (c->is_ge()) {
assign_ineq(*c, is_true);
}
else {
assign_eq(*c, is_true);
}
VERIFY(c->is_ge());
assign_ineq(*c, is_true);
}
ptr_vector<card>* cards = m_var_infos[v].m_lit_cwatch[nlit.sign()];
@ -1213,7 +1217,7 @@ namespace smt {
*/
void theory_pb::assign_eq(ineq& c, bool is_true) {
SASSERT(c.is_eq());
UNREACHABLE();
}
@ -2363,21 +2367,58 @@ namespace smt {
}
void theory_pb::validate_final_check() {
for (unsigned i = 0; i < m_var_infos.size(); ++i) {
ineq* c = m_var_infos[i].m_ineq;
if (c) {
validate_final_check(*c);
TRACE("pb", tout << "validate " << m_var_infos.size() << "\n";);
for (auto & vi : m_var_infos) {
if (vi.m_ineq) {
validate_final_check(*vi.m_ineq);
}
if (vi.m_card) {
validate_final_check(*vi.m_card);
}
}
}
void theory_pb::validate_final_check(card& c) {
context& ctx = get_context();
if (ctx.get_assignment(c.lit()) == l_undef) {
TRACE("pb", display(tout << "is undef ", c, true););
return;
}
if (!ctx.is_relevant(c.lit())) {
TRACE("pb", display(tout << "not relevant ", c, true););
return;
}
unsigned sum = 0, maxsum = 0;
for (unsigned i = 0; i < c.size(); ++i) {
switch(ctx.get_assignment(c.lit(i))) {
case l_true:
++sum;
case l_undef:
++maxsum;
break;
case l_false:
break;
}
}
TRACE("pb", display(tout << "validate: ", c, true);
tout << "sum: " << sum << " " << maxsum << " ";
tout << ctx.get_assignment(c.lit()) << "\n";);
SASSERT(sum <= maxsum);
SASSERT((sum >= c.k()) == (ctx.get_assignment(c.lit()) == l_true));
SASSERT((maxsum < c.k()) == (ctx.get_assignment(c.lit()) == l_false));
}
void theory_pb::validate_final_check(ineq& c) {
context& ctx = get_context();
if (ctx.get_assignment(c.lit()) == l_undef) {
TRACE("pb", tout << c.lit() << " is undef\n";);
return;
}
if (!ctx.is_relevant(c.lit())) {
TRACE("pb", tout << c.lit() << " is not relevant\n";);
return;
}
numeral sum = numeral::zero(), maxsum = numeral::zero();

1
src/smt/theory_pb.h
View file

@ -406,6 +406,7 @@ namespace smt {
bool validate_lemma();
void validate_final_check();
void validate_final_check(ineq& c);
void validate_final_check(card& c);
void validate_assign(ineq const& c, literal_vector const& lits, literal l) const;
void validate_watch(ineq const& c) const;
bool validate_unit_propagation(card const& c);

10
src/smt/theory_wmaxsat.cpp
View file

@ -103,8 +103,8 @@ namespace smt {
m_normalize = true;
bool_var bv = register_var(var, true);
(void)bv;
TRACE("opt", tout << "enable: v" << m_bool2var[bv] << " b" << bv << " " << mk_pp(var, get_manager()) << "\n";
tout << wfml << "\n";);
TRACE("opt", tout << "inc: " << ctx.inconsistent() << " enable: v" << m_bool2var[bv]
<< " b" << bv << " " << mk_pp(var, get_manager()) << "\n" << wfml << "\n";);
return var;
}
@ -134,8 +134,10 @@ namespace smt {
theory_var v = mk_var(x);
ctx.attach_th_var(x, this, v);
m_bool2var.insert(bv, v);
SASSERT(v == static_cast<theory_var>(m_var2bool.size()));
m_var2bool.push_back(bv);
while (m_var2bool.size() <= static_cast<unsigned>(v)) {
m_var2bool.push_back(null_bool_var);
}
m_var2bool[v] = bv;
SASSERT(ctx.bool_var2enode(bv));
}
return bv;