mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

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

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner 2015-04-01 16:21:56 -07:00
parent 52619b9dbb
commit f8d04118d8
6 changed files with 40 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/opt/opt_context.cpp
View file

@ -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;
}

2
src/opt/opt_context.h
View file

@ -144,6 +144,8 @@ namespace opt {
ref<solver> m_solver;
ref<solver> m_sat_solver;
scoped_ptr<pareto_base> m_pareto;
sref_vector<model> m_box_models;
unsigned m_box_index;
params_ref m_params;
optsmt m_optsmt;
map_t m_maxsmts;

9
src/opt/opt_solver.cpp
View file

@ -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;
}

4
src/opt/opt_solver.h
View file

@ -76,6 +76,7 @@ namespace opt {
bool m_objective_enabled;
svector<smt::theory_var> m_objective_vars;
vector<inf_eps> m_objective_values;
sref_vector<model> m_models;
sort_ref_vector m_objective_sorts;
svector<bool> 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<expr> & 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<symbol> & 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];
}

4
src/opt/optsmt.cpp
View file

@ -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;
}

2
src/opt/optsmt.h
View file

@ -38,6 +38,7 @@ namespace opt {
svector<smt::theory_var> m_vars;
symbol m_optsmt_engine;
model_ref m_model;
sref_vector<model> 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);