mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 09:05:31 +00:00
testing maxres with sat core
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
b928734348
commit
8814ba0629
12 changed files with 187 additions and 298 deletions
|
|
@ -321,9 +321,12 @@ public:
|
|||
}
|
||||
|
||||
lbool minimize_core(ptr_vector<expr>& core) {
|
||||
if (m_sat_enabled) {
|
||||
return l_true;
|
||||
}
|
||||
m_mus.reset();
|
||||
for (unsigned i = 0; i < core.size(); ++i) {
|
||||
m_mus.add_soft(core[i], 1, core.c_ptr() + i);
|
||||
m_mus.add_soft(core[i]);
|
||||
}
|
||||
unsigned_vector mus_idx;
|
||||
lbool is_sat = m_mus.get_mus(mus_idx);
|
||||
|
|
|
|||
|
|
@ -27,16 +27,9 @@ using namespace opt;
|
|||
|
||||
|
||||
class maxres : public maxsmt_solver_base {
|
||||
struct info {
|
||||
app* m_cls;
|
||||
rational m_weight;
|
||||
info(app* cls, rational const& w):
|
||||
m_cls(cls), m_weight(w) {}
|
||||
info(): m_cls(0) {}
|
||||
};
|
||||
expr_ref_vector m_B;
|
||||
expr_ref_vector m_asms;
|
||||
obj_map<expr, info> m_asm2info;
|
||||
obj_map<expr, rational> m_asm2weight;
|
||||
ptr_vector<expr> m_new_core;
|
||||
mus m_mus;
|
||||
expr_ref_vector m_trail;
|
||||
|
|
@ -63,14 +56,12 @@ public:
|
|||
TRACE("opt", tout << mk_pp(e, m) << "\n";);
|
||||
expr_ref asum(m), fml(m);
|
||||
app_ref cls(m);
|
||||
info inf(0,rational(0));
|
||||
if (m_asm2info.find(e, inf)) {
|
||||
inf.m_weight += w;
|
||||
m_asm2info.insert(e, inf);
|
||||
rational weight(0);
|
||||
if (m_asm2weight.find(e, weight)) {
|
||||
weight += w;
|
||||
m_asm2weight.insert(e, weight);
|
||||
return;
|
||||
}
|
||||
cls = mk_cls(e);
|
||||
m_trail.push_back(cls);
|
||||
if (is_literal(e)) {
|
||||
asum = e;
|
||||
}
|
||||
|
|
@ -79,21 +70,18 @@ public:
|
|||
fml = m.mk_iff(asum, e);
|
||||
m_s->assert_expr(fml);
|
||||
}
|
||||
new_assumption(asum, cls, w);
|
||||
new_assumption(asum, w);
|
||||
m_upper += w;
|
||||
}
|
||||
|
||||
void new_assumption(expr* e, app* cls, rational const& w) {
|
||||
void new_assumption(expr* e, rational const& w) {
|
||||
TRACE("opt", tout << "insert: " << mk_pp(e, m) << " : " << w << "\n";);
|
||||
info inf(cls, w);
|
||||
m_asm2info.insert(e, inf);
|
||||
m_asm2weight.insert(e, w);
|
||||
m_asms.push_back(e);
|
||||
m_trail.push_back(e);
|
||||
}
|
||||
|
||||
lbool operator()() {
|
||||
expr_ref fml(m);
|
||||
ptr_vector<expr> core;
|
||||
solver::scoped_push _sc(*m_s.get());
|
||||
init();
|
||||
init_local();
|
||||
|
|
@ -125,28 +113,13 @@ public:
|
|||
m_upper = m_lower;
|
||||
return l_true;
|
||||
}
|
||||
case l_false:
|
||||
is_sat = process_unsat();
|
||||
if (is_sat != l_true) return is_sat;
|
||||
break;
|
||||
case l_undef:
|
||||
return l_undef;
|
||||
default:
|
||||
core.reset();
|
||||
m_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 (is_sat != l_true) {
|
||||
return is_sat;
|
||||
}
|
||||
remove_core(core);
|
||||
rational w = split_core(core);
|
||||
TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr()););
|
||||
max_resolve(core, w);
|
||||
fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr()));
|
||||
m_s->assert_expr(fml);
|
||||
m_lower += w;
|
||||
break;
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.max_res [" << m_lower << ":" << m_upper << "])\n";);
|
||||
|
|
@ -154,13 +127,78 @@ public:
|
|||
return l_true;
|
||||
}
|
||||
|
||||
lbool get_cores(vector<ptr_vector<expr> >& cores) {
|
||||
// assume m_s is unsat.
|
||||
lbool is_sat = l_false;
|
||||
expr_ref_vector asms(m_asms);
|
||||
cores.reset();
|
||||
ptr_vector<expr> core;
|
||||
while (is_sat == l_false) {
|
||||
core.reset();
|
||||
m_s->get_unsat_core(core);
|
||||
is_sat = minimize_core(core);
|
||||
if (is_sat != l_true) {
|
||||
break;
|
||||
}
|
||||
cores.push_back(core);
|
||||
// TBD: ad hoc to avoid searching for large cores..
|
||||
if (core.size() >= 3) {
|
||||
break;
|
||||
}
|
||||
remove_soft(core, asms);
|
||||
TRACE("opt",
|
||||
display_vec(tout << "core: ", core.size(), core.c_ptr());
|
||||
display_vec(tout << "assumptions: ", asms.size(), asms.c_ptr()););
|
||||
is_sat = m_s->check_sat(asms.size(), asms.c_ptr());
|
||||
}
|
||||
TRACE("opt",
|
||||
tout << "num cores: " << cores.size() << "\n";
|
||||
for (unsigned i = 0; i < cores.size(); ++i) {
|
||||
for (unsigned j = 0; j < cores[i].size(); ++j) {
|
||||
tout << mk_pp(cores[i][j], m) << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
}
|
||||
tout << "num satisfying: " << asms.size() << "\n";);
|
||||
|
||||
return is_sat;
|
||||
}
|
||||
|
||||
|
||||
lbool process_unsat() {
|
||||
vector<ptr_vector<expr> > cores;
|
||||
lbool is_sat = get_cores(cores);
|
||||
if (is_sat != l_true) {
|
||||
return is_sat;
|
||||
}
|
||||
if (cores.empty()) {
|
||||
return l_false;
|
||||
}
|
||||
for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) {
|
||||
is_sat = process_unsat(cores[i]);
|
||||
}
|
||||
return is_sat;
|
||||
}
|
||||
|
||||
lbool process_unsat(ptr_vector<expr>& core) {
|
||||
expr_ref fml(m);
|
||||
remove_core(core);
|
||||
rational w = split_core(core);
|
||||
TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr()););
|
||||
max_resolve(core, w);
|
||||
fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr()));
|
||||
m_s->assert_expr(fml);
|
||||
m_lower += w;
|
||||
return l_true;
|
||||
}
|
||||
|
||||
lbool minimize_core(ptr_vector<expr>& core) {
|
||||
if (m_sat_enabled) {
|
||||
return l_true;
|
||||
}
|
||||
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());
|
||||
m_mus.add_soft(core[i]);
|
||||
}
|
||||
unsigned_vector mus_idx;
|
||||
lbool is_sat = m_mus.get_mus(mus_idx);
|
||||
|
|
@ -177,11 +215,7 @@ public:
|
|||
}
|
||||
|
||||
rational get_weight(expr* e) {
|
||||
return m_asm2info.find(e).m_weight;
|
||||
}
|
||||
|
||||
app* get_clause(expr* e) {
|
||||
return m_asm2info.find(e).m_cls;
|
||||
return m_asm2weight.find(e);
|
||||
}
|
||||
|
||||
rational split_core(ptr_vector<expr> const& core) {
|
||||
|
|
@ -200,7 +234,7 @@ public:
|
|||
rational w2 = get_weight(core[i]);
|
||||
if (w2 > w) {
|
||||
rational w3 = w2 - w;
|
||||
new_assumption(core[i], get_clause(core[i]), w3);
|
||||
new_assumption(core[i], w3);
|
||||
}
|
||||
}
|
||||
return w;
|
||||
|
|
@ -246,55 +280,25 @@ public:
|
|||
asum = mk_fresh_bool("a");
|
||||
cls = m.mk_or(b_i1, d);
|
||||
fml = m.mk_iff(asum, cls);
|
||||
cls = mk_cls(cls);
|
||||
m_trail.push_back(cls);
|
||||
new_assumption(asum, cls, w);
|
||||
new_assumption(asum, w);
|
||||
m_s->assert_expr(fml);
|
||||
}
|
||||
}
|
||||
|
||||
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_asms.pop_back();
|
||||
void remove_soft(ptr_vector<expr> const& core, expr_ref_vector& asms) {
|
||||
for (unsigned i = 0; i < asms.size(); ++i) {
|
||||
if (core.contains(asms[i].get())) {
|
||||
asms[i] = asms.back();
|
||||
asms.pop_back();
|
||||
--i;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void remove_core(ptr_vector<expr> const& core) {
|
||||
remove_soft(core, m_asms);
|
||||
}
|
||||
|
||||
virtual void set_cancel(bool f) {
|
||||
maxsmt_solver_base::set_cancel(f);
|
||||
m_mus.set_cancel(f);
|
||||
|
|
@ -303,7 +307,6 @@ public:
|
|||
void init_local() {
|
||||
m_upper.reset();
|
||||
m_lower.reset();
|
||||
m_asm2info.reset();
|
||||
m_trail.reset();
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
add_soft(m_soft[i].get(), m_weights[i]);
|
||||
|
|
|
|||
|
|
@ -130,6 +130,7 @@ namespace opt {
|
|||
}
|
||||
|
||||
void maxsmt_solver_base::enable_inc_bvsat() {
|
||||
m_params.set_bool("minimize_core", true);
|
||||
solver* sat_solver = mk_inc_sat_solver(m, m_params);
|
||||
unsigned sz = s().get_num_assertions();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
|
|
@ -138,25 +139,11 @@ namespace opt {
|
|||
m_s = sat_solver;
|
||||
}
|
||||
|
||||
void maxsmt_solver_base::enable_noninc_bvsat() {
|
||||
tactic_ref pb2bv = mk_card2bv_tactic(m, m_params);
|
||||
tactic_ref bv2sat = mk_qfbv_tactic(m, m_params);
|
||||
tactic_ref tac = and_then(pb2bv.get(), bv2sat.get());
|
||||
solver* sat_solver = mk_tactic2solver(m, tac.get(), m_params);
|
||||
unsigned sz = s().get_num_assertions();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
sat_solver->assert_expr(s().get_assertion(i));
|
||||
}
|
||||
unsigned lvl = m_s->get_scope_level();
|
||||
while (lvl > 0) { sat_solver->push(); --lvl; }
|
||||
m_s = sat_solver;
|
||||
}
|
||||
|
||||
|
||||
void maxsmt_solver_base::enable_bvsat() {
|
||||
if (m_enable_sat && !m_sat_enabled && probe_bv()) {
|
||||
enable_inc_bvsat();
|
||||
// enable_noninc_bvsat();
|
||||
m_sat_enabled = true;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -99,7 +99,6 @@ namespace opt {
|
|||
app* mk_fresh_bool(char const* name);
|
||||
private:
|
||||
void enable_inc_bvsat();
|
||||
void enable_noninc_bvsat();
|
||||
};
|
||||
|
||||
/**
|
||||
|
|
|
|||
133
src/opt/mus.cpp
133
src/opt/mus.cpp
|
|
@ -7,7 +7,7 @@ Module Name:
|
|||
|
||||
Abstract:
|
||||
|
||||
Faster MUS extraction based on Belov et.al. HYB (Algorithm 3, 4)
|
||||
MUS extraction.
|
||||
|
||||
Author:
|
||||
|
||||
|
|
@ -35,58 +35,28 @@ struct mus::imp {
|
|||
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;
|
||||
volatile bool m_cancel;
|
||||
bool m_rmr_enabled;
|
||||
|
||||
imp(ref<solver>& s, ast_manager& m):
|
||||
m_s(s), m(m), m_cls2expr(m), m_vars(m), m_cancel(false),
|
||||
m_rmr_enabled(false) {}
|
||||
m_s(s), m(m), m_cls2expr(m), m_cancel(false)
|
||||
{}
|
||||
|
||||
void reset() {
|
||||
m_cls2expr.reset();
|
||||
m_expr2cls.reset();
|
||||
m_cls2lits.reset();
|
||||
m_vars.reset();
|
||||
m_var2idx.reset();
|
||||
m_vars.push_back(m.mk_true());
|
||||
}
|
||||
|
||||
void set_cancel(bool f) {
|
||||
m_cancel = f;
|
||||
}
|
||||
|
||||
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) {
|
||||
unsigned add_soft(expr* cls) {
|
||||
SASSERT(is_uninterp_const(cls) || m.is_not(cls) && is_uninterp_const(to_app(cls)->get_arg(0)));
|
||||
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();
|
||||
unsigned idx = m_cls2expr.size();
|
||||
m_expr2cls.insert(cls, idx);
|
||||
m_cls2expr.push_back(cls);
|
||||
m_cls2lits.push_back(lits);
|
||||
TRACE("opt",
|
||||
tout << idx << ": " << mk_pp(cls, m) << "\n";
|
||||
display_vec(tout, lits);
|
||||
);
|
||||
TRACE("opt", tout << idx << ": " << mk_pp(cls, m) << "\n";);
|
||||
return idx;
|
||||
}
|
||||
|
||||
|
|
@ -99,11 +69,6 @@ struct mus::imp {
|
|||
|
||||
lbool get_mus(unsigned_vector& mus) {
|
||||
// SASSERT: mus does not have duplicates.
|
||||
TRACE("opt",
|
||||
for (unsigned i = 0; i < m_cls2lits.size(); ++i) {
|
||||
display_vec(tout, m_cls2lits[i]);
|
||||
}
|
||||
);
|
||||
unsigned_vector core;
|
||||
for (unsigned i = 0; i < m_cls2expr.size(); ++i) {
|
||||
core.push_back(i);
|
||||
|
|
@ -114,16 +79,13 @@ struct mus::imp {
|
|||
}
|
||||
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(1, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";);
|
||||
unsigned cls_id = core.back();
|
||||
TRACE("opt",
|
||||
display_vec(tout << "core: ", core);
|
||||
display_vec(tout << "mus: ", mus);
|
||||
// display_vec(tout << "model: ", model);
|
||||
);
|
||||
core.pop_back();
|
||||
expr* cls = m_cls2expr[cls_id].get();
|
||||
|
|
@ -140,13 +102,6 @@ struct mus::imp {
|
|||
case l_true:
|
||||
assumptions.push_back(cls);
|
||||
mus.push_back(cls_id);
|
||||
if (m_rmr_enabled) {
|
||||
extract_model(model);
|
||||
sz = core.size();
|
||||
core.append(mus);
|
||||
rmr(core, mus, model);
|
||||
core.resize(sz);
|
||||
}
|
||||
break;
|
||||
default:
|
||||
core_exprs.reset();
|
||||
|
|
@ -192,78 +147,6 @@ struct mus::imp {
|
|||
out << "\n";
|
||||
}
|
||||
|
||||
void extract_model(svector<bool>& model) {
|
||||
model_ref mdl;
|
||||
m_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);
|
||||
}
|
||||
TRACE("opt",
|
||||
display_vec(tout << "model: ", model);
|
||||
model_smt2_pp(tout, m, *mdl, 0);
|
||||
);
|
||||
|
||||
}
|
||||
|
||||
/**
|
||||
Recursive model rotation.
|
||||
*/
|
||||
void rmr(unsigned_vector& M, unsigned_vector& mus, svector<bool>& model) {
|
||||
TRACE("opt",
|
||||
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];
|
||||
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) &&
|
||||
!mus.contains(cls_id) &&
|
||||
model_check(model, cls_id)) {
|
||||
mus.push_back(cls_id);
|
||||
rmr(M, mus, model);
|
||||
}
|
||||
model[lit.var()] = !model[lit.var()]; // swap assignment back
|
||||
}
|
||||
}
|
||||
|
||||
bool model_check(svector<bool> const& model, unsigned cls_id) {
|
||||
// model has to work for hard constraints.
|
||||
return false;
|
||||
}
|
||||
|
||||
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;
|
||||
}
|
||||
}
|
||||
}
|
||||
TRACE("opt", display_vec(tout << "clause: " << cls_id << " model: ", model););
|
||||
return cls_id != UINT_MAX;
|
||||
}
|
||||
|
||||
bool eval(svector<bool> const& model, smt::literal_vector const& cls) const {
|
||||
bool result = false;
|
||||
for (unsigned i = 0; !result && i < cls.size(); ++i) {
|
||||
result = (model[cls[i].var()] != cls[i].sign());
|
||||
}
|
||||
TRACE("opt", display_vec(tout << "model: ", model);
|
||||
display_vec(tout << "clause: ", cls);
|
||||
tout << "result: " << result << "\n";);
|
||||
return result;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
mus::mus(ref<solver>& s, ast_manager& m) {
|
||||
|
|
@ -274,8 +157,8 @@ mus::~mus() {
|
|||
dealloc(m_imp);
|
||||
}
|
||||
|
||||
unsigned mus::add_soft(expr* cls, unsigned sz, expr* const* args) {
|
||||
return m_imp->add_soft(cls, sz, args);
|
||||
unsigned mus::add_soft(expr* cls) {
|
||||
return m_imp->add_soft(cls);
|
||||
}
|
||||
|
||||
lbool mus::get_mus(unsigned_vector& mus) {
|
||||
|
|
|
|||
|
|
@ -33,7 +33,7 @@ namespace opt {
|
|||
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);
|
||||
unsigned add_soft(expr* cls);
|
||||
|
||||
lbool get_mus(unsigned_vector& mus);
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue