mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 11:25:51 +00:00
work on Gomory cut
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev
parent
5bbe0508e4
commit
ca3ce964ce
6 changed files with 160 additions and 47 deletions
|
|
@ -23,6 +23,16 @@
|
|||
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
|
||||
|
|
@ -43,32 +53,31 @@ class gomory::imp {
|
|||
void int_case_in_gomory_cut(const mpq & a, unsigned j,
|
||||
mpq & lcm_den, const mpq& f0, const mpq& one_minus_f0) {
|
||||
lp_assert(is_int(j) && !a.is_int());
|
||||
mpq fj = int_solver::fractional_part(a);
|
||||
lp_assert(fj.is_pos());
|
||||
mpq fj = fractional_part(a);
|
||||
TRACE("gomory_cut_detail",
|
||||
tout << a << " j=" << j << " k = " << m_k;
|
||||
tout << ", fj: " << fj << ", ";
|
||||
tout << "f0: " << f0 << ", ";
|
||||
tout << "1 - f0: " << 1 - f0 << ", ";
|
||||
tout << "a - fj = " << a - fj << ", ";
|
||||
tout << (at_lower(j)?"at_lower":"at_upper")<< std::endl;
|
||||
);
|
||||
lp_assert(fj.is_pos() && (a - fj).is_int());
|
||||
mpq new_a;
|
||||
mpq one_minus_fj = 1 - fj;
|
||||
if (at_lower(j)) {
|
||||
new_a = fj < one_minus_f0? fj / one_minus_f0 : one_minus_fj / f0;
|
||||
new_a = fj < one_minus_f0? fj / one_minus_f0 : (- one_minus_fj / f0);
|
||||
m_k.addmul(new_a, lower_bound(j).x);
|
||||
m_ex.push_justification(column_lower_bound_constraint(j), new_a);
|
||||
}
|
||||
else {
|
||||
lp_assert(at_upper(j));
|
||||
// the upper terms are inverted: therefore we have the minus
|
||||
new_a = - (fj < f0? fj / f0 : one_minus_fj / one_minus_f0);
|
||||
new_a = - (fj < f0? fj / f0 : (- one_minus_fj / one_minus_f0));
|
||||
m_k.addmul(new_a, upper_bound(j).x);
|
||||
m_ex.push_justification(column_upper_bound_constraint(j), new_a);
|
||||
}
|
||||
TRACE("gomory_cut_detail", tout << "new_a: " << new_a << " k: " << m_k << "\n";);
|
||||
m_t.add_monomial(new_a, j);
|
||||
lcm_den = lcm(lcm_den, denominator(new_a));
|
||||
TRACE("gomory_cut_detail", tout << "new_a = " << new_a << ", k = " << m_k << ", lcm_den = " << lcm_den << "\n";);
|
||||
}
|
||||
|
||||
void real_case_in_gomory_cut(const mpq & a, unsigned x_j, const mpq& f0, const mpq& one_minus_f0) {
|
||||
|
|
@ -150,10 +159,117 @@ class gomory::imp {
|
|||
TRACE("gomory_cut_detail", tout << "k = " << m_k << std::endl;);
|
||||
lp_assert(m_k.is_int());
|
||||
}
|
||||
|
||||
std::string var_name(unsigned j) const {
|
||||
return std::string("x") + std::to_string(j);
|
||||
}
|
||||
|
||||
void dump_coeff_val(std::ostream & out, const mpq & a) const {
|
||||
if (a.is_int()) {
|
||||
if ( a >= zero_of_type<mpq>())
|
||||
out << a;
|
||||
else {
|
||||
out << "( - " << - a << ") ";
|
||||
}
|
||||
} else {
|
||||
if ( a >= zero_of_type<mpq>())
|
||||
out << "(div " << numerator(a) << " " << denominator(a) << ")";
|
||||
else {
|
||||
out << "(- ( div " << numerator(-a) << " " << denominator(-a) << "))";
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
void dump_coeff(std::ostream & out, const T& c) const {
|
||||
out << "( * ";
|
||||
dump_coeff_val(out, c.coeff());
|
||||
out << " " << var_name(c.var()) << ")";
|
||||
}
|
||||
|
||||
void dump_row_coefficients(std::ostream & out) const {
|
||||
for (const auto& p : m_row) {
|
||||
dump_coeff(out, p);
|
||||
}
|
||||
}
|
||||
|
||||
void dump_the_row(std::ostream& out) const {
|
||||
out << "; the row\n";
|
||||
out << "(assert ( = ( + ";
|
||||
dump_row_coefficients(out);
|
||||
out << ") 0))\n";
|
||||
}
|
||||
|
||||
void dump_declarations(std::ostream& out) const {
|
||||
// for a column j the var name is vj
|
||||
for (const auto & p : m_row) {
|
||||
out << "(declare-fun " << var_name(p.var()) << " () "
|
||||
<< (is_int(p.var())? "Int" : "Real") << ")\n";
|
||||
}
|
||||
}
|
||||
|
||||
void dump_lower_bound_expl(std::ostream & out, unsigned j) const {
|
||||
out << "(assert ( >= " << var_name(j) << " " << lower_bound(j).x << "))\n";
|
||||
}
|
||||
void dump_upper_bound_expl(std::ostream & out, unsigned j) const {
|
||||
out << "(assert ( <= " << var_name(j) << " " << upper_bound(j).x << "))\n";
|
||||
}
|
||||
|
||||
void dump_explanations(std::ostream& out) const {
|
||||
for (const auto & p : m_row) {
|
||||
unsigned j = p.var();
|
||||
if (j == m_inf_col) {
|
||||
continue;
|
||||
}
|
||||
|
||||
if (column_is_fixed(j)) {
|
||||
dump_lower_bound_expl(out, j);
|
||||
dump_upper_bound_expl(out, j);
|
||||
continue;
|
||||
}
|
||||
|
||||
if (at_lower(j)) {
|
||||
dump_lower_bound_expl(out, j);
|
||||
} else {
|
||||
dump_upper_bound_expl(out, j);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void dump_terms_coefficients(std::ostream & out) const {
|
||||
for (const auto& p : m_t) {
|
||||
dump_coeff(out, p);
|
||||
}
|
||||
}
|
||||
|
||||
void dump_term_sum(std::ostream & out) const {
|
||||
out << "( + ";
|
||||
dump_terms_coefficients(out);
|
||||
out << ")";
|
||||
}
|
||||
|
||||
void dump_term_le_k(std::ostream & out) const {
|
||||
out << "( <= ";
|
||||
dump_term_sum(out);
|
||||
out << m_k << ")";
|
||||
}
|
||||
void dump_the_cut_assert(std::ostream & out) const {
|
||||
out <<"(assert (not ";
|
||||
dump_term_le_k(out);
|
||||
out << "))\n";
|
||||
}
|
||||
void dump_cut_and_constraints_as_smt_lemma(std::ostream& out) const {
|
||||
dump_declarations(out);
|
||||
dump_the_row(out);
|
||||
dump_explanations(out);
|
||||
dump_the_cut_assert(out);
|
||||
out << "(check-sat)\n";
|
||||
}
|
||||
public:
|
||||
lia_move create_cut() {
|
||||
TRACE("gomory_cut",
|
||||
tout << "applying cut at:\n"; m_int_solver.m_lar_solver->print_row(m_row, tout); tout << std::endl;
|
||||
tout << "applying cut at:\n"; print_linear_combination_of_column_indices_only(m_row, tout); tout << std::endl;
|
||||
for (auto & p : m_row) {
|
||||
m_int_solver.m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), tout);
|
||||
}
|
||||
|
|
@ -164,7 +280,11 @@ public:
|
|||
m_k = 1;
|
||||
mpq lcm_den(1);
|
||||
bool some_int_columns = false;
|
||||
mpq f0 = int_solver::fractional_part(get_value(m_inf_col));
|
||||
mpq f0 = fractional_part(get_value(m_inf_col));
|
||||
TRACE("gomory_cut_detail", tout << "f0: " << f0 << ", ";
|
||||
tout << "1 - f0: " << 1 - f0 << ", get_value(m_inf_col).x - f0 = " << get_value(m_inf_col).x - f0;);
|
||||
lp_assert(f0.is_pos() && (get_value(m_inf_col).x - f0).is_int());
|
||||
|
||||
mpq one_min_f0 = 1 - f0;
|
||||
for (const auto & p : m_row) {
|
||||
unsigned j = p.var();
|
||||
|
|
@ -194,7 +314,8 @@ public:
|
|||
adjust_term_and_k_for_some_ints_case_gomory(lcm_den);
|
||||
lp_assert(m_int_solver.current_solution_is_inf_on_cut());
|
||||
m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k);
|
||||
TRACE("gomory_cut", tout<<"gomory cut:"; m_int_solver.m_lar_solver->print_term(m_t, tout); tout << " <= " << m_k << std::endl;);
|
||||
TRACE("gomory_cut", tout<<"gomory cut:"; print_linear_combination_of_column_indices_only(m_t, tout); tout << " <= " << m_k << std::endl;);
|
||||
TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout););
|
||||
return lia_move::cut;
|
||||
}
|
||||
imp(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip<mpq>& row, const int_solver& int_slv ) :
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue