add branch / cut selection heuristic from solver=2

disabled for testing.

src/ast/rewriter/arith_rewriter.cpp

@@ -16,6 +16,7 @@ Module Name:
 Notes:
 
 --*/
+
 #include "params/arith_rewriter_params.hpp"
 #include "ast/rewriter/arith_rewriter.h"
 #include "ast/rewriter/poly_rewriter_def.h"
@@ -1046,27 +1047,29 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
     set_curr_sort(arg1->get_sort());
     numeral v1, v2;
     bool is_int;
-    if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
+    bool is_num1 = m_util.is_numeral(arg1, v1, is_int);
+    bool is_num2 = m_util.is_numeral(arg2, v2, is_int);
+    if (is_num1 && is_num2 && !v2.is_zero()) {
         result = m_util.mk_numeral(div(v1, v2), is_int);
         return BR_DONE;
     }
-    if (m_util.is_numeral(arg2, v2, is_int) && v2.is_one()) {
+    if (is_num2 && v2.is_one()) {
         result = arg1; 
         return BR_DONE; 
     } 
-    if (m_util.is_numeral(arg2, v2, is_int) && v2.is_minus_one()) {
+    if (is_num2 && v2.is_minus_one()) {
         result = m_util.mk_mul(m_util.mk_int(-1), arg1); 
         return BR_REWRITE1; 
     }
-    if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) { 
+    if (is_num2 && v2.is_zero()) { 
         return BR_FAILED; 
     } 
     if (arg1 == arg2) { 
         expr_ref zero(m_util.mk_int(0), m); 
         result = m.mk_ite(m.mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1)); 
         return BR_REWRITE3; 
     } 
-    if (m_util.is_numeral(arg2, v2, is_int) && v2.is_pos() && m_util.is_add(arg1)) { 
+    if (is_num2 && v2.is_pos() && m_util.is_add(arg1)) { 
         expr_ref_buffer args(m);
         bool change = false;
         rational add(0);
@@ -1092,7 +1095,14 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
         expr_ref zero(m_util.mk_int(0), m); 
         result = m.mk_ite(m.mk_eq(zero, arg2), m_util.mk_idiv(arg1, zero), result);
         return BR_REWRITE_FULL; 
-    } 
+    }
+#if 0
+    expr* x = nullptr, *y = nullptr, *z = nullptr;
+    if (is_num2 && m_util.is_idiv(arg1, x, y) && m_util.is_numeral(y, v1) && v1 > 0 && v2 > 0) {
+        result = m_util.mk_idiv(x, m_util.mk_numeral(v1*v2, is_int));
+        return BR_DONE;
+    }
+#endif
     return BR_FAILED;
 }
 

src/math/lp/gomory.cpp

