From f8d04118d8eb4b020fa3b9ea821b2c2897fbf7f0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Apr 2015 16:21:56 -0700 Subject: [PATCH] switch models for multiple box objectives. Feature request at codeplex issue 194, George Karpenov. Usage model is same as Pareto fronts you call check-sat multiple times until retrieving unsat Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 24 +++++++++++++++++++++++- src/opt/opt_context.h | 2 ++ src/opt/opt_solver.cpp | 9 +++++++-- src/opt/opt_solver.h | 4 +++- src/opt/optsmt.cpp | 4 +++- src/opt/optsmt.h | 2 ++ 6 files changed, 40 insertions(+), 5 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index b98343013..6718f401e 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -118,6 +118,7 @@ namespace opt { m_bv(m), m_hard_constraints(m), m_solver(0), + m_box_index(UINT_MAX), m_optsmt(m), m_scoped_state(m), m_fm(m), @@ -199,6 +200,9 @@ namespace opt { if (m_pareto) { return execute_pareto(); } + if (m_box_index != UINT_MAX) { + return execute_box(); + } init_solver(); import_scoped_state(); normalize(); @@ -313,13 +317,31 @@ namespace opt { } lbool context::execute_box() { + if (m_box_index < m_objectives.size()) { + m_model = m_box_models[m_box_index]; + ++m_box_index; + return l_true; + } + if (m_box_index != UINT_MAX && m_box_index >= m_objectives.size()) { + m_box_index = UINT_MAX; + return l_false; + } + m_box_index = 1; lbool r = m_optsmt.box(); - for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) { + for (unsigned i = 0, j = 0; r == l_true && i < m_objectives.size(); ++i) { objective const& obj = m_objectives[i]; if (obj.m_type == O_MAXSMT) { solver::scoped_push _sp(get_solver()); r = execute(obj, false, false); + if (r == l_true) m_box_models.push_back(m_model.get()); } + else { + m_box_models.push_back(m_optsmt.get_model(j)); + ++j; + } + } + if (r == l_true && m_objectives.size() > 0) { + m_model = m_box_models[0]; } return r; } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 001dd1b62..0815e0061 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -144,6 +144,8 @@ namespace opt { ref m_solver; ref m_sat_solver; scoped_ptr m_pareto; + sref_vector m_box_models; + unsigned m_box_index; params_ref m_params; optsmt m_optsmt; map_t m_maxsmts; diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 08bc20004..4556cd080 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -219,9 +219,13 @@ namespace opt { } m_objective_values[i] = val; - TRACE("opt", { model_ref mdl; tout << m_objective_values[i] << "\n"; + model_ref mdl; + get_model(mdl); + m_models.set(i, mdl.get()); + + TRACE("opt", { tout << m_objective_values[i] << "\n"; tout << blocker << "\n"; - get_model(mdl); model_smt2_pp(tout << "update model:\n", m, *mdl, 0); }); + model_smt2_pp(tout << "update model:\n", m, *mdl, 0); }); } void opt_solver::decrement_value(unsigned i, inf_eps& val) { @@ -288,6 +292,7 @@ namespace opt { m_objective_values.push_back(inf_eps(rational(-1), inf_rational())); m_objective_sorts.push_back(m.get_sort(term)); m_valid_objectives.push_back(true); + m_models.push_back(0); return v; } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index e45f4be91..9ceee89a7 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -76,6 +76,7 @@ namespace opt { bool m_objective_enabled; svector m_objective_vars; vector m_objective_values; + sref_vector m_models; sort_ref_vector m_objective_sorts; svector m_valid_objectives; bool m_dump_benchmarks; @@ -94,7 +95,7 @@ namespace opt { virtual void pop_core(unsigned n); virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions); virtual void get_unsat_core(ptr_vector & r); - virtual void get_model(model_ref & _m); + virtual void get_model(model_ref & _m); virtual proof * get_proof(); virtual std::string reason_unknown() const; virtual void get_labels(svector & r); @@ -111,6 +112,7 @@ namespace opt { void maximize_objectives(expr_ref_vector& blockers); inf_eps const & saved_objective_value(unsigned obj_index); inf_eps current_objective_value(unsigned obj_index); + model* get_model(unsigned obj_index) { return m_models[obj_index]; } bool objective_is_model_valid(unsigned obj_index) const { return m_valid_objectives[obj_index]; } diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 1148e3411..d64730335 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -50,6 +50,7 @@ namespace opt { for (unsigned i = 0; i < src.size(); ++i) { if (src[i] >= dst[i]) { dst[i] = src[i]; + m_models.set(i, m_s->get_model(i)); m_lower_fmls[i] = fmls[i].get(); if (dst[i].is_pos() && !dst[i].is_finite()) { // review: likely done already. m_lower_fmls[i] = m.mk_false(); @@ -57,7 +58,7 @@ namespace opt { } } else if (src[i] < dst[i] && !m.is_true(m_lower_fmls[i].get())) { - fmls[i] = m_lower_fmls[i].get(); + fmls[i] = m_lower_fmls[i].get(); } } } @@ -410,6 +411,7 @@ namespace opt { m_lower.push_back(inf_eps(rational(-1),inf_rational(0))); m_upper.push_back(inf_eps(rational(1), inf_rational(0))); m_lower_fmls.push_back(m.mk_true()); + m_models.push_back(0); return m_objs.size()-1; } diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index 8ec35c98e..0a6882b24 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -38,6 +38,7 @@ namespace opt { svector m_vars; symbol m_optsmt_engine; model_ref m_model; + sref_vector m_models; public: optsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_objs(m), m_lower_fmls(m) {} @@ -60,6 +61,7 @@ namespace opt { inf_eps get_upper(unsigned index) const; bool objective_is_model_valid(unsigned index) const; void get_model(model_ref& mdl); + model* get_model(unsigned index) const { return m_models[index]; } void update_lower(unsigned idx, inf_eps const& r); void update_upper(unsigned idx, inf_eps const& r);