mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

integrate bounds from original model

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-15 15:11:31 -07:00
parent ce18421a7a
commit 630a3d6ea8
3 changed files with 12 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/opt/opt_context.cpp
View file

@ -843,7 +843,6 @@ namespace opt {
void context::update_bound(bool is_lower) {
expr_ref val(m);
if (!m_model.get()) return;
bool override = true;
for (unsigned i = 0; i < m_objectives.size(); ++i) {
objective const& obj = m_objectives[i];
rational r;
@ -852,10 +851,10 @@ namespace opt {
if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) {
inf_eps val = inf_eps(obj.m_adjust_value(r));
if (is_lower) {
m_optsmt.update_lower(obj.m_index, val, override);
m_optsmt.update_lower(obj.m_index, val);
}
else {
m_optsmt.update_upper(obj.m_index, val, override);
m_optsmt.update_upper(obj.m_index, val);
}
}
break;
@ -863,10 +862,10 @@ namespace opt {
if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) {
inf_eps val = inf_eps(obj.m_adjust_value(r));
if (is_lower) {
m_optsmt.update_lower(obj.m_index, val, override);
m_optsmt.update_lower(obj.m_index, val);
}
else {
m_optsmt.update_upper(obj.m_index, val, override);
m_optsmt.update_upper(obj.m_index, val);
}
}
break;

16
src/opt/optsmt.cpp
View file

@ -48,7 +48,7 @@ namespace opt {
void optsmt::set_max(vector<inf_eps>& dst, vector<inf_eps> const& src, expr_ref_vector& fmls) {
for (unsigned i = 0; i < src.size(); ++i) {
if (src[i] > dst[i]) {
if (src[i] >= dst[i]) {
dst[i] = src[i];
m_lower_fmls[i] = fmls[i].get();
if (dst[i].is_pos() && !dst[i].is_finite()) { // review: likely done already.
@ -60,7 +60,6 @@ namespace opt {
fmls[i] = m_lower_fmls[i].get();
}
}
std::cout << "\n";
}
/*
@ -170,16 +169,13 @@ namespace opt {
return basic_opt();
}
void optsmt::update_lower(unsigned idx, inf_eps const& v, bool override) {
if (m_lower[idx] < v || override) {
m_lower[idx] = v;
}
void optsmt::update_lower(unsigned idx, inf_eps const& v) {
m_lower_fmls[idx] = m_s->mk_ge(idx, v);
m_lower[idx] = v;
}
void optsmt::update_upper(unsigned idx, inf_eps const& v, bool override) {
if (m_upper[idx] > v || override) {
m_upper[idx] = v;
}
void optsmt::update_upper(unsigned idx, inf_eps const& v) {
m_upper[idx] = v;
}
void optsmt::update_lower() {

4
src/opt/optsmt.h
View file

@ -60,8 +60,8 @@ namespace opt {
inf_eps get_upper(unsigned index) const;
void get_model(model_ref& mdl);
void update_lower(unsigned idx, inf_eps const& r, bool override);
void update_upper(unsigned idx, inf_eps const& r, bool override);
void update_lower(unsigned idx, inf_eps const& r);
void update_upper(unsigned idx, inf_eps const& r);
void reset();