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

adding scoped state

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-05-09 17:21:16 -07:00
parent 252b9e8819
commit cf55854d22
2 changed files with 141 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

160
src/opt/opt_context.cpp
View file

@ -39,65 +39,44 @@ Notes:
namespace opt { namespace opt {
context::context(ast_manager& m): void context::scoped_state::push() {
m(m), m_hard_lim.push_back(m_hard.size());
m_arith(m), m_objectives_lim.push_back(m_objectives.size());
m_bv(m),
m_hard_constraints(m),
m_optsmt(m),
m_objective_refs(m)
{
m_params.set_bool("model", true);
m_params.set_bool("unsat_core", true);
m_solver = alloc(opt_solver, m, m_params, symbol());
} }
context::~context() { void context::scoped_state::pop() {
map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end(); m_hard.resize(m_hard_lim.back());
for (; it != end; ++it) { unsigned k = m_objectives_term_trail_lim.back();
dealloc(it->m_value); while (m_objectives_term_trail.size() > k) {
unsigned idx = m_objectives_term_trail.back();
m_objectives[idx].m_terms.pop_back();
m_objectives[idx].m_weights.pop_back();
m_objectives_term_trail.pop_back();
} }
} m_objectives_term_trail_lim.pop_back();
k = m_objectives_lim.back();
void context::push() { while (m_objectives.size() > k) {
m_objectives_lim.push_back(m_objectives.size()); objective& obj = m_objectives.back();
m_objectives_term_trail_lim.push_back(m_objectives_term_trail.size()); if (obj.m_type == O_MAXSMT) {
m_solver->push(); m_indices.erase(obj.m_id);
}
void context::pop(unsigned n) {
m_solver->pop(n);
while (n > 0) {
--n;
unsigned k = m_objectives_term_trail_lim.back();
while (m_objectives_term_trail.size() > k) {
unsigned idx = m_objectives_term_trail.back();
m_objectives[idx].m_terms.pop_back();
m_objectives[idx].m_weights.pop_back();
m_objectives_term_trail.pop_back();
} }
m_objectives_term_trail_lim.pop_back(); m_objectives.pop_back();
k = m_objectives_lim.back();
while (m_objectives.size() > k) {
objective& obj = m_objectives.back();
if (obj.m_type == O_MAXSMT) {
dealloc(m_maxsmts[obj.m_id]);
m_maxsmts.erase(obj.m_id);
m_indices.erase(obj.m_id);
}
m_objectives.pop_back();
}
m_objectives_lim.pop_back();
} }
m_objectives_lim.pop_back();
m_hard_lim.pop_back();
} }
void context::set_hard_constraints(ptr_vector<expr>& fmls) {
m_hard_constraints.reset(); void context::scoped_state::add(expr* hard) {
m_hard_constraints.append(fmls.size(), fmls.c_ptr()); m_hard.push_back(hard);
} }
unsigned context::add_soft_constraint(expr* f, rational const& w, symbol const& id) { void context::scoped_state::set(ptr_vector<expr> & hard) {
maxsmt* ms; m_hard.reset();
m_hard.append(hard.size(), hard.c_ptr());
}
unsigned context::scoped_state::add(expr* f, rational const& w, symbol const& id) {
if (w.is_neg()) { if (w.is_neg()) {
throw default_exception("Negative weight supplied. Weight should be positive"); throw default_exception("Negative weight supplied. Weight should be positive");
} }
@ -107,10 +86,7 @@ namespace opt {
if (!m.is_bool(f)) { if (!m.is_bool(f)) {
throw default_exception("Soft constraint should be Boolean"); throw default_exception("Soft constraint should be Boolean");
} }
if (!m_maxsmts.find(id, ms)) { if (!m_indices.contains(id)) {
ms = alloc(maxsmt, m);
ms->updt_params(m_params);
m_maxsmts.insert(id, ms);
m_objectives.push_back(objective(m, id)); m_objectives.push_back(objective(m, id));
m_indices.insert(id, m_objectives.size() - 1); m_indices.insert(id, m_objectives.size() - 1);
} }
@ -122,7 +98,7 @@ namespace opt {
return idx; return idx;
} }
unsigned context::add_objective(app* t, bool is_max) { unsigned context::scoped_state::add(app* t, bool is_max) {
app_ref tr(t, m); app_ref tr(t, m);
if (!m_bv.is_bv(t) && !m_arith.is_int_real(t)) { if (!m_bv.is_bv(t) && !m_arith.is_int_real(t)) {
throw default_exception("Objective must be bit-vector, integer or real"); throw default_exception("Objective must be bit-vector, integer or real");
@ -132,8 +108,79 @@ namespace opt {
return index; return index;
} }
lbool context::optimize() { context::context(ast_manager& m):
m(m),
m_arith(m),
m_bv(m),
m_hard_constraints(m),
m_optsmt(m),
m_scoped_state(m),
m_objective_refs(m)
{
m_params.set_bool("model", true);
m_params.set_bool("unsat_core", true);
m_solver = alloc(opt_solver, m, m_params, symbol());
}
context::~context() {
reset_maxsmts();
}
void context::reset_maxsmts() {
map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
for (; it != end; ++it) {
dealloc(it->m_value);
}
}
void context::push() {
m_scoped_state.push();
m_solver->push();
}
void context::pop(unsigned n) {
m_solver->pop(n);
for (unsigned i = 0; i < n; ++i) {
m_scoped_state.pop();
}
}
void context::set_hard_constraints(ptr_vector<expr>& fmls) {
m_scoped_state.set(fmls);
}
void context::add_hard_constraint(expr* f) {
m_scoped_state.add(f);
}
unsigned context::add_soft_constraint(expr* f, rational const& w, symbol const& id) {
return m_scoped_state.add(f, w, id);
}
unsigned context::add_objective(app* t, bool is_max) {
return m_scoped_state.add(t, is_max);
}
void context::import_scoped_state() {
m_optsmt.reset(); m_optsmt.reset();
reset_maxsmts();
m_objectives.reset();
m_hard_constraints.reset();
scoped_state& s = m_scoped_state;
for (unsigned i = 0; i < s.m_objectives.size(); ++i) {
objective& obj = s.m_objectives[i];
m_objectives.push_back(obj);
if (obj.m_type == O_MAXSMT) {
maxsmt* ms = alloc(maxsmt, m);
ms->updt_params(m_params);
m_maxsmts.insert(obj.m_id, ms);
}
}
m_hard_constraints.append(s.m_hard);
}
lbool context::optimize() {
import_scoped_state();
normalize(); normalize();
internalize(); internalize();
opt_solver& s = get_solver(); opt_solver& s = get_solver();
@ -640,7 +687,6 @@ namespace opt {
maxsmt* ms = alloc(maxsmt, m); maxsmt* ms = alloc(maxsmt, m);
ms->updt_params(m_params); ms->updt_params(m_params);
m_maxsmts.insert(id, ms); m_maxsmts.insert(id, ms);
m_indices.insert(id, index);
} }
SASSERT(obj.m_id == id); SASSERT(obj.m_id == id);
obj.m_terms.reset(); obj.m_terms.reset();

47
src/opt/opt_context.h
View file

@ -75,6 +75,35 @@ namespace opt {
m_index(0) m_index(0)
{} {}
}; };
class scoped_state {
ast_manager& m;
arith_util m_arith;
bv_util m_bv;
unsigned_vector m_hard_lim;
unsigned_vector m_objectives_lim;
unsigned_vector m_objectives_term_trail;
unsigned_vector m_objectives_term_trail_lim;
map_id m_indices;
public:
expr_ref_vector m_hard;
vector<objective> m_objectives;
scoped_state(ast_manager& m):
m(m),
m_arith(m),
m_bv(m),
m_hard(m)
{}
void push();
void pop();
void add(expr* hard);
void set(ptr_vector<expr> & hard);
unsigned add(expr* soft, rational const& weight, symbol const& id);
unsigned add(app* obj, bool is_max);
};
ast_manager& m; ast_manager& m;
arith_util m_arith; arith_util m_arith;
bv_util m_bv; bv_util m_bv;
@ -82,25 +111,23 @@ namespace opt {
ref<opt_solver> m_solver; ref<opt_solver> m_solver;
scoped_ptr<pareto_base> m_pareto; scoped_ptr<pareto_base> m_pareto;
params_ref m_params; params_ref m_params;
optsmt m_optsmt; optsmt m_optsmt;
map_t m_maxsmts; map_t m_maxsmts;
map_id m_indices; scoped_state m_scoped_state;
vector<objective> m_objectives; vector<objective> m_objectives;
unsigned_vector m_objectives_lim;
unsigned_vector m_objectives_term_trail;
unsigned_vector m_objectives_term_trail_lim;
model_ref m_model; model_ref m_model;
model_converter_ref m_model_converter; model_converter_ref m_model_converter;
obj_map<func_decl, unsigned> m_objective_fns; obj_map<func_decl, unsigned> m_objective_fns;
obj_map<func_decl, expr*> m_objective_orig; obj_map<func_decl, expr*> m_objective_orig;
func_decl_ref_vector m_objective_refs; func_decl_ref_vector m_objective_refs;
tactic_ref m_simplify; tactic_ref m_simplify;
public: public:
context(ast_manager& m); context(ast_manager& m);
virtual ~context(); virtual ~context();
unsigned add_soft_constraint(expr* f, rational const& w, symbol const& id); unsigned add_soft_constraint(expr* f, rational const& w, symbol const& id);
unsigned add_objective(app* t, bool is_max); unsigned add_objective(app* t, bool is_max);
void add_hard_constraint(expr* f) { m_hard_constraints.push_back(f); } void add_hard_constraint(expr* f);
virtual void push(); virtual void push();
virtual void pop(unsigned n); virtual void pop(unsigned n);
@ -138,6 +165,8 @@ namespace opt {
lbool execute_pareto(); lbool execute_pareto();
expr_ref to_expr(inf_eps const& n); expr_ref to_expr(inf_eps const& n);
void reset_maxsmts();
void import_scoped_state();
void normalize(); void normalize();
void internalize(); void internalize();
bool is_maximize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index); bool is_maximize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index);