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

bug fixes to pb; working on model extraction

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-10 15:16:58 -08:00
parent 26bf64a0c3
commit 2c577a304d
15 changed files with 348 additions and 197 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/opt/core_maxsat.cpp
View file

@ -50,13 +50,13 @@ namespace opt {
case l_undef:
return l_undef;
case l_true: {
model_ref model;
model_ref mdl;
expr_ref_vector ans(m);
s.get_model(model);
s.get_model(mdl);
for (unsigned i = 0; i < aux.size(); ++i) {
expr_ref val(m);
VERIFY(model->eval(m_soft[i].get(), val));
VERIFY(mdl->eval(m_soft[i].get(), val));
if (m.is_true(val)) {
ans.push_back(m_soft[i].get());
}
@ -69,6 +69,7 @@ namespace opt {
if (ans.size() > m_answer.size()) {
m_answer.reset();
m_answer.append(ans);
m_model = mdl.get();
}
if (m_answer.size() == m_upper) {
return l_true;
@ -150,6 +151,9 @@ namespace opt {
void core_maxsat::collect_statistics(statistics& st) const {
// nothing specific
}
void core_maxsat::get_model(model_ref& mdl) {
mdl = m_model.get();
}
};

3
src/opt/core_maxsat.h
View file

@ -31,6 +31,7 @@ namespace opt {
expr_ref_vector m_soft;
expr_ref_vector m_answer;
unsigned m_upper;
model_ref m_model;
public:
core_maxsat(ast_manager& m, solver& s, expr_ref_vector& soft_constraints);
virtual ~core_maxsat();
@ -41,7 +42,7 @@ namespace opt {
virtual expr_ref_vector get_assignment() const;
virtual void set_cancel(bool f);
virtual void collect_statistics(statistics& st) const;
virtual void get_model(model_ref& mdl);
private:
void set2vector(expr_set const& set, ptr_vector<expr>& es) const;
expr_ref mk_at_most(expr_set const& set, unsigned k);

14
src/opt/fu_malik.cpp
View file

@ -48,6 +48,7 @@ namespace opt {
expr_ref_vector m_aux;
expr_ref_vector m_assignment;
unsigned m_upper_size;
model_ref m_model;
ref<solver> m_s;
solver & m_original_solver;
@ -300,13 +301,12 @@ namespace opt {
if (is_sat == l_true) {
// Get a list of satisfying m_soft
model_ref model;
s().get_model(model);
s().get_model(m_model);
m_assignment.reset();
for (unsigned i = 0; i < m_orig_soft.size(); ++i) {
expr_ref val(m);
VERIFY(model->eval(m_orig_soft[i].get(), val));
VERIFY(m_model->eval(m_orig_soft[i].get(), val));
if (m.is_true(val)) {
m_assignment.push_back(m_orig_soft[i].get());
}
@ -318,6 +318,10 @@ namespace opt {
return is_sat;
}
void get_model(model_ref& mdl) {
mdl = m_model.get();
}
};
fu_malik::fu_malik(ast_manager& m, solver& s, expr_ref_vector& soft_constraints) {
@ -348,6 +352,10 @@ namespace opt {
void fu_malik::collect_statistics(statistics& st) const {
m_imp->collect_statistics(st);
}
void fu_malik::get_model(model_ref& m) {
m_imp->get_model(m);
}

1
src/opt/fu_malik.h
View file

@ -42,6 +42,7 @@ namespace opt {
virtual expr_ref_vector get_assignment() const;
virtual void set_cancel(bool f);
virtual void collect_statistics(statistics& st) const;
virtual void get_model(model_ref& m);
};
};

7
src/opt/maxsmt.cpp
View file

@ -52,6 +52,9 @@ namespace opt {
if (m_msolver) {
is_sat = (*m_msolver)();
m_answer.append(m_msolver->get_assignment());
if (is_sat == l_true) {
m_msolver->get_model(m_model);
}
}
// Infrastructure for displaying and storing solution is TBD.
@ -105,6 +108,10 @@ namespace opt {
if (m_lower > r) m_lower = r;
}
void maxsmt::get_model(model_ref& mdl) {
mdl = m_model.get();
}
void maxsmt::commit_assignment() {
SASSERT(m_s);
for (unsigned i = 0; i < m_answer.size(); ++i) {

10
src/opt/maxsmt.h
View file

@ -35,6 +35,7 @@ namespace opt {
virtual expr_ref_vector get_assignment() const = 0;
virtual void set_cancel(bool f) = 0;
virtual void collect_statistics(statistics& st) const = 0;
virtual void get_model(model_ref& mdl) = 0;
};
/**
Takes solver with hard constraints added.
@ -52,6 +53,7 @@ namespace opt {
rational m_upper;
scoped_ptr<maxsmt_solver> m_msolver;
symbol m_maxsat_engine;
model_ref m_model;
public:
maxsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {}
@ -78,15 +80,11 @@ namespace opt {
rational get_lower() const;
rational get_upper() const;
void update_lower(rational const& r);
void get_model(model_ref& mdl);
expr_ref_vector get_assignment() const;
void display_answer(std::ostream& out) const;
void display_answer(std::ostream& out) const;
void collect_statistics(statistics& st) const;
private:
bool is_maxsat_problem(vector<rational> const& ws) const;

8
src/opt/opt_context.cpp
View file

@ -108,12 +108,16 @@ namespace opt {
void context::get_model(model_ref& mdl) {
mdl = m_model;
if (m_model_converter) {
(*m_model_converter)(mdl, 0);
}
}
lbool context::execute_min_max(unsigned index, bool committed, bool is_max) {
// HACK: reuse m_optsmt without regard for box reuse and not considering
// use-case of lex.
lbool result = m_optsmt(get_solver());
if (result == l_true) m_optsmt.get_model(m_model);
if (committed) m_optsmt.commit_assignment(index);
return result;
}
@ -122,6 +126,7 @@ namespace opt {
lbool context::execute_maxsat(symbol const& id, bool committed) {
maxsmt& ms = *m_maxsmts.find(id);
lbool result = ms(get_solver());
if (result == l_true) ms.get_model(m_model);
if (committed) ms.commit_assignment();
return result;
}
@ -177,11 +182,10 @@ namespace opt {
tactic_ref tac1 = mk_elim01_tactic(m);
tactic_ref tac2 = mk_lia2card_tactic(m);
tactic_ref tac = and_then(tac1.get(), tac2.get());
model_converter_ref mc; // TBD: expose model converter upwards and apply to returned model.
proof_converter_ref pc;
expr_dependency_ref core(m);
goal_ref_buffer result;
(*tac)(g, result, mc, pc, core); // TBD: have this an attribute so we can cancel.
(*tac)(g, result, m_model_converter, pc, core); // TBD: have this an attribute so we can cancel.
SASSERT(result.size() == 1);
goal* r = result[0];
fmls.reset();

2
src/opt/opt_context.h
View file

@ -29,6 +29,7 @@ Notes:
#include "opt_solver.h"
#include "optsmt.h"
#include "maxsmt.h"
#include "model_converter.h"
namespace opt {
@ -83,6 +84,7 @@ namespace opt {
map_id m_indices;
vector<objective> m_objectives;
model_ref m_model;
model_converter_ref m_model_converter;
obj_map<func_decl, unsigned> m_objective_fns;
public:
context(ast_manager& m);

5
src/opt/optsmt.cpp
View file

@ -121,6 +121,7 @@ namespace opt {
inf_eps v(r);
if (m_lower[idx] < v) {
m_lower[idx] = v;
s->get_model(m_model);
}
}
@ -261,6 +262,10 @@ namespace opt {
return m_is_max[i]?m_upper[i]:-m_lower[i];
}
void optsmt::get_model(model_ref& mdl) {
mdl = m_model.get();
}
// force lower_bound(i) <= objective_value(i)
void optsmt::commit_assignment(unsigned i) {
inf_eps mid(0);

2
src/opt/optsmt.h
View file

@ -37,6 +37,7 @@ namespace opt {
svector<bool> m_is_max;
svector<smt::theory_var> m_vars;
symbol m_engine;
model_ref m_model;
public:
optsmt(ast_manager& m): m(m), s(0), m_cancel(false), m_objs(m) {}
@ -56,6 +57,7 @@ namespace opt {
inf_eps get_value(unsigned index) const;
inf_eps get_lower(unsigned index) const;
inf_eps get_upper(unsigned index) const;
void get_model(model_ref& mdl);
void update_lower(unsigned idx, rational const& r);

17
src/opt/weighted_maxsat.cpp
View file

@ -35,6 +35,7 @@ namespace smt {
rational m_min_cost; // current maximal cost assignment.
u_map<theory_var> m_bool2var; // bool_var -> theory_var
svector<bool_var> m_var2bool; // theory_var -> bool_var
model_ref m_model;
public:
theory_weighted_maxsat(ast_manager& m):
theory(m.mk_family_id("weighted_maxsat")),
@ -186,6 +187,7 @@ namespace smt {
m_bool2var.reset();
m_var2bool.reset();
m_min_cost_atom = 0;
m_model = 0;
}
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_weighted_maxsat, new_ctx->get_manager()); }
@ -194,6 +196,9 @@ namespace smt {
virtual void new_eq_eh(theory_var v1, theory_var v2) { }
virtual void new_diseq_eh(theory_var v1, theory_var v2) { }
void get_model(model_ref& mdl) {
mdl = m_model.get();
}
private:
@ -239,9 +244,11 @@ namespace smt {
m_min_cost = weight;
m_cost_save.reset();
m_cost_save.append(m_costs);
ctx.get_model(m_model);
}
return false;
}
};
}
@ -284,6 +291,7 @@ namespace opt {
expr_ref_vector m_assignment;
vector<rational> m_weights;
rational m_upper;
model_ref m_model;
imp(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights):
m(m), s(s), m_soft(soft_constraints), m_assignment(m), m_weights(weights)
@ -337,6 +345,7 @@ namespace opt {
}
}
m_upper = wth.get_min_cost();
wth.get_model(m_model);
TRACE("opt", tout << "min cost: " << m_upper << "\n";);
wth.reset();
return result;
@ -349,6 +358,11 @@ namespace opt {
rational get_upper() const {
return m_upper;
}
void get_model(model_ref& mdl) {
mdl = m_model.get();
}
};
wmaxsmt::wmaxsmt(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights) {
@ -380,6 +394,9 @@ namespace opt {
void wmaxsmt::collect_statistics(statistics& st) const {
// no-op
}
void wmaxsmt::get_model(model_ref& mdl) {
m_imp->get_model(mdl);
}

1
src/opt/weighted_maxsat.h
View file

@ -40,6 +40,7 @@ namespace opt {
virtual expr_ref_vector get_assignment() const;
virtual void set_cancel(bool f);
virtual void collect_statistics(statistics& st) const;
virtual void get_model(model_ref& mdl);
};
};

11
src/smt/theory_arith_core.h
View file

@ -348,13 +348,24 @@ namespace smt {
context & ctx = get_context();
simplifier & s = ctx.get_simplifier();
expr_ref s_ante(m), s_conseq(m);
expr* s_conseq_n, * s_ante_n;
bool negated;
proof_ref pr(m);
s(ante, s_ante, pr);
negated = m.is_not(s_ante, s_ante_n);
if (negated) s_ante = s_ante_n;
ctx.internalize(s_ante, false);
literal l_ante = ctx.get_literal(s_ante);
if (negated) l_ante.neg();
s(conseq, s_conseq, pr);
negated = m.is_not(s_conseq, s_conseq_n);
if (negated) s_conseq = s_conseq_n;
ctx.internalize(s_conseq, false);
literal l_conseq = ctx.get_literal(s_conseq);
if (negated) l_conseq.neg();
literal lits[2] = {l_ante, l_conseq};
ctx.mk_th_axiom(get_id(), 2, lits);
if (ctx.relevancy()) {

437
src/smt/theory_pb.cpp
View file

@ -38,9 +38,9 @@ namespace smt {
}
void theory_pb::ineq::reset() {
m_max_coeff.reset();
m_max_watch.reset();
m_watch_sz = 0;
m_max_sum.reset();
m_watch_sum.reset();
m_num_propagations = 0;
m_compilation_threshold = UINT_MAX;
m_compiled = l_false;
@ -341,10 +341,10 @@ namespace smt {
// TBD: special cases: args.size() == 1
// maximal coefficient:
numeral& max_coeff = c->m_max_coeff;
max_coeff = numeral::zero();
numeral& max_watch = c->m_max_watch;
max_watch = numeral::zero();
for (unsigned i = 0; i < args.size(); ++i) {
max_coeff = std::max(max_coeff, args[i].second);
max_watch = std::max(max_watch, args[i].second);
}
@ -448,13 +448,13 @@ namespace smt {
std::swap(c.m_args[ineq_index], c.m_args[c.watch_size()-1]);
}
--c.m_watch_sz;
c.m_max_sum -= coeff;
if (c.max_coeff() == coeff) {
c.m_watch_sum -= coeff;
if (c.max_watch() == coeff) {
coeff = c.coeff(0);
for (unsigned i = 1; coeff != c.max_coeff() && i < c.m_watch_sz; ++i) {
for (unsigned i = 1; coeff != c.max_watch() && i < c.watch_size(); ++i) {
if (coeff < c.coeff(i)) coeff = c.coeff(i);
}
c.set_max_coeff(coeff);
c.set_max_watch(coeff);
}
// current index of unwatched literal is c.watch_size().
@ -463,12 +463,18 @@ namespace smt {
void theory_pb::add_watch(ineq& c, unsigned i) {
literal lit = c.lit(i);
bool_var v = lit.var();
c.m_max_sum += c.coeff(i);
numeral coeff = c.coeff(i);
c.m_watch_sum += coeff;
SASSERT(i >= c.watch_size());
if (i > c.watch_size()) {
std::swap(c.m_args[i], c.m_args[c.watch_size()]);
}
++c.m_watch_sz;
if (coeff > c.max_watch()) {
c.set_max_watch(coeff);
}
ptr_vector<ineq>* ineqs;
if (!m_watch.find(lit.index(), ineqs)) {
ineqs = alloc(ptr_vector<ineq>);
@ -515,43 +521,6 @@ namespace smt {
return FC_DONE;
}
void theory_pb::validate_final_check() {
u_map<ineq*>::iterator itc = m_ineqs.begin(), endc = m_ineqs.end();
for (; itc != endc; ++itc) {
validate_final_check(*itc->m_value);
}
}
void theory_pb::validate_final_check(ineq& c) {
context& ctx = get_context();
if (ctx.get_assignment(c.lit()) == l_undef) {
return;
}
if (!ctx.is_relevant(c.lit())) {
return;
}
numeral sum = numeral::zero(), maxsum = numeral::zero();
for (unsigned i = 0; i < c.size(); ++i) {
switch(ctx.get_assignment(c.lit(i))) {
case l_true:
sum += c.coeff(i);
case l_undef:
maxsum += c.coeff(i);
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::assign_eh(bool_var v, bool is_true) {
context& ctx = get_context();
ptr_vector<ineq>* ineqs = 0;
@ -636,15 +605,17 @@ namespace smt {
add_clause(c, lits);
}
else {
c.m_max_sum = numeral::zero();
c.m_watch_sum = numeral::zero();
c.m_watch_sz = 0;
for (unsigned i = 0; c.max_sum() < c.k() + c.max_coeff() && i < c.size(); ++i) {
c.m_max_watch = numeral::zero();
for (unsigned i = 0; c.watch_sum() < c.k() + c.max_watch() && i < c.size(); ++i) {
if (ctx.get_assignment(c.lit(i)) != l_false) {
add_watch(c, i);
}
}
SASSERT(c.max_sum() >= c.k());
SASSERT(c.watch_sum() >= c.k());
m_assign_ineqs_trail.push_back(&c);
DEBUG_CODE(validate_watch(c););
}
// perform unit propagation
@ -653,7 +624,7 @@ namespace smt {
lits.push_back(c.lit());
for (unsigned i = 0; i < c.size(); ++i) {
if (ctx.get_assignment(c.lit(i)) == l_undef) {
SASSERT(validate_assign(c, lits, c.lit(i)));
DEBUG_CODE(validate_assign(c, lits, c.lit(i)););
add_assign(c, lits, c.lit(i));
}
}
@ -677,20 +648,20 @@ namespace smt {
SASSERT(is_true == c.lit(w).sign());
//
// max_sum is decreased.
// watch_sum is decreased.
// Adjust set of watched literals.
//
numeral k = c.k();
numeral coeff = c.coeff(w);
for (unsigned i = c.watch_size(); c.max_sum() - coeff < k + c.max_coeff() && i < c.size(); ++i) {
for (unsigned i = c.watch_size(); c.watch_sum() - coeff < k + c.max_watch() && i < c.size(); ++i) {
if (ctx.get_assignment(c.lit(i)) != l_false) {
add_watch(c, i);
}
}
if (c.max_sum() - coeff < k) {
if (c.watch_sum() - coeff < k) {
//
// L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0, x2 <- 0
// create clause x1 or x2 or ~L
@ -702,12 +673,13 @@ namespace smt {
else {
del_watch(watch, watch_index, c, w);
removed = true;
if (c.max_sum() < k + c.max_coeff()) {
SASSERT(c.watch_sum() >= k);
if (c.watch_sum() < k + c.max_watch()) {
//
// opportunities for unit propagation for unassigned
// literals whose coefficients satisfy
// c.max_sum() < k
// c.watch_sum() < k
//
// L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0
// Create clauses x1 or ~L or x2
@ -717,18 +689,14 @@ namespace smt {
literal_vector& lits = get_unhelpful_literals(c, true);
lits.push_back(c.lit());
for (unsigned i = 0; i < c.size(); ++i) {
if (c.max_sum() - c.coeff(i) < k && ctx.get_assignment(c.lit(i)) == l_undef) {
SASSERT(validate_assign(c, lits, c.lit(i)));
if (c.watch_sum() - c.coeff(i) < k && ctx.get_assignment(c.lit(i)) == l_undef) {
DEBUG_CODE(validate_assign(c, lits, c.lit(i)););
add_assign(c, lits, c.lit(i));
}
}
}
//
// else: c.max_sum() >= k + c.max_coeff()
// we might miss opportunities for unit propagation if
// max_coeff is not the maximal coefficient
// of the current unassigned literal, but we can
// rely on eventually learning this from propagations.
// else: c.watch_sum() >= k + c.max_watch()
//
}
@ -875,12 +843,10 @@ namespace smt {
void theory_pb::inc_propagations(ineq& c) {
++c.m_num_propagations;
#if 1
if (c.m_compiled == l_false && c.m_num_propagations > c.m_compilation_threshold) {
c.m_compiled = l_undef;
m_to_compile.push_back(&c);
}
#endif
}
void theory_pb::restart_eh() {
@ -970,69 +936,6 @@ namespace smt {
m_ineqs_lim.resize(new_lim);
}
void theory_pb::display(std::ostream& out) const {
u_map<ptr_vector<ineq>*>::iterator it = m_watch.begin(), end = m_watch.end();
for (; it != end; ++it) {
out << "watch: " << to_literal(it->m_key) << " |-> ";
watch_list const& wl = *it->m_value;
for (unsigned i = 0; i < wl.size(); ++i) {
out << wl[i]->lit() << " ";
}
out << "\n";
}
u_map<ineq*>::iterator itc = m_ineqs.begin(), endc = m_ineqs.end();
for (; itc != endc; ++itc) {
ineq& c = *itc->m_value;
display(out, c);
}
}
std::ostream& theory_pb::display(std::ostream& out, ineq const& c, bool values) const {
ast_manager& m = get_manager();
context& ctx = get_context();
out << c.lit();
if (c.lit() != null_literal) {
if (values) {
out << "@(" << ctx.get_assignment(c.lit());
if (ctx.get_assignment(c.lit()) != l_undef) {
out << ":" << ctx.get_assign_level(c.lit());
}
out << ")";
}
expr_ref tmp(m);
ctx.literal2expr(c.lit(), tmp);
out << " " << tmp << "\n";
}
else {
out << " ";
}
for (unsigned i = 0; i < c.size(); ++i) {
literal l(c.lit(i));
if (!c.coeff(i).is_one()) {
out << c.coeff(i) << "*";
}
out << l;
if (values) {
out << "@(" << ctx.get_assignment(l);
if (ctx.get_assignment(l) != l_undef) {
out << ":" << ctx.get_assign_level(l);
}
out << ")";
}
if (i + 1 < c.size()) {
out << " + ";
}
}
out << " >= " << c.m_k << "\n";
if (c.m_num_propagations) out << "propagations: " << c.m_num_propagations << " ";
if (c.max_coeff().is_pos()) out << "max_coeff: " << c.max_coeff() << " ";
if (c.watch_size()) out << "watch size: " << c.watch_size() << " ";
if (c.max_sum().is_pos()) out << "max-sum: " << c.max_sum() << " ";
if (c.m_num_propagations || c.max_coeff().is_pos() || c.watch_size() || c.max_sum().is_pos()) out << "\n";
return out;
}
literal_vector& theory_pb::get_lits() {
m_literals.reset();
return m_literals;
@ -1087,34 +990,6 @@ namespace smt {
verbose_stream() << "\n";);
}
bool theory_pb::validate_assign(ineq const& c, literal_vector const& lits, literal l) const {
uint_set nlits;
context& ctx = get_context();
for (unsigned i = 0; i < lits.size(); ++i) {
SASSERT(ctx.get_assignment(lits[i]) == l_false);
nlits.insert((~lits[i]).index());
}
SASSERT(ctx.get_assignment(l) == l_undef);
SASSERT(ctx.get_assignment(c.lit()) == l_true);
nlits.insert(l.index());
numeral sum = numeral::zero();
for (unsigned i = 0; i < c.size(); ++i) {
literal lit = c.lit(i);
if (!nlits.contains(lit.index())) {
sum += c.coeff(i);
}
}
if (sum >= c.k()) {
IF_VERBOSE(0,
display(verbose_stream(), c, true);
for (unsigned i = 0; i < lits.size(); ++i) {
verbose_stream() << lits[i] << " ";
}
verbose_stream() << " => " << l << "\n";);
}
SASSERT(sum < c.k());
return true;
}
void theory_pb::set_mark(bool_var v, unsigned idx) {
SASSERT(v != null_bool_var);
@ -1149,7 +1024,12 @@ namespace smt {
}
else if (lvl > ctx.get_base_level()) {
if (is_marked(v)) {
m_lemma.m_args[m_conseq_index[v]].second += coeff;
numeral& lcoeff = m_lemma.m_args[m_conseq_index[v]].second;
lcoeff += coeff;
if (lcoeff.is_zero()) {
IF_VERBOSE(1, display(verbose_stream() << "remove 0 consequence", m_lemma, true););
remove_from_lemma(m_lemma, m_conseq_index[v]);
}
}
else {
if (lvl == m_conflict_lvl) {
@ -1243,10 +1123,9 @@ namespace smt {
while (m_num_marks > 0) {
m_lemma.normalize();
lbool is_sat = m_lemma.normalize();
if (is_sat != l_undef) {
IF_VERBOSE(0, display(verbose_stream() << "created non-tautology lemma: ", m_lemma, true););
IF_VERBOSE(0, display(verbose_stream() << "lemma already evaluated ", m_lemma, true););
return false;
}
TRACE("pb", display(tout, m_lemma, true););
@ -1261,11 +1140,22 @@ namespace smt {
--idx;
}
while (!is_marked(v) && idx > 0);
if (idx == 0) {
IF_VERBOSE(1, verbose_stream() << "BUG?!\n";);
if (idx == 0 && !is_marked(v)) {
//
// Yes, this can (currently) happen because
// the decisions for performing unit propagation
// are made asynchronously.
// In other words, PB unit propagation does not follow the
// same order as the assignment stack.
// It is not a correctness bug but causes to miss lemmas.
//
IF_VERBOSE(1, display_resolved_lemma(verbose_stream()););
for (unsigned i = 0; i < m_lemma.size(); ++i) {
unset_mark(m_lemma.lit(i));
}
return false;
}
unsigned conseq_index = m_conseq_index[v];
numeral conseq_coeff = m_lemma.coeff(conseq_index);
@ -1274,16 +1164,8 @@ namespace smt {
SASSERT(~conseq == m_lemma.lit(conseq_index));
// Remove conseq from lemma:
unsigned last = m_lemma.size()-1;
if (conseq_index != last) {
m_lemma.m_args[conseq_index] = m_lemma.m_args[last];
m_conseq_index[m_lemma.lit(conseq_index).var()] = conseq_index;
}
m_lemma.m_args.pop_back();
unset_mark(conseq);
remove_from_lemma(m_lemma, conseq_index);
--m_num_marks;
b_justification js = ctx.get_justification(v);
//
@ -1359,14 +1241,19 @@ namespace smt {
lbool is_true = m_lemma.normalize();
IF_VERBOSE(1, display(verbose_stream() << "lemma: ", m_lemma););
IF_VERBOSE(2, display(verbose_stream() << "lemma: ", m_lemma););
switch(is_true) {
case l_true:
UNREACHABLE();
return false;
case l_false:
//add_assign(c, m_ineq_literals, false_literal);
//break;
case l_false:
inc_propagations(c);
m_stats.m_num_conflicts++;
for (unsigned i = 0; i < m_ineq_literals.size(); ++i) {
m_ineq_literals[i].neg();
}
ctx.mk_clause(m_ineq_literals.size(), m_ineq_literals.c_ptr(), 0, CLS_AUX_LEMMA, 0);
break;
default: {
app_ref tmp = m_lemma.to_expr(ctx, get_manager());
internalize_atom(tmp, false);
@ -1389,4 +1276,204 @@ namespace smt {
}
}
}
void theory_pb::remove_from_lemma(ineq& c, unsigned idx) {
// Remove conseq from lemma:
literal lit = c.lit(idx);
unsigned last = c.size()-1;
if (idx != last) {
c.m_args[idx] = c.m_args[last];
m_conseq_index[c.lit(idx).var()] = idx;
}
c.m_args.pop_back();
unset_mark(lit);
--m_num_marks;
}
// debug methods
void theory_pb::validate_watch(ineq const& c) const {
context& ctx = get_context();
numeral sum = numeral::zero();
numeral max = numeral::zero();
for (unsigned i = 0; i < c.watch_size(); ++i) {
sum += c.coeff(i);
if (c.coeff(i) > max) {
max = c.coeff(i);
}
}
SASSERT(c.watch_sum() == sum);
SASSERT(sum >= c.k());
SASSERT(max == c.max_watch());
}
void theory_pb::validate_assign(ineq const& c, literal_vector const& lits, literal l) const {
uint_set nlits;
context& ctx = get_context();
for (unsigned i = 0; i < lits.size(); ++i) {
SASSERT(ctx.get_assignment(lits[i]) == l_true);
nlits.insert((~lits[i]).index());
}
SASSERT(ctx.get_assignment(l) == l_undef);
SASSERT(ctx.get_assignment(c.lit()) == l_true);
nlits.insert(l.index());
numeral sum = numeral::zero();
for (unsigned i = 0; i < c.size(); ++i) {
literal lit = c.lit(i);
if (!nlits.contains(lit.index())) {
sum += c.coeff(i);
}
}
if (sum >= c.k()) {
IF_VERBOSE(0,
display(verbose_stream(), c, true);
for (unsigned i = 0; i < lits.size(); ++i) {
verbose_stream() << lits[i] << " ";
}
verbose_stream() << " => " << l << "\n";);
}
SASSERT(sum < c.k());
}
void theory_pb::validate_final_check() {
u_map<ineq*>::iterator itc = m_ineqs.begin(), endc = m_ineqs.end();
for (; itc != endc; ++itc) {
validate_final_check(*itc->m_value);
}
}
void theory_pb::validate_final_check(ineq& c) {
context& ctx = get_context();
if (ctx.get_assignment(c.lit()) == l_undef) {
return;
}
if (!ctx.is_relevant(c.lit())) {
return;
}
numeral sum = numeral::zero(), maxsum = numeral::zero();
for (unsigned i = 0; i < c.size(); ++i) {
switch(ctx.get_assignment(c.lit(i))) {
case l_true:
sum += c.coeff(i);
case l_undef:
maxsum += c.coeff(i);
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));
}
// display methods
void theory_pb::display_resolved_lemma(std::ostream& out) const {
context& ctx = get_context();
literal_vector const& lits = ctx.assigned_literals();
bool_var v;
unsigned lvl;
out << "num marks: " << m_num_marks << "\n";
out << "conflict level: " << m_conflict_lvl << "\n";
for (unsigned i = 0; i < lits.size(); ++i) {
v = lits[i].var();
lvl = ctx.get_assign_level(v);
out << lits[i]
<< "@ " << lvl
<< " " << (is_marked(v)?"m":"u")
<< "\n";
if (lvl == m_conflict_lvl && is_marked(v)) {
out << "skipped: " << lits[i] << ":"<< i << "\n";
}
}
display(out, m_lemma, true);
unsigned nc = 0;
for (unsigned i = 0; i < m_lemma.size(); ++i) {
v = m_lemma.lit(i).var();
lvl = ctx.get_assign_level(v);
if (lvl == m_conflict_lvl) ++nc;
out << m_lemma.lit(i)
<< "@" << lvl
<< " " << (is_marked(v)?"m":"u")
<< " " << ctx.get_assignment(m_lemma.lit(i))
<< "\n";
}
out << "num conflicts: " << nc << "\n";
}
std::ostream& theory_pb::display(std::ostream& out, ineq const& c, bool values) const {
ast_manager& m = get_manager();
context& ctx = get_context();
out << c.lit();
if (c.lit() != null_literal) {
if (values) {
out << "@(" << ctx.get_assignment(c.lit());
if (ctx.get_assignment(c.lit()) != l_undef) {
out << ":" << ctx.get_assign_level(c.lit());
}
out << ")";
}
expr_ref tmp(m);
ctx.literal2expr(c.lit(), tmp);
out << " " << tmp << "\n";
}
else {
out << " ";
}
for (unsigned i = 0; i < c.size(); ++i) {
literal l(c.lit(i));
if (!c.coeff(i).is_one()) {
out << c.coeff(i) << "*";
}
out << l;
if (values) {
out << "@(" << ctx.get_assignment(l);
if (ctx.get_assignment(l) != l_undef) {
out << ":" << ctx.get_assign_level(l);
}
out << ")";
}
if (i + 1 == c.watch_size()) {
out << " .w ";
}
if (i + 1 < c.size()) {
out << " + ";
}
}
out << " >= " << c.m_k << "\n";
if (c.m_num_propagations) out << "propagations: " << c.m_num_propagations << " ";
if (c.max_watch().is_pos()) out << "max_watch: " << c.max_watch() << " ";
if (c.watch_size()) out << "watch size: " << c.watch_size() << " ";
if (c.watch_sum().is_pos()) out << "watch-sum: " << c.watch_sum() << " ";
if (c.m_num_propagations || c.max_watch().is_pos() || c.watch_size() || c.watch_sum().is_pos()) out << "\n";
return out;
}
void theory_pb::display(std::ostream& out) const {
u_map<ptr_vector<ineq>*>::iterator it = m_watch.begin(), end = m_watch.end();
for (; it != end; ++it) {
out << "watch: " << to_literal(it->m_key) << " |-> ";
watch_list const& wl = *it->m_value;
for (unsigned i = 0; i < wl.size(); ++i) {
out << wl[i]->lit() << " ";
}
out << "\n";
}
u_map<ineq*>::iterator itc = m_ineqs.begin(), endc = m_ineqs.end();
for (; itc != endc; ++itc) {
ineq& c = *itc->m_value;
display(out, c);
}
}
}

17
src/smt/theory_pb.h
View file

@ -48,11 +48,11 @@ namespace smt {
numeral m_k; // invariants: m_k > 0, coeffs[i] > 0
// Watch the first few positions until the sum satisfies:
// sum coeffs[i] >= m_lower + max_coeff
// sum coeffs[i] >= m_lower + max_watch
numeral m_max_coeff; // maximal coefficient.
numeral m_max_watch; // maximal coefficient.
unsigned m_watch_sz; // number of literals being watched.
numeral m_max_sum; // maximal sum of watch literals.
numeral m_watch_sum; // maximal sum of watch literals.
unsigned m_num_propagations;
unsigned m_compilation_threshold;
lbool m_compiled;
@ -69,9 +69,9 @@ namespace smt {
unsigned size() const { return m_args.size(); }
numeral const& max_sum() const { return m_max_sum; }
numeral const& max_coeff() const { return m_max_coeff; }
void set_max_coeff(numeral const& n) { m_max_coeff = n; }
numeral const& watch_sum() const { return m_watch_sum; }
numeral const& max_watch() const { return m_max_watch; }
void set_max_watch(numeral const& n) { m_max_watch = n; }
unsigned watch_size() const { return m_watch_sz; }
@ -118,6 +118,7 @@ namespace smt {
std::ostream& display(std::ostream& out, ineq const& c, bool values = false) const;
virtual void display(std::ostream& out) const;
void display_resolved_lemma(std::ostream& out) const;
void add_clause(ineq& c, literal_vector const& lits);
void add_assign(ineq& c, literal_vector const& lits, literal l);
@ -152,12 +153,14 @@ namespace smt {
bool resolve_conflict(ineq& c);
void process_antecedent(literal l, numeral coeff);
void process_ineq(ineq& c, literal conseq, numeral coeff);
void remove_from_lemma(ineq& c, unsigned idx);
void hoist_maximal_values();
void validate_final_check();
void validate_final_check(ineq& c);
bool validate_assign(ineq const& c, literal_vector const& lits, literal l) const;
void validate_assign(ineq const& c, literal_vector const& lits, literal l) const;
void validate_watch(ineq const& c) const;
public:
theory_pb(ast_manager& m);