mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

Merge branch 'opt' of https://github.com/Z3Prover/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-04-02 15:22:41 -07:00
parent dca0fb77c2 6b995c4077
commit 26c53d055a
3 changed files with 13 additions and 5 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);
};

2
src/smt/asserted_formulas.cpp
View file

@ -603,7 +603,7 @@ void asserted_formulas::propagate_values() {
proof_ref_vector new_prs1(m_manager);
expr_ref_vector new_exprs2(m_manager);
proof_ref_vector new_prs2(m_manager);
unsigned i = 0;
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i);