crash

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

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/dioph_eq.cpp

@@ -0,0 +1,64 @@
+#include "math/lp/dioph_eq.h"
+#include "math/lp/int_solver.h"
+#include "math/lp/lar_solver.h"
+#include "math/lp/lp_utils.h"
+
+namespace lp {
+    struct imp {
+    
+        int_solver& lia;
+        lar_solver& lra;
+
+        imp(int_solver& lia, lar_solver& lra): lia(lia), lra(lra) {}
+        vector<lar_term> m_e;
+            
+        void init() {
+            int n_of_rows = lra.r_basis().size();
+            unsigned skipped = 0;
+            for (unsigned i = 0; i < lra.r_basis().size(); i++) {
+                auto & row = lra.get_row(i);
+                lar_term t;
+                bool is_int = true;
+                for (const auto & p : row) {
+                    if (!lia.column_is_int(p.var()))
+                        is_int = false;
+                }
+                if (is_int) {
+                    lar_term t;
+                    const auto lcm = get_denominators_lcm(row);
+                    for (const auto & p: row) {
+                        t.add_monomial(lcm * p.coeff(), p.var());
+                    }
+                    m_e.push_back(t);
+                } else {
+                    skipped ++;
+                }
+            }
+            if (m_e.size() > 0) {
+                std::cout << "collected " << m_e.size() << ", skipped " << skipped << "\n";
+                for (const auto & t: m_e) {
+                    lra.print_term(t, std::cout) << "\n";
+                }
+                std::cout << "________________________\n";
+            }
+        }
+
+        lia_move check() {
+            init();
+            return lia_move::undef;
+        }
+    };
+// Constructor definition
+    dioph_eq::dioph_eq(int_solver& lia): lia(lia) {
+        m_imp = alloc(imp, lia, lia.lra);
+    }
+    dioph_eq::~dioph_eq() {
+        dealloc(m_imp);
+    }
+    
+    lia_move dioph_eq::check() {
+        return m_imp->check();
+        
+    }
+    
+}

src/math/lp/dioph_eq.h

@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2024 Microsoft Corporation
+
+Module Name:
+
+    diophantine equations
+
+Abstract:
+
+    Following "A Practical Approach to Satisfiability  Modulo Linear Integer Arithmetic"
+    by Alberto Griggio(griggio@fbk.eu)
+
+Author:
+    Lev Nachmanson (levnach)
+
+Revision History:
+--*/
+#pragma once
+#include "math/lp/lia_move.h"
+
+namespace lp {
+    struct imp;
+    class int_solver;
+    class dioph_eq {
+        int_solver& lia;
+        imp*        m_imp;
+    public:
+        dioph_eq(int_solver& lia);
+        ~dioph_eq();
+        lia_move check();
+    };
+}

src/math/lp/int_gcd_test.cpp

@@ -101,13 +101,6 @@ namespace lp {
         return true;
     }
         
-    static mpq get_denominators_lcm(const row_strip<mpq> & row) {
-        mpq r(1);
-        for (auto & c : row) 
-            r = lcm(r, denominator(c.coeff()));
-        return r;
-    }
-    
     bool int_gcd_test::gcd_test_for_row(const static_matrix<mpq, numeric_pair<mpq>> & A, unsigned i) {
         auto const& row = A.m_rows[i];
         unsigned basic_var = lra.r_basis()[i];

src/math/lp/int_solver.cpp

@@ -9,6 +9,7 @@
 #include "math/lp/gomory.h"
 #include "math/lp/int_branch.h"
 #include "math/lp/int_cube.h"
+#include "math/lp/dioph_eq.h"
 
 namespace lp {
     bool get_patching_deltas(const rational& x, const rational& alpha,
@@ -39,7 +40,6 @@ namespace lp {
         mpq                 m_k;               // the right side of the cut
         hnf_cutter          m_hnf_cutter;
         unsigned            m_hnf_cut_period;
-        unsigned_vector     m_cut_vars;        // variables that should not be selected for cuts
         int_gcd_test        m_gcd;
 
         bool column_is_int_inf(unsigned j) const {
@@ -163,11 +163,8 @@ namespace lp {
             return lia_move::undef;     
         }
 
-        void init_dioph_eq() {
-        }
-
         lia_move solve_dioph_eq() {
-            init_dioph_eq();
+            //dioph_eq de(lia);
             return lia_move::undef;
         }
 
@@ -209,7 +206,6 @@ namespace lp {
             m_ex = e;
             m_ex->clear();
             m_upper = false;
-            m_cut_vars.reset();
         
             lia_move r = lia_move::undef;
 
@@ -278,8 +274,6 @@ namespace lp {
             for (unsigned j : lra.r_basis()) {
                 if (!column_is_int_inf(j))
                     continue;
-                if (m_cut_vars.contains(j))
-                    continue;
 
                 SASSERT(!lia.is_fixed(j));
 
@@ -489,6 +483,7 @@ namespace lp {
         return lra.column_count();
     }
 
+
     static void set_lower(impq & l, bool & inf_l, impq const & v ) {
         if (inf_l || v > l) {
             l = v;

src/math/lp/int_solver.h

@@ -40,7 +40,7 @@ class int_solver {
     friend class int_gcd_test;
     friend class hnf_cutter;
     friend struct imp;
-
+    friend class dioph_eq;
     lar_solver&         lra;
     lar_core_solver&    lrac;
     imp*                m_imp; 

src/math/lp/lia_move.h

@@ -18,6 +18,8 @@ Revision History:
 
 --*/
 #pragma once
+#include <string>
+#include "util/debug.h"
 namespace lp {
     enum class lia_move {
         sat,

src/math/lp/static_matrix.cpp

@@ -26,6 +26,13 @@ Revision History:
 #include "math/lp/lp_primal_core_solver.h"
 #include "math/lp/lar_solver.h"
 namespace lp {
+mpq get_denominators_lcm(const row_strip<mpq> & row) {
+    mpq r(1);
+    for (auto & c : row) 
+        r = lcm(r, denominator(c.coeff()));
+    return r;
+}
+    
 template std::set<std::pair<unsigned, unsigned>> lp::static_matrix<lp::mpq, lp::mpq>::get_domain();
 template std::set<std::pair<unsigned, unsigned>> lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::get_domain();
 template void static_matrix<mpq, mpq>::add_column_to_vector(mpq const&, unsigned int, mpq*) const;

src/math/lp/static_matrix.h

@@ -45,6 +45,8 @@ typedef vector<column_cell> column_strip;
 
 template <typename T>
 using row_strip = vector<row_cell<T>>; 
+mpq get_denominators_lcm(const row_strip<mpq> & row);
+    
 template <typename T>
 std::ostream& operator<<(std::ostream& out, const row_strip<T>& r) {
     for (auto const& c : r)