expose only necessary methods of lar_solver

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/gomory.cpp

@@ -282,7 +282,7 @@ class create_cut {
     void dump(std::ostream& out) {
         out << "applying cut at:\n"; print_linear_combination_indices_only<row_strip<mpq>, mpq>(m_row, out); out << std::endl;
         for (auto & p : m_row) {
-            lia.lra.m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), out);
+            lia.lra.print_column_info(p.var(), out);
         }
         out << "inf_col = " << m_inf_col << std::endl;
     }

src/math/lp/hnf_cutter.cpp

@@ -155,10 +155,12 @@ namespace lp  {
 
     bool hnf_cutter::overflow() const { return m_overflow; }
 
-    lia_move hnf_cutter::create_cut(lar_term& t, mpq& k, explanation* ex, bool & upper, const vector<mpq> & x0) {
-        // we suppose that x0 has at least one non integer element 
-        (void)x0;
-
+    lia_move hnf_cutter::create_cut(lar_term& t, mpq& k, explanation* ex, bool & upper
+#ifdef Z3DEBUG
+                                    , const vector<mpq> & x0
+                                    // we suppose that x0 has at least one non integer element 
+#endif                                                                                                            
+                                    ) {
         init_matrix_A();
         svector<unsigned> basis_rows;
         mpq big_number = m_abs_max.expt(3);
@@ -179,7 +181,10 @@ namespace lp  {
 
         hnf<general_matrix> h(m_A, d);        
         vector<mpq> b = create_b(basis_rows);
+#ifdef Z3DEBUG
         lp_assert(m_A * x0 == b);
+#endif
+
         find_h_minus_1_b(h.W(), b);
         int cut_row = find_cut_row_index(b);
 
@@ -238,11 +243,13 @@ namespace lp  {
               tout << lra.constraints();
               );
 #ifdef Z3DEBUG
-        vector<mpq> x0 = transform_to_local_columns(lra.m_mpq_lar_core_solver.m_r_x);
-#else
-        vector<mpq> x0;
+        vector<mpq> x0 = transform_to_local_columns(lra.r_x());
+#endif
+        lia_move r =  create_cut(lia.m_t, lia.m_k, lia.m_ex, lia.m_upper
+#ifdef Z3DEBUG
+                                 , x0
 #endif
-        lia_move r =  create_cut(lia.m_t, lia.m_k, lia.m_ex, lia.m_upper, x0);
+                                 );
 
         if (r == lia_move::cut) {      
             TRACE("hnf_cut",

src/math/lp/int_branch.cpp

@@ -56,7 +56,7 @@ namespace lp {
     }
 
     bool int_branch::left_branch_is_more_narrow_than_right(unsigned j) {
-        switch (lra.m_mpq_lar_core_solver.m_r_solver.m_column_types[j] ) {
+        switch (lra.get_column_type(j)) {
         case column_type::fixed:
             return false;
         case column_type::boxed: {

src/math/lp/int_branch.h

@@ -17,6 +17,8 @@ Revision History:
 --*/
 #pragma once
 
+#include "math/lp/lar_solver.h"
+#include "math/lp/int_solver.h"
 #include "math/lp/lia_move.h"
 
 namespace lp {

src/math/lp/int_cube.cpp

@@ -27,7 +27,7 @@ namespace lp {
     lia_move int_cube::operator()() {
         lia.settings().stats().m_cube_calls++;
         TRACE("cube",
-              for (unsigned j = 0; j < lra.A_r().column_count(); j++)
+              for (unsigned j = 0; j < lra.number_of_vars(); j++)
                   lia.display_column(tout, j);
               tout << lra.constraints();
               );

src/math/lp/int_gcd_test.cpp

@@ -56,7 +56,7 @@ namespace lp {
     }
 
     bool int_gcd_test::gcd_test() {
-        auto & A = lra.A_r(); // getting the matrix
+        const auto & A = lra.A_r(); // getting the matrix
         for (unsigned i = 0; i < A.row_count(); i++)
             if (!gcd_test_for_row(A, i)) 
                 return false;        
@@ -71,10 +71,9 @@ namespace lp {
         return r;
     }
 
-    bool int_gcd_test::gcd_test_for_row(static_matrix<mpq, numeric_pair<mpq>> & A, unsigned i) {
+    bool int_gcd_test::gcd_test_for_row(const static_matrix<mpq, numeric_pair<mpq>> & A, unsigned i) {
         auto const& row = A.m_rows[i];
-        auto & lcs = lra.m_mpq_lar_core_solver;
-        unsigned basic_var = lcs.m_r_basis[i];
+        unsigned basic_var = lra.r_basis()[i];
 
         if (!lia.column_is_int(basic_var) || lia.get_value(basic_var).is_int())
             return true;
@@ -154,7 +153,7 @@ namespace lp {
         unsigned j;
         for (const auto & c : row) {
             j = c.var();
-            TRACE("ext_gcd_test", tout << "col = "; lra.m_mpq_lar_core_solver.m_r_solver.print_column_bound_info(j, tout););
+            TRACE("ext_gcd_test", tout << "col = "; lra.print_column_info(j, tout););
             const mpq & a = c.coeff();
             if (lra.column_is_fixed(j))
                 continue;

src/math/lp/int_gcd_test.h

@@ -38,7 +38,7 @@ namespace lp {
         unsigned m_delay;
 
         bool gcd_test();
-        bool gcd_test_for_row(static_matrix<mpq, numeric_pair<mpq>> & A, unsigned i);
+        bool gcd_test_for_row(const static_matrix<mpq, numeric_pair<mpq>> & A, unsigned i);
         bool ext_gcd_test(const row_strip<mpq> & row,
                                         mpq const & least_coeff, 
                                         mpq const & lcm_den,

src/math/lp/int_solver.cpp

@@ -126,17 +126,13 @@ int_solver::int_solver(lar_solver& lar_slv) :
 // this will allow to enable and disable tracking of the pivot rows
 struct check_return_helper {
     lar_solver&      lra;
-    lar_core_solver& lrac;
     bool             m_track_pivoted_rows;
     check_return_helper(lar_solver& ls) :
         lra(ls),
-        lrac(ls.m_mpq_lar_core_solver),
         m_track_pivoted_rows(lra.get_track_pivoted_rows()) {
-        TRACE("pivoted_rows", tout << "pivoted rows = " << lrac.m_r_solver.m_pivoted_rows->size() << std::endl;);
         lra.set_track_pivoted_rows(false);
     }
     ~check_return_helper() {
-        TRACE("pivoted_rows", tout << "pivoted rows = " << lrac.m_r_solver.m_pivoted_rows->size() << std::endl;);
         lra.set_track_pivoted_rows(m_track_pivoted_rows);
     }
 };

src/math/lp/lar_solver.cpp

@@ -7,8 +7,6 @@
 namespace lp {
 
 ////////////////// methods ////////////////////////////////
-static_matrix<mpq, numeric_pair<mpq>> & lar_solver::A_r() { return m_mpq_lar_core_solver.m_r_A;}
-static_matrix<mpq, numeric_pair<mpq>> const & lar_solver::A_r() const { return m_mpq_lar_core_solver.m_r_A;}
 static_matrix<double, double> & lar_solver::A_d() { return m_mpq_lar_core_solver.m_d_A;}
 static_matrix<double, double > const & lar_solver::A_d() const { return m_mpq_lar_core_solver.m_d_A;}
 
@@ -965,10 +963,6 @@ bool lar_solver::try_to_set_fixed(column_info<mpq> & ci) {
     return false;
 }
 
-column_type lar_solver::get_column_type(unsigned j) const{
-    return m_mpq_lar_core_solver.m_column_types[j];
-}
-
 bool lar_solver::all_constrained_variables_are_registered(const vector<std::pair<mpq, var_index>>& left_side) {
     for (auto it : left_side) {
         if (! var_is_registered(it.second))