From 045448e5b2236a4854ee857ae5cef7f0043e8720 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Jan 2020 11:47:37 -0600 Subject: [PATCH] fix build of test Signed-off-by: Nikolaj Bjorner --- src/test/algebraic.cpp | 2 +- src/util/lp/gomory.cpp | 12 +++++++++--- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/test/algebraic.cpp b/src/test/algebraic.cpp index fe6aca26d..508bc7a2f 100644 --- a/src/test/algebraic.cpp +++ b/src/test/algebraic.cpp @@ -397,7 +397,7 @@ static void tst_isolate_roots(polynomial_ref const & p, anum_manager & am, std::cout << "x1 -> "; am.display_root(std::cout, v1); std::cout << "\n"; std::cout << "x2 -> "; am.display_root(std::cout, v2); std::cout << "\n"; scoped_anum_vector roots(am); - svector signs; + svector<::sign> signs; am.isolate_roots(p, x2v, roots, signs); ENSURE(roots.size() + 1 == signs.size()); std::cout << "roots:\n"; diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index d5fae828f..691828b9f 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -277,7 +277,7 @@ public: bool some_int_columns = false; mpq m_f = fractional_part(get_value(m_inf_col)); TRACE("gomory_cut_detail", tout << "m_f: " << m_f << ", "; - tout << "1 - m_f: " << 1 - m_f << ", get_value(m_inf_col).x - m_f = " << get_value(m_inf_col).x - m_f;); + tout << "1 - m_f: " << 1 - m_f << ", get_value(m_inf_col).x - m_f = " << get_value(m_inf_col).x - m_f << "\n";); lp_assert(m_f.is_pos() && (get_value(m_inf_col).x - m_f).is_int()); mpq one_min_m_f = 1 - m_f; @@ -285,7 +285,7 @@ public: unsigned j = p.var(); if (j == m_inf_col) { lp_assert(p.coeff() == one_of_type()); - TRACE("gomory_cut_detail", tout << "seeing basic var";); + TRACE("gomory_cut_detail", tout << "seeing basic var\n";); continue; } @@ -295,11 +295,17 @@ public: } else { if (p.coeff().is_int()) { // m_fj will be zero and no monomial will be added + if (at_lower(j)) { + m_ex.push_justification(column_lower_bound_constraint(j)); + } + if (at_upper(j)) { + m_ex.push_justification(column_upper_bound_constraint(j)); + } continue; } some_int_columns = true; m_fj = fractional_part(-p.coeff()); - m_one_minus_fj = 1 - m_fj; + m_one_minus_fj = 1 - m_fj; int_case_in_gomory_cut(j); } }