rebase with upstream

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

src/smt/theory_lra.cpp

@@ -1747,7 +1747,7 @@ public:
         return atom;
     }
 
-    bool make_sure_all_vars_have_bounds() {
+    /*    bool make_sure_all_vars_have_bounds() {
         if (!m_has_int) {
             return true;
         }
@@ -1767,7 +1767,7 @@ public:
             }
         }
         return all_bounded;
-    }
+        }*/
 
     /**
      * n = (div p q)
@@ -1928,6 +1928,9 @@ public:
         case lp::GE: fml = a.mk_ge(a.mk_add(ts.size(), ts.c_ptr()), a.mk_numeral(rhs, true)); break;
         case lp::GT: fml = a.mk_gt(a.mk_add(ts.size(), ts.c_ptr()), a.mk_numeral(rhs, true)); break;
         case lp::EQ: fml = m.mk_eq(a.mk_add(ts.size(), ts.c_ptr()), a.mk_numeral(rhs, true)); break;
+        case lp::NE:
+            SASSERT(false); // unexpected
+            break;
         }
         return fml;
     }
@@ -1945,11 +1948,11 @@ public:
                 out << "v" << m_solver->local2external(wi) << "\n";
             }
         }
-        for (auto const& ev : ex.m_explanation) {
+        for (auto const& ev : ex) {
             m_solver->print_constraint(ev.second, out << ev.first << ": ");
         }
         expr_ref_vector fmls(m);
-        for (auto const& ev : ex.m_explanation) {
+        for (auto const& ev : ex) {
             fmls.push_back(constraint2fml(ev.second));
         }        
         expr_ref t(term2expr(term), m);
@@ -2040,7 +2043,7 @@ public:
             m_eqs.reset();
             m_core.reset();
             m_params.reset();
-            for (auto const& ev : ex.m_explanation) {
+            for (auto const& ev : ex) {
                 if (!ev.first.is_zero()) { 
                     set_evidence(ev.second);
                 }

src/util/lp/gomory.cpp

@@ -68,9 +68,9 @@ class gomory::imp {
             m_k.addmul(new_a, upper_bound(j).x);
             m_ex.push_justification(column_upper_bound_constraint(j));
         }
-        m_t.add_monomial(new_a, j);
+        m_t.add_coeff_var(new_a, j);
-        m_lcm_den = lcm(m_lcm_den, denominator(new_a));
+        lcm_den = lcm(lcm_den, denominator(new_a));
-        TRACE("gomory_cut_detail", tout << "v" << j << " new_a = " << new_a << ", k = " << m_k << ", m_lcm_den = " << m_lcm_den << "\n";);
+        TRACE("gomory_cut_detail", tout << "new_a = " << new_a << ", k = " << m_k << ", lcm_den = " << lcm_den << "\n";);
     }
 
     void real_case_in_gomory_cut(const mpq & a, unsigned j) {
@@ -98,8 +98,8 @@ class gomory::imp {
             m_k.addmul(new_a, upper_bound(j).x); //  k += upper_bound(j).x * new_a; 
             m_ex.push_justification(column_upper_bound_constraint(j));
         }
-        TRACE("gomory_cut_detail_real", tout << a << "*v" << j << " k: " << m_k << "\n";);
+        TRACE("gomory_cut_detail_real", tout << a << "*v" << x_j << " k: " << m_k << "\n";);
-        m_t.add_monomial(new_a, j);
+        m_t.add_coeff_var(new_a, x_j);
     }
 
     lia_move report_conflict_from_gomory_cut() {
@@ -124,12 +124,12 @@ class gomory::imp {
                 if (!m_k.is_int())
                     m_k = ceil(m_k);
                 // switch size
-                m_t.add_monomial(- mpq(1), v);
+                m_t.add_coeff_var(- mpq(1), v);
                 m_k.neg();
             } else {
                 if (!m_k.is_int())
                     m_k = floor(m_k);
-                m_t.add_monomial(mpq(1), v);
+                m_t.add_coeff_var(mpq(1), v);
             }
         } else {
             m_lcm_den = lcm(m_lcm_den, denominator(m_k));
@@ -144,10 +144,8 @@ class gomory::imp {
                 m_k *= m_lcm_den;
             }
             // negate everything to return -pol <= -m_k
-            for (const auto & pi: pol) {
+            for (const auto & pi: pol)
-                TRACE("gomory_cut", tout << pi.first << "* " << "v" << pi.second << "\n";);
+                m_t.add_coeff_var(-pi.first, pi.second);
-                m_t.add_monomial(-pi.first, pi.second);
-            }
             m_k.neg();
         }
         TRACE("gomory_cut_detail", tout << "k = " << m_k << std::endl;);

src/util/lp/int_solver.cpp

@@ -118,6 +118,17 @@ constraint_index int_solver::column_upper_bound_constraint(unsigned j) const {
     return m_lar_solver->get_column_upper_bound_witness(j);
 }
 
+bool int_solver::current_solution_is_inf_on_cut() const {
+    const auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x;
+    impq v = m_t->apply(x);
+    mpq sign = *m_upper ? one_of_type<mpq>()  : -one_of_type<mpq>();
+    CTRACE("current_solution_is_inf_on_cut", v * sign <= (*m_k) * sign,
+           tout << "m_upper = " << *m_upper << std::endl;
+           tout << "v = " << v << ", k = " << (*m_k) << std::endl;
+          );
+    return v * sign > (*m_k) * sign;
+}
+
 constraint_index int_solver::column_lower_bound_constraint(unsigned j) const {
     return m_lar_solver->get_column_lower_bound_witness(j);
 }

src/util/lp/lar_solver.cpp

@@ -1253,7 +1253,7 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign(
 void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values) const {
     lp_assert(m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis());
     mpq delta = mpq(1, 2); // start from 0.5 to have less clashes
-    unsigned j;
+    unsigned i;
     unsigned n = m_mpq_lar_core_solver.m_r_x.size();
     variable_values.resize(n);
     do {
@@ -1261,9 +1261,8 @@ void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values)
         std::unordered_set<impq> set_of_different_pairs; 
         std::unordered_set<mpq> set_of_different_singles;
         delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta);
-        for (j = 0; j < n; j++ ) {
+        for (i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) {
-            
+            const numeric_pair<mpq> & rp = m_mpq_lar_core_solver.m_r_x[i];
-            const numeric_pair<mpq> & rp = m_mpq_lar_core_solver.m_r_x[j];
             set_of_different_pairs.insert(rp);
             mpq x = rp.x + delta * rp.y;
             set_of_different_singles.insert(x);
@@ -1276,9 +1275,10 @@ void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values)
             if (!column_corresponds_to_term(j))
                 variable_values[j] = x;
         }
-    } while (j != m_mpq_lar_core_solver.m_r_x.size());
+    } while (i != m_mpq_lar_core_solver.m_r_x.size());
 }
 
+
 void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map<var_index, mpq> & variable_values) const {
     mpq delta = mpq(1);
     delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta);

src/util/lp/lar_solver.h

@@ -487,6 +487,8 @@ public:
 
     std::ostream& print_terms(std::ostream& out) const;
 
+    std::ostream& print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out) const;
+
     std::ostream& print_term(lar_term const& term, std::ostream & out) const;
 
     std::ostream& print_term_as_indices(lar_term const& term, std::ostream & out) const;