#4702

initial gcd test implementation for accumulated parity constraints

src/math/lp/int_gcd_test.cpp

@@ -42,6 +42,8 @@ Accumulative:
     - Otherwise accumulate x = (c1 * lcm(b1,b2) / b2) + (c2 * lcm(b1,b2) / b1) mod lcm(b,b2)
       and accumulate the rows from R1, R2
 
+ 
+
 --*/
 
 #include "math/lp/int_solver.h"
@@ -53,10 +55,7 @@ namespace lp {
     int_gcd_test::int_gcd_test(int_solver& lia): lia(lia), lra(lia.lra), m_next_gcd(0), m_delay(0) {}
 
     bool int_gcd_test::should_apply() {
-
+        return lia.settings().int_run_gcd_test();
-        if (!lia.settings().int_run_gcd_test())
-            return false;
-        return true;
     }
 
     lia_move int_gcd_test::operator()() {              
@@ -76,6 +75,8 @@ namespace lp {
     }
 
     bool int_gcd_test::gcd_test() {
+        std::cout << "gcd-test\n";
+        reset_parities();
         const auto & A = lra.A_r(); // getting the matrix
         for (unsigned i = 0; i < A.row_count(); i++)
             if (!gcd_test_for_row(A, i)) 
@@ -95,44 +96,50 @@ namespace lp {
         auto const& row = A.m_rows[i];
         unsigned basic_var = lra.r_basis()[i];
         
-        if (!lia.column_is_int(basic_var) || lia.get_value(basic_var).is_int())
+        if (!lia.column_is_int(basic_var))
             return true;
-        mpq lcm_den = get_denominators_lcm(row);
+        m_lcm_den = get_denominators_lcm(row);
-        mpq consts(0);
+        m_consts = 0;
         mpq gcds(0);
-        mpq least_coeff(0);
+        m_least_coeff = 0;
-        bool    least_coeff_is_bounded = false;
+        bool least_coeff_is_bounded = false;
-        unsigned j;
+        bool least_coeff_is_unique = false;
+        unsigned least_coeff_index = 0;
         for (auto &c : A.m_rows[i]) {
-            j = c.var();
+            unsigned j = c.var();
             const mpq& a = c.coeff();
             if (lra.column_is_fixed(j)) {
-                mpq aux = lcm_den * a;
+                mpq aux = m_lcm_den * a;
-                consts += aux * lra.column_lower_bound(j).x;
+                m_consts += aux * lra.column_lower_bound(j).x;
             }
             else if (lra.column_is_real(j)) {
                 return true;
             }
             else if (gcds.is_zero()) {
-                gcds = abs(lcm_den * a);
+                gcds = abs(m_lcm_den * a);
-                least_coeff = gcds;
+                m_least_coeff = gcds;
                 least_coeff_is_bounded = lra.column_is_bounded(j);
+                least_coeff_is_unique = true;
+                least_coeff_index = j;
             }
             else {
-                mpq aux = abs(lcm_den * a);
+                mpq aux = abs(m_lcm_den * a);
                 gcds = gcd(gcds, aux);
-                if (aux < least_coeff) {
+                if (aux < m_least_coeff) {
-                    least_coeff = aux;
+                    m_least_coeff = aux;
                     least_coeff_is_bounded = lra.column_is_bounded(j);
+                    least_coeff_is_unique = true;
+                    least_coeff_index = j;
                 }
-                else if (least_coeff_is_bounded && aux == least_coeff) {
+                else if (least_coeff_is_bounded && aux == m_least_coeff) {
                     least_coeff_is_bounded = lra.column_is_bounded(j);
+                    least_coeff_is_unique = false;
                 }
             }
             SASSERT(gcds.is_int());
-            SASSERT(least_coeff.is_int());
+            SASSERT(m_least_coeff.is_int());
             TRACE("gcd_test_bug", tout << "coeff: " << a << ", gcds: " << gcds 
-                  << " least_coeff: " << least_coeff << " consts: " << consts << "\n";);
+                  << " least_coeff: " << m_least_coeff << " consts: " << m_consts << "\n";);
             
         }
         
@@ -143,31 +150,36 @@ namespace lp {
             return true;
         }
         
-        if (!(consts / gcds).is_int()) {
+        if (!(m_consts / gcds).is_int()) {
             TRACE("gcd_test", tout << "row failed the GCD test:\n"; lia.display_row_info(tout, i););
             fill_explanation_from_fixed_columns(A.m_rows[i]);
             return false;
         }
+
+        if (!least_coeff_is_unique)
+            lia.display_row(std::cout << "non-unique ", row);
         
-        if (least_coeff.is_one() && !least_coeff_is_bounded) {
+        if (m_least_coeff.is_one() && !least_coeff_is_bounded) {
             SASSERT(gcds.is_one());
-            return true;
+            if (!least_coeff_is_unique)
+                return true;
+            return accumulate_parity(row, least_coeff_index);
         }
         
-        if (least_coeff_is_bounded) {
+        if (least_coeff_is_bounded && !ext_gcd_test(A.m_rows[i]))
-            return ext_gcd_test(A.m_rows[i], least_coeff, lcm_den, consts);
+            return false;    
-        }
+
-        return true;
+        if (!least_coeff_is_unique)
+            return true;
+    
+        return accumulate_parity(row, least_coeff_index);
     }
     
-    bool int_gcd_test::ext_gcd_test(const row_strip<mpq> & row,
+    bool int_gcd_test::ext_gcd_test(const row_strip<mpq> & row) {
-                                  mpq const & least_coeff, 
-                                  mpq const & lcm_den,
-                                  mpq const & consts) {
         TRACE("ext_gcd_test", tout << "row = "; lra.print_row(row, tout););
         mpq gcds(0);
-        mpq l(consts);
+        mpq l(m_consts);
-        mpq u(consts);
+        mpq u(m_consts);
         
         mpq a;
         unsigned j;
@@ -178,10 +190,10 @@ namespace lp {
             if (lra.column_is_fixed(j))
                 continue;
             SASSERT(!lra.column_is_real(j));
-            mpq ncoeff = lcm_den * a;
+            mpq ncoeff = m_lcm_den * a;
             SASSERT(ncoeff.is_int());
             mpq abs_ncoeff = abs(ncoeff);
-            if (abs_ncoeff == least_coeff) {
+            if (abs_ncoeff == m_least_coeff) {
                 SASSERT(lra.column_is_bounded(j));
                 if (ncoeff.is_pos()) {
                     // l += ncoeff * lra.column_lower_bound(j).x;
@@ -235,4 +247,63 @@ namespace lp {
         lia.m_ex->push_back(uc);
     }
 
+    bool int_gcd_test::accumulate_parity(const row_strip<mpq> & row, unsigned least_idx) {
+
+        // remove this line to enable new functionality.
+        return true;
+
+        mpq modulus(0);
+        bool least_sign = false;
+        for (const auto & c : row) {
+            unsigned j = c.var();
+            const mpq& a = c.coeff();
+            if (j == least_idx) 
+                least_sign = a.is_neg();
+            else if (!lra.column_is_fixed(j)) {
+                mpq aux = abs(m_lcm_den * a);
+                if (gcd(m_least_coeff, aux) != m_least_coeff)
+                    return true;
+                modulus = modulus == 0 ? aux : gcd(modulus, aux);
+                if (modulus.is_one())
+                    return true;
+            }
+        }
+        modulus /= m_least_coeff;
+        if (modulus == 0)
+            return true;
+        SASSERT(modulus.is_int());
+        mpq parity = m_consts / m_least_coeff;
+        if (!parity.is_int())
+            return true;
+        parity = mod(parity, modulus);
+        if (!least_sign && parity != 0)
+            parity = modulus - parity;
+        TRACE("gcd_test", tout << least_idx << " modulus: " << modulus << " consts: " << m_consts << " sign " << least_sign << " parity: " << parity << "\n";);
+
+        SASSERT(0 <= parity && parity < modulus);
+        return insert_row_parity(least_idx, row, parity, modulus);
+    }
+
+    void int_gcd_test::reset_parities() {
+        for (auto j : m_inserted_rows)
+            m_row_parities[j].pop_back();
+        m_inserted_rows.reset();
+    }
+
+    bool int_gcd_test::insert_row_parity(unsigned j, row_strip<mpq> const& r, mpq const& parity, mpq const& modulo) {
+        m_row_parities.reserve(j + 1);
+
+        // incomplete parity check.
+        for (auto const& p : m_row_parities[j]) {            
+            if (p.m_modulo == modulo && parity != p.m_parity) {
+                fill_explanation_from_fixed_columns(r);
+                fill_explanation_from_fixed_columns(*p.m_row);
+                return false;
+            }
+        }
+        m_inserted_rows.push_back(j);        
+        m_row_parities[j].push_back(row_parity(parity, modulo, r));
+        return true;
+    }
+
 }

src/math/lp/int_gcd_test.h

@@ -32,19 +32,36 @@ namespace lp {
     class int_solver;
     class lar_solver;
     class int_gcd_test {
+
+        struct row_parity {
+            mpq m_parity;
+            mpq m_modulo;
+            const row_strip<mpq>* m_row = nullptr;
+            row_parity(mpq const& p, mpq const& m, row_strip<mpq> const& r):
+                m_parity(p),
+                m_modulo(m),
+                m_row(&r)
+            {}
+        };
         class int_solver& lia;
         class lar_solver& lra;
         unsigned m_next_gcd;
         unsigned m_delay;
+        mpq m_consts;
+        mpq m_least_coeff;
+        mpq m_lcm_den;
+        unsigned_vector            m_inserted_rows;
+        vector<vector<row_parity>> m_row_parities;
+
+        void reset_parities();
+        bool insert_row_parity(unsigned j, row_strip<mpq> const& r, mpq const& parity, mpq const& modulo);
 
         bool gcd_test();
         bool gcd_test_for_row(const static_matrix<mpq, numeric_pair<mpq>> & A, unsigned i);
-        bool ext_gcd_test(const row_strip<mpq> & row,
+        bool ext_gcd_test(const row_strip<mpq> & row);
-                                        mpq const & least_coeff, 
-                                        mpq const & lcm_den,
-                                        mpq const & consts);
         void fill_explanation_from_fixed_columns(const row_strip<mpq> & row);
         void add_to_explanation_from_fixed_or_boxed_column(unsigned j);
+        bool accumulate_parity(const row_strip<mpq> & row, unsigned least_coeff_index);
     public:
         int_gcd_test(int_solver& lia);
         lia_move operator()();

src/smt/theory_lra.cpp

@@ -1541,8 +1541,8 @@ public:
 
         switch (is_sat) {
         case l_true:
-            TRACE("arith", /*display(tout);*/
+            TRACE("arith", display(tout);
-                  ctx().display(tout);
+                  /* ctx().display(tout);*/
                   );
 
             switch (check_lia()) {