separate out int-branch

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

src/math/lp/CMakeLists.txt

@@ -12,8 +12,9 @@ z3_add_component(lp
     gomory.cpp
     horner.cpp
     indexed_vector.cpp
-    int_solver.cpp
+    int_branch.cpp
     int_cube.cpp
+    int_solver.cpp
     lar_solver.cpp
     lar_core_solver.cpp
     lp_core_solver_base.cpp

src/math/lp/int_branch.cpp

@@ -0,0 +1,134 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    int_branch.cpp
+
+Abstract:
+
+    Branch heuristic
+
+Author:
+    Nikolaj Bjorner (nbjorner)
+    Lev Nachmanson (levnach)
+
+Revision History:
+--*/
+
+#include "math/lp/int_solver.h"
+#include "math/lp/lar_solver.h"
+#include "math/lp/int_branch.h"
+
+namespace lp {
+
+    int_branch::int_branch(int_solver& lia):lia(lia), lra(lia.lra) {}
+
+    lia_move int_branch::operator()() {
+        int j = find_any_inf_int_column_basis_first();
+        return j == -1? lia_move::sat : create_branch_on_column(j);        
+    }
+
+    int int_branch::find_any_inf_int_column_basis_first() {
+        int j = find_inf_int_base_column();
+        return j != -1 ? j : find_inf_int_nbasis_column();
+    }
+
+    lia_move int_branch::create_branch_on_column(int j) {
+        TRACE("check_main_int", tout << "branching" << std::endl;);
+        lp_assert(lia.m_t.is_empty());
+        lp_assert(j != -1);
+        lia.m_t.add_monomial(mpq(1), lra.adjust_column_index_to_term_index(j));
+        if (lia.is_free(j)) {
+            lia.m_upper = lia.random() % 2;
+            lia.m_k = mpq(0);
+        }
+        else {
+            lia.m_upper = left_branch_is_more_narrow_than_right(j);
+            lia.m_k = lia.m_upper? floor(lia.get_value(j)) : ceil(lia.get_value(j));        
+        }
+        
+        TRACE("int_solver",
+              lia.display_column(tout << "branching v" << j << " = " << get_value(j) << "\n", j);
+              tout << "k = " << m_k << std::endl;);
+        return lia_move::branch;        
+    }
+
+    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] ) {
+        case column_type::fixed:
+            return false;
+        case column_type::boxed: {
+            auto k = floor(lia.get_value(j));
+            return k - lia.lower_bound(j).x < lia.upper_bound(j).x - (k + mpq(1));
+        }
+        case column_type::lower_bound: 
+            return true;
+        case column_type::upper_bound:
+            return false;
+        default:
+            return false;
+        }       
+    }
+
+    int int_branch::find_inf_int_base_column() {
+        unsigned inf_int_count = 0;
+        int j = find_inf_int_boxed_base_column_with_smallest_range(inf_int_count);
+        if (j != -1) {
+            return j;
+        }
+        if (inf_int_count == 0)
+            return -1;
+        unsigned k = lia.random() % inf_int_count;
+        return get_kth_inf_int(k);
+    }
+    
+    int int_branch::get_kth_inf_int(unsigned k) const {
+        for (unsigned j : lra.r_basis()) 
+            if (lia.column_is_int_inf(j) && k-- == 0)
+                return j;
+        lp_assert(false);
+        return -1;
+    }
+    
+    int int_branch::find_inf_int_nbasis_column() const {
+        for (unsigned j : lra.r_nbasis())
+            if (!lia.column_is_int_inf(j)) {
+                return j;    
+            }
+        return -1; 
+    }
+    
+    int int_branch::find_inf_int_boxed_base_column_with_smallest_range(unsigned & inf_int_count) {
+        inf_int_count = 0;
+        int result = -1;
+        mpq range;
+        mpq new_range;
+        mpq small_range_thresold(1024);
+        unsigned n = 0;
+        lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
+        
+        for (unsigned j : lra.r_basis()) {
+            if (!lia.column_is_int_inf(j))
+                continue;
+            inf_int_count++;
+            if (!lia.is_boxed(j))
+                continue;
+            lp_assert(!is_fixed(j));
+            new_range  = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x;
+            if (new_range > small_range_thresold) 
+                continue;
+            if (result == -1 || new_range < range) {
+                result = j;
+                range  = new_range;
+                n      = 1;
+            }
+            else if (new_range == range && lia.random() % (++n) == 0) {
+                lp_assert(n > 1);
+                result = j;
+            }
+        }
+        return result;    
+    }
+    
+}

