diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index db373494a..27185228d 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -255,9 +255,9 @@ namespace opt { } } - lbool context::execute_min_max(unsigned index, bool committed, bool scoped) { + lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) { if (scoped) get_solver().push(); - lbool result = m_optsmt.lex(index); + lbool result = m_optsmt.lex(index, is_max); if (result == l_true) m_optsmt.get_model(m_model); if (scoped) get_solver().pop(1); if (result == l_true && committed) m_optsmt.commit_assignment(index); @@ -277,8 +277,8 @@ namespace opt { lbool context::execute(objective const& obj, bool committed, bool scoped) { switch(obj.m_type) { - case O_MAXIMIZE: return execute_min_max(obj.m_index, committed, scoped); - case O_MINIMIZE: return execute_min_max(obj.m_index, committed, scoped); + case O_MAXIMIZE: return execute_min_max(obj.m_index, committed, scoped, true); + case O_MINIMIZE: return execute_min_max(obj.m_index, committed, scoped, false); case O_MAXSMT: return execute_maxsat(obj.m_id, committed, scoped); default: UNREACHABLE(); return l_undef; } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index a22c18373..09ddb725a 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -189,7 +189,7 @@ namespace opt { void validate_feasibility(maxsmt& ms); lbool execute(objective const& obj, bool committed, bool scoped); - lbool execute_min_max(unsigned index, bool committed, bool scoped); + lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max); lbool execute_maxsat(symbol const& s, bool committed, bool scoped); lbool execute_lex(); lbool execute_box(); diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 0a441755b..6cc6eeeab 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -15,7 +15,6 @@ Author: Notes: - Suppose we obtain solution t1 = k1, ..., tn = kn-epsilon Assert: t1 > k1 \/ t2 > k2 \/ ... \/ tn >= kn @@ -24,15 +23,7 @@ Notes: Claim: we don't necessarily have to freeze assignments of t_i when optimizing assignment for t_j because the state will always satisfy the disjunction. - If one of the k_i is unbounded, then omit a disjunction for it. - Claim: the end result (when the constraints are no longer feasible) - is Pareto optimal, but convergence will probably not be as fast - as when fixing one parameter at a time. - E.g., a different approach is first to find a global maximal for one - variable. Then add a method to "freeze" that variable at the extremum if it is finite. - To do this, add lower and upper bounds for that variable using infinitesimals. - If the variable is unbounded, then this is of course not sufficient by itself. - + If one of the k_i is unbounded, then omit a disjunction for it. --*/ @@ -234,14 +225,14 @@ namespace opt { } } - lbool optsmt::lex(unsigned obj_index) { + lbool optsmt::lex(unsigned obj_index, bool is_maximize) { TRACE("opt", tout << "optsmt:lex\n";); solver::scoped_push _push(*m_s); SASSERT(obj_index < m_vars.size()); - return basic_lex(obj_index); + return basic_lex(obj_index, is_maximize); } - lbool optsmt::basic_lex(unsigned obj_index) { + lbool optsmt::basic_lex(unsigned obj_index, bool is_maximize) { lbool is_sat = l_true; expr_ref block(m), tmp(m); @@ -253,8 +244,13 @@ namespace opt { m_s->get_model(m_model); inf_eps obj = m_s->get_objective_value(obj_index); if (obj > m_lower[obj_index]) { - m_lower[obj_index] = obj; - IF_VERBOSE(1, verbose_stream() << "(optsmt lower bound: " << obj << ")\n";); + m_lower[obj_index] = obj; + IF_VERBOSE(1, + if (is_maximize) + verbose_stream() << "(optsmt lower bound: " << obj << ")\n"; + else + verbose_stream() << "(optsmt upper bound: " << (-obj) << ")\n"; + ); for (unsigned i = obj_index+1; i < m_vars.size(); ++i) { m_s->maximize_objective(i, tmp); m_lower[i] = m_s->get_objective_value(i); @@ -281,53 +277,6 @@ namespace opt { } - lbool optsmt::pareto(unsigned obj_index) { - lbool is_sat = l_true; - expr_ref block(m); - for (unsigned i = 0; i < m_lower.size(); ++i) { - m_lower[i] = inf_eps(rational(-1),inf_rational(0)); - m_upper[i] = inf_eps(rational(1), inf_rational(0)); - } - bool was_sat = false; - - while (is_sat == l_true && !m_cancel) { - is_sat = m_s->check_sat(0, 0); - if (is_sat != l_true) break; - was_sat = true; - m_s->maximize_objective(obj_index, block); - m_s->get_model(m_model); - inf_eps obj = m_s->get_objective_value(obj_index); - if (obj > m_lower[obj_index]) { - m_lower[obj_index] = obj; - IF_VERBOSE(1, verbose_stream() << "(optsmt lower bound: " << obj << ")\n";); - } - m_s->assert_expr(block); - } - - if (m_cancel || is_sat == l_undef) { - return l_undef; - } - if (!was_sat) { - return l_false; - } - - // set the solution tight. - // and set lower bounds on other values. - m_upper[obj_index] = m_lower[obj_index]; - expr_ref val(m); - rational r; - arith_util a(m); - for (unsigned i = 0; i < m_lower.size(); ++i) { - if (i != obj_index) { - VERIFY(m_model->eval(m_objs[i].get(), val) && a.is_numeral(val, r)); - m_lower[i] = inf_eps(r); - } - } - - return l_true; - } - - /** Takes solver with hard constraints added. Returns an optimal assignment to objective functions. diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index 5f4a2988f..95e24a439 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -44,9 +44,7 @@ namespace opt { lbool box(); - lbool lex(unsigned obj_index); - - lbool pareto(unsigned obj_index); + lbool lex(unsigned obj_index, bool is_maximize); unsigned add(app* t); @@ -69,7 +67,7 @@ namespace opt { lbool basic_opt(); - lbool basic_lex(unsigned idx); + lbool basic_lex(unsigned idx, bool is_maximize); lbool farkas_opt();