na

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

src/math/lp/gomory.cpp

@@ -355,7 +355,7 @@ public:
 };
 
 lia_move gomory::cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip<mpq>& row) {
-    create_cut cc(t, k, ex, basic_inf_int_j, row, s);
+    create_cut cc(t, k, ex, basic_inf_int_j, row, lia);
     return cc.cut();
 }
 
@@ -364,10 +364,10 @@ bool gomory::is_gomory_cut_target(const row_strip<mpq>& row) {
     unsigned j;
     for (const auto & p : row) {
         j = p.var();
-        if (!s.is_base(j) && (!s.at_bound(j) || !is_zero(s.get_value(j).y))) {
+        if (!lia.is_base(j) && (!lia.at_bound(j) || !is_zero(lia.get_value(j).y))) {
             TRACE("gomory_cut", tout << "row is not gomory cut target:\n";
-                  s.display_column(tout, j);
-                  tout << "infinitesimal: " << !is_zero(s.get_value(j).y) << "\n";);
+                  lia.display_column(tout, j);
+                  tout << "infinitesimal: " << !is_zero(lia.get_value(j).y) << "\n";);
             return false;
         }
     }
@@ -388,17 +388,17 @@ int gomory::find_basic_var() {
     // Prefer boxed to non-boxed
     // Prefer smaller ranges
 
-    for (unsigned j : s.lra.r_basis()) {
-        if (!s.column_is_int_inf(j))
+    for (unsigned j : lra.r_basis()) {
+        if (!lia.column_is_int_inf(j))
             continue;
-        const row_strip<mpq>& row = s.lra.get_row(s.row_of_basic_column(j));
+        const row_strip<mpq>& row = lra.get_row(lia.row_of_basic_column(j));
         if (!is_gomory_cut_target(row)) 
             continue;
 
 #if 0
         if (is_boxed(j) && (min_row_size == UINT_MAX || 4*row.size() < 5*min_row_size)) {
             lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
-            auto new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x;
+            auto new_range = lclia.m_r_upper_bounds()[j].x - lclia.m_r_lower_bounds()[j].x;
             if (!boxed) {
                 result = j;
                 n = 1;
@@ -419,7 +419,7 @@ int gomory::find_basic_var() {
 
         if (min_row_size == UINT_MAX || 
             2*row.size() < min_row_size || 
-            (4*row.size() < 5*min_row_size && s.random() % (++n) == 0)) {
+            (4*row.size() < 5*min_row_size && lia.random() % (++n) == 0)) {
             result = j;
             n = 1;
             min_row_size = std::min(min_row_size, row.size());
@@ -428,24 +428,24 @@ int gomory::find_basic_var() {
     return result;
 }
     
-lia_move gomory::operator()(lar_term & t, mpq & k, explanation* ex, bool& upper) {
-    if (s.lra.move_non_basic_columns_to_bounds()) {
-        lp_status st = s.lra.find_feasible_solution();
+lia_move gomory::operator()() {
+    if (lra.move_non_basic_columns_to_bounds()) {
+        lp_status st = lra.find_feasible_solution();
         (void)st;
         lp_assert(st == lp_status::FEASIBLE || st == lp_status::OPTIMAL);
     }
         
     int j = find_basic_var();
     if (j == -1) return lia_move::undef;
-    unsigned r = s.row_of_basic_column(j);
-    const row_strip<mpq>& row = s.lra.get_row(r);
-    SASSERT(s.lra.row_is_correct(r));
+    unsigned r = lia.row_of_basic_column(j);
+    const row_strip<mpq>& row = lra.get_row(r);
+    SASSERT(lra.row_is_correct(r));
     SASSERT(is_gomory_cut_target(row));
-    upper = true;
-    return cut(t, k, ex, j, row);
+    lia.m_upper = true;
+    return cut(lia.m_t, lia.m_k, lia.m_ex, j, row);
 }
 
 
-gomory::~gomory() { }
+gomory::gomory(int_solver& lia): lia(lia), lra(lia.lra) { }
 
 }

src/math/lp/gomory.h

@@ -23,14 +23,16 @@ Revision History:
 
 namespace lp {
     class int_solver;
+    class lar_solver;
     class gomory {
-        class int_solver& s;
+        class int_solver& lia;
+        class lar_solver& lra;
         int find_basic_var();
         bool is_gomory_cut_target(const row_strip<mpq>& row);
         lia_move cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip<mpq>& row);
     public:
-        gomory(int_solver& s): s(s) {}
-        ~gomory();
-        lia_move operator()(lar_term & t, mpq & k, explanation* ex, bool& upper);
+        gomory(int_solver& lia);
+        ~gomory() {}
+        lia_move operator()();
     };
 }

src/math/lp/int_solver.cpp

@@ -3,25 +3,33 @@
   Author: Lev Nachmanson
 */
 
+#include <utility>
 #include "math/lp/int_solver.h"
 #include "math/lp/lar_solver.h"
 #include "math/lp/lp_utils.h"
-#include <utility>
 #include "math/lp/monic.h"
 #include "math/lp/gomory.h"
 #include "math/lp/int_branch.h"
 #include "math/lp/int_gcd_test.h"
 #include "math/lp/int_cube.h"
+
 namespace lp {
 
+int_solver::int_solver(lar_solver& lar_slv) :
+    lra(lar_slv),
+    m_number_of_calls(0),
+    m_hnf_cutter(settings()),
+    m_hnf_cut_period(settings().hnf_cut_period()) {
+    lra.set_int_solver(this);
+}
+
 // this will allow to enable and disable tracking of the pivot rows
 struct check_return_helper {
     lar_solver&      lra;
     bool             m_track_pivoted_rows;
     check_return_helper(lar_solver& ls) :
         lra(ls),
-        m_track_pivoted_rows(lra.get_track_pivoted_rows())
-    {
+        m_track_pivoted_rows(lra.get_track_pivoted_rows()) {
         TRACE("pivoted_rows", tout << "pivoted rows = " << lra.m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
         lra.set_track_pivoted_rows(false);
     }
@@ -42,9 +50,9 @@ lia_move int_solver::check(lp::explanation * e) {
     m_upper = false;
     lia_move r = lia_move::undef;
 
-    gomory gc(*this);
-    int_cube cube(*this);
-    int_branch branch(*this);
+    gomory       gc(*this);
+    int_cube     cube(*this);
+    int_branch   branch(*this);
     int_gcd_test gcd(*this);
 
     if (should_run_gcd_test()) r = gcd();
@@ -59,7 +67,7 @@ lia_move int_solver::check(lp::explanation * e) {
     ++m_number_of_calls;
     if (r == lia_move::undef && should_find_cube()) r = cube();
     if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut();
-    if (r == lia_move::undef && should_gomory_cut()) r = gc(m_t, m_k, m_ex, m_upper);
+    if (r == lia_move::undef && should_gomory_cut()) r = gc();
     if (r == lia_move::undef) r = branch();
     return r;
 }
@@ -140,6 +148,10 @@ const impq& int_solver::upper_bound(unsigned j) const {
     return lra.column_upper_bound(j);
 }
 
+const impq& int_solver::lower_bound(unsigned j) const {
+    return lra.column_lower_bound(j);
+}
+
 bool int_solver::is_term(unsigned j) const {
     return lra.column_corresponds_to_term(j);
 }
@@ -148,7 +160,6 @@ unsigned int_solver::column_count() const  {
     return lra.column_count(); 
 }
 
-
 bool int_solver::should_find_cube() {
     return m_number_of_calls % settings().m_int_find_cube_period == 0;
 }
@@ -311,17 +322,6 @@ lia_move int_solver::patch_nbasic_columns() {
     return lia_move::undef;
 }
 
-// TBD: move to gcd-test
-
-
-int_solver::int_solver(lar_solver& lar_slv) :
-    lra(lar_slv),
-    m_number_of_calls(0),
-    m_hnf_cutter(settings()),
-    m_hnf_cut_period(settings().hnf_cut_period()) {
-    lra.set_int_solver(this);
-}
-
 
 bool int_solver::has_lower(unsigned j) const {
     switch (lra.m_mpq_lar_core_solver.m_column_types()[j]) {
@@ -616,10 +616,6 @@ bool int_solver::non_basic_columns_are_at_bounds() const {
     }
     return true;
 }
-
-const impq& int_solver::lower_bound(unsigned j) const {
-    return lra.column_lower_bound(j);
-}
     
 
 }

src/math/lp/int_solver.h

@@ -30,28 +30,24 @@ Revision History:
 namespace lp {
 class lar_solver;
 
-template <typename T, typename X>
-struct lp_constraint;
-
-
 class int_solver {
+    friend class create_cut;
     friend class gomory;
     friend class int_cube;
     friend class int_branch;
     friend class int_gcd_test;
-public:
-    // fields
+
     lar_solver&         lra;
     unsigned            m_number_of_calls;
-    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
-    bool                m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise
+    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
+    bool                m_upper;           // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise
     hnf_cutter          m_hnf_cutter;
     unsigned            m_hnf_cut_period;
-    // methods
-    int_solver(lar_solver& lp);
 
+public:
+    int_solver(lar_solver& lp);
 
     // main function to check that the solution provided by lar_solver is valid for integral values,
     // or provide a way of how it can be adjusted.
@@ -59,7 +55,7 @@ public:
     lar_term const& get_term() const { return m_t; }
     mpq const& get_offset() const { return m_k; }
     bool is_upper() const { return m_upper; }
-    lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex);    
+    //lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex);    
     bool is_base(unsigned j) const;
     bool is_real(unsigned j) const;
     const impq & lower_bound(unsigned j) const;
@@ -109,7 +105,6 @@ public:
     unsigned column_count() const;
     bool all_columns_are_bounded() const;
     void find_feasible_solution();
-    lia_move run_gcd_test();
     lia_move hnf_cut();
     lia_move make_hnf_cut();
     bool init_terms_for_hnf_cut();