fixes in branching

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

src/math/lp/gomory.cpp

@@ -442,12 +442,7 @@ int gomory::find_basic_var() {
 }
 
 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);
-    }
-
+    lra.move_non_basic_columns_to_bounds();
     int j = find_basic_var();
     if (j == -1) return lia_move::undef;
     unsigned r = lia.row_of_basic_column(j);

src/math/lp/int_branch.cpp

@@ -45,7 +45,7 @@ namespace lp {
             lia.m_k = mpq(0);
         }
         else {
-            lia.m_upper = lra.settings().branch_flip()? lia.random() % 2 : left_branch_is_more_narrow_than_right(j);
+            lia.m_upper = lia.random() % 2;
             lia.m_k = lia.m_upper? floor(lia.get_value(j)) : ceil(lia.get_value(j));        
         }
 
@@ -55,23 +55,6 @@ namespace lp {
         return lia_move::branch;        
     }
 
-    bool int_branch::left_branch_is_more_narrow_than_right(unsigned j) {
-        switch (lra.get_column_type(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);
@@ -93,8 +76,9 @@ namespace lp {
     }
 
     int int_branch::find_inf_int_nbasis_column() const {
+
         for (unsigned j : lra.r_nbasis())
-            if (!lia.column_is_int_inf(j)) {
+            if (lia.column_is_int_inf(j)) {
                 return j;    
             }
         return -1; 

src/math/lp/int_branch.h

@@ -28,7 +28,6 @@ namespace lp {
         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;

src/math/lp/int_cube.cpp

@@ -42,8 +42,8 @@ namespace lp {
         if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) {
             TRACE("cube", tout << "cannot find a feasiblie solution";);
             lra.pop();
+            lra.set_status(lp_status::OPTIMAL);
             lra.move_non_basic_columns_to_bounds();
-            find_feasible_solution();
             // it can happen that we found an integer solution here
             return !lra.r_basis_has_inf_int()? lia_move::sat: lia_move::undef;
         }

src/math/lp/lar_solver.cpp

@@ -445,8 +445,7 @@ void lar_solver::set_costs_to_zero(const lar_term& term) {
 void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {        
     TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";);
     m_basic_columns_with_changed_cost.resize(m_mpq_lar_core_solver.m_r_x.size());
-    if (move_non_basic_columns_to_bounds())
-        find_feasible_solution();
+    move_non_basic_columns_to_bounds();
     auto & rslv = m_mpq_lar_core_solver.m_r_solver;
     rslv.set_using_infeas_costs(false);
     lp_assert(costs_are_zeros_for_r_solver());
@@ -464,17 +463,26 @@ void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {
     lp_assert(rslv.reduced_costs_are_correct_tableau());
 }
 
-bool lar_solver::move_non_basic_columns_to_bounds() {
+bool feasible(lp_status st) {
+    return st == lp_status::FEASIBLE || st == lp_status::OPTIMAL;
+}
+
+void lar_solver::move_non_basic_columns_to_bounds() {
     auto & lcs = m_mpq_lar_core_solver;
     bool change = false;
+    bool feas = feasible(get_status());
     for (unsigned j : lcs.m_r_nbasis) {
         if (move_non_basic_column_to_bounds(j))
             change = true;
     }
 
-    if (settings().simplex_strategy() == simplex_strategy_enum::tableau_costs)
+    if (settings().simplex_strategy() == simplex_strategy_enum::tableau_costs && change)
         update_x_and_inf_costs_for_columns_with_changed_bounds_tableau();
-    return change;
+
+    if (feas && change) {
+        find_feasible_solution();
+        SASSERT(feasible(get_status()));
+    }
 }
 
 bool lar_solver::move_non_basic_column_to_bounds(unsigned j) {

src/math/lp/lar_solver.h

@@ -421,7 +421,7 @@ class lar_solver : public column_namer {
     inline int_solver * get_int_solver() { return m_int_solver; }
     inline const lar_term & get_term(tv const& t) const { lp_assert(t.is_term()); return *m_terms[t.id()]; }
     lp_status find_feasible_solution();   
-    bool move_non_basic_columns_to_bounds();
+    void move_non_basic_columns_to_bounds();
     bool move_non_basic_column_to_bounds(unsigned j);
     inline bool r_basis_has_inf_int() const {
         for (unsigned j : r_basis()) {

src/math/lp/lp_settings.h

@@ -200,7 +200,6 @@ struct lp_settings {
     unsigned         limit_on_columns_for_hnf_cutter;
     bool             m_enable_hnf;
     bool             m_print_external_var_name;
-    bool             m_branch_flip;
 #ifdef Z3DEBUG
     unsigned         m_counter_for_debug;
 #endif
@@ -271,15 +270,12 @@ struct lp_settings {
                     limit_on_rows_for_hnf_cutter(75),
                     limit_on_columns_for_hnf_cutter(150),
                     m_enable_hnf(true),
-                    m_print_external_var_name(false),
-                    m_branch_flip(false)
+                    m_print_external_var_name(false)
 #ifdef Z3DEBUG
                   , m_counter_for_debug(0)
 #endif
     {}
 
-    bool branch_flip() const { return m_branch_flip; }
-    void set_branch_flip(bool f) { m_branch_flip = f; }
     void set_resource_limit(lp_resource_limit& lim) { m_resource_limit = &lim; }
     bool get_cancel_flag() const { return m_resource_limit->get_cancel_flag(); }
 

src/smt/params/smt_params_helper.pyg

@@ -62,7 +62,6 @@ def_module_params(module_name='smt',
                           ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
                           ('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'),
                           ('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'),
-                          ('arith.branch_flip', BOOL, False, 'flip branches randomly'),
                           ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
                           ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
                           ('arith.ignore_int', BOOL, False, 'treat integer variables as real'),

src/smt/theory_lra.cpp

@@ -396,7 +396,6 @@ class theory_lra::imp {
         lp().settings().print_statistics = lpar.arith_print_stats();
 
         // todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts
-        lp().settings().set_branch_flip(lpar.arith_branch_flip());
         unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;
         lp().set_cut_strategy(branch_cut_ratio);