rebase with master

Signed-off-by: Lev Nachmanson <[email protected]>

src/math/lp/bound_analyzer_on_row.h

@@ -300,7 +300,7 @@ public :
                 int a_sign = is_pos(a) ? 1 : -1;
                 int sign = j_sign * a_sign;
                 u_dependency* witness = sign > 0 ? lar->get_column_upper_bound_witness(j) : lar->get_column_lower_bound_witness(j);
-                ret = lar->mk_join(ret, witness);
+                ret = lar->join_deps(ret, witness);
             }
             return ret;
         };

src/math/lp/dioph_eq.cpp

@@ -843,7 +843,8 @@ namespace lp {
                 if (!lia.column_is_int(p.var()))
                     return false;
             }
-            return true;
+            return lia.column_is_int(term.j());
+
         } 
 
         void delete_column(unsigned j) {
@@ -1470,9 +1471,9 @@ namespace lp {
             if (lra.has_upper_bound(j, b_dep, rs, is_strict)) {
                 if (m_c > rs || (is_strict && m_c == rs)) {
                     u_dependency* dep =
-                        lra.mk_join(explain_fixed(lra.get_term(j)),
+                        lra.join_deps(explain_fixed(lra.get_term(j)),
                                     explain_fixed_in_meta_term(m_term_with_index.m_data));
-                    dep = lra.mk_join(
+                    dep = lra.join_deps(
                         dep, lra.get_bound_constraint_witnesses_for_column(j));
                     for (constraint_index ci : lra.flatten(dep)) {
                         m_infeas_explanation.push_back(ci);
@@ -1483,9 +1484,9 @@ namespace lp {
             if (lra.has_lower_bound(j, b_dep, rs, is_strict)) {
                 if (m_c < rs || (is_strict && m_c == rs)) {
                     u_dependency* dep =
-                        lra.mk_join(explain_fixed(lra.get_term(j)),
+                        lra.join_deps(explain_fixed(lra.get_term(j)),
                                     explain_fixed_in_meta_term(m_term_with_index.m_data));
-                    dep = lra.mk_join(
+                    dep = lra.join_deps(
                         dep, lra.get_bound_constraint_witnesses_for_column(j));
                     for (constraint_index ci : lra.flatten(dep)) {
                         m_infeas_explanation.push_back(ci);
@@ -1539,14 +1540,14 @@ namespace lp {
             lconstraint_kind kind =
                 upper ? lconstraint_kind::LE : lconstraint_kind::GE;
             u_dependency* dep = prev_dep;
-            dep = lra.mk_join(dep, explain_fixed_in_meta_term(m_term_with_index.m_data));
+            dep = lra.join_deps(dep, explain_fixed_in_meta_term(m_term_with_index.m_data));
             u_dependency* j_bound_dep = upper
                 ? lra.get_column_upper_bound_witness(j)
                 : lra.get_column_lower_bound_witness(j);
-            dep = lra.mk_join(dep, j_bound_dep);
-            dep = lra.mk_join(dep, explain_fixed(lra.get_term(j)));
+            dep = lra.join_deps(dep, j_bound_dep);
+            dep = lra.join_deps(dep, explain_fixed(lra.get_term(j)));
             dep =
-                lra.mk_join(dep, lra.get_bound_constraint_witnesses_for_column(j));
+                lra.join_deps(dep, lra.get_bound_constraint_witnesses_for_column(j));
             TRACE("dioph_eq", tout << "jterm:";
                   print_lar_term_L(lra.get_term(j), tout) << "\ndep:";
                   print_deps(tout, dep) << std::endl;);
@@ -1570,7 +1571,7 @@ namespace lp {
                 if (is_fixed(p.j())) {
                     u_dependency* bound_dep =
                         lra.get_bound_constraint_witnesses_for_column(p.j());
-                    dep = lra.mk_join(dep, bound_dep);
+                    dep = lra.join_deps(dep, bound_dep);
                 }
             }
             return dep;

src/math/lp/explanation.h

@@ -26,10 +26,10 @@ class explanation {
     typedef vector<std::pair<unsigned, mpq>> pair_vec;
     typedef    hashtable<unsigned, u_hash, u_eq>  ci_set;
     // Only one of the fields below is used. The first call adding an entry decides which one it is.
-public:
     vector<std::pair<constraint_index, mpq>> m_vector;
     ci_set  m_set;   
-    explanation() {}
+public:
+    explanation() = default;
 
     template <typename T>
     explanation(const T& t) {

src/math/lp/gomory.cpp

@@ -323,7 +323,7 @@ struct create_cut {
 
         m_dep = nullptr;
         for (auto c : *m_ex) 
-         	m_dep = lia.lra.mk_join(lia.lra.dep_manager().mk_leaf(c.ci()), m_dep);
+         	m_dep = lia.lra.join_deps(lia.lra.dep_manager().mk_leaf(c.ci()), m_dep);
 
         TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);
               lia.lra.display(tout));
@@ -470,10 +470,10 @@ struct create_cut {
             if (!p.coeff().is_int()) continue;
             // the explanation for all above have been already added
             if (lia.at_lower(j))
-                ret = lia.lra.dep_manager().mk_join(lia.column_lower_bound_constraint(j), ret);
+                ret = lia.lra.join_deps(lia.column_lower_bound_constraint(j), ret);
             else {
                 SASSERT(lia.at_upper(j));
-                ret = lia.lra.dep_manager().mk_join(lia.column_upper_bound_constraint(j), ret);
+                ret = lia.lra.join_deps(lia.column_upper_bound_constraint(j), ret);
             }
         }
         return ret;

src/math/lp/lar_solver.h

@@ -606,7 +606,7 @@ class lar_solver : public column_namer {
     }
 
     void explain_fixed_column(unsigned j, explanation& ex);
-    u_dependency* mk_join(u_dependency* a, u_dependency *b) { return m_dependencies.mk_join(a, b); }
+    u_dependency* join_deps(u_dependency* a, u_dependency *b) { return m_dependencies.mk_join(a, b); }
     inline constraint_set const& constraints() const { return m_constraints; }
     void push();
     void pop();