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

fix bug introduced when clearing state between calls to Pareto/Box

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-04-02 02:36:01 -07:00
parent fc36d861a7
commit e944f89505
2 changed files with 12 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/opt/opt_context.cpp
View file

@ -75,9 +75,14 @@ namespace opt {
m_hard.push_back(hard);
}
void context::scoped_state::set(ptr_vector<expr> & hard) {
bool context::scoped_state::set(ptr_vector<expr> & hard) {
bool eq = hard.size() == m_hard.size();
for (unsigned i = 0; eq && i < hard.size(); ++i) {
eq = hard[i] == m_hard[i].get();
}
m_hard.reset();
m_hard.append(hard.size(), hard.c_ptr());
return !eq;
}
unsigned context::scoped_state::add(expr* f, rational const& w, symbol const& id) {
@ -161,8 +166,9 @@ namespace opt {
}
void context::set_hard_constraints(ptr_vector<expr>& fmls) {
m_scoped_state.set(fmls);
clear_state();
if (m_scoped_state.set(fmls)) {
clear_state();
}
}
void context::add_hard_constraint(expr* f) {
@ -203,6 +209,7 @@ namespace opt {
if (m_box_index != UINT_MAX) {
return execute_box();
}
clear_state();
init_solver();
import_scoped_state();
normalize();
@ -327,6 +334,7 @@ namespace opt {
return l_false;
}
m_box_index = 1;
m_box_models.reset();
lbool r = m_optsmt.box();
for (unsigned i = 0, j = 0; r == l_true && i < m_objectives.size(); ++i) {
objective const& obj = m_objectives[i];

2
src/opt/opt_context.h
View file

@ -131,7 +131,7 @@ namespace opt {
void push();
void pop();
void add(expr* hard);
void set(ptr_vector<expr> & hard);
bool set(ptr_vector<expr> & hard);
unsigned add(expr* soft, rational const& weight, symbol const& id);
unsigned add(app* obj, bool is_max);
};