Integrate Diophantine handler

src/math/lp/.clang-format

@@ -2,4 +2,4 @@ BasedOnStyle: Google
 IndentWidth: 4
 ColumnLimit: 0
 NamespaceIndentation: All
-BreakBeforeBraces: Stroustrup
+BreakBeforeBraces: Attach

src/math/lp/CMakeLists.txt

@@ -2,6 +2,7 @@ z3_add_component(lp
   SOURCES
     core_solver_pretty_printer.cpp
     dense_matrix.cpp
+    dioph_eq.cpp
     emonics.cpp
     factorization.cpp
     factorization_factory_imp.cpp

src/math/lp/column.h

@@ -36,14 +36,10 @@ inline std::ostream& operator<<(std::ostream& out, lconstraint_kind k) {
     return out << "??";
 }
 
-inline bool compare(const std::pair<mpq, lpvar> & a, const std::pair<mpq, lpvar> & b) {
-    return a.second < b.second;
-}
 class lar_term; // forward definition
 class column {
     u_dependency* m_lower_bound_witness = nullptr;
     u_dependency* m_upper_bound_witness = nullptr;
-    bool          m_associated_with_row = false;  
     lar_term*     m_term = nullptr;
 public:
     lar_term*  term() const { return m_term; }
@@ -53,26 +49,11 @@ class column {
     u_dependency*& upper_bound_witness() { return m_upper_bound_witness; }
     u_dependency* upper_bound_witness() const { return m_upper_bound_witness; }
 
-    // equality is used by stackedvector operations.
-    // this appears to be a low level reason
-
-    bool operator!=(const column & p) const {
-        return !(*this == p);
-    }
-
-    bool operator==(const column & p) const {
-        return m_lower_bound_witness == p.m_lower_bound_witness
-            && m_upper_bound_witness == p.m_upper_bound_witness 
-            && m_associated_with_row == p.m_associated_with_row;
-    }
-    column()  = delete;
-    column(bool) = delete;
+    column() {}
 
-
-    column(bool associated_with_row, lar_term* term) :
-        m_associated_with_row(associated_with_row), m_term(term) {}
+    column(lar_term* term) : m_term(term) {}
 
-    bool associated_with_row() const { return m_associated_with_row; }
+    bool associated_with_row() const { return m_term != nullptr; }
 };
 
 }