From 6ea0bcb454acee3d668f828caaa1b821ff8dc1a6 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 7 Mar 2020 13:57:08 -0800 Subject: [PATCH] round the bound for columns and terms when it can be deduced that they are integral Signed-off-by: Lev Nachmanson --- src/math/lp/hnf_cutter.cpp | 4 ++-- src/math/lp/lar_solver.cpp | 44 ++++++++++++++++++++++++++++++++------ src/math/lp/lar_solver.h | 3 +++ src/math/lp/var_register.h | 4 ---- 4 files changed, 43 insertions(+), 12 deletions(-) diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp index ace42ca1c..5b675fa64 100644 --- a/src/math/lp/hnf_cutter.cpp +++ b/src/math/lp/hnf_cutter.cpp @@ -50,7 +50,7 @@ namespace lp { m_constraints_for_explanation.push_back(ci); for (const auto &p : *t) { - m_var_register.add_var(p.var()); + m_var_register.add_var(p.var(), true); // hnf only deals with integral variables for now mpq t = abs(ceil(p.coeff())); if (t > m_abs_max) m_abs_max = t; @@ -63,7 +63,7 @@ namespace lp { void hnf_cutter::initialize_row(unsigned i) { mpq sign = m_terms_upper[i]? one_of_type(): - one_of_type(); - m_A.init_row_from_container(i, * m_terms[i], [this](unsigned j) { return m_var_register.add_var(j);}, sign); + m_A.init_row_from_container(i, * m_terms[i], [this](unsigned j) { return m_var_register.add_var(j, true);}, sign);// hnf only deals with integral variables for now } void hnf_cutter::init_matrix_A() { diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 47e10d488..89c518bf6 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1539,6 +1539,13 @@ bool lar_solver::term_is_int(const lar_term * t) const { return true; } +bool lar_solver::term_is_int(const vector>& coeffs) const { + for (auto const& p : coeffs) + if (! (column_is_int(p.second) && p.first.is_int())) + return false; + return true; +} + bool lar_solver::var_is_int(var_index v) const { if (is_term(v)) { lar_term const& t = get_term(v); @@ -1701,7 +1708,7 @@ bool lar_solver::all_vars_are_registered(const vector> var_index lar_solver::add_term(const vector> & coeffs, unsigned ext_i) { TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";); - m_term_register.add_var(ext_i); + m_term_register.add_var(ext_i, term_is_int(coeffs)); lp_assert(all_vars_are_registered(coeffs)); if (strategy_is_undecided()) return add_term_undecided(coeffs); @@ -1774,12 +1781,33 @@ void lar_solver::activate(constraint_index ci) { update_column_type_and_bound(c.column(), c.kind(), c.rhs(), ci); } +mpq lar_solver::adjust_bound_for_int(lpvar j, lconstraint_kind k, const mpq& bound) { + if (!column_is_int(j)) + return bound; + switch (k) { + case LT: + case LE: + return floor(bound); + case GT: + case GE: + return ceil(bound); + case EQ: + return bound; + default: + UNREACHABLE(); + } + + return bound; + +} + constraint_index lar_solver::mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) { TRACE("lar_solver", tout << "j = " << j << " " << lconstraint_kind_string(kind) << " " << right_side<< std::endl;); constraint_index ci; if (!is_term(j)) { // j is a var - lp_assert(bound_is_integer_for_integer_column(j, right_side)); - ci = m_constraints.add_var_constraint(j, kind, right_side); + mpq rs = adjust_bound_for_int(j, kind, right_side); + lp_assert(bound_is_integer_for_integer_column(j, rs)); + ci = m_constraints.add_var_constraint(j, kind, rs); } else { ci = add_var_bound_on_constraint_for_term(j, kind, right_side); @@ -1821,9 +1849,11 @@ constraint_index lar_solver::add_var_bound_on_constraint_for_term(var_index j, l unsigned adjusted_term_index = adjust_term_index(j); // lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int()); unsigned term_j; - lar_term const* term = m_terms[adjusted_term_index]; + lar_term const* term = m_terms[adjusted_term_index]; if (m_var_register.external_is_used(j, term_j)) { - return m_constraints.add_term_constraint(term_j, term, kind, right_side); + mpq rs = adjust_bound_for_int(term_j, kind, right_side); + lp_assert(bound_is_integer_for_integer_column(term_j, rs)); + return m_constraints.add_term_constraint(term_j, term, kind, rs); } else { return add_constraint_from_term_and_create_new_column_row(j, term, kind, right_side); @@ -1834,7 +1864,9 @@ constraint_index lar_solver::add_constraint_from_term_and_create_new_column_row( unsigned term_j, const lar_term* term, lconstraint_kind kind, const mpq & right_side) { add_row_from_term_no_constraint(term, term_j); unsigned j = A_r().column_count() - 1; - return m_constraints.add_term_constraint(j, term, kind, right_side); + mpq rs = adjust_bound_for_int(j, kind, right_side); + lp_assert(bound_is_integer_for_integer_column(j, rs)); + return m_constraints.add_term_constraint(j, term, kind, rs); } void lar_solver::decide_on_strategy_and_adjust_initial_state() { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 6e59c6607..333ddd65b 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -159,6 +159,8 @@ public: bool term_is_int(const lar_term * t) const; + bool term_is_int(const vector> & coeffs) const; + bool var_is_int(var_index v) const; void add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int); @@ -167,6 +169,7 @@ public: void add_new_var_to_core_fields_for_mpq(bool register_in_basis); + mpq adjust_bound_for_int(lpvar j, lconstraint_kind, const mpq&); // terms diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h index 6dedc69e3..8f0e0e882 100644 --- a/src/math/lp/var_register.h +++ b/src/math/lp/var_register.h @@ -41,10 +41,6 @@ class var_register { public: var_register(unsigned offset) : m_local_offset(offset) {} - unsigned add_var(unsigned user_var) { - return add_var(user_var, true); - } - void set_name(unsigned j, std::string name) { m_local_to_external[j].set_name(name); }