From ddd0bf875d3e7bec6435ef88179c5b586fedced8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Dec 2013 08:46:24 +0200 Subject: [PATCH] fix bugs in optimization for integers Signed-off-by: Nikolaj Bjorner --- src/opt/weighted_maxsat.cpp | 2 +- src/smt/theory_arith_aux.h | 9 +++++++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 45eab4d76..cd4a867a2 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -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); diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index f9f98b867..7007232b6 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -479,10 +479,11 @@ namespace smt { bool theory_arith::all_coeff_int(row const & r) const { typename vector::const_iterator it = r.begin_entries(); typename vector::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;