test and bugfix

src/math/polysat/slicing.cpp

@@ -42,7 +42,7 @@ namespace polysat {
     }
 
     void slicing::add_var(unsigned bit_width) {
-        pvar const v = m_var2slice.size();
+        // pvar const v = m_var2slice.size();
         slice_idx const s = alloc_slice();
         m_slice_width[s] = bit_width;
         m_var2slice.push_back(s);
@@ -147,6 +147,7 @@ namespace polysat {
     }
 
     void slicing::merge(slice_idx s1, slice_idx s2) {
+        SASSERT_EQ(m_slice_width[s1], m_slice_width[s2]);
         SASSERT(!has_sub(s1));
         SASSERT(!has_sub(s2));
         slice_idx r1 = find(s1);
@@ -174,33 +175,42 @@ namespace polysat {
     }
 
     void slicing::merge(slice_vector& xs, slice_vector& ys) {
+        // LOG_H2("Merging " << xs << " with " << ys);
         while (!xs.empty()) {
             SASSERT(!ys.empty());
             slice x = xs.back();
             slice y = ys.back();
             xs.pop_back();
             ys.pop_back();
-            SASSERT_EQ(x.lo, y.lo);
             SASSERT(!has_sub(x));
             SASSERT(!has_sub(y));
-            if (x.hi == y.hi) {
+            if (x.width() == y.width()) {
+                // LOG("Match " << x << " and " << y);
                 merge(x.idx, y.idx);
             }
-            else if (x.hi > y.hi) {
+            else if (x.width() > y.width()) {
                 // need to split x according to y
-                mk_slice(x, y.hi, y.lo, xs);
+                // LOG("Splitting " << x << " to fit " << y);
+                mk_slice(x, y.hi - y.lo + x.lo, x.lo, xs, true);
                 ys.push_back(y);
             }
             else {
-                SASSERT(y.hi > x.hi);
+                SASSERT(y.width() > x.width());
                 // need to split y according to x
-                mk_slice(y, x.hi, x.lo, ys);
+                // LOG("Splitting " << y << " to fit " << x);
+                mk_slice(y, x.hi - x.lo + y.lo, y.lo, ys, true);
                 xs.push_back(x);
             }
         }
         SASSERT(ys.empty());
     }
 
+    void slicing::merge(slice_vector& xs, slice y) {
+        slice_vector tmp;
+        tmp.push_back(y);
+        merge(xs, tmp);
+    }
+
     void slicing::find_base(slice src, slice_vector& out_base) const {
         // splits are only stored for the representative
         SASSERT_EQ(src.idx, find(src.idx));
@@ -224,7 +234,7 @@ namespace polysat {
         SASSERT(todo.empty());
     }
 
-    void slicing::mk_slice(slice src, unsigned const hi, unsigned const lo, slice_vector& out_base) {
+    void slicing::mk_slice(slice src, unsigned const hi, unsigned const lo, slice_vector& out_base, bool output_full_src) {
         // splits are only stored for the representative
         SASSERT_EQ(src.idx, find(src.idx));
         // extracted range must be fully contained inside the src slice
@@ -252,6 +262,8 @@ namespace polysat {
             // [src.hi, src.lo] has no subdivision yet
             if (src.hi > hi) {
                 split(src, hi);
+                if (output_full_src)
+                    out_base.push_back(sub_hi(src));
                 mk_slice(sub_lo(src), hi, lo, out_base);
                 return;
             }
@@ -263,6 +275,8 @@ namespace polysat {
                 SASSERT_EQ(s.hi, hi);
                 SASSERT_EQ(s.lo, lo);
                 out_base.push_back(s);
+                if (output_full_src)
+                    out_base.push_back(sub_lo(src));
                 return;
             }
         }
@@ -349,4 +363,17 @@ namespace polysat {
     void slicing::propagate(pvar v) {
     }
 
+    std::ostream& slicing::display(std::ostream& out) const {
+        slice_vector base;
+        for (pvar v = 0; v < m_var2slice.size(); ++v) {
+            out << "v" << v << ":";
+            base.reset();
+            find_base(var2slice(v), base);
+            for (slice s : base)
+                out << " {id:" << s.idx << ",w:" << s.width() << "}";
+            out << "\n";
+        }
+        return out;
+    }
+
 }

src/math/polysat/slicing.h

@@ -97,8 +97,11 @@ namespace polysat {
             slice_idx idx = null_slice_idx;
             unsigned hi = UINT_MAX;
             unsigned lo = UINT_MAX;
+            unsigned width() const { return hi - lo + 1; }
         };
+        friend std::ostream& operator<<(std::ostream& out, slice const& s) { return out << "{id:" << s.idx << ",w:" << s.width() << "}"; }
         using slice_vector = svector<slice>;
+        // Return slice v[|v|-1..0]
         slice var2slice(pvar v) const;
         bool has_sub(slice_idx i) const { return m_slice_sub[i] != null_slice_idx; }
         bool has_sub(slice const& s) const { return has_sub(s.idx); }
@@ -111,7 +114,8 @@ namespace polysat {
         // Retrieve base slices s_1,...,s_n such that src == s_1 ++ ... + s_n
         void find_base(slice src, slice_vector& out_base) const;
         // Retrieve (or create) base slices s_1,...,s_n such that src[hi:lo] == s_1 ++ ... ++ s_n
-        void mk_slice(slice src, unsigned hi, unsigned lo, slice_vector& out_base);
+        // If output_full_src is true, returns the new base for src, i.e., src == s_1 ++ ... ++ s_n
+        void mk_slice(slice src, unsigned hi, unsigned lo, slice_vector& out_base, bool output_full_src = false);
 
         // Find representative
         slice_idx find(slice_idx i) const;
@@ -124,8 +128,8 @@ namespace polysat {
         // Precondition:
         // - sequence of base slices (equal total width)
         // - ordered from msb to lsb
-        // - slices have the same reference point
         void merge(slice_vector& xs, slice_vector& ys);
+        void merge(slice_vector& xs, slice y);
 
         void set_extract(pvar v, pvar src, unsigned hi_bit, unsigned lo_bit);
 
@@ -184,6 +188,10 @@ namespace polysat {
         // - fixed bits
         // - intervals ?????  -- that will also need changes in the viable algorithm
         void propagate(pvar v);
+
+        std::ostream& display(std::ostream& out) const;
     };
 
+    inline std::ostream& operator<<(std::ostream& out, slicing const& s) { return s.display(out); }
+
 }

src/test/slicing.cpp

@@ -16,11 +16,47 @@ namespace polysat {
     class test_slicing {
     public:
 
+        // x[7:3] = a
+        // y[5:0] = b
+        // x = y
         static void test1() {
             std::cout << __func__ << "\n";
             scoped_solver_slicing s;
             slicing& sl = s.sl();
             pvar x = s.add_var(8);
+            pvar y = s.add_var(8);
+            pvar a = s.add_var(5);
+            pvar b = s.add_var(6);
+
+            std::cout << sl << "\n";
+            slicing::slice_vector x_7_3;
+            sl.mk_slice(sl.var2slice(x), 7, 3, x_7_3);
+            std::cout << sl << "\n";
+            slicing::slice_vector a_4_0;
+            sl.mk_slice(sl.var2slice(a), 4, 0, a_4_0);
+            std::cout << sl << "\n";
+            sl.merge(x_7_3, a_4_0);
+            std::cout << sl << "\n";
+
+            slicing::slice_vector y_5_0;
+            sl.mk_slice(sl.var2slice(y), 5, 0, y_5_0);
+            sl.merge(y_5_0, sl.var2slice(b));
+            std::cout << sl << "\n";
+
+            slicing::slice_vector x_base;
+            sl.find_base(sl.var2slice(x), x_base);
+            std::cout << "v" << x << "_base: " << x_base << "\n";
+            slicing::slice_vector y_base;
+            sl.find_base(sl.var2slice(y), y_base);
+            std::cout << "v" << y << "_base: " << y_base << "\n";
+            sl.merge(x_base, y_base);
+            std::cout << sl << "\n";
+        }
+
+        // x[7:3] = a
+        // x = y
+        // y[5:0] = b
+        static void test2() {
         }
 
     };