enable fixed propagation from inequalities

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

src/math/bigfix/u256.cpp

@@ -43,6 +43,11 @@ u256::u256(uint64_t const* v) {
     std::uninitialized_copy(v, v + 4, m_num);
 }
 
+unsigned u256::hash() const {
+    uint64_t h = m_num[0] + m_num[1] + m_num[2] + m_num[3];
+    return static_cast<unsigned>(h ^ (h >> 32ull));
+}
+
 u256 u256::operator*(u256 const& other) const {
     // TBD: maybe just use mpn_manager::mul?
     uint64_t result[8];

src/math/bigfix/u256.h

@@ -16,6 +16,7 @@ public:
         *this = u256(n);
         return *this;
     }
+    unsigned hash() const;
     u256 operator*(u256 const& other) const;
     u256 operator+(u256 const& other) const { u256 r = *this; return r += other; }
     u256 operator-(u256 const& other) const { u256 r = *this; return r -= other; }

src/math/polysat/fixplex.h

@@ -33,6 +33,11 @@ Author:
 inline rational to_rational(uint64_t n) { return rational(n, rational::ui64()); }
 inline unsigned trailing_zeros(unsigned short n) { return trailing_zeros((uint32_t)n); }
 inline unsigned trailing_zeros(unsigned char n) { return trailing_zeros((uint32_t)n); }
+inline unsigned numeral2hash(unsigned char const& n) { return n; }
+inline unsigned numeral2hash(unsigned short const& n) { return n; }
+inline unsigned numeral2hash(uint32_t const& n) { return n; }
+inline unsigned numeral2hash(uint64_t const& n) { return static_cast<unsigned>(n ^ (n >> 32)); }
+
 
 namespace polysat {
 
@@ -86,9 +91,9 @@ namespace polysat {
 
         struct var_eq {
             var_t x, y;
-            row r1, r2;
+            u_dependency* dep;
-            var_eq(var_t x, var_t y, row const& r1, row const& r2):
+            var_eq(var_t x, var_t y, u_dependency* dep):
-                x(x), y(y), r1(r1), r2(r2) {}
+                x(x), y(y), dep(dep) {}
         };
 
     protected:
@@ -152,10 +157,10 @@ namespace polysat {
         };
 
         struct fix_entry {
-            var_t x;
+            var_t x = null_var;
-            row r;
+            u_dependency* dep = nullptr;
-            fix_entry(var_t x, row const& r): x(x), r(r) {}
+            fix_entry(var_t x, u_dependency* dep): x(x), dep(dep) {}
-            fix_entry():x(null_var), r(0) {}
+            fix_entry() {}
         };
 
         enum trail_i {
@@ -163,7 +168,9 @@ namespace polysat {
             set_bound_i,
             set_inconsistent_i,
             add_ineq_i,
-            add_row_i
+            add_row_i,
+            add_eq_i,
+            fixed_val_i
         };
 
         static const var_t null_var = UINT_MAX;
@@ -177,6 +184,7 @@ namespace polysat {
         vector<var_info>            m_vars;
         vector<row_info>            m_rows;
         vector<var_eq>              m_var_eqs;
+        vector<numeral>             m_fixed_vals;
         bool                        m_bland = false ;
         unsigned                    m_blands_rule_threshold = 1000;
         unsigned                    m_num_repeated = 0;
@@ -238,12 +246,11 @@ namespace polysat {
         unsigned get_num_vars() const { return m_vars.size(); }
         void reset();
 
-        svector<std::pair<unsigned, ineq>> stack;
+        svector<std::pair<unsigned, unsigned>> stack;
         uint_set on_stack;
-        lbool propagate_ineqs(ineq& i0);
+        lbool propagate_ineqs(unsigned idx);
         void propagate_eqs();
         vector<var_eq> const& var_eqs() const { return m_var_eqs; }
-        void reset_eqs() { m_var_eqs.reset(); }
 
         void add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs);
         
@@ -268,8 +275,8 @@ namespace polysat {
         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 fixed_var_eh(row const& r, var_t x);
+        void fixed_var_eh(u_dependency* dep, var_t x);
-        void eq_eh(var_t x, var_t y, row const& r1, row const& r2);
+        void eq_eh(var_t x, var_t y, u_dependency* dep);
         bool propagate_row(row const& r);
         bool propagate_ineq(ineq const& i);
         bool propagate_strict_bounds(ineq const& i);
@@ -349,7 +356,7 @@ namespace polysat {
             typedef uint_type numeral;
             struct hash {
                 unsigned operator()(numeral const& n) const { 
-                    return static_cast<unsigned>(n); 
+                    return numeral2hash(n); 
                 }
             };
             struct eq {

src/math/polysat/fixplex_def.h

@@ -82,7 +82,6 @@ namespace polysat {
         reset();
     }
 
-
     template<typename Ext>
     void fixplex<Ext>::updt_params(params_ref const& p) {
         m_max_iterations = p.get_uint("max_iterations", m_max_iterations);
@@ -117,6 +116,13 @@ namespace polysat {
                 m_inconsistent = false;
                 m_unsat_core.reset();
                 break;
+            case trail_i::add_eq_i:
+                m_var_eqs.pop_back();
+                break;
+            case trail_i::fixed_val_i:
+                m_value2fixed_var.erase(m_fixed_vals.back());
+                m_fixed_vals.pop_back();
+                break;
             default:
                 UNREACHABLE();
             }
@@ -142,7 +148,6 @@ namespace polysat {
         m_rows.reset();
         m_left_basis.reset();
         m_base_vars.reset();
-        m_var_eqs.reset();
     }
 
     template<typename Ext>
@@ -275,7 +280,6 @@ namespace polysat {
 
     template<typename Ext>
     void fixplex<Ext>::del_row(row const& r) {
-        m_var_eqs.reset();
         var_t var = row2base(r);
         m_vars[var].m_is_base = false;
         m_vars[var].set_free();
@@ -668,13 +672,12 @@ namespace polysat {
     template<typename Ext>
     bool fixplex<Ext>::propagate() {
         lbool r;
-        for (unsigned idx : m_ineqs_to_propagate) {
+        while (!m_ineqs_to_propagate.empty()) {
-            if (idx >= m_ineqs.size())
+            unsigned idx = *m_ineqs_to_propagate.begin();        
-                continue;
+            if (idx < m_ineqs.size() && (r = propagate_ineqs(idx), r == l_false))
-            if (r = propagate_ineqs(m_ineqs[idx]), r == l_false)
                 return false;
-        }
+            m_ineqs_to_propagate.remove(idx);
-        m_ineqs_to_propagate.reset();
+        }        
         return true;
     }
 
@@ -1111,9 +1114,9 @@ namespace polysat {
                 std::swap(cz, cu);
             }
             if (z == x && u != y && cx == cz && cu == cy && value(u) == value(y)) 
-                eq_eh(u, y, r1, r2);                
+                eq_eh(u, y, m_deps.mk_join(row2dep(r1), row2dep(r2)));                
             if (z == x && u != y && cx + cz == 0 && cu + cy == 0 && value(u) == value(y)) 
-                eq_eh(u, y, r1, r2);                
+                eq_eh(u, y, m_deps.mk_join(row2dep(r1), row2dep(r2)));
 
         }
     }
@@ -1122,18 +1125,24 @@ namespace polysat {
      * Accumulate equalities between variables fixed to the same values.
      */
     template<typename Ext>
-    void fixplex<Ext>::fixed_var_eh(row const& r, var_t x) {
+    void fixplex<Ext>::fixed_var_eh(u_dependency* dep, var_t x) {
         numeral val = value(x);
         fix_entry e;
-        if (m_value2fixed_var.find(val, e) && is_valid_variable(e.x) && is_fixed(e.x) && value(e.x) == val && e.x != x) 
+        if (m_value2fixed_var.find(val, e)) {
-            eq_eh(x, e.x, e.r, r);
+            SASSERT(x != e.x);
-        else 
+            eq_eh(x, e.x, m_deps.mk_join(e.dep, dep));
-            m_value2fixed_var.insert(val, fix_entry(x, r));
+        }
+        else {
+            m_value2fixed_var.insert(val, fix_entry(x, dep));
+            m_fixed_vals.push_back(val);
+            m_trail.push_back(trail_i::fixed_val_i);
+        }
     }
 
     template<typename Ext>
-    void fixplex<Ext>::eq_eh(var_t x, var_t y, row const& r1, row const& r2) {
+    void fixplex<Ext>::eq_eh(var_t x, var_t y, u_dependency* dep) {
-        m_var_eqs.push_back(var_eq(x, y, r1, r2));
+        m_var_eqs.push_back(var_eq(x, y, dep));
+        m_trail.push_back(trail_i::add_eq_i);
     }    
 
 #if 0
@@ -1165,7 +1174,8 @@ namespace polysat {
     //
 
     template<typename Ext>
-    lbool fixplex<Ext>::propagate_ineqs(ineq& i0) {
+    lbool fixplex<Ext>::propagate_ineqs(unsigned i0_idx) {
+        ineq i0 = m_ineqs[i0_idx];
         numeral old_lo = m_vars[i0.w].lo;
         SASSERT(!m_inconsistent);
         // std::cout << "propagate " << i0 << "\n";
@@ -1173,12 +1183,13 @@ namespace polysat {
             return l_false;
         on_stack.reset();
         stack.reset();
-        stack.push_back(std::make_pair(0, i0));
+        stack.push_back(std::make_pair(0, i0_idx));
         on_stack.insert(i0.v);
         while (!stack.empty()) {
             if (!m_limit.inc())
                 return l_undef;
-            auto [ineq_out, i] = stack.back();        
+            auto [ineq_out, i_idx] = stack.back();        
+            ineq i = m_ineqs[i_idx];
             auto const& ineqs = m_var2ineqs[i.w];
             for (; ineq_out < ineqs.size(); ++ineq_out) {
                 auto& i_out = m_ineqs[ineqs[ineq_out]];
@@ -1192,10 +1203,10 @@ namespace polysat {
                     return l_false;      
                 
                 bool is_onstack = on_stack.contains(i_out.w);
-                if ((old_lo != m_vars[i_out.w].lo) && !is_onstack) {
+                if ((old_lo != m_vars[i_out.w].lo || m_ineqs_to_propagate.contains(ineqs[ineq_out])) && !is_onstack) {
                     on_stack.insert(i_out.w);
                     stack.back().first = ineq_out + 1;
-                    stack.push_back(std::make_pair(0, i_out));
+                    stack.push_back(std::make_pair(0, ineqs[ineq_out]));
                     break;
                 }
 
@@ -1208,7 +1219,7 @@ namespace polysat {
                 auto bound = m_vars[i_out.w];
                 unsigned j = stack.size();
                 for (; !found && j-- > 0; ) {
-                    ineq i2 = stack[j].second;
+                    ineq i2 = m_ineqs[stack[j].second];
                     strict |= i2.strict;
                     bound &= m_vars[i2.w];
                     if (i2.v == i_out.w) 
@@ -1219,12 +1230,13 @@ namespace polysat {
                 if ((empty || strict) && found) {
                     auto* d = i_out.dep;
                     for (; j < stack.size(); ++j) 
-                        d = m_deps.mk_join(d, stack[j].second.dep);
+                        d = m_deps.mk_join(d, m_ineqs[stack[j].second].dep);
                     conflict(d);
                     return l_false;
                 }
             }
             if (ineq_out == ineqs.size()) {
+                m_ineqs_to_propagate.remove(i_idx);
                 on_stack.remove(i.w);
                 stack.pop_back();
             }
@@ -1523,36 +1535,36 @@ namespace polysat {
             d = m_deps.mk_join(m_vars[v].m_lo_dep, d);
             d = m_deps.mk_join(m_vars[v].m_hi_dep, d);
         }
-return d;
+        return d;
     }
 
     template<typename Ext>
     bool fixplex<Ext>::new_bound(ineq const& i, var_t x, numeral const& l, numeral const& h, u_dependency* a, u_dependency* b, u_dependency* c, u_dependency* d) {
-        bool was_fixed = lo(x) + 1 == hi(x);
+        bool was_fixed = is_fixed(x);
         SASSERT(!inconsistent());
         u_dependency* dep = m_deps.mk_join(i.dep, m_deps.mk_join(a, m_deps.mk_join(b, m_deps.mk_join(c, d))));
         update_bounds(x, l, h, dep);
         if (inconsistent())
             return false;
-        else if (!was_fixed && lo(x) + 1 == hi(x)) {
+        if (!was_fixed && is_fixed(x)) 
-            // TBD: track based on inequality not row
+            fixed_var_eh(dep, x);
-            // fixed_var_eh(r, x);
+        
-        }
         return true;
     }
 
     template<typename Ext>
     bool fixplex<Ext>::new_bound(row const& r, var_t x, mod_interval<numeral> const& range) {
-        if (range.is_free())
+        if (range.contains(m_vars[x]))
             return l_true;
         SASSERT(!inconsistent());
-        bool was_fixed = lo(x) + 1 == hi(x);
+        bool was_fixed = is_fixed(x);
-        update_bounds(x, range.lo, range.hi, row2dep(r));
+        u_dependency* dep = row2dep(r);
+        update_bounds(x, range.lo, range.hi, dep);
         IF_VERBOSE(0, verbose_stream() << "new-bound v" << x << " " << m_vars[x] << "\n");
         if (inconsistent())
             return false;
-        else if (!was_fixed && lo(x) + 1 == hi(x))
+        if (!was_fixed && is_fixed(x))
-            fixed_var_eh(r, x);
+            fixed_var_eh(dep, x);
         return true;
     }
 

src/math/polysat/linear_solver.cpp

@@ -17,6 +17,7 @@ Author:
 #include "math/polysat/fixplex_def.h"
 #include "math/polysat/solver.h"
 
+inline unsigned numeral2hash(u256 const& n) { return n.hash(); }
 
 namespace polysat {