mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
fix the real case in gomory cuts, create a cut in a form t >= k
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
37bc4a4407
commit
65de3f748a
1 changed files with 31 additions and 21 deletions
|
|
@ -43,7 +43,9 @@ class create_cut {
|
|||
struct found_big {};
|
||||
|
||||
const impq & get_value(unsigned j) const { return lia.get_value(j); }
|
||||
bool is_real(unsigned j) const { return lia.is_real(j); }
|
||||
bool is_int(unsigned j) const { return lia.column_is_int(j) || (lia.is_fixed(j) &&
|
||||
lia.lra.column_lower_bound(j).is_int()); }
|
||||
bool is_real(unsigned j) const { return !is_int(j); }
|
||||
bool at_lower(unsigned j) const { return lia.at_lower(j); }
|
||||
bool at_upper(unsigned j) const { return lia.at_upper(j); }
|
||||
const impq & lower_bound(unsigned j) const { return lia.lower_bound(j); }
|
||||
|
|
@ -53,7 +55,7 @@ class create_cut {
|
|||
bool column_is_fixed(unsigned j) const { return lia.lra.column_is_fixed(j); }
|
||||
|
||||
void int_case_in_gomory_cut(unsigned j) {
|
||||
lp_assert(lia.column_is_int(j) && m_fj.is_pos());
|
||||
lp_assert(is_int(j) && m_fj.is_pos());
|
||||
TRACE("gomory_cut_detail",
|
||||
tout << " k = " << m_k;
|
||||
tout << ", fj: " << m_fj << ", ";
|
||||
|
|
@ -61,6 +63,7 @@ class create_cut {
|
|||
);
|
||||
mpq new_a;
|
||||
if (at_lower(j)) {
|
||||
// here we have the product of new_a*(xj - lb(j)), so new_a*lb(j) is added to m_k
|
||||
new_a = m_fj <= m_one_minus_f ? m_fj / m_one_minus_f : ((1 - m_fj) / m_f);
|
||||
lp_assert(new_a.is_pos());
|
||||
m_k.addmul(new_a, lower_bound(j).x);
|
||||
|
|
@ -68,7 +71,7 @@ class create_cut {
|
|||
}
|
||||
else {
|
||||
lp_assert(at_upper(j));
|
||||
// the upper terms are inverted: therefore we have the minus
|
||||
// here we have the expression new_a*(xj - ub), so new_a*lb(j) is added to m_k
|
||||
new_a = - (m_fj <= m_f ? m_fj / m_f : ((1 - m_fj) / m_one_minus_f));
|
||||
lp_assert(new_a.is_neg());
|
||||
m_k.addmul(new_a, upper_bound(j).x);
|
||||
|
|
@ -84,13 +87,15 @@ class create_cut {
|
|||
}
|
||||
|
||||
void real_case_in_gomory_cut(const mpq & a, unsigned j) {
|
||||
TRACE("gomory_cut_detail_real", tout << "real\n";);
|
||||
TRACE("gomory_cut_detail_real", tout << "j = " << j << ", a = " << a << ", m_k = " << m_k << "\n";);
|
||||
mpq new_a;
|
||||
if (at_lower(j)) {
|
||||
if (a.is_pos()) {
|
||||
// the delta is a (x - f) is positive it has to grow and fight m_one_minus_f
|
||||
new_a = a / m_one_minus_f;
|
||||
}
|
||||
else {
|
||||
// the delta is negative and it works again m_f
|
||||
new_a = - a / m_f;
|
||||
}
|
||||
m_k.addmul(new_a, lower_bound(j).x); // is it a faster operation than
|
||||
|
|
@ -100,16 +105,20 @@ class create_cut {
|
|||
else {
|
||||
lp_assert(at_upper(j));
|
||||
if (a.is_pos()) {
|
||||
// the delta is works again m_f
|
||||
new_a = - a / m_f;
|
||||
}
|
||||
else {
|
||||
// the delta is positive works again m_one_minus_f
|
||||
new_a = a / m_one_minus_f;
|
||||
}
|
||||
m_k.addmul(new_a, upper_bound(j).x); // k += upper_bound(j).x * new_a;
|
||||
m_ex->push_justification(column_upper_bound_constraint(j));
|
||||
}
|
||||
TRACE("gomory_cut_detail_real", tout << a << "*v" << j << " k: " << m_k << "\n";);
|
||||
m_t.add_monomial(new_a, j);
|
||||
TRACE("gomory_cut_detail_real", tout << "add " << new_a << "*v" << j << ", k: " << m_k << "\n";
|
||||
tout << "m_t = "; lia.lra.print_term(m_t, tout) << "\nk: " << m_k << "\n";);
|
||||
|
||||
#if SMALL_CUTS
|
||||
// if (numerator(new_a).is_big()) throw found_big();
|
||||
if (numerator(new_a) > m_big_number) throw found_big();
|
||||
|
|
@ -119,7 +128,6 @@ class create_cut {
|
|||
lia_move report_conflict_from_gomory_cut() {
|
||||
lp_assert(m_k.is_pos());
|
||||
// conflict 0 >= k where k is positive
|
||||
m_k.neg(); // returning 0 <= -k
|
||||
return lia_move::conflict;
|
||||
}
|
||||
|
||||
|
|
@ -131,19 +139,18 @@ class create_cut {
|
|||
if (pol.size() == 1) {
|
||||
TRACE("gomory_cut_detail", tout << "pol.size() is 1" << std::endl;);
|
||||
unsigned v = pol[0].second;
|
||||
lp_assert(lia.column_is_int(v));
|
||||
lp_assert(is_int(v));
|
||||
const mpq& a = pol[0].first;
|
||||
m_k /= a;
|
||||
if (a.is_pos()) { // we have av >= k
|
||||
m_k /= a;
|
||||
if (!m_k.is_int())
|
||||
m_k = ceil(m_k);
|
||||
// switch size
|
||||
m_t.add_monomial(- mpq(1), v);
|
||||
m_k.neg();
|
||||
} else {
|
||||
if (!m_k.is_int())
|
||||
m_k = floor(m_k);
|
||||
m_t.add_monomial(mpq(1), v);
|
||||
} else {
|
||||
m_k /= -a;
|
||||
if (!m_k.is_int())
|
||||
m_k = ceil(m_k);
|
||||
m_t.add_monomial(-mpq(1), v);
|
||||
}
|
||||
} else {
|
||||
m_lcm_den = lcm(m_lcm_den, denominator(m_k));
|
||||
|
|
@ -153,14 +160,12 @@ class create_cut {
|
|||
// normalize coefficients of integer parameters to be integers.
|
||||
for (auto & pi: pol) {
|
||||
pi.first *= m_lcm_den;
|
||||
SASSERT(!lia.column_is_int(pi.second) || pi.first.is_int());
|
||||
SASSERT(!is_int(pi.second) || pi.first.is_int());
|
||||
}
|
||||
m_k *= m_lcm_den;
|
||||
}
|
||||
// negate everything to return -pol <= -m_k
|
||||
for (const auto & pi: pol)
|
||||
m_t.add_monomial(-pi.first, pi.second);
|
||||
m_k.neg();
|
||||
m_t.add_monomial(pi.first, pi.second);
|
||||
}
|
||||
TRACE("gomory_cut_detail", tout << "k = " << m_k << std::endl;);
|
||||
lp_assert(m_k.is_int());
|
||||
|
|
@ -207,7 +212,7 @@ class create_cut {
|
|||
}
|
||||
|
||||
void dump_declaration(std::ostream& out, unsigned v) const {
|
||||
out << "(declare-const " << var_name(v) << (lia.column_is_int(v) ? " Int" : " Real") << ")\n";
|
||||
out << "(declare-const " << var_name(v) << (is_int(v) ? " Int" : " Real") << ")\n";
|
||||
}
|
||||
|
||||
void dump_declarations(std::ostream& out) const {
|
||||
|
|
@ -313,6 +318,11 @@ public:
|
|||
|
||||
// use -p.coeff() to make the format compatible with the format used in: Integrating Simplex with DPLL(T)
|
||||
try {
|
||||
if (lia.is_fixed(j)) {
|
||||
m_ex->push_justification(column_lower_bound_constraint(j));
|
||||
m_ex->push_justification(column_upper_bound_constraint(j));
|
||||
continue;
|
||||
}
|
||||
if (is_real(j)) {
|
||||
real_case_in_gomory_cut(- p.coeff(), j);
|
||||
}
|
||||
|
|
@ -334,8 +344,8 @@ public:
|
|||
return report_conflict_from_gomory_cut();
|
||||
if (some_int_columns)
|
||||
adjust_term_and_k_for_some_ints_case_gomory();
|
||||
lp_assert(lia.current_solution_is_inf_on_cut());
|
||||
TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout););
|
||||
lp_assert(lia.current_solution_is_inf_on_cut());
|
||||
lia.lra.subs_term_columns(m_t);
|
||||
TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t.coeffs_as_vector(), tout << "gomory cut:"); tout << " <= " << m_k << std::endl;);
|
||||
return lia_move::cut;
|
||||
|
|
@ -441,7 +451,7 @@ lia_move gomory::operator()() {
|
|||
const row_strip<mpq>& row = lra.get_row(r);
|
||||
SASSERT(lra.row_is_correct(r));
|
||||
SASSERT(is_gomory_cut_target(row));
|
||||
lia.m_upper = true;
|
||||
lia.m_upper = false;
|
||||
return cut(lia.m_t, lia.m_k, lia.m_ex, j, row);
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue