From 080dbb13b0adaf9620273f1e29ad7892c79f7b25 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 5 Apr 2020 03:35:19 -0700
Subject: [PATCH] tv alignment, code review comments
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/math/lp/gomory.cpp | 3 +++
src/math/lp/hnf_cutter.cpp | 8 ++++----
src/math/lp/hnf_cutter.h | 2 +-
src/math/lp/int_branch.cpp | 2 +-
src/math/lp/int_cube.cpp | 2 +-
src/math/lp/lar_solver.cpp | 22 +++++++++++-----------
src/math/lp/lar_solver.h | 17 +++++++++++------
7 files changed, 32 insertions(+), 24 deletions(-)
diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index 37b201497..62bd4ba7e 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -346,6 +346,9 @@ public:
adjust_term_and_k_for_some_ints_case_gomory();
TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout););
lp_assert(lia.current_solution_is_inf_on_cut());
+ // NSB code review: this is also used in nla_core.
+ // but it isn't consistent: when theory_lra accesses lar_solver::get_term, the term that is returned uses
+ // column indices, not terms.
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;
diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp
index 7c8dd42d7..cbc5eb4f8 100644
--- a/src/math/lp/hnf_cutter.cpp
+++ b/src/math/lp/hnf_cutter.cpp
@@ -201,13 +201,13 @@ namespace lp {
svector<unsigned> hnf_cutter::vars() const { return m_var_register.vars(); }
- void hnf_cutter::try_add_term_to_A_for_hnf(unsigned i) {
+ void hnf_cutter::try_add_term_to_A_for_hnf(tv const &i) {
mpq rs;
- const lar_term* t = lra.terms()[i];
+ const lar_term& t = lra.get_term(i);
constraint_index ci;
bool upper_bound;
if (!is_full() && lra.get_equality_and_right_side_for_term_on_current_x(i, rs, ci, upper_bound)) {
- add_term(t, rs, ci, upper_bound);
+ add_term(&t, rs, ci, upper_bound);
}
}
@@ -221,7 +221,7 @@ namespace lp {
bool hnf_cutter::init_terms_for_hnf_cut() {
clear();
for (unsigned i = 0; i < lra.terms().size() && !is_full(); i++) {
- try_add_term_to_A_for_hnf(i);
+ try_add_term_to_A_for_hnf(tv::term(i));
}
return hnf_has_var_with_non_integral_value();
}
diff --git a/src/math/lp/hnf_cutter.h b/src/math/lp/hnf_cutter.h
index 027f2c7b1..dd0f7b093 100644
--- a/src/math/lp/hnf_cutter.h
+++ b/src/math/lp/hnf_cutter.h
@@ -49,7 +49,7 @@ public:
private:
bool init_terms_for_hnf_cut();
bool hnf_has_var_with_non_integral_value() const;
- void try_add_term_to_A_for_hnf(unsigned i);
+ void try_add_term_to_A_for_hnf(tv const& i);
unsigned terms_count() const { return m_terms.size(); }
const mpq & abs_max() const { return m_abs_max; }
diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp
index d840888e5..c9ab221eb 100644
--- a/src/math/lp/int_branch.cpp
+++ b/src/math/lp/int_branch.cpp
@@ -10,8 +10,8 @@ Abstract:
Branch heuristic
Author:
- Nikolaj Bjorner (nbjorner)
Lev Nachmanson (levnach)
+ Nikolaj Bjorner (nbjorner)
Revision History:
--*/
diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp
index 1f918bc7c..24609ec25 100644
--- a/src/math/lp/int_cube.cpp
+++ b/src/math/lp/int_cube.cpp
@@ -64,7 +64,7 @@ namespace lp {
TRACE("cube", lra.print_term_as_indices(*t, tout); tout << ", delta = " << delta;);
if (is_zero(delta))
return true;
- return lra.tighten_term_bounds_by_delta(i, delta);
+ return lra.tighten_term_bounds_by_delta(tv::term(i), delta);
}
bool int_cube::tighten_terms_for_cube() {
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index f7a1c1a19..99c79f5e3 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -113,7 +113,7 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be,
}
rs_of_evidence /= ratio;
} else {
- lar_term & t = *m_terms[tv::unmask_term(be.m_j)];
+ lar_term const& t = get_term(be.m_j);
auto first_coeff = t.begin();
unsigned j = (*first_coeff).var().index();
auto it = coeff_map.find(j);
@@ -182,7 +182,7 @@ void lar_solver::substitute_basis_var_in_terms_for_row(unsigned i) {
}
void lar_solver::calculate_implied_bounds_for_row(unsigned i, lp_bound_propagator & bp) {
- if(use_tableau()) {
+ if (use_tableau()) {
analyze_new_bounds_on_row_tableau(i, bp);
} else {
m_mpq_lar_core_solver.calculate_pivot_row(i);
@@ -2192,9 +2192,9 @@ var_index lar_solver::to_column(unsigned ext_j) const {
return m_var_register.external_to_local(ext_j);
}
-bool lar_solver::tighten_term_bounds_by_delta(unsigned term_index, const impq& delta) {
- SASSERT(!tv::is_term(term_index));
- unsigned tj = tv::mask_term(term_index);
+bool lar_solver::tighten_term_bounds_by_delta(tv const& t, const impq& delta) {
+ SASSERT(t.is_term());
+ unsigned tj = t.index();
unsigned j;
if (m_var_register.external_is_used(tj, j) == false)
return true; // the term is not a column so it has no bounds
@@ -2282,21 +2282,21 @@ bool lar_solver::sum_first_coords(const lar_term& t, mpq & val) const {
return true;
}
-bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term_index, mpq & rs, constraint_index& ci, bool &upper_bound) const {
- unsigned tj = tv::mask_term(term_index);
+bool lar_solver::get_equality_and_right_side_for_term_on_current_x(tv const& t, mpq & rs, constraint_index& ci, bool &upper_bound) const {
+ lp_assert(t.is_term())
unsigned j;
bool is_int;
- if (m_var_register.external_is_used(tj, j, is_int) == false)
+ if (m_var_register.external_is_used(t.index(), j, is_int) == false)
return false; // the term does not have a bound because it does not correspond to a column
if (!is_int) // todo - allow for the next version of hnf
return false;
bool rs_is_calculated = false;
mpq b;
bool is_strict;
- const lar_term& t = *terms()[term_index];
+ const lar_term& term = get_term(t);
if (has_upper_bound(j, ci, b, is_strict) && !is_strict) {
lp_assert(b.is_int());
- if (!sum_first_coords(t, rs))
+ if (!sum_first_coords(term, rs))
return false;
rs_is_calculated = true;
if (rs == b) {
@@ -2306,7 +2306,7 @@ bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term
}
if (has_lower_bound(j, ci, b, is_strict) && !is_strict) {
if (!rs_is_calculated){
- if (!sum_first_coords(t, rs))
+ if (!sum_first_coords(term, rs))
return false;
}
lp_assert(b.is_int());
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index f4270eddd..e28737a7a 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -583,6 +583,11 @@ public:
return m_columns_to_ul_pairs()[j].lower_bound_witness();
}
+ // NSB code review - seems superfluous to translate back and forth because
+ // get_term(..) that is exposed over API does not ensure that columns that
+ // are based on terms are translated back to term indices.
+ // would be better to have consistent typing, either lar_term uses cv (and not tv)
+ // or they are created to use tv consistently.
void subs_term_columns(lar_term& t) {
svector<std::pair<unsigned,unsigned>> columns_to_subs;
for (const auto & m : t) {
@@ -594,15 +599,15 @@ public:
t.subst_index(p.first, p.second);
}
}
+
std::ostream& print_column_info(unsigned j, std::ostream& out) const {
m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
if (tv::is_term(j)) {
- const lar_term& t = * m_terms[tv::unmask_term(j)];
- print_term_as_indices(t, out) << "\n";
+ print_term_as_indices(get_term(j), out) << "\n";
- } else if(column_corresponds_to_term(j)) {
- const lar_term& t = * m_terms[tv::unmask_term(m_var_register.local_to_external(j))];
+ } else if (column_corresponds_to_term(j)) {
+ const lar_term& t = get_term(m_var_register.local_to_external(j));
print_term_as_indices(t, out) << "\n";
}
return out;
@@ -630,7 +635,7 @@ public:
bool column_corresponds_to_term(unsigned) const;
void catch_up_in_updating_int_solver();
var_index to_column(unsigned ext_j) const;
- bool tighten_term_bounds_by_delta(unsigned, const impq&);
+ bool tighten_term_bounds_by_delta(tv const& t, const impq&);
void round_to_integer_solution();
void fix_terms_with_rounded_columns();
void update_delta_for_terms(const impq & delta, unsigned j, const vector<unsigned>&);
@@ -639,7 +644,7 @@ public:
unsigned row_count() const { return A_r().row_count(); }
const vector<unsigned> & r_basis() const { return m_mpq_lar_core_solver.r_basis(); }
const vector<unsigned> & r_nbasis() const { return m_mpq_lar_core_solver.r_nbasis(); }
- bool get_equality_and_right_side_for_term_on_current_x(unsigned i, mpq &rs, constraint_index& ci, bool &upper_bound) const;
+ bool get_equality_and_right_side_for_term_on_current_x(tv const& t, mpq &rs, constraint_index& ci, bool &upper_bound) const;
bool remove_from_basis(unsigned);
lar_term get_term_to_maximize(unsigned ext_j) const;
void set_cut_strategy(unsigned cut_frequency);