mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

fix #6986

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-11-08 13:49:30 +01:00
parent e6385f8c85
commit bd4d580b17
1 changed files with 22 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/math/lp/gomory.cpp
View file

@ -32,7 +32,7 @@ class create_cut {
unsigned m_inf_col; // a basis column which has to be an integer but has a non integral value unsigned m_inf_col; // a basis column which has to be an integer but has a non integral value
const row_strip<mpq>& m_row; const row_strip<mpq>& m_row;
int_solver& lia; int_solver& lia;
mpq m_lcm_den; mpq m_lcm_den = { mpq(1) };
mpq m_f; mpq m_f;
mpq m_one_minus_f; mpq m_one_minus_f;
mpq m_fj; mpq m_fj;
@ -82,8 +82,7 @@ class create_cut {
push_explanation(column_upper_bound_constraint(j)); push_explanation(column_upper_bound_constraint(j));
} }
m_t.add_monomial(new_a, j); m_t.add_monomial(new_a, j);
m_lcm_den = lcm(m_lcm_den, denominator(new_a)); TRACE("gomory_cut_detail", tout << "new_a = " << new_a << ", k = " << m_k << "\n";);
TRACE("gomory_cut_detail", tout << "new_a = " << new_a << ", k = " << m_k << ", lcm_den = " << m_lcm_den << "\n";);
#if SMALL_CUTS #if SMALL_CUTS
// if (numerator(new_a).is_big()) throw found_big(); // if (numerator(new_a).is_big()) throw found_big();
if (numerator(new_a) > m_big_number) if (numerator(new_a) > m_big_number)
@ -181,7 +180,9 @@ class create_cut {
} }
} }
else { else {
m_lcm_den = lcm(m_lcm_den, denominator(m_k)); m_lcm_den = denominator(m_k);
for (auto const& [c, v] : pol)
m_lcm_den = lcm(m_lcm_den, denominator(c));
lp_assert(m_lcm_den.is_pos()); lp_assert(m_lcm_den.is_pos());
TRACE("gomory_cut_detail", tout << "pol.size() > 1 den: " << m_lcm_den << std::endl;); TRACE("gomory_cut_detail", tout << "pol.size() > 1 den: " << m_lcm_den << std::endl;);
if (!m_lcm_den.is_one()) { if (!m_lcm_den.is_one()) {
@ -192,6 +193,21 @@ class create_cut {
} }
m_k *= m_lcm_den; m_k *= m_lcm_den;
} }
#if 0
unsigned j = 0, i = 0;
for (auto & [c, v] : pol) {
if (lia.is_fixed(v)) {
push_explanation(column_lower_bound_constraint(v));
push_explanation(column_upper_bound_constraint(v));
m_k -= c;
IF_VERBOSE(0, verbose_stream() << "got fixed " << v << "\n");
}
else
pol[j++] = pol[i];
++i;
}
pol.shrink(j);
#endif
// gcd reduction is loss-less: // gcd reduction is loss-less:
mpq g(1); mpq g(1);
@ -219,8 +235,8 @@ class create_cut {
} }
#endif #endif
for (const auto & [c, v]: pol) for (const auto & [c, v]: pol)
m_t.add_monomial(c, v); m_t.add_monomial(c, v);
VERIFY(m_t.size() > 0); VERIFY(m_t.size() > 0);
} }
@ -343,7 +359,6 @@ public:
// gomory will be t >= k and the current solution has a property t < k // gomory will be t >= k and the current solution has a property t < k
m_k = 1; m_k = 1;
m_t.clear(); m_t.clear();
mpq m_lcm_den(1);
bool some_int_columns = false; bool some_int_columns = false;
mpq m_f = fractional_part(get_value(m_inf_col)); mpq m_f = fractional_part(get_value(m_inf_col));
TRACE("gomory_cut_detail", tout << "m_f: " << m_f << ", "; TRACE("gomory_cut_detail", tout << "m_f: " << m_f << ", ";
@ -415,7 +430,6 @@ public:
m_inf_col(basic_inf_int_j), m_inf_col(basic_inf_int_j),
m_row(row), m_row(row),
lia(lia), lia(lia),
m_lcm_den(1),
m_f(fractional_part(get_value(basic_inf_int_j).x)), m_f(fractional_part(get_value(basic_inf_int_j).x)),
m_one_minus_f(1 - m_f) {} m_one_minus_f(1 - m_f) {}