fix #2949 fix #2955 experiment with cut selection

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

src/math/lp/int_solver.cpp

@@ -37,6 +37,55 @@ bool int_solver::has_inf_int() const {
     return m_lar_solver->has_inf_int();
 }
 
+int int_solver::find_gomory_cut_column() {
+    int result = -1;
+    unsigned n = 0;
+    bool boxed = false;
+    unsigned min_row_size = UINT_MAX;
+    mpq min_range;
+
+    // Prefer smaller row size
+#if 0
+    // Prefer boxed to non-boxed
+    // Prefer smaller ranges
+#endif
+
+    for (unsigned j : m_lar_solver->r_basis()) {
+        if (!column_is_int_inf(j))
+            continue;
+        const row_strip<mpq>& row = m_lar_solver->get_row(row_of_basic_column(j));
+        if (!is_gomory_cut_target(row)) 
+            continue;
+#if 1
+        if (is_boxed(j) && (min_row_size == UINT_MAX || 4*row.size() < 5*min_row_size)) {
+            lar_core_solver & lcs = m_lar_solver->m_mpq_lar_core_solver;
+            auto new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x;
+            if (!boxed) {
+                result = j;
+                n = 1;
+                min_row_size = row.size();
+                boxed = true;
+                min_range = new_range;
+                continue;
+            }
+            if (min_range > 2*new_range || ((5*min_range > 4*new_range && (random() % (++n)) == 0))) { 
+                result = j;
+                n = 1;
+                min_row_size = row.size();
+                min_range = std::min(min_range, new_range);
+                continue;
+            }
+        }
+#endif
+        if (min_row_size == UINT_MAX || (4*row.size() < 5*min_row_size && random() % (++n) == 0)) {
+            result = j;
+            n = 1;
+            min_row_size = std::min(min_row_size, row.size());
+        }
+    }
+    return result;
+}
+
 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);
@@ -304,7 +353,8 @@ lia_move int_solver::gomory_cut() {
         lp_assert(st == lp_status::FEASIBLE || st == lp_status::OPTIMAL);
     }
         
-    int j = find_inf_int_base_column(); 
+//    int j = find_inf_int_base_column();
+    int j = find_gomory_cut_column(); 
     if (j == -1) {
         j = find_inf_int_nbasis_column();
         return j == -1? lia_move::sat : create_branch_on_column(j);
@@ -1019,7 +1069,8 @@ lia_move int_solver::create_branch_on_column(int j) {
     if (is_free(j)) {
         m_upper = random() % 2;
         m_k = mpq(0);
-    } else {
+    }
+    else {
         m_upper = left_branch_is_more_narrow_than_right(j);
         m_k = m_upper? floor(get_value(j)) : ceil(get_value(j));        
     }

src/math/lp/int_solver.h

@@ -107,6 +107,7 @@ private:
     lia_move branch_or_sat();
     int find_any_inf_int_column_basis_first();
     int find_inf_int_base_column();
+    int find_gomory_cut_column();
     int find_inf_int_boxed_base_column_with_smallest_range(unsigned&);
     int get_kth_inf_int(unsigned) const;
     lp_settings& settings();

src/math/lp/lar_constraints.h

@@ -158,10 +158,6 @@ public:
     }
 
     void pop(unsigned k) {
-        m_constraint_count.pop(k);        
-        for (unsigned i = m_constraints.size(); i-- > m_constraint_count; )
-            m_constraints[i]->~lar_base_constraint();        
-        m_constraints.shrink(m_constraint_count);
 #if 1
         m_active_lim.pop(k);
         for (unsigned i = m_active.size(); i-- > m_active_lim; ) {
@@ -169,6 +165,11 @@ public:
         }
         m_active.shrink(m_active_lim);
 #endif
+        m_constraint_count.pop(k);        
+        for (unsigned i = m_constraints.size(); i-- > m_constraint_count; )
+            m_constraints[i]->~lar_base_constraint();        
+        m_constraints.shrink(m_constraint_count);
+
         m_region.pop_scope(k);
     }
 

src/smt/smt_context.cpp

@@ -1861,13 +1861,15 @@ namespace smt {
                             break;
                         }
                     }
