mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
disjoint cores
This commit is contained in:
TheRealNebus
parent
3a7efb91ae
commit
e5aa79ba6a
|
|
@ -11,45 +11,85 @@ class mss_solver: public maxsmt_solver_base {
|
|||
|
||||
private:
|
||||
typedef ptr_vector<expr> exprs;
|
||||
typedef obj_hashtable<expr> expr_set;
|
||||
mss m_mss;
|
||||
unsigned m_index;
|
||||
expr_ref_vector m_asms;
|
||||
exprs m_asms;
|
||||
unsigned m_mss_found;
|
||||
vector<exprs> m_cores;
|
||||
unsigned m_core_idx;
|
||||
model_ref m_last_model;
|
||||
exprs m_mss_trail;
|
||||
exprs m_mcs_trail;
|
||||
unsigned_vector m_mss_trail_lim;
|
||||
unsigned_vector m_mcs_trail_lim;
|
||||
unsigned m_max_mss;
|
||||
bool m_disjoint_cores;
|
||||
|
||||
public:
|
||||
mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft):
|
||||
maxsmt_solver_base(c, ws, soft),
|
||||
m_mss(c.get_solver(), m),
|
||||
m_index(id),
|
||||
m_asms(m),
|
||||
m_max_mss(UINT_MAX) {
|
||||
m_mss_found(0),
|
||||
m_core_idx(0),
|
||||
m_max_mss(UINT_MAX),
|
||||
m_disjoint_cores(false) {
|
||||
}
|
||||
|
||||
virtual ~mss_solver() {}
|
||||
|
||||
virtual lbool operator()() {
|
||||
if (!init()) return l_undef;
|
||||
init_asms();
|
||||
lbool is_sat = check_sat(m_asms);
|
||||
if (is_sat == l_undef) return l_undef;
|
||||
if (is_sat == l_true) {
|
||||
IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << m_asms.size() << " :mcs " << 0 << ")\n";);
|
||||
model_ref mdl;
|
||||
s().get_model(mdl);
|
||||
update_assignment(mdl.get());
|
||||
return l_true;
|
||||
init_local();
|
||||
lbool is_sat = disjoint_cores();
|
||||
if (is_sat != l_true) return is_sat;
|
||||
if (m_cores.size() == 0) return l_true;
|
||||
update_model();
|
||||
exprs asms;
|
||||
while (true) {
|
||||
exprs mss, mcs;
|
||||
mss.append(m_cores[m_core_idx]);
|
||||
is_sat = cld(m_last_model, mss, mcs);
|
||||
if (is_sat == l_undef || m.canceled()) return l_undef;
|
||||
SASSERT(is_sat == l_true);
|
||||
update_trails(mss, mcs);
|
||||
if (m_core_idx < m_cores.size()-1) {
|
||||
m_core_idx++;
|
||||
}
|
||||
else {
|
||||
IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << m_mss_trail.size() + m_asms.size() << " :mcs " << m_mcs_trail.size() << ")\n";);
|
||||
if (++m_mss_found >= m_max_mss) return l_true;
|
||||
asms.push_back(relax_and_assert(m.mk_or(m_mcs_trail.size(), m_mcs_trail.c_ptr())));
|
||||
is_sat = backtrack(asms);
|
||||
if (is_sat == l_false) {
|
||||
SASSERT(m_core_idx == 0);
|
||||
is_sat = disjoint_cores(asms);
|
||||
}
|
||||
if (is_sat == l_undef) return l_undef;
|
||||
if (is_sat == l_false) return l_true;
|
||||
}
|
||||
}
|
||||
return enumerate_mss();
|
||||
return l_true;
|
||||
}
|
||||
|
||||
virtual void updt_params(params_ref& p) {
|
||||
maxsmt_solver_base::updt_params(p);
|
||||
opt_params _p(p);
|
||||
m_max_mss = _p.mss_max();
|
||||
m_disjoint_cores = _p.mss_disjoint_cores();
|
||||
}
|
||||
|
||||
private:
|
||||
void init_asms() {
|
||||
void init_local() {
|
||||
m_cores.reset();
|
||||
m_core_idx = 0;
|
||||
m_mss_found = 0;
|
||||
m_last_model.reset();
|
||||
m_mss_trail.reset();
|
||||
m_mcs_trail.reset();
|
||||
m_mss_trail_lim.reset();
|
||||
m_mcs_trail_lim.reset();
|
||||
m_asms.reset();
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
expr* e = m_soft[i];
|
||||
|
|
@ -74,42 +114,84 @@ private:
|
|||
return is_uninterp_const(l) || (m.is_not(l, l) && is_uninterp_const(l));
|
||||
}
|
||||
|
||||
lbool enumerate_mss() {
|
||||
expr_ref_vector asms(m);
|
||||
for (unsigned i = 0; i < m_max_mss; ++i) {
|
||||
exprs mss, mcs;
|
||||
lbool is_sat = next_mss(asms, mss, mcs);
|
||||
if (is_sat == l_false && i == 0) return l_false;
|
||||
if (is_sat == l_undef && i == 0) return l_undef;
|
||||
if (is_sat == l_false || is_sat == l_undef) return l_true;
|
||||
asms.push_back(relax_and_assert(m.mk_or(mcs.size(), mcs.c_ptr())));
|
||||
lbool disjoint_cores(exprs const& asms) {
|
||||
expr_set asm_lits, core_lits;
|
||||
for (unsigned i = 0; i < asms.size(); ++i) {
|
||||
asm_lits.insert(asms[i]);
|
||||
}
|
||||
return l_true;
|
||||
lbool is_sat = l_false;
|
||||
exprs core;
|
||||
while (is_sat == l_false) {
|
||||
exprs tmp_asms;
|
||||
tmp_asms.append(asms);
|
||||
tmp_asms.append(m_asms);
|
||||
is_sat = check_sat(tmp_asms);
|
||||
if (is_sat == l_true) {
|
||||
update_model();
|
||||
}
|
||||
else if (is_sat == l_false) {
|
||||
core.reset();
|
||||
s().get_unsat_core(core);
|
||||
for (unsigned i = 0; i < core.size();) {
|
||||
if (asm_lits.contains(core[i])) {
|
||||
core[i] = core.back();
|
||||
core.pop_back();
|
||||
}
|
||||
else {
|
||||
core_lits.insert(core[i]);
|
||||
++i;
|
||||
}
|
||||
}
|
||||
if (core.empty()) {
|
||||
IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver empty core)\n";);
|
||||
return l_false;
|
||||
}
|
||||
if (m_disjoint_cores) {
|
||||
m_cores.push_back(core);
|
||||
IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :core-size " << core.size() << " :num-cores " << m_cores.size() << ")\n";);
|
||||
for (unsigned i = 0; i < m_asms.size();) {
|
||||
if (core_lits.contains(m_asms[i]) || !m_disjoint_cores) {
|
||||
m_asms[i] = m_asms.back();
|
||||
m_asms.pop_back();
|
||||
}
|
||||
else {
|
||||
++i;
|
||||
}
|
||||
}
|
||||
}
|
||||
else {
|
||||
m_cores.push_back(m_asms);
|
||||
m_asms.reset();
|
||||
}
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :num-cores " << m_cores.size() << ")\n";);
|
||||
// TODO: update m_lower?
|
||||
return is_sat;
|
||||
}
|
||||
|
||||
lbool next_mss(expr_ref_vector const& asms, exprs& mss, exprs& mcs) {
|
||||
mss.reset();
|
||||
mcs.reset();
|
||||
lbool is_sat = check_sat(asms);
|
||||
if (is_sat != l_true) return is_sat;
|
||||
model_ref mdl;
|
||||
s().get_model(mdl);
|
||||
update_assignment(mdl.get());
|
||||
vector<exprs> dummy;
|
||||
push_exprs(mss, m_asms);
|
||||
push_exprs(mss, asms);
|
||||
is_sat = cld(mdl.get(), mss, mcs);
|
||||
if (is_sat == l_true) {
|
||||
IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";);
|
||||
lbool disjoint_cores() {
|
||||
return disjoint_cores(exprs());
|
||||
}
|
||||
|
||||
lbool backtrack(exprs& asms) {
|
||||
SASSERT(m_mss_trail_lim.size() == m_mcs_trail_lim.size());
|
||||
lbool is_sat = l_false;
|
||||
while (is_sat == l_false && m_core_idx > 0) {
|
||||
m_core_idx--;
|
||||
m_mss_trail.resize(m_mss_trail_lim.back());
|
||||
m_mss_trail_lim.pop_back();
|
||||
m_mcs_trail.resize(m_mcs_trail_lim.back());
|
||||
m_mcs_trail_lim.pop_back();
|
||||
exprs tmp_asms;
|
||||
tmp_asms.append(asms);
|
||||
get_trail_asms(tmp_asms);
|
||||
is_sat = check_sat(tmp_asms);
|
||||
if (is_sat == l_true) {
|
||||
update_model();
|
||||
}
|
||||
}
|
||||
/*is_sat = m_mss(mdl.get(), dummy, mss, mcs);
|
||||
SASSERT(is_sat != l_false);
|
||||
if (is_sat == l_true) {
|
||||
mdl.reset();
|
||||
m_mss.get_model(mdl);
|
||||
update_assignment(mdl.get());
|
||||
IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";);
|
||||
}*/
|
||||
IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :backtrack-lvl " << m_core_idx << ")\n";);
|
||||
return is_sat;
|
||||
}
|
||||
|
||||
|
|
@ -118,19 +200,19 @@ private:
|
|||
undef.append(mss);
|
||||
update_sat(initial_model, sat, undef);
|
||||
lbool is_sat = l_true;
|
||||
while (is_sat == l_true) {
|
||||
while (is_sat == l_true && !undef.empty()) {
|
||||
expr_ref asum = relax_and_assert(m.mk_or(undef.size(), undef.c_ptr()));
|
||||
sat.push_back(asum);
|
||||
is_sat = check_sat(sat);
|
||||
sat.pop_back();
|
||||
exprs asms;
|
||||
asms.append(sat);
|
||||
get_trail_asms(asms);
|
||||
asms.push_back(asum);
|
||||
is_sat = check_sat(asms);
|
||||
if (is_sat == l_true) {
|
||||
model_ref mdl;
|
||||
s().get_model(mdl);
|
||||
update_sat(mdl, sat, undef);
|
||||
update_assignment(mdl.get());
|
||||
update_model();
|
||||
update_sat(m_last_model, sat, undef);
|
||||
}
|
||||
}
|
||||
if (is_sat == l_false) {
|
||||
if (is_sat == l_false || undef.empty()) {
|
||||
mss.reset();
|
||||
mcs.reset();
|
||||
mss.append(sat);
|
||||
|
|
@ -140,6 +222,26 @@ private:
|
|||
return is_sat;
|
||||
}
|
||||
|
||||
void get_trail_asms(exprs& asms) {
|
||||
asms.append(m_mss_trail);
|
||||
for (unsigned i = 0; i < m_mcs_trail.size(); ++i) {
|
||||
asms.push_back(m.mk_not(m_mcs_trail[i]));
|
||||
}
|
||||
}
|
||||
|
||||
void update_trails(exprs const& mss, exprs const& mcs) {
|
||||
m_mss_trail_lim.push_back(m_mss_trail.size());
|
||||
m_mcs_trail_lim.push_back(m_mcs_trail.size());
|
||||
m_mss_trail.append(mss);
|
||||
m_mcs_trail.append(mcs);
|
||||
}
|
||||
|
||||
void update_model() {
|
||||
m_last_model.reset();
|
||||
s().get_model(m_last_model);
|
||||
update_assignment(m_last_model.get());
|
||||
}
|
||||
|
||||
void update_sat(model_ref mdl, exprs& sat, exprs& undef) {
|
||||
for (unsigned i = 0; i < undef.size();) {
|
||||
if (is_true(mdl.get(), undef[i])) {
|
||||
|
|
@ -160,12 +262,7 @@ private:
|
|||
}
|
||||
|
||||
lbool check_sat() {
|
||||
expr_ref_vector dummy(m);
|
||||
return check_sat(dummy);
|
||||
}
|
||||
|
||||
lbool check_sat(expr_ref_vector const& asms) {
|
||||
return s().check_sat(asms);
|
||||
return check_sat(exprs());
|
||||
}
|
||||
|
||||
lbool check_sat(exprs const& asms) {
|
||||
|
|
@ -186,7 +283,7 @@ private:
|
|||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
m_assignment[i] = is_true(m_soft[i]);
|
||||
}
|
||||
// TODO: DEBUG verify assignment
|
||||
// TODO: DEBUG verify assignment?
|
||||
m_upper = upper;
|
||||
trace_bounds("mss-solver");
|
||||
}
|
||||
|
|
|
|||
|
|
@ -21,7 +21,8 @@ def_module_params('opt',
|
|||
('maxres.max_correction_set_size', UINT, 3, 'allow generating correction set constraints up to maximal size'),
|
||||
('maxres.wmax', BOOL, False, 'use weighted theory solver to constrain upper bounds'),
|
||||
('maxres.pivot_on_correction_set', BOOL, True, 'reduce soft constraints if the current correction set is smaller than current core'),
|
||||
('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate')
|
||||
('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate'),
|
||||
('mss.disjoint_cores', BOOL, True, 'partition soft based on disjoint cores')
|
||||
))
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue