3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00

Revert "disjoint cores"

This reverts commit e5aa79ba6a.
This commit is contained in:
TheRealNebus 2018-04-26 22:39:55 +01:00
parent 37852807b0
commit bf2a031f7b
2 changed files with 63 additions and 161 deletions

View file

@ -11,85 +11,45 @@ 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;
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;
expr_ref_vector m_asms;
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_mss_found(0),
m_core_idx(0),
m_max_mss(UINT_MAX),
m_disjoint_cores(false) {
m_asms(m),
m_max_mss(UINT_MAX) {
}
virtual ~mss_solver() {}
virtual lbool operator()() {
if (!init()) return l_undef;
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;
}
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;
}
return l_true;
return enumerate_mss();
}
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_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();
void init_asms() {
m_asms.reset();
for (unsigned i = 0; i < m_soft.size(); ++i) {
expr* e = m_soft[i];
@ -114,84 +74,42 @@ private:
return is_uninterp_const(l) || (m.is_not(l, l) && is_uninterp_const(l));
}
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]);
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 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;
return l_true;
}
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();
}
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";);
}
IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :backtrack-lvl " << m_core_idx << ")\n";);
/*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";);
}*/
return is_sat;
}
@ -200,19 +118,19 @@ private:
undef.append(mss);
update_sat(initial_model, sat, undef);
lbool is_sat = l_true;
while (is_sat == l_true && !undef.empty()) {
while (is_sat == l_true) {
expr_ref asum = relax_and_assert(m.mk_or(undef.size(), undef.c_ptr()));
exprs asms;
asms.append(sat);
get_trail_asms(asms);
asms.push_back(asum);
is_sat = check_sat(asms);
sat.push_back(asum);
is_sat = check_sat(sat);
sat.pop_back();
if (is_sat == l_true) {
update_model();
update_sat(m_last_model, sat, undef);
model_ref mdl;
s().get_model(mdl);
update_sat(mdl, sat, undef);
update_assignment(mdl.get());
}
}
if (is_sat == l_false || undef.empty()) {
if (is_sat == l_false) {
mss.reset();
mcs.reset();
mss.append(sat);
@ -222,26 +140,6 @@ 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])) {
@ -262,7 +160,12 @@ private:
}
lbool check_sat() {
return check_sat(exprs());
expr_ref_vector dummy(m);
return check_sat(dummy);
}
lbool check_sat(expr_ref_vector const& asms) {
return s().check_sat(asms);
}
lbool check_sat(exprs const& asms) {
@ -283,7 +186,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");
}

View file

@ -21,8 +21,7 @@ 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.disjoint_cores', BOOL, True, 'partition soft based on disjoint cores')
('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate')
))