diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h index 03ad5b187..501ad9e1a 100644 --- a/src/test/lp/gomory_test.h +++ b/src/test/lp/gomory_test.h @@ -1,4 +1,5 @@ namespace lp { +#include "util/lp/lp_utils.h" struct gomory_test { gomory_test( std::function name_function_p, @@ -88,7 +89,7 @@ struct gomory_test { lp_assert(is_int(x_j)); lp_assert(!a.is_int()); lp_assert(f_0 > zero_of_type() && f_0 < one_of_type()); - mpq f_j = int_solver::fractional_part(a); + mpq f_j = fractional_part(a); TRACE("gomory_cut_detail", tout << a << " x_j = " << x_j << ", k = " << k << "\n"; tout << "f_j: " << f_j << "\n"; @@ -206,7 +207,7 @@ struct gomory_test { unsigned x_j; mpq a; bool some_int_columns = false; - mpq f_0 = int_solver::fractional_part(get_value(inf_col)); + mpq f_0 = fractional_part(get_value(inf_col)); mpq one_min_f_0 = 1 - f_0; for ( auto pp : row) { a = pp.first; diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index 377c6125c..f0bbd2348 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -20,19 +20,10 @@ #include "util/lp/gomory.h" #include "util/lp/int_solver.h" #include "util/lp/lar_solver.h" +#include "util/lp/lp_utils.h" namespace lp { class gomory::imp { - inline static bool is_rational(const impq & n) { return is_zero(n.y); } - - inline static mpq fractional_part(const impq & n) { - lp_assert(is_rational(n)); - return n.x - floor(n.x); - } - inline static mpq fractional_part(const mpq & n) { - return n - floor(n); - } - lar_term & m_t; // the term to return in the cut mpq & m_k; // the right side of the cut explanation& m_ex; // the conflict explanation diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index 71be7258a..1bbefd154 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -433,7 +433,15 @@ inline void ensure_increasing(vector & v) { } } +inline static bool is_rational(const impq & n) { return is_zero(n.y); } +inline static mpq fractional_part(const impq & n) { + lp_assert(is_rational(n)); + return n.x - floor(n.x); +} +inline static mpq fractional_part(const mpq & n) { + return n - floor(n); +} #if Z3DEBUG bool D();