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

fix #7493

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-02-02 15:00:31 -08:00
parent 99cbfa715c
commit 17d47ca8c7
3 changed files with 14 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/opt/opt_solver.cpp
View file

@ -241,6 +241,7 @@ namespace opt {
smt::theory_var v = m_objective_vars[i]; smt::theory_var v = m_objective_vars[i];
bool has_shared = false; bool has_shared = false;
m_last_model = nullptr; m_last_model = nullptr;
blocker = nullptr;
// //
// compute an optimization hint. // compute an optimization hint.
// The hint is valid if there are no shared symbols (a pure LP). // The hint is valid if there are no shared symbols (a pure LP).
@ -256,6 +257,7 @@ namespace opt {
if (!m_models[i]) if (!m_models[i])
m_models.set(i, m_last_model.get()); m_models.set(i, m_last_model.get());
TRACE("opt", tout << "maximize " << i << " " << val << " " << m_objective_values[i] << " " << blocker << "\n";);
if (val > m_objective_values[i]) { if (val > m_objective_values[i]) {
m_objective_values[i] = val; m_objective_values[i] = val;
} }

6
src/opt/optsmt.cpp
View file

@ -202,9 +202,6 @@ namespace opt {
for (unsigned i = 0; i < obj_index; ++i) for (unsigned i = 0; i < obj_index; ++i)
commit_assignment(i); commit_assignment(i);
// m_s->maximize_objective(obj_index, bound);
// m_s->assert_expr(bound);
unsigned steps = 0; unsigned steps = 0;
unsigned step_incs = 0; unsigned step_incs = 0;
rational delta_per_step(1); rational delta_per_step(1);
@ -216,9 +213,10 @@ namespace opt {
SASSERT(delta_per_step.is_pos()); SASSERT(delta_per_step.is_pos());
is_sat = m_s->check_sat(0, nullptr); is_sat = m_s->check_sat(0, nullptr);
TRACE("opt", tout << "check " << is_sat << "\n"; TRACE("opt", tout << "check " << is_sat << "\n";
tout << "last bound: " << last_bound << "\n"; tout << "last bound: " << last_bound << " bound " << bound << "\n";
tout << "lower: " << m_lower[obj_index] << "\n"; tout << "lower: " << m_lower[obj_index] << "\n";
tout << "upper: " << m_upper[obj_index] << "\n"; tout << "upper: " << m_upper[obj_index] << "\n";
if (is_sat == l_true) m_s->display(tout);
); );
if (is_sat == l_true) { if (is_sat == l_true) {
m_s->maximize_objective(obj_index, bound); m_s->maximize_objective(obj_index, bound);

9
src/smt/theory_lra.cpp
View file

@ -3858,12 +3858,21 @@ public:
vi = get_lpvar(v); vi = get_lpvar(v);
st = lp().maximize_term(vi, term_max); st = lp().maximize_term(vi, term_max);
if (has_int() && lp().has_inf_int()) { if (has_int() && lp().has_inf_int()) {
st = lp::lp_status::FEASIBLE; st = lp::lp_status::FEASIBLE;
lp().restore_x(); lp().restore_x();
} }
if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) { if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) {
switch (check_nla()) {
case FC_DONE:
st = lp::lp_status::FEASIBLE; st = lp::lp_status::FEASIBLE;
break;
case FC_GIVEUP:
case FC_CONTINUE:
st = lp::lp_status::UNBOUNDED;
break;
}
lp().restore_x(); lp().restore_x();
} }
} }