src/math/lp/int_branch.h

@@ -0,0 +1,41 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    int_branch.h
+
+Abstract:
+
+    Branch heuristic
+
+Author:
+    Nikolaj Bjorner (nbjorner)
+    Lev Nachmanson (levnach)
+
+Revision History:
+--*/
+#pragma once
+
+#include "math/lp/lia_move.h"
+
+namespace lp {
+    class int_solver;
+    class lar_solver;
+    class int_branch {
+        class int_solver& lia;
+        class lar_solver& lra;
+        lia_move create_branch_on_column(int j);
+        bool left_branch_is_more_narrow_than_right(unsigned j);
+        int find_inf_int_base_column();
+        int get_kth_inf_int(unsigned k) const;
+        int find_inf_int_nbasis_column() const;
+        int find_any_inf_int_column_basis_first();
+        int find_inf_int_boxed_base_column_with_smallest_range(unsigned & inf_int_count);
+
+    public:
+        int_branch(int_solver& lia);
+        ~int_branch() {}
+        lia_move operator()();
+    };
+}

src/math/lp/int_solver.cpp

@@ -10,6 +10,7 @@
 #include "math/lp/monic.h"
 #include "math/lp/gomory.h"
 #include "math/lp/int_cube.h"
+#include "math/lp/int_branch.h"
 namespace lp {
 
 
@@ -34,66 +35,6 @@ std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
     return out;
 }
 
