tv alignment, code review comments

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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;

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();
     }

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; }

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:
 --*/

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() {

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) {
+bool lar_solver::tighten_term_bounds_by_delta(tv const& t, const impq& delta) {
-    SASSERT(!tv::is_term(term_index));
+    SASSERT(t.is_term());
-    unsigned tj = tv::mask_term(term_index);
+    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 {
+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 {
-    unsigned tj = tv::mask_term(term_index);
+    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());

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(get_term(j), out) << "\n";
-            print_term_as_indices(t, out) << "\n";
             
-        } else if(column_corresponds_to_term(j)) { 
+        } else if (column_corresponds_to_term(j)) { 
-            const lar_term& t = * m_terms[tv::unmask_term(m_var_register.local_to_external(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);