diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 579a7c6e9..11d87a98e 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -12,62 +12,79 @@
using namespace opt;
struct maxres::imp {
- ast_manager& m;
- solver& s;
- expr_ref_vector m_B;
- expr_ref_vector m_D;
- expr_ref_vector m_asms;
- app_ref_vector m_clss;
- model_ref m_model;
- expr_ref_vector m_soft_constraints;
- volatile bool m_cancel;
- rational m_lower;
- rational m_upper;
- obj_map<expr, app*> m_asm2cls;
+ struct info {
+ app* m_cls;
+ rational m_weight;
+ info(app* cls, rational const& w):
+ m_cls(cls), m_weight(w) {}
+ info(): m_cls(0) {}
+ };
+ ast_manager& m;
+ solver& s;
+ expr_ref_vector m_B;
+ expr_ref_vector m_D;
+ expr_ref_vector m_asms;
+ model_ref m_model;
+ expr_ref_vector m_soft_constraints;
+ volatile bool m_cancel;
+ rational m_lower;
+ rational m_upper;
+ obj_map<expr, info> m_asm2info;
+ ptr_vector<expr> m_new_core;
+ mus m_mus;
+ expr_ref_vector m_trail;
- imp(ast_manager& m, solver& s, expr_ref_vector& soft_constraints):
- m(m), s(s), m_B(m), m_D(m), m_asms(m), m_clss(m), m_soft_constraints(soft_constraints),
- m_cancel(false)
+ imp(ast_manager& m, solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights):
+ m(m), s(s), m_B(m), m_D(m), m_asms(m), m_soft_constraints(m),
+ m_cancel(false),
+ m_mus(s, m),
+ m_trail(m)
{
+ // TBD: this introduces an assertion to solver.
+ init_soft(weights, soft_constraints);
}
bool is_literal(expr* l) {
return
is_uninterp_const(l) ||
- m.is_not(l, l) && is_uninterp_const(l);
+ (m.is_not(l, l) && is_uninterp_const(l));
}
- void add_soft(expr* e) {
+ void add_soft(expr* e, rational const& w) {
TRACE("opt", tout << mk_pp(e, m) << "\n";);
expr_ref asum(m), fml(m);
app_ref cls(m);
cls = mk_cls(e);
- m_clss.push_back(cls);
+ m_trail.push_back(cls);
if (is_literal(e)) {
- m_asms.push_back(e);
+ asum = e;
}
else {
asum = m.mk_fresh_const("soft", m.mk_bool_sort());
fml = m.mk_iff(asum, e);
s.assert_expr(fml);
- m_asms.push_back(asum);
}
- m_asm2cls.insert(m_asms.back(), cls.get());
+ new_assumption(asum, cls, w);
+ m_upper += w;
+ }
+
+ void new_assumption(expr* e, app* cls, rational const& w) {
+ info inf(cls, w);
+ m_asm2info.insert(e, inf);
+ m_asms.push_back(e);
+ m_trail.push_back(e);
}
lbool operator()() {
expr_ref fml(m);
- ptr_vector<expr> core, new_core;
+ ptr_vector<expr> core;
solver::scoped_push _sc(s);
- for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
- add_soft(m_soft_constraints[i].get());
- }
- m_upper = rational(m_soft_constraints.size());
while (true) {
TRACE("opt",
display_vec(tout, m_asms.size(), m_asms.c_ptr());
s.display(tout);
tout << "\n";
+ display(tout);
);
lbool is_sat = s.check_sat(m_asms.size(), m_asms.c_ptr());
if (m_cancel) {
@@ -85,37 +102,21 @@ struct maxres::imp {
s.get_unsat_core(core);
TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr()););
SASSERT(!core.empty());
+ is_sat = minimize_core(core);
+ SASSERT(!core.empty());
if (core.empty()) {
return l_false;
}
-#if 1
- // minimize core:
- mus ms(s, m);
- for (unsigned i = 0; i < core.size(); ++i) {
- app* cls = 0;
- VERIFY(m_asm2cls.find(core[i], cls));
- SASSERT(cls);
- SASSERT(m.is_or(cls));
- ms.add_soft(core[i], cls->get_num_args(), cls->get_args());
- }
- unsigned_vector mus_idx;
- is_sat = ms.get_mus(mus_idx);
if (is_sat != l_true) {
return is_sat;
}
- new_core.reset();
- for (unsigned i = 0; i < mus_idx.size(); ++i) {
- new_core.push_back(core[mus_idx[i]]);
- }
- core.reset();
- core.append(new_core);
-
-#endif
+ remove_core(core);
+ rational w = split_core(core);
TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr()););
- max_resolve(core);
+ max_resolve(core, w);
fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr()));
s.assert_expr(fml);
- m_lower += rational::one();
+ m_lower += w;
break;
}
IF_VERBOSE(1, verbose_stream() << "(opt.max_res lower: " << m_lower << ")\n";);
@@ -123,6 +124,57 @@ struct maxres::imp {
return l_true;
}
+ lbool minimize_core(ptr_vector<expr>& core) {
+ m_mus.reset();
+ for (unsigned i = 0; i < core.size(); ++i) {
+ app* cls = get_clause(core[i]);
+ SASSERT(cls);
+ SASSERT(m.is_or(cls));
+ m_mus.add_soft(core[i], cls->get_num_args(), cls->get_args());
+ }
+ unsigned_vector mus_idx;
+ lbool is_sat = m_mus.get_mus(mus_idx);
+ if (is_sat != l_true) {
+ return is_sat;
+ }
+ m_new_core.reset();
+ for (unsigned i = 0; i < mus_idx.size(); ++i) {
+ m_new_core.push_back(core[mus_idx[i]]);
+ }
+ core.reset();
+ core.append(m_new_core);
+ return l_true;
+ }
+
+ rational get_weight(expr* e) {
+ return m_asm2info.find(e).m_weight;
+ }
+
+ app* get_clause(expr* e) {
+ return m_asm2info.find(e).m_cls;
+ }
+
+ rational split_core(ptr_vector<expr> const& core) {
+
+ // find the minimal weight:
+ SASSERT(!core.empty());
+ rational w = get_weight(core[0]);
+ for (unsigned i = 1; i < core.size(); ++i) {
+ rational w2 = get_weight(core[i]);
+ if (w2 < w) {
+ w = w2;
+ }
+ }
+ // add fresh soft clauses for weights that are above w.
+ for (unsigned i = 0; i < core.size(); ++i) {
+ rational w2 = get_weight(core[i]);
+ if (w2 > w) {
+ new_assumption(core[i], get_clause(core[i]), w2 - w);
+ }
+ }
+ return w;
+ }
+
void display_vec(std::ostream& out, unsigned sz, expr* const* args) {
for (unsigned i = 0; i < sz; ++i) {
out << mk_pp(args[i], m) << " ";
@@ -130,7 +182,14 @@ struct maxres::imp {
out << "\n";
}
- void max_resolve(ptr_vector<expr>& core) {
+ void display(std::ostream& out) {
+ for (unsigned i = 0; i < m_asms.size(); ++i) {
+ expr* a = m_asms[i].get();
+ out << mk_pp(a, m) << " : " << get_weight(a) << "\n";
+ }
+ }
+
+ void max_resolve(ptr_vector<expr>& core, rational const& w) {
SASSERT(!core.empty());
expr_ref fml(m), asum(m);
app_ref cls(m);
@@ -144,7 +203,6 @@ struct maxres::imp {
// d_i := (!core_{i+1} or d_{i+1}) for i = 0...sz-2
// soft (!d_i or core_i)
//
- remove_core(core);
for (unsigned i = core.size()-1; i > 0; ) {
--i;
expr* d_i1 = m_D[i+1].get();
@@ -155,11 +213,10 @@ struct maxres::imp {
asum = m.mk_fresh_const("a", m.mk_bool_sort());
cls = m.mk_implies(d_i, b_i);
fml = m.mk_iff(asum, cls);
- s.assert_expr(fml);
- m_asms.push_back(asum);
cls = mk_cls(cls);
- m_clss.push_back(cls);
- m_asm2cls.insert(asum, cls);
+ m_trail.push_back(cls);
+ new_assumption(asum, cls, w);
+ s.assert_expr(fml);
}
}
@@ -199,9 +256,7 @@ struct maxres::imp {
for (unsigned i = 0; i < m_asms.size(); ++i) {
if (core.contains(m_asms[i].get())) {
m_asms[i] = m_asms.back();
- m_clss[i] = m_clss.back();
m_asms.pop_back();
- m_clss.pop_back();
--i;
}
}
@@ -217,11 +272,12 @@ struct maxres::imp {
bool get_assignment(unsigned index) const {
expr_ref tmp(m);
- m_model->eval(m_soft_constraints[index], tmp);
+ VERIFY(m_model->eval(m_soft_constraints[index], tmp));
return m.is_true(tmp);
}
void set_cancel(bool f) {
m_cancel = f;
+ m_mus.set_cancel(f);
}
void collect_statistics(statistics& st) const {
}
@@ -232,10 +288,22 @@ struct maxres::imp {
;
}
+ void init_soft(vector<rational> const& weights, expr_ref_vector const& soft) {
+ m_soft_constraints.reset();
+ m_upper.reset();
+ m_lower.reset();
+ m_asm2info.reset();
+ m_trail.reset();
+ m_soft_constraints.append(soft);
+ for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
+ add_soft(m_soft_constraints[i].get(), weights[i]);
+ }
+ }
+
};
-maxres::maxres(ast_manager& m, solver& s, expr_ref_vector& soft_constraints) {
- m_imp = alloc(imp, m, s, soft_constraints);
+maxres::maxres(ast_manager& m, solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights) {
+ m_imp = alloc(imp, m, s, soft_constraints, weights);
}
maxres::~maxres() {
diff --git a/src/opt/maxres.h b/src/opt/maxres.h
index 8b90158fb..41b57456f 100644
--- a/src/opt/maxres.h
+++ b/src/opt/maxres.h
@@ -4,7 +4,7 @@ namespace opt {
struct imp;
imp* m_imp;
public:
- maxres(ast_manager& m, solver& s, expr_ref_vector& soft_constraints);
+ maxres(ast_manager& m, solver& s, expr_ref_vector& soft_constraints, vector<rational>const& weights);
~maxres();
virtual lbool operator()();
virtual rational get_lower() const;
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 2eb6e426b..1cc98d328 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -39,16 +39,16 @@ namespace opt {
m_msolver = 0;
is_sat = m_s->check_sat(0, 0);
}
+ else if (m_maxsat_engine == symbol("maxres")) {
+ m_msolver = alloc(maxres, m, *m_s, m_soft_constraints, m_weights);
+ }
else if (is_maxsat_problem(m_weights)) {
if (m_maxsat_engine == symbol("core_maxsat")) {
m_msolver = alloc(core_maxsat, m, *m_s, m_soft_constraints);
}
else if (m_maxsat_engine == symbol("weighted_maxsat")) {
m_msolver = alloc(wmaxsmt, m, m_s.get(), m_soft_constraints, m_weights);
- }
- else if (m_maxsat_engine == symbol("maxres")) {
- m_msolver = alloc(maxres, m, *m_s, m_soft_constraints);
- }
+ }
else {
m_msolver = alloc(fu_malik, m, *m_s, m_soft_constraints);
}
diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp
index 1bed42f7d..9d9278a27 100644
--- a/src/opt/mus.cpp
+++ b/src/opt/mus.cpp
@@ -16,9 +16,21 @@ struct mus::imp {
vector<smt::literal_vector> m_cls2lits;
expr_ref_vector m_vars;
obj_map<expr, unsigned> m_var2idx;
+ volatile bool m_cancel;
-public:
- imp(solver& s, ast_manager& m): s(s), m(m), m_cls2expr(m), m_vars(m) {}
+ imp(solver& s, ast_manager& m): s(s), m(m), m_cls2expr(m), m_vars(m), m_cancel(false) {}
+
+ void reset() {
+ m_cls2expr.reset();
+ m_expr2cls.reset();
+ m_cls2lits.reset();
+ m_vars.reset();
+ m_var2idx.reset();
+ }
+
+ void set_cancel(bool f) {
+ m_cancel = f;
+ }
unsigned add_var(expr* v) {
unsigned idx = m_vars.size();
@@ -47,10 +59,16 @@ public:
m_cls2lits.push_back(lits);
return idx;
}
+
+ expr* mk_not(expr* e) {
+ if (m.is_not(e, e)) {
+ return e;
+ }
+ return m.mk_not(e);
+ }
lbool get_mus(unsigned_vector& mus) {
TRACE("opt", tout << "\n";);
- solver::scoped_push _sc(s);
unsigned_vector core;
for (unsigned i = 0; i < m_cls2expr.size(); ++i) {
core.push_back(i);
@@ -61,12 +79,17 @@ public:
ptr_vector<expr> core_exprs;
model.resize(m_vars.size());
while (!core.empty()) {
- IF_VERBOSE(0, display_vec(tout << "core: ", core););
+ TRACE("opt",
+ display_vec(tout << "core: ", core);
+ display_vec(tout << "mus: ", mus);
+ display_vec(tout << "model: ", model);
+ );
+ IF_VERBOSE(1, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";);
unsigned cls_id = core.back();
core.pop_back();
expr* cls = m_cls2expr[cls_id].get();
expr_ref not_cls(m);
- not_cls = m.mk_not(cls);
+ not_cls = mk_not(cls);
unsigned sz = assumptions.size();
assumptions.push_back(not_cls);
add_core(core, assumptions);
@@ -113,7 +136,7 @@ public:
template<class T>
void display_vec(std::ostream& out, T const& v) const {
for (unsigned i = 0; i < v.size(); ++i) {
- out << mk_pp(v[i], m) << " ";
+ out << v[i] << " ";
}
out << "\n";
}
@@ -133,19 +156,18 @@ public:
*/
void rmr(unsigned_vector& M, unsigned_vector& mus, svector<bool>& model) {
TRACE("opt",
- display_vec(tout << "M:", M);
- display_vec(tout << "mus:", mus);
- display_vec(tout << "model:", model););
+ display_vec(tout << "core: ", M);
+ display_vec(tout << "mus: ", mus);
+ display_vec(tout << "model: ", model););
unsigned cls_id = mus.back();
smt::literal_vector const& cls = m_cls2lits[cls_id];
- unsigned cls_id_new;
for (unsigned i = 0; i < cls.size(); ++i) {
smt::literal lit = cls[i];
SASSERT(model[lit.var()] == lit.sign()); // literal evaluates to false.
model[lit.var()] = !model[lit.var()]; // swap assignment
- if (has_single_unsat(model, cls_id_new)) {
- mus.push_back(cls_id_new);
+ if (!mus.contains(cls_id) && has_single_unsat(model, cls_id)) {
+ mus.push_back(cls_id);
rmr(M, mus, model);
}
model[lit.var()] = !model[lit.var()]; // swap assignment back
@@ -176,13 +198,6 @@ public:
return false;
}
- template<class T>
- void display_vec(std::ostream& out, T const& v) {
- for (unsigned i = 0; i < v.size(); ++i) {
- out << v[i] << " ";
- }
- out << "\n";
- }
};
mus::mus(solver& s, ast_manager& m) {
@@ -201,3 +216,10 @@ lbool mus::get_mus(unsigned_vector& mus) {
return m_imp->get_mus(mus);
}
+void mus::set_cancel(bool f) {
+ m_imp->set_cancel(f);
+}
+
+void mus::reset() {
+ m_imp->reset();
+}
diff --git a/src/opt/mus.h b/src/opt/mus.h
index a2ba36f14..e3cb4c963 100644
--- a/src/opt/mus.h
+++ b/src/opt/mus.h
@@ -16,6 +16,10 @@ namespace opt {
unsigned add_soft(expr* cls, unsigned sz, expr* const* args);
lbool get_mus(unsigned_vector& mus);
+
+ void reset();
+
+ void set_cancel(bool f);
};
};