-int int_solver::find_inf_int_base_column() {
-    unsigned inf_int_count = 0;
-    int j = find_inf_int_boxed_base_column_with_smallest_range(inf_int_count);
-    if (j != -1) {
-        return j;
-    }
-    if (inf_int_count == 0)
-        return -1;
-    unsigned k = random() % inf_int_count;
-    return get_kth_inf_int(k);
-}
-
-int int_solver::get_kth_inf_int(unsigned k) const {
-    for (unsigned j : lra.r_basis()) 
-        if (column_is_int_inf(j) && k-- == 0)
-            return j;
-    lp_assert(false);
-    return -1;
-}
-
-int int_solver::find_inf_int_nbasis_column() const {
-    for (unsigned j : lra.r_nbasis())
-        if (!column_is_int_inf(j)) {
-            return j;    
-        }
-    return -1; 
-}
-
-int int_solver::find_inf_int_boxed_base_column_with_smallest_range(unsigned & inf_int_count) {
-    inf_int_count = 0;
-    int result = -1;
-    mpq range;
-    mpq new_range;
-    mpq small_range_thresold(1024);
-    unsigned n = 0;
-    lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
-
-    for (unsigned j : lra.r_basis()) {
-        if (!column_is_int_inf(j))
-            continue;
-        inf_int_count++;
-        if (!is_boxed(j))
-            continue;
-        lp_assert(!is_fixed(j));
-        new_range  = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x;
-        if (new_range > small_range_thresold) 
-            continue;
-        if (result == -1 || new_range < range) {
-            result = j;
-            range  = new_range;
-            n      = 1;
-        }
-        else if (new_range == range && settings().random_next() % (++n) == 0) {
-            lp_assert(n > 1);
-            result = j;
-        }
-    }
-    return result;    
-}
-
 bool int_solver::current_solution_is_inf_on_cut() const {
     const auto & x = lra.m_mpq_lar_core_solver.m_r_x;
     impq v = m_t.apply(x);
@@ -338,14 +279,10 @@ lia_move int_solver::check(lp::explanation * e) {
 }
 
 lia_move int_solver::branch_or_sat() {
-    int j = find_any_inf_int_column_basis_first();
-    return j == -1? lia_move::sat : create_branch_on_column(j);
+    int_branch b(*this);
+    return b();
 }
 
-int int_solver::find_any_inf_int_column_basis_first() {
-   int j = find_inf_int_base_column();
-   return j != -1 ? j : find_inf_int_nbasis_column();
-}
 
 void int_solver::set_value_for_nbasic_column_ignore_old_values(unsigned j, const impq & new_val) {
     lp_assert(!is_base(j));
@@ -881,45 +818,6 @@ bool int_solver::non_basic_columns_are_at_bounds() const {
 const impq& int_solver::lower_bound(unsigned j) const {
     return lra.column_lower_bound(j);
 }
-
-lia_move int_solver::create_branch_on_column(int j) {
-    TRACE("check_main_int", tout << "branching" << std::endl;);
-    lp_assert(m_t.is_empty());
-    lp_assert(j != -1);
-    m_t.add_monomial(mpq(1), lra.adjust_column_index_to_term_index(j));
-    if (is_free(j)) {
-        m_upper = random() % 2;
-        m_k = mpq(0);
-    }
-    else {
-        m_upper = left_branch_is_more_narrow_than_right(j);
-        m_k = m_upper? floor(get_value(j)) : ceil(get_value(j));        
-    }
-
-    TRACE("int_solver",
-          display_column(tout << "branching v" << j << " = " << get_value(j) << "\n", j);
-          tout << "k = " << m_k << std::endl;);
-    return lia_move::branch;
-
-}
-
-bool int_solver::left_branch_is_more_narrow_than_right(unsigned j) {
-    switch (lra.m_mpq_lar_core_solver.m_r_solver.m_column_types[j] ) {
-    case column_type::fixed:
-        return false;
-    case column_type::boxed:
-        {
-            auto k = floor(get_value(j));
-            return k - lower_bound(j).x < upper_bound(j).x - (k + mpq(1));
-        }
-    case column_type::lower_bound: 
-        return true;
-    case column_type::upper_bound:
-        return false;
-    default:
-        return false;
-    }       
-}
     
 
 }

src/math/lp/int_solver.h

@@ -37,6 +37,7 @@ struct lp_constraint;
 class int_solver {
     friend class gomory;
     friend class int_cube;
+    friend class int_branch;
 public:
     // fields
     lar_solver&         lra;
@@ -107,13 +108,8 @@ private:
     bool should_hnf_cut();
 
     lia_move branch_or_sat();
-    int find_any_inf_int_column_basis_first();
-    int find_inf_int_base_column();
-    int find_inf_int_boxed_base_column_with_smallest_range(unsigned&);
-    int get_kth_inf_int(unsigned) const;
     lp_settings& settings();
     const lp_settings& settings() const;
-    void branch_infeasible_int_var(unsigned);
     bool at_bound(unsigned j) const;
     bool has_lower(unsigned j) const;
     bool has_upper(unsigned j) const;
@@ -130,18 +126,12 @@ private:
     void display_row_info(std::ostream & out, unsigned row_index) const;
     unsigned random();
     bool has_inf_int() const;
-    lia_move create_branch_on_column(int j);
 public:
     bool is_term(unsigned j) const;
-    bool left_branch_is_more_narrow_than_right(unsigned);
     lia_move find_cube();
-    bool tighten_terms_for_cube();
-    bool tighten_term_for_cube(unsigned);
     unsigned column_count() const;
     bool all_columns_are_bounded() const;
-    impq get_cube_delta_for_term(const lar_term&) const;
     void find_feasible_solution();
-    int find_inf_int_nbasis_column() const;
     lia_move run_gcd_test();
     lia_move gomory_cut();
     lia_move hnf_cut();