-                    if (m_lit_occs[l.index()] == 0) {
+                    if (track_occs()) {
-                        is_pos = false;
+                        if (m_lit_occs[l.index()] == 0) {
-                        break;
+                            is_pos = false;
-                    }
+                            break;
-                    if (m_lit_occs[(~l).index()] == 0) {
+                        }
-                        is_pos = true;
+                        if (m_lit_occs[(~l).index()] == 0) {
-                        break;
+                            is_pos = true;
+                            break;
+                        }
                     }
                     is_pos = m_phase_default;                    
                     break;

src/smt/smt_context.h

@@ -839,7 +839,7 @@ namespace smt {
 
         void mk_ite_cnstr(app * n);
 
-        bool track_occs() const { return m_fparams.m_phase_selection == PS_THEORY; }
+        bool track_occs() const { return m_fparams.m_phase_selection == PS_OCCURRENCE; }
         
         void dec_ref(literal l);
 

src/smt/theory_lra.cpp

@@ -1864,28 +1864,6 @@ public:
         return atom;
     }
 
-    // bool make_sure_all_vars_have_bounds() {
-    //     if (!has_int()) {
-    //         return true;
-    //     }
-        
-    //     unsigned nv = std::min(th.get_num_vars(), m_theory_var2var_index.size());
-    //     bool all_bounded = true;
-    //     for (unsigned v = 0; v < nv; ++v) {
-    //         lpvar vi = m_theory_var2var_index[v];
-    //         if (vi == UINT_MAX)
-    //             continue;
-    //         if (!lp().is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) {
-    //             lp::lar_term term;
-    //             term.add_coeff_var(rational::one(), vi);
-    //             app_ref b = mk_bound(term, rational::zero(), true);
-    //             TRACE("arith", tout << "added bound " << b << "\n";);
-    //             IF_VERBOSE(2, verbose_stream() << "bound: " << b << "\n");
-    //             all_bounded = false;
-    //         }
-    //     }
-    //     return all_bounded;
-    // }
 
     /**
      * n = (div p q)
@@ -1919,7 +1897,6 @@ public:
         if (m_idiv_terms.empty()) {
             return true;
         }
-        // init_variable_values();
         bool all_divs_valid = true;        
         for (expr* n : m_idiv_terms) {
             expr* p = nullptr, *q = nullptr;
@@ -1927,10 +1904,9 @@ public:
             theory_var v  = mk_var(n);
             theory_var v1 = mk_var(p);
             lp::impq r1 = get_ivalue(v1);
-            SASSERT(r1.y.is_zero());
             rational r2;
 
-            if (!r1.x.is_int() || r1.x.is_neg()) {
+            if (!r1.x.is_int() || r1.x.is_neg() || !r1.y.is_zero()) {
                 // TBD
                 // r1 = 223/4, r2 = 2, r = 219/8 
                 // take ceil(r1), floor(r1), ceil(r2), floor(r2), for floor(r2) > 0
@@ -1946,8 +1922,7 @@ public:
                     continue;
                 }
                 lp::impq val_v = get_ivalue(v);
-                SASSERT(val_v.y.is_zero());
+                if (val_v.y.is_zero() && val_v.x == div(r1.x, r2)) continue;
-                if (val_v.x == div(r1.x, r2)) continue;
             
                 TRACE("arith", tout << get_value(v) << " != " << r1 << " div " << r2 << "\n";);
                 rational div_r = div(r1.x, r2);

src/util/mpz.cpp

@@ -1680,6 +1680,9 @@ double mpz_manager<SYNCH>::get_double(mpz const & a) const {
         else
             d *= static_cast<double>(UINT_MAX);   // 32-bit version
     }
+    if (!(r >= 0.0)) {
+        r = static_cast<double>(UINT64_MAX); // some large number
+    }
     return a.m_val < 0 ? -r : r;
 #else
     return mpz_get_d(*a.m_ptr);