use offset/length for fixed slices to allow super-slices

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

src/sat/smt/polysat/fixed_bits.cpp

@@ -32,28 +32,35 @@ namespace polysat {
     // if x[hi:lo] = value, then 
     // 2^(w-hi+1)* x >= 
     bool fixed_bits::check(rational const& val, fi_record& fi) {
+        unsigned sz = c.size(m_var);
         for (auto const& s : m_fixed_slices) {
-            rational bw = rational::power_of_two(s.hi - s.lo + 1);
+            rational bw = rational::power_of_two(s.length);
-            if (s.value != mod(machine_div2k(val, s.lo + 1), bw)) {
+            // slice is properly contained in bit-vector variable
+            if (s.length <= sz && s.value != mod(machine_div2k(val, s.offset + 1), bw)) {
+                SASSERT(s.offset + s.length <= sz);
                 rational hi_val = s.value;
                 rational lo_val = mod(s.value + 1, bw);                
-                unsigned sz = c.size(m_var);
+                pdd lo = c.value(rational::power_of_two(sz - s.offset - s.length) * lo_val, c.size(m_var));
-                pdd lo = c.value(rational::power_of_two(sz - s.hi - 1) * lo_val, c.size(m_var));
+                pdd hi = c.value(rational::power_of_two(sz - s.offset - s.length) * hi_val, c.size(m_var));
-                pdd hi = c.value(rational::power_of_two(sz - s.hi - 1) * hi_val, c.size(m_var));
                 fi.reset();
                 fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
                 fi.deps.push_back(dependency({ m_var, s }));
-                fi.bit_width = s.hi - s.lo + 1;
+                fi.bit_width = s.length;
                 fi.coeff = 1;
                 return false;
             }
+            // slice, properly contains variable.
+            // s.offset refers to offset in containing value.
+            if (s.length > sz) {
+                NOT_IMPLEMENTED_YET();
+            }
         }
         return true;
     }
 
     std::ostream& fixed_bits::display(std::ostream& out) const {
         for (auto const& s : m_fixed_slices)
-            out << s.hi << " " << s.lo << " " << s.value << "\n";  
+            out << s.value << "[" << s.length << "]@" << s.offset << "\n";  
         return out;
     }
 
@@ -80,7 +87,7 @@ namespace polysat {
         if (d.parity(N) < k)
             return false;
         rational const b = machine_div2k(d, k);
-        out = fixed_slice(N - k - 1, 0, b);
+        out = fixed_slice(b, 0, N - k);
         SASSERT_EQ(d, b * rational::power_of_two(k));
         SASSERT_EQ(p, (p.manager().mk_var(p.var()) - out.value) * rational::power_of_two(k));
         return true;
@@ -148,8 +155,8 @@ namespace polysat {
             rational const c = is_strict ? rhs.val() : (rhs.val() + 1);
             unsigned const k = c.next_power_of_two();
             if (k < N) {
-                out.hi = N - 1;
+                out.length = N - k;
-                out.lo = k;
+                out.offset = k;
                 out.value = 0;
                 return true;
             }

src/sat/smt/polysat/types.h

@@ -36,17 +36,17 @@ namespace polysat {
     class signed_constraint;
 
     struct fixed_slice {
-        unsigned hi = 0;
+        unsigned offset = 0;
-        unsigned lo = 0;
+        unsigned length = 0;
         rational value;
         fixed_slice() = default;
-        fixed_slice(unsigned hi, unsigned lo, rational value) : hi(hi), lo(lo), value(value) {}
+        fixed_slice(rational value, unsigned offset, unsigned length) : offset(offset), length(length), value(value) {}
     };
 
     struct fixed_claim : public fixed_slice {
         pvar v;
         fixed_claim() = default;
-        fixed_claim(pvar v, unsigned hi, unsigned lo, rational value) : fixed_slice(hi, lo, value), v(v) {}
+        fixed_claim(pvar v, rational value, unsigned offset, unsigned length) : fixed_slice(value, offset, length), v(v) {}
         fixed_claim(pvar, fixed_slice const& s) : fixed_slice(s), v(v) {}
     };
 
@@ -100,7 +100,7 @@ namespace polysat {
         }
         else if (d.is_fixed_claim()) {
             auto fixed = d.fixed();
-            return out << fixed.value << " == v" << fixed.v << " [" << fixed.hi << ":" << fixed.lo << "]";
+            return out << fixed.value << " == v" << fixed.v << " [" << fixed.length << "]@" << fixed.offset;
         }
         else {
             UNREACHABLE();

src/sat/smt/polysat_egraph.cpp

@@ -96,6 +96,7 @@ namespace polysat {
     void solver::get_fixed_bits(pvar pv, fixed_bits_vector& out) {
         
         std::function<bool(euf::enode*, unsigned)> consume_slice = [&](euf::enode* n, unsigned offset) {
+            // verbose_stream() << "sub-slice " << ctx.bpp(n) << " " << offset << "\n";
             if (!n->interpreted())
                 return true;
             auto w = n->get_root()->get_th_var(get_id());
@@ -104,13 +105,14 @@ namespace polysat {
             auto const& p = m_var2pdd[w];
             if (!p.is_var())
                 return true;
-            unsigned lo = offset, hi = bv.get_bv_size(n->get_expr());
+            unsigned length = bv.get_bv_size(n->get_expr());
             rational value;
             VERIFY(bv.is_numeral(n->get_expr(), value));
-            out.push_back({ fixed_slice(lo, hi, value) });
+            out.push_back({ fixed_slice(value, offset, length) });
             return false;
         };
         theory_var v = m_pddvar2var[pv];
+        // verbose_stream() << "Get fixed_bits " << ctx.bpp(var2enode(v)) << "\n";
         m_bv_plugin->sub_slices(var2enode(v), consume_slice);
     }
     
@@ -120,12 +122,12 @@ namespace polysat {
         m_bv_plugin->explain_slice(var2enode(v), offset, var2enode(w), consume_eq);
     }
 
-    void solver::explain_fixed(pvar pv, unsigned lo, unsigned hi, rational const& value, std::function<void(euf::enode*, euf::enode*)>& consume_eq) {
+    void solver::explain_fixed(pvar pv, fixed_slice const& slice, std::function<void(euf::enode*, euf::enode*)>& consume_eq) {
         euf::theory_var v = m_pddvar2var[pv];
-        expr_ref val(bv.mk_numeral(value, hi - lo + 1), m);
+        expr_ref val(bv.mk_numeral(slice.value, slice.length), m);
         euf::enode* b = ctx.get_egraph().find(val);
         SASSERT(b);
-        m_bv_plugin->explain_slice(var2enode(v), lo, b, consume_eq);
+        m_bv_plugin->explain_slice(var2enode(v), slice.offset, b, consume_eq);
     }
 
 }

src/sat/smt/polysat_solver.cpp

@@ -147,7 +147,7 @@ namespace polysat {
             std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
                 eqs.push_back({ a, b });
                 };
-            explain_fixed(o.v, o.lo, o.hi, o.value, consume);
+            explain_fixed(o.v, o, consume);
         }
         else if (d.is_offset_claim()) {
             auto const& offs = d.offset();

src/sat/smt/polysat_solver.h

@@ -112,7 +112,7 @@ namespace polysat {
         sat::check_result intblast();
 
         void explain_slice(pvar v, pvar w, unsigned offset, std::function<void(euf::enode*, euf::enode*)>& consume);
-        void explain_fixed(pvar v, unsigned lo, unsigned hi, rational const& value, std::function<void(euf::enode*, euf::enode*)>& consume_eq);
+        void explain_fixed(pvar v, fixed_slice const& s, std::function<void(euf::enode*, euf::enode*)>& consume_eq);
 
         // internalize
         bool visit(expr* e) override;