mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

implemented CLD

Browse source
This commit is contained in:
TheRealNebus 2018-02-16 19:48:29 +00:00
parent 3bbc09c1d2
commit 3a7efb91ae
2 changed files with 62 additions and 12 deletions
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;
for (unsigned i = 0; is_sat == l_true && i < m_cores.size(); ++i) {
bool has_mcs = false;
bool is_last = i + 1 < m_cores.size();
bool not_last = i + 1 < m_cores.size();
SASSERT(check_invariant());
update_core(m_cores[i]); // remove members of mss
is_sat = process_core(1, m_cores[i], has_mcs, is_last);
is_sat = process_core(1, m_cores[i], has_mcs, not_last);
}
if (is_sat == l_true) {
SASSERT(check_invariant());
@ -183,7 +183,7 @@ namespace opt {
// at least one literal in core is false in current model.
// pick literals in core that are not yet in mss.
//
lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last) {
lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool not_last) {
SASSERT(sz > 0);
if (core.empty()) {
return l_true;
@ -191,7 +191,7 @@ namespace opt {
if (m.canceled()) {
return l_undef;
}
if (sz == 1 && core.size() == 1 && is_last && !has_mcs) {
if (sz == 1 && core.size() == 1 && not_last && !has_mcs) {
// there has to be at least one false
// literal in the core.
TRACE("opt", tout << "mcs: " << mk_pp(core[0], m) << "\n";);
@ -214,7 +214,7 @@ namespace opt {
SASSERT(m_mss_set.contains(core[i]));
});
update_core(core);
return process_core(2*sz, core, has_mcs, is_last);
return process_core(2*sz, core, has_mcs, not_last);
case l_false:
if (sz == 1) {
has_mcs = true;
@ -232,7 +232,7 @@ namespace opt {
}
update_core(core);
}
return process_core(1, core, has_mcs, is_last);
return process_core(1, core, has_mcs, not_last);
case l_undef:
return l_undef;
}

62
src/opt/mss_solver.cpp
View file

@ -98,15 +98,61 @@ private:
vector<exprs> dummy;
push_exprs(mss, m_asms);
push_exprs(mss, asms);
is_sat = m_mss(mdl.get(), dummy, mss, mcs);
SASSERT(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";);
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";);
}
/*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;
}
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) {
for (unsigned i = 0; i < src.size(); ++i) {
dst.push_back(src[i]);
@ -122,6 +168,10 @@ private:
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) {
rational upper(0);
for (unsigned i = 0; i < m_soft.size(); ++i) {