@@ -377,10 +377,20 @@ bool gomory::is_gomory_cut_target(const row_strip<mpq>& row) {
 }
 
 int gomory::find_basic_var() {
-    int result = -1;
     unsigned n = 0;
+    int result = -1;
     unsigned min_row_size = UINT_MAX;
-    // Prefer smaller row size
+
+#if 0
+    result = lia.select_int_infeasible_var();
+
+    if (result == -1)
+        return result;
+
+    const row_strip<mpq>& row = lra.get_row(lia.row_of_basic_column(result));
+    if (is_gomory_cut_target(row)) 
+        return result;
+#endif
 
     for (unsigned j : lra.r_basis()) {
         if (!lia.column_is_int_inf(j))
@@ -389,6 +399,7 @@ int gomory::find_basic_var() {
         if (!is_gomory_cut_target(row)) 
             continue;
         IF_VERBOSE(20, lia.display_row_info(verbose_stream(), lia.row_of_basic_column(j)));
+        // Prefer smaller row size
         if (min_row_size == UINT_MAX || 
             2*row.size() < min_row_size || 
             (4*row.size() < 5*min_row_size && lia.random() % (++n) == 0)) {

src/math/lp/int_branch.cpp

@@ -52,29 +52,36 @@ lia_move int_branch::create_branch_on_column(int j) {
 
 
 int int_branch::find_inf_int_base_column() {
+
+#if 0
+    return lia.select_int_infeasible_var();
+#endif
+
     int result = -1;
     mpq range;
     mpq new_range;
-    mpq small_range_thresold(1024);
+    mpq small_value(1024);
     unsigned n = 0;
     lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
     unsigned prev_usage = 0; // to quiet down the compile
     unsigned k = 0;
     unsigned usage;
     unsigned j;
+
     // this loop looks for a column with the most usages, but breaks when
     // a column with a small span of bounds is found
     for (; k < lra.r_basis().size(); k++) {
         j = lra.r_basis()[k];
         if (!lia.column_is_int_inf(j))
             continue;
         usage = lra.usage_in_terms(j);
-        if (lia.is_boxed(j) &&  (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_range_thresold) {
+        if (lia.is_boxed(j) &&  (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_value) {
             result = j;
             k++;            
             n = 1;
             break;
         }
+
         if (n == 0 || usage > prev_usage) {
             result = j;
             prev_usage = usage;

src/math/lp/int_solver.cpp

@@ -632,4 +632,73 @@ bool int_solver::non_basic_columns_are_at_bounds() const {
     return true;
 }
 
+int int_solver::select_int_infeasible_var() {
+    int result = -1;
+    mpq range;
+    mpq new_range;
+    mpq small_value(1024);
+    unsigned n = 0;
+    lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
+    unsigned prev_usage = 0; // to quiet down the compile
+    unsigned k = 0;
+    unsigned usage;
+    unsigned j;
+
+    enum state { small_box, is_small_value,  any_value, not_found };
+    state st = not_found;
+
+    // 1. small box
+    // 2. small value
+    // 3. any value
+    for (; k < lra.r_basis().size(); k++) {
+        j = lra.r_basis()[k];
+        if (!column_is_int_inf(j))
+            continue;
+        usage = lra.usage_in_terms(j);
+        if (is_boxed(j) && (new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_value) {
+            SASSERT(!is_fixed(j));
+            if (st != small_box) {
+                n = 0;
+                st = small_box;
+            }
+            if (n == 0 || new_range < range) {
+                result = j;
+                range = new_range;
+                n = 1;
+            }
+            else if (new_range == range && (random() % (++n) == 0)) {
+                result = j;
+            }
+            continue;
+        }
+        if (st == small_box)
+            continue;
+        impq const& value = get_value(j);
+        if (abs(value.x) < small_value ||
+            (has_upper(j) && small_value > upper_bound(j).x - value.x) ||
+            (has_lower(j) && small_value > value.x - lower_bound(j).x)) {
+            if (st != is_small_value) {
+                n = 0;
+                st = is_small_value;
+            }
+            if (random() % (++n) == 0)
+                result = j;
+        }
+        if (st == is_small_value)
+            continue;
+        SASSERT(st == not_found || st == any_value);
+        st = any_value;
+        if (n == 0 /*|| usage > prev_usage*/) {
+            result = j;
+            prev_usage = usage;
+            n = 1;
+        } 
+        else if (usage > 0 && /*usage == prev_usage && */ (random() % (++n) == 0)) 
+            result = j;
+    }
+
+    return result;
+}
+
+
 }

src/math/lp/int_solver.h

@@ -129,5 +129,8 @@ class int_solver {
     void find_feasible_solution();
     lia_move hnf_cut();
     void patch_nbasic_column(unsigned j) { m_patcher.patch_nbasic_column(j); }
+
+    int select_int_infeasible_var();
+
   };
 }

src/smt/theory_arith_int.h

@@ -514,9 +514,11 @@ namespace smt {
         // SASSERT(m_value[x_i].is_rational()); // infinitesimals are not used for integer variables
         SASSERT(!m_value[x_i].is_int());     // the base variable is not assigned to an integer value.
 
-        if (constrain_free_vars(r) || !is_gomory_cut_target(r)) {
+        bool cfv = constrain_free_vars(r);
+
+        if (cfv || !is_gomory_cut_target(r)) {
             TRACE("gomory_cut", tout << "failed to apply gomory cut:\n";
-                  tout << "constrain_free_vars(r):  " << constrain_free_vars(r) << "\n";);
+                  tout << "constrain_free_vars(r):  " << cfv << "\n";);
             return false;
         }