mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix bugs in optimization for integers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b764c7bbee
commit
ddd0bf875d
|
@ -111,7 +111,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
if (m_min_cost_atom) {
|
||||
if (!initialized && m_min_cost_atom) {
|
||||
app* var = m_min_cost_atom;
|
||||
if (!ctx.e_internalized(var)) {
|
||||
ctx.mk_enode(var, false, true, true);
|
||||
|
|
|
@ -479,10 +479,11 @@ namespace smt {
|
|||
bool theory_arith<Ext>::all_coeff_int(row const & r) const {
|
||||
typename vector<row_entry>::const_iterator it = r.begin_entries();
|
||||
typename vector<row_entry>::const_iterator end = r.end_entries();
|
||||
for (; it != end; ++it) {
|
||||
if (!it->is_dead() && !it->m_coeff.is_int())
|
||||
for (; it != end; ++it) {
|
||||
if (!it->is_dead() && !it->m_coeff.is_int()) {
|
||||
TRACE("gomory_cut", display_row(tout, r, true););
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
@ -949,6 +950,10 @@ namespace smt {
|
|||
if (curr_gain.is_neg())
|
||||
curr_gain.neg();
|
||||
if (x_i == null_theory_var || (curr_gain < gain) || (gain.is_zero() && curr_gain.is_zero() && s < x_i)) {
|
||||
if (is_int(s) && !curr_gain.is_int())
|
||||
continue;
|
||||
if (is_int(x_j) && !curr_gain.is_int())
|
||||
continue;
|
||||
x_i = s;
|
||||
a_ij = coeff;
|
||||
gain = curr_gain;
|
||||
|
|
Loading…
Reference in a new issue