na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/polysat/fixplex.h

@@ -30,11 +30,15 @@ namespace polysat {
 
     template<typename Ext>
     class fixplex {
-
+    public:
         typedef typename Ext::numeral numeral;
         typedef typename Ext::scoped_numeral scoped_numeral;
         typedef typename Ext::manager manager;
         typedef simplex::sparse_matrix<Ext> matrix;
+        typedef typename matrix::row row;
+        typedef typename matrix::row_iterator row_iterator;
+        typedef typename matrix::col_iterator col_iterator;
+    protected:
         struct var_lt {
             bool operator()(var_t v1, var_t v2) const { return v1 < v2; }
         };
@@ -76,6 +80,13 @@ namespace polysat {
             numeral m_base_coeff;            
         };
 
+        struct offset_eq {
+            var_t x, y;
+            row r1, r2;
+            offset_eq(var_t x, var_t y, row const& r1, row const& r2):
+                x(x), y(y), r1(r1), r2(r2) {}
+        };
+
         static const var_t null_var = UINT_MAX;
         reslimit&                   m_limit;
         mutable manager             m;
@@ -85,6 +96,7 @@ namespace polysat {
         var_heap                    m_to_patch;
         vector<var_info>            m_vars;
         vector<row_info>            m_rows;
+        vector<offset_eq>           m_offset_eqs;
         bool                        m_bland { false };
         unsigned                    m_blands_rule_threshold { 1000 };
         random_gen                  m_random;
@@ -101,9 +113,6 @@ namespace polysat {
 
         ~fixplex();
 
-        typedef typename matrix::row row;
-        typedef typename matrix::row_iterator row_iterator;
-        typedef typename matrix::col_iterator col_iterator;
 
         void set_bounds(var_t v, numeral const& lo, numeral const& hi);
         void unset_bounds(var_t v) { m_vars[v].m_lo = m_vars[v].m_hi; }
@@ -141,7 +150,10 @@ namespace polysat {
         lbool make_var_feasible(var_t x_i);
         bool is_infeasible_row(var_t x);
         bool is_parity_infeasible_row(var_t x);
-        bool is_offset_row(row const& r, var_t& x, var_t & y) const;
+        bool is_offset_row(row const& r, numeral& cx, var_t& x, numeral& cy, var_t & y) const;
+        void lookahead_eq(row const& r1, numeral const& cx, var_t x, numeral const& cy, var_t y);
+        void get_offset_eqs(row const& r);
+        void eq_eh(var_t x, var_t y, row const& r1, row const& r2);
         void pivot(var_t x_i, var_t x_j, numeral const& b, numeral const& value);
         numeral value2delta(var_t v, numeral const& new_value) const;
         void update_value(var_t v, numeral const& delta);
@@ -153,6 +165,7 @@ namespace polysat {
         bool in_bounds(numeral const& val, numeral const& lo, numeral const& hi) const;        
         bool is_free(var_t v) const { return lo(v) == hi(v); }
         bool is_non_free(var_t v) const { return !is_free(v); }
+        bool is_fixed(var_t v) const { return lo(v) + 1 == hi(v); }
         bool is_base(var_t x) const { return m_vars[x].m_is_base; }
         unsigned base2row(var_t x) const { return m_vars[x].m_base2row; }
         numeral const& row2value(row const& r) const { return m_rows[r.id()].m_value; }
@@ -198,6 +211,7 @@ namespace polysat {
             void del(numeral const& n) {}
             bool is_zero(numeral const& n) const { return n == 0; }
             bool is_one(numeral const& n) const { return n == 1; }
+            bool is_even(numeral const& n) const { return (n & 1) == 0; }
             bool is_minus_one(numeral const& n) const { return max_numeral == n; }
             void add(numeral const& a, numeral const& b, numeral& r) { r = a + b; }
             void sub(numeral const& a, numeral const& b, numeral& r) { r = a - b; }
@@ -206,6 +220,7 @@ namespace polysat {
             void neg(numeral& a) { a = 0 - a; }
             numeral inv(numeral const& a) { return 0 - a; }
             void swap(numeral& a, numeral& b) { std::swap(a, b); }
+            unsigned trailing_zeros(numeral const& a) const { return ::trailing_zeros(a); }
 
             // treat numerals as signed and check for overflow/underflow
             bool signed_mul(numeral& r, numeral const& x, numeral const& y) { 
@@ -218,7 +233,9 @@ namespace polysat {
                 r = x + y; 
                 return x <= r;
             }
-            std::ostream& display(std::ostream& out, numeral const& x) const { return out << x; }
+            std::ostream& display(std::ostream& out, numeral const& x) const { 
+                return out << x; 
+            }
         };
         typedef _scoped_numeral<manager> scoped_numeral;
     };

src/math/polysat/fixplex_def.h

@@ -216,7 +216,11 @@ namespace polysat {
                 return l_undef;
         }
 
+        
         pivot(x, y, b, new_value);
+
+        get_offset_eqs(row(base2row(y)));
+
         return l_true;
     }
 
@@ -345,12 +349,12 @@ namespace polysat {
      */
     template<typename Ext>
     bool fixplex<Ext>::has_minimal_trailing_zeros(var_t y, numeral const& b) {
-        unsigned tz1 = trailing_zeros(b);
+        unsigned tz1 = m.trailing_zeros(b);
         if (tz1 == 0)
             return true;
         for (auto col : M.col_entries(y)) {
             numeral c = col.get_row_entry().m_coeff;
-            unsigned tz2 = trailing_zeros(c);
+            unsigned tz2 = m.trailing_zeros(c);
             if (tz1 > tz2)
                 return false;
         }
@@ -420,10 +424,10 @@ namespace polysat {
             if (is_fixed(v))
                 fixed += value(v)*c;
             else 
-                parity = std::min(trailing_zeros(c), parity);
+                parity = std::min(m.trailing_zeros(c), parity);
         }
 
-        if (trailing_zeros(fixed) < parity)
+        if (m.trailing_zeros(fixed) < parity)
             return true;
         
         return false;
@@ -484,7 +488,7 @@ namespace polysat {
         add_patch(y);
         SASSERT(well_formed_row(r_x));
 
-        unsigned tz1 = trailing_zeros(b);
+        unsigned tz1 = m.trailing_zeros(b);
  
         for (auto col : M.col_entries(y)) {
             row r_z = col.get_row();
@@ -495,7 +499,7 @@ namespace polysat {
             auto& row_z = m_rows[rz];
             var_info& zI = m_vars[z];
             numeral c = col.get_row_entry().m_coeff;
-            unsigned tz2 = trailing_zeros(c);
+            unsigned tz2 = m.trailing_zeros(c);
             SASSERT(tz1 <= tz2);
             numeral b1 = b >> tz1;
             numeral c1 = m.inv(c >> (tz2 - tz1));
@@ -631,24 +635,83 @@ namespace polysat {
 
     /**
      * Equality detection.
+     *
+     * Offset equality detection
+     * -------------------------
+     * is_offset_row: determine if row is cx*x + cy*y + k == 0 where k is a constant.
+     * Then walk every row containing x, y, respectively
+     * If there is a row cx*x + cy*z + k' == 0, where y, z are two different variables
+     * but value(y) = value(z), cy is odd
+     * then it follows that k = k' and y = z is implied.
+     * 
+     * Offset equality detection is only applied to integral rows where the current  
+     * evaluation satisfies the row equality.
+     *
+     * Fixed variable equalities
+     * -------------------------
+     * 
      */
+
     template<typename Ext>
-    bool fixplex<Ext>::is_offset_row(row const& r, var_t& x, var_t & y) const {
+    void fixplex<Ext>::get_offset_eqs(row const& r) {
+        var_t x, y;
+        numeral cx, cy;
+        if (!is_offset_row(r, cx, x, cy, y))
+            return;
+        lookahead_eq(r, cx, x, cy, y);
+        lookahead_eq(r, cy, y, cx, x);
+    }
+
+    template<typename Ext>
+    bool fixplex<Ext>::is_offset_row(row const& r, numeral& cx, var_t& x, numeral& cy, var_t & y) const {
         x = null_var;
         y = null_var;
+        if (!row2integral(r))
+            return false;
         for (auto const& e : M.row_entries(r)) {
             var_t v = e.m_var;
             if (is_fixed(v))
                 continue;
             numeral const& c = e.m_coeff;
-            if (c == 1 && x == null_var)
+            if (x == null_var) {
+                cx = c;
                 x = v;
-            else if (c + 1 == 0 && y == null_var)
+            }
+            else if (y == null_var) {
+                cy = c;
                 y = v;
+            }
             else
                 return false;
         }        
-        return true;
+        return y != null_var;
+    }
+
+
+    template<typename Ext>
+    void fixplex<Ext>::lookahead_eq(row const& r1, numeral const& cx, var_t x, numeral const& cy, var_t y) {   
+        if (m.is_even(cy))
+            return;
+        var_t z, u;
+        numeral cz, cu;
+        for (auto c : M.col_entries(x)) {
+            auto r2 = c.get_row();
+            if (r1.id() == r2.id())
+                continue;
+            if (!is_offset_row(r2, cz, z, cu, u))
+                continue;
+            if (u == x) {
+                std::swap(z, u);
+                std::swap(cz, cu);
+            }
+            if (z == x && cx == cz && u != y && cu == cy && value(u) == value(y)) 
+                eq_eh(u, y, r1, r2);                
+        }
+    }
+
+    template<typename Ext>
+    void fixplex<Ext>::eq_eh(var_t x, var_t y, row const& r1, row const& r2) {
+        m_offset_eqs.push_back(offset_eq(x, y, r1, r2));
     }
     
 
@@ -681,11 +744,12 @@ namespace polysat {
     bool fixplex<Ext>::well_formed() const { 
         SASSERT(M.well_formed());
         for (unsigned i = 0; i < m_rows.size(); ++i) {
-            var_t s = m_rows[i].m_base;
+            row r(i);
+            var_t s = row2base(r);
             if (s == null_var) 
                 continue;
             SASSERT(i == base2row(s));
-            VERIFY(well_formed_row(row(i)));            
+            VERIFY(well_formed_row(r));
         }
         for (unsigned i = 0; i < m_vars.size(); ++i) {
             SASSERT(is_base(i) || in_bounds(i));