mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

edits

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-05-13 10:33:09 -07:00
parent cad1e5cab3
commit 1ea376e310
1 changed files with 0 additions and 85 deletions
Download patch file Download diff file Expand all files Collapse all files

85
src/opt/opt_pareto.cpp
View file

@ -110,88 +110,3 @@ namespace opt {
}
#if 0
opt_solver& s = get_solver();
expr_ref val(m);
rational r;
lbool is_sat = l_true;
vector<bounds_t> bounds;
for (unsigned i = 0; i < m_objectives.size(); ++i) {
objective const& obj = m_objectives[i];
if (obj.m_type == O_MAXSMT) {
IF_VERBOSE(0, verbose_stream() << "Pareto optimization is not supported for MAXSMT\n";);
return l_undef;
}
solver::scoped_push _sp(s);
is_sat = m_optsmt.pareto(obj.m_index);
if (is_sat != l_true) {
return is_sat;
}
if (!m_optsmt.get_upper(obj.m_index).is_finite()) {
return l_undef;
}
bounds_t bound;
for (unsigned j = 0; j < m_objectives.size(); ++j) {
objective const& obj_j = m_objectives[j];
inf_eps lo = m_optsmt.get_lower(obj_j.m_index);
inf_eps hi = m_optsmt.get_upper(obj_j.m_index);
bound.push_back(std::make_pair(lo, hi));
}
bounds.push_back(bound);
}
for (unsigned i = 0; i < bounds.size(); ++i) {
for (unsigned j = 0; j < bounds.size(); ++j) {
objective const& obj = m_objectives[j];
bounds[i][j].second = bounds[j][j].second;
}
IF_VERBOSE(0, display_bounds(verbose_stream() << "new bound\n", bounds[i]););
}
for (unsigned i = 0; i < bounds.size(); ++i) {
bounds_t b = bounds[i];
vector<inf_eps> mids;
solver::scoped_push _sp(s);
for (unsigned j = 0; j < b.size(); ++j) {
objective const& obj = m_objectives[j];
inf_eps mid = (b[j].second - b[j].first)/rational(2);
mids.push_back(mid);
expr_ref ge = s.mk_ge(obj.m_index, mid);
s.assert_expr(ge);
}
is_sat = execute_box();
switch(is_sat) {
case l_undef:
return is_sat;
case l_true: {
bool at_bound = true;
for (unsigned j = 0; j < b.size(); ++j) {
objective const& obj = m_objectives[j];
if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) {
mids[j] = inf_eps(r);
}
at_bound = at_bound && mids[j] == b[j].second;
b[j].second = mids[j];
}
IF_VERBOSE(0, display_bounds(verbose_stream() << "new bound\n", b););
if (!at_bound) {
bounds.push_back(b);
}
break;
}
case l_false: {
bounds_t b2(b);
for (unsigned j = 0; j < b.size(); ++j) {
b2[j].second = mids[j];
if (j > 0) {
b2[j-1].second = b[j-1].second;
}
IF_VERBOSE(0, display_bounds(verbose_stream() << "refined bound\n", b2););
bounds.push_back(b2);
}
break;
}
}
}
return is_sat;
#endif