mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-24 05:19:13 +00:00
Code Activity

fix box mode: reset bounds before each objective

Browse source 
update_lower_lex updates m_lower for subsequent objectives with saved
values from the current model. Reset m_lower[i] and m_upper[i] to
their initial values before optimizing each objective so earlier
objectives do not contaminate later ones.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-03-19 13:16:27 -10:00 • committed by Lev Nachmanson
parent fbbb582650
commit 8cc75d444e
1 changed files with 4 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/opt/optsmt.cpp
View file

@ -545,28 +545,20 @@ namespace opt {
// m_optsmt_engine is "symba", because symba_opt and geometric_opt
// optimize all objectives jointly, violating box mode semantics.
//
// Save and restore m_lower/m_upper across iterations because
// geometric_lex's update_lower_lex updates m_lower for all
// subsequent objectives with saved values from the current model,
// which would contaminate later objectives' starting bounds.
vector<inf_eps> saved_lower(m_lower);
vector<inf_eps> saved_upper(m_upper);
m_context.get_base_model(m_best_model);
for (unsigned i = 0; i < m_vars.size() && m.inc(); ++i) {
m_lower = saved_lower;
m_upper = saved_upper;
// Reset bounds for objective i so that update_lower_lex
// contamination from earlier objectives does not affect it.
m_lower[i] = inf_eps(rational(-1), inf_rational(0));
m_upper[i] = inf_eps(rational(1), inf_rational(0));
solver::scoped_push _push(*m_s);
is_sat = geometric_lex(i, true, true);
if (is_sat == l_undef)
return l_undef;
if (is_sat == l_false)
return l_false;
saved_lower[i] = m_lower[i];
saved_upper[i] = m_upper[i];
m_models.set(i, m_best_model.get());
}
m_lower = saved_lower;
m_upper = saved_upper;
return l_true;
}