mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

Revert "implemented CLD"

Browse source 
This reverts commit 3a7efb91ae.
This commit is contained in:
TheRealNebus 2018-04-26 22:39:58 +01:00
parent bf2a031f7b
commit 7e8ed0762d
2 changed files with 12 additions and 62 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/opt/mss.cpp
View file

@ -155,10 +155,10 @@ namespace opt {
lbool is_sat = l_true; lbool is_sat = l_true;
for (unsigned i = 0; is_sat == l_true && i < m_cores.size(); ++i) { for (unsigned i = 0; is_sat == l_true && i < m_cores.size(); ++i) {
bool has_mcs = false; bool has_mcs = false;
bool not_last = i + 1 < m_cores.size(); bool is_last = i + 1 < m_cores.size();
SASSERT(check_invariant()); SASSERT(check_invariant());
update_core(m_cores[i]); // remove members of mss update_core(m_cores[i]); // remove members of mss
is_sat = process_core(1, m_cores[i], has_mcs, not_last); is_sat = process_core(1, m_cores[i], has_mcs, is_last);
} }
if (is_sat == l_true) { if (is_sat == l_true) {
SASSERT(check_invariant()); SASSERT(check_invariant());
@ -183,7 +183,7 @@ namespace opt {
// at least one literal in core is false in current model. // at least one literal in core is false in current model.
// pick literals in core that are not yet in mss. // pick literals in core that are not yet in mss.
// //
lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool not_last) { lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last) {
SASSERT(sz > 0); SASSERT(sz > 0);
if (core.empty()) { if (core.empty()) {
return l_true; return l_true;
@ -191,7 +191,7 @@ namespace opt {
if (m.canceled()) { if (m.canceled()) {
return l_undef; return l_undef;
} }
if (sz == 1 && core.size() == 1 && not_last && !has_mcs) { if (sz == 1 && core.size() == 1 && is_last && !has_mcs) {
// there has to be at least one false // there has to be at least one false
// literal in the core. // literal in the core.
TRACE("opt", tout << "mcs: " << mk_pp(core[0], m) << "\n";); TRACE("opt", tout << "mcs: " << mk_pp(core[0], m) << "\n";);
@ -214,7 +214,7 @@ namespace opt {
SASSERT(m_mss_set.contains(core[i])); SASSERT(m_mss_set.contains(core[i]));
}); });
update_core(core); update_core(core);
return process_core(2*sz, core, has_mcs, not_last); return process_core(2*sz, core, has_mcs, is_last);
case l_false: case l_false:
if (sz == 1) { if (sz == 1) {
has_mcs = true; has_mcs = true;
@ -232,7 +232,7 @@ namespace opt {
} }
update_core(core); update_core(core);
} }
return process_core(1, core, has_mcs, not_last); return process_core(1, core, has_mcs, is_last);
case l_undef: case l_undef:
return l_undef; return l_undef;
} }

62
src/opt/mss_solver.cpp
View file

@ -98,61 +98,15 @@ private:
vector<exprs> dummy; vector<exprs> dummy;
push_exprs(mss, m_asms); push_exprs(mss, m_asms);
push_exprs(mss, asms); push_exprs(mss, asms);
is_sat = cld(mdl.get(), mss, mcs); is_sat = m_mss(mdl.get(), dummy, mss, mcs);
if (is_sat == l_true) { SASSERT(is_sat == l_true);
IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); mdl.reset();
} m_mss.get_model(mdl);
/*is_sat = m_mss(mdl.get(), dummy, mss, mcs); update_assignment(mdl.get());
SASSERT(is_sat != l_false); IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";);
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; return is_sat;
} }
lbool cld(model_ref initial_model, exprs& mss, exprs& mcs) {
exprs sat, undef;
undef.append(mss);
update_sat(initial_model, sat, undef);
lbool is_sat = l_true;
while (is_sat == l_true) {
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();
if (is_sat == l_true) {
model_ref mdl;
s().get_model(mdl);
update_sat(mdl, sat, undef);
update_assignment(mdl.get());
}
}
if (is_sat == l_false) {
mss.reset();
mcs.reset();
mss.append(sat);
mcs.append(undef);
is_sat = l_true;
}
return is_sat;
}
void update_sat(model_ref mdl, exprs& sat, exprs& undef) {
for (unsigned i = 0; i < undef.size();) {
if (is_true(mdl.get(), undef[i])) {
sat.push_back(undef[i]);
undef[i] = undef.back();
undef.pop_back();
}
else {
++i;
}
}
}
void push_exprs(exprs& dst, expr_ref_vector const& src) { void push_exprs(exprs& dst, expr_ref_vector const& src) {
for (unsigned i = 0; i < src.size(); ++i) { for (unsigned i = 0; i < src.size(); ++i) {
dst.push_back(src[i]); dst.push_back(src[i]);
@ -168,10 +122,6 @@ private:
return s().check_sat(asms); return s().check_sat(asms);
} }
lbool check_sat(exprs const& asms) {
return s().check_sat(asms.size(), asms.c_ptr());
}
void update_assignment(model* mdl) { void update_assignment(model* mdl) {
rational upper(0); rational upper(0);
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {