mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 20:38:43 +00:00
adding mus extraction
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
582dbe509c
commit
bf35a62da7
|
|
@ -1,8 +1,13 @@
|
|||
/**
|
||||
MaxRes (weighted) max-sat algorithm by Nina and Bacchus, AAAI 2014.
|
||||
|
||||
*/
|
||||
|
||||
#include "solver.h"
|
||||
#include "maxsmt.h"
|
||||
#include "maxres.h"
|
||||
#include "ast_pp.h"
|
||||
|
||||
#include "mus.h"
|
||||
|
||||
using namespace opt;
|
||||
|
||||
|
|
@ -12,14 +17,16 @@ struct maxres::imp {
|
|||
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;
|
||||
|
||||
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_soft_constraints(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)
|
||||
{
|
||||
}
|
||||
|
|
@ -32,20 +39,25 @@ struct maxres::imp {
|
|||
|
||||
void add_soft(expr* e) {
|
||||
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);
|
||||
if (is_literal(e)) {
|
||||
m_asms.push_back(e);
|
||||
}
|
||||
else {
|
||||
expr_ref asum(m), fml(m);
|
||||
asum = m.mk_fresh_const("soft", m.mk_bool_sort());
|
||||
fml = m.mk_implies(asum, e);
|
||||
fml = m.mk_iff(asum, e);
|
||||
s.assert_expr(fml);
|
||||
m_asms.push_back(asum);
|
||||
}
|
||||
m_asm2cls.insert(m_asms.back(), cls.get());
|
||||
}
|
||||
|
||||
lbool operator()() {
|
||||
expr_ref fml(m);
|
||||
ptr_vector<expr> core, new_core;
|
||||
solver::scoped_push _sc(s);
|
||||
for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
|
||||
add_soft(m_soft_constraints[i].get());
|
||||
|
|
@ -69,12 +81,37 @@ struct maxres::imp {
|
|||
case l_undef:
|
||||
return l_undef;
|
||||
default:
|
||||
ptr_vector<expr> core;
|
||||
core.reset();
|
||||
s.get_unsat_core(core);
|
||||
TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr()););
|
||||
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
|
||||
TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr()););
|
||||
max_resolve(core);
|
||||
fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr()));
|
||||
s.assert_expr(fml);
|
||||
|
|
@ -96,6 +133,7 @@ struct maxres::imp {
|
|||
void max_resolve(ptr_vector<expr>& core) {
|
||||
SASSERT(!core.empty());
|
||||
expr_ref fml(m), asum(m);
|
||||
app_ref cls(m);
|
||||
m_B.reset();
|
||||
m_D.reset();
|
||||
m_D.resize(core.size());
|
||||
|
|
@ -115,17 +153,55 @@ struct maxres::imp {
|
|||
m_D[i] = m.mk_implies(b_i1, d_i1);
|
||||
expr* d_i = m_D[i].get();
|
||||
asum = m.mk_fresh_const("a", m.mk_bool_sort());
|
||||
fml = m.mk_implies(asum, m.mk_implies(d_i, b_i));
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
||||
app_ref mk_cls(expr* e) {
|
||||
expr_ref_vector disj(m), todo(m);
|
||||
expr_ref f(m);
|
||||
app_ref result(m);
|
||||
expr* e1, *e2;
|
||||
todo.push_back(e);
|
||||
while (!todo.empty()) {
|
||||
f = todo.back();
|
||||
todo.pop_back();
|
||||
if (m.is_implies(f, e1, e2)) {
|
||||
todo.push_back(m.mk_not(e1));
|
||||
todo.push_back(e2);
|
||||
}
|
||||
else if (m.is_not(f, e1) && m.is_not(e1, e2)) {
|
||||
todo.push_back(e2);
|
||||
}
|
||||
else if (m.is_or(f)) {
|
||||
todo.append(to_app(f)->get_num_args(), to_app(f)->get_args());
|
||||
}
|
||||
else if (m.is_not(f, e1) && m.is_and(e1)) {
|
||||
for (unsigned i = 0; i < to_app(e1)->get_num_args(); ++i) {
|
||||
todo.push_back(m.mk_not(to_app(e1)->get_arg(i)));
|
||||
}
|
||||
}
|
||||
else {
|
||||
disj.push_back(f);
|
||||
}
|
||||
}
|
||||
result = m.mk_or(disj.size(), disj.c_ptr());
|
||||
return result;
|
||||
}
|
||||
|
||||
void remove_core(ptr_vector<expr> const& core) {
|
||||
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;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
203
src/opt/mus.cpp
Normal file
203
src/opt/mus.cpp
Normal file
|
|
@ -0,0 +1,203 @@
|
|||
#include "solver.h"
|
||||
#include "smt_literal.h"
|
||||
#include "mus.h"
|
||||
#include "ast_pp.h"
|
||||
|
||||
using namespace opt;
|
||||
|
||||
// Faster MUS extraction based on Belov et.al. HYB (Algorithm 3, 4)
|
||||
|
||||
|
||||
struct mus::imp {
|
||||
solver& s;
|
||||
ast_manager& m;
|
||||
expr_ref_vector m_cls2expr;
|
||||
obj_map<expr, unsigned> m_expr2cls;
|
||||
vector<smt::literal_vector> m_cls2lits;
|
||||
expr_ref_vector m_vars;
|
||||
obj_map<expr, unsigned> m_var2idx;
|
||||
|
||||
public:
|
||||
imp(solver& s, ast_manager& m): s(s), m(m), m_cls2expr(m), m_vars(m) {}
|
||||
|
||||
unsigned add_var(expr* v) {
|
||||
unsigned idx = m_vars.size();
|
||||
if (!m_var2idx.find(v, idx)) {
|
||||
m_var2idx.insert(v, idx);
|
||||
m_vars.push_back(v);
|
||||
}
|
||||
return idx;
|
||||
}
|
||||
|
||||
unsigned add_soft(expr* cls, unsigned sz, expr* const* args) {
|
||||
TRACE("opt", tout << sz << ": " << mk_pp(cls, m) << "\n";);
|
||||
smt::literal_vector lits;
|
||||
expr* arg;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (m.is_not(args[i], arg)) {
|
||||
lits.push_back(smt::literal(add_var(arg), true));
|
||||
}
|
||||
else {
|
||||
lits.push_back(smt::literal(add_var(args[i]), false));
|
||||
}
|
||||
}
|
||||
unsigned idx = m_cls2lits.size();
|
||||
m_expr2cls.insert(cls, idx);
|
||||
m_cls2expr.push_back(cls);
|
||||
m_cls2lits.push_back(lits);
|
||||
return idx;
|
||||
}
|
||||
|
||||
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);
|
||||
}
|
||||
mus.reset();
|
||||
expr_ref_vector assumptions(m);
|
||||
svector<bool> model;
|
||||
ptr_vector<expr> core_exprs;
|
||||
model.resize(m_vars.size());
|
||||
while (!core.empty()) {
|
||||
IF_VERBOSE(0, display_vec(tout << "core: ", core););
|
||||
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);
|
||||
unsigned sz = assumptions.size();
|
||||
assumptions.push_back(not_cls);
|
||||
add_core(core, assumptions);
|
||||
lbool is_sat = s.check_sat(assumptions.size(), assumptions.c_ptr());
|
||||
assumptions.resize(sz);
|
||||
switch(is_sat) {
|
||||
case l_undef:
|
||||
return is_sat;
|
||||
case l_true:
|
||||
assumptions.push_back(cls);
|
||||
mus.push_back(cls_id);
|
||||
extract_model(s, model);
|
||||
sz = core.size();
|
||||
core.append(mus);
|
||||
rmr(core, mus, model);
|
||||
core.resize(sz);
|
||||
break;
|
||||
default:
|
||||
core_exprs.reset();
|
||||
s.get_unsat_core(core_exprs);
|
||||
if (!core_exprs.contains(not_cls)) {
|
||||
// core := core_exprs \ mus
|
||||
core.reset();
|
||||
for (unsigned i = 0; i < core_exprs.size(); ++i) {
|
||||
cls = core_exprs[i];
|
||||
cls_id = m_expr2cls.find(cls);
|
||||
if (!mus.contains(cls_id)) {
|
||||
core.push_back(cls_id);
|
||||
}
|
||||
}
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
return l_true;
|
||||
}
|
||||
|
||||
void add_core(unsigned_vector const& core, expr_ref_vector& assumptions) {
|
||||
for (unsigned i = 0; i < core.size(); ++i) {
|
||||
assumptions.push_back(m_cls2expr[core[i]].get());
|
||||
}
|
||||
}
|
||||
|
||||
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 << "\n";
|
||||
}
|
||||
|
||||
void extract_model(solver& s, svector<bool>& model) {
|
||||
model_ref mdl;
|
||||
s.get_model(mdl);
|
||||
for (unsigned i = 0; i < m_vars.size(); ++i) {
|
||||
expr_ref tmp(m);
|
||||
mdl->eval(m_vars[i].get(), tmp);
|
||||
model[i] = m.is_true(tmp);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
Recursive model rotation.
|
||||
*/
|
||||
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););
|
||||
|
||||
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);
|
||||
rmr(M, mus, model);
|
||||
}
|
||||
model[lit.var()] = !model[lit.var()]; // swap assignment back
|
||||
}
|
||||
}
|
||||
|
||||
bool has_single_unsat(svector<bool> const& model, unsigned& cls_id) const {
|
||||
cls_id = UINT_MAX;
|
||||
for (unsigned i = 0; i < m_cls2lits.size(); ++i) {
|
||||
if (!eval(model, m_cls2lits[i])) {
|
||||
if (cls_id == UINT_MAX) {
|
||||
cls_id = i;
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
return cls_id != UINT_MAX;
|
||||
}
|
||||
|
||||
bool eval(svector<bool> const& model, smt::literal_vector const& cls) const {
|
||||
for (unsigned i = 0; i < cls.size(); ++i) {
|
||||
if (model[cls[i].var()] != cls[i].sign()) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
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) {
|
||||
m_imp = alloc(imp, s, m);
|
||||
}
|
||||
|
||||
mus::~mus() {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
||||
unsigned mus::add_soft(expr* cls, unsigned sz, expr* const* args) {
|
||||
return m_imp->add_soft(cls, sz, args);
|
||||
}
|
||||
|
||||
lbool mus::get_mus(unsigned_vector& mus) {
|
||||
return m_imp->get_mus(mus);
|
||||
}
|
||||
|
||||
21
src/opt/mus.h
Normal file
21
src/opt/mus.h
Normal file
|
|
@ -0,0 +1,21 @@
|
|||
|
||||
namespace opt {
|
||||
class mus {
|
||||
struct imp;
|
||||
imp * m_imp;
|
||||
public:
|
||||
mus(solver& s, ast_manager& m);
|
||||
~mus();
|
||||
/**
|
||||
Add soft constraint.
|
||||
|
||||
Assume that the solver context enforces that
|
||||
cls is equivalent to a disjunction of args.
|
||||
Assume also that cls is a literal.
|
||||
*/
|
||||
unsigned add_soft(expr* cls, unsigned sz, expr* const* args);
|
||||
|
||||
lbool get_mus(unsigned_vector& mus);
|
||||
};
|
||||
|
||||
};
|
||||
Loading…
Reference in a new issue