mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 06:13:40 +00:00
Code Activity

bug fixes in hsmax

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-06-15 05:44:03 -07:00
parent ef62a52fff
commit 63550d8a1a
3 changed files with 75 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

52
src/opt/hitting_sets.cpp
View file

@ -58,7 +58,10 @@ namespace opt {
m_cancel(false), m_cancel(false),
m_max_weight(0), m_max_weight(0),
m_weights_var(0), m_weights_var(0),
m_solver(m_params,0) {} m_solver(m_params,0) {
m_params.set_bool("elim_vars", false);
m_solver.updt_params(m_params);
}
~imp() {} ~imp() {}
void add_weight(rational const& w) { void add_weight(rational const& w) {
@ -245,6 +248,9 @@ namespace opt {
unsigned i = 0, j = 0; unsigned i = 0, j = 0;
set_undef_to_false(); set_undef_to_false();
if (values_satisfy_Ts(i)) { if (values_satisfy_Ts(i)) {
if (m_upper > m_max_weight) {
IF_VERBOSE(1, verbose_stream() << "(hs.bound_degradation " << m_upper << " )\n";);
}
return l_true; return l_true;
} }
@ -282,21 +288,44 @@ namespace opt {
} }
lbool compute_U2() { lbool compute_U2() {
lbool is_sat = m_solver.check(); lbool is_sat = l_true;
if (is_sat == l_true) { while (true) {
sat::model const& model = m_solver.get_model(); is_sat = m_solver.check();
m_value_saved.reset(); if (is_sat == l_true) {
m_upper.reset(); sat::model const& model = m_solver.get_model();
for (unsigned i = 0; i < m_vars.size(); ++i) { m_value_saved.reset();
m_value_saved.push_back(model[m_vars[i]]); m_upper.reset();
if (model[m_vars[i]] == l_true) { for (unsigned i = 0; i < m_vars.size(); ++i) {
m_upper += m_weights[i]; m_value_saved.push_back(model[m_vars[i]]);
if (model[m_vars[i]] == l_true) {
m_upper += m_weights[i];
}
} }
IF_VERBOSE(1, verbose_stream() << "(hs.upper " << m_upper << ")\n";);
m_solver.pop(m_solver.scope_lvl());
} }
break;
} }
return is_sat; return is_sat;
} }
bool block_model(sat::model const& model) {
rational value(0);
svector<sat::literal> lits;
for (unsigned i = 0; i < m_vars.size(); ++i) {
if (value >= m_max_weight) {
m_solver.mk_clause(lits.size(), lits.c_ptr());
return true;
}
if (model[m_vars[i]] == l_true) {
value += m_weights[i];
lits.push_back(sat::literal(m_vars[i], true));
}
}
return false;
}
// compute upper bound for hitting set. // compute upper bound for hitting set.
bool compute_U1() { bool compute_U1() {
rational w(0); rational w(0);
@ -329,9 +358,6 @@ namespace opt {
m_upper = w; m_upper = w;
m_value_saved.reset(); m_value_saved.reset();
m_value_saved.append(m_value); m_value_saved.append(m_value);
if (m_upper > m_max_weight) {
IF_VERBOSE(1, verbose_stream() << "(hs.bound_degradation " << m_upper << " )\n";);
}
return !m_cancel; return !m_cancel;
} }

2
src/opt/opt_solver.cpp
View file

@ -125,7 +125,7 @@ namespace opt {
} }
lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) { lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
TRACE("opt", { TRACE("opt_verbose", {
tout << "context size: " << m_context.size() << "\n"; tout << "context size: " << m_context.size() << "\n";
for (unsigned i = 0; i < m_context.size(); ++i) { for (unsigned i = 0; i < m_context.size(); ++i) {
tout << mk_pp(m_context.get_formulas()[i], m_context.m()) << "\n"; tout << mk_pp(m_context.get_formulas()[i], m_context.m()) << "\n";

57
src/opt/weighted_maxsat.cpp
View file

@ -928,30 +928,36 @@ namespace opt {
model_ref mdl; model_ref mdl;
s().get_model(mdl); s().get_model(mdl);
for (unsigned i = 0; i < num_soft(); ++i) { for (unsigned i = 0; i < num_soft(); ++i) {
if (!m_seed[i]) { ensure_active(i);
if (is_true(mdl, m_soft[i].get())) { m_seed[i] = false;
}
for (unsigned i = 0; i < m_asms.size(); ++i) {
m_seed[m_aux2index.find(m_asms[i])] = true;
}
for (unsigned i = 0; i < num_soft(); ++i) {
if (m_seed[i]) {
// already an assumption
}
else if (is_true(mdl, m_soft[i].get())) {
m_seed[i] = true;
m_asms.push_back(m_aux[i].get());
}
else {
m_asms.push_back(m_aux[i].get());
lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
switch(is_sat) {
case l_undef:
return false;
case l_false:
++m_stats.m_num_model_expansions_failure;
m_asms.pop_back();
break;
case l_true:
++m_stats.m_num_model_expansions_success;
s().get_model(mdl);
m_seed[i] = true; m_seed[i] = true;
} break;
else {
ensure_active(i);
m_asms.push_back(m_aux[i].get());
lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
TRACE("opt", tout
<< "check: " << mk_pp(m_asms.back(), m)
<< ":" << is_sat << "\n";);
switch(is_sat) {
case l_undef:
return false;
case l_false:
++m_stats.m_num_model_expansions_failure;
m_asms.pop_back();
break;
case l_true:
++m_stats.m_num_model_expansions_success;
s().get_model(mdl);
m_seed[i] = true;
break;
}
} }
} }
} }
@ -971,6 +977,11 @@ namespace opt {
tout << "new upper: " << m_upper << "\n"; tout << "new upper: " << m_upper << "\n";
model_smt2_pp(tout, m, *(mdl.get()), 0);); model_smt2_pp(tout, m, *(mdl.get()), 0););
} }
DEBUG_CODE(
for (unsigned i = 0; i < num_soft(); ++i) {
SASSERT(is_true(mdl, m_soft[i].get()) == m_seed[i]);
});
return true; return true;
} }