diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp index 3290dadd1..b61fc301e 100644 --- a/src/math/polysat/slicing.cpp +++ b/src/math/polysat/slicing.cpp @@ -73,62 +73,30 @@ namespace polysat { m_next.pop_back(); } - slicing::slice slicing::var2slice(pvar v) const { - slice_idx const idx = find(m_var2slice[v]); - slice s; - s.idx = idx; - s.hi = m_slice_width[idx] - 1; - // s.hi = m_solver.size(v) - 1; - s.lo = 0; - return s; + slicing::slice_idx slicing::find_sub_hi(slice_idx parent) const { + SASSERT(has_sub(parent)); + return find(m_slice_sub[parent]); } - slicing::slice slicing::sub_hi(slice const& parent) const { + slicing::slice_idx slicing::find_sub_lo(slice_idx parent) const { SASSERT(has_sub(parent)); - SASSERT(parent.hi >= parent.lo); - slice s; - s.idx = find(m_slice_sub[parent.idx]); - // |parent|-1 ... cut+1 and cut ............ 0 - // hi ........... lo+cut+1 lo+cut ........ lo - s.hi = parent.hi; - s.lo = parent.lo + m_slice_cut[parent.idx] + 1; - SASSERT(s.hi >= s.lo); - SASSERT_EQ(m_slice_width[s.idx], s.hi - s.lo + 1); - return s; - } - - slicing::slice slicing::sub_lo(slice const& parent) const { - SASSERT(has_sub(parent)); - slice s; - s.idx = find(m_slice_sub[parent.idx] + 1); - // |parent|-1 ... cut+1 and cut ............ 0 - // hi ........... lo+cut+1 lo+cut ........ lo - s.hi = parent.lo + m_slice_cut[parent.idx]; - s.lo = parent.lo; - SASSERT(s.hi >= s.lo); - SASSERT_EQ(m_slice_width[s.idx], s.hi - s.lo + 1); - return s; + return find(m_slice_sub[parent] + 1); } void slicing::split(slice_idx s, unsigned cut) { SASSERT(!has_sub(s)); + SASSERT(width(s) - 1 >= cut + 1); slice_idx const sub1 = alloc_slice(); slice_idx const sub2 = alloc_slice(); m_slice_cut[s] = cut; m_slice_sub[s] = sub1; SASSERT_EQ(sub2, sub1 + 1); - m_slice_width[sub1] = m_slice_width[s] - cut - 1; + m_slice_width[sub1] = width(s) - cut - 1; m_slice_width[sub2] = cut + 1; - m_trail.push_back(trail_item::split_slice); m_split_trail.push_back(s); } - void slicing::split(slice const& s, unsigned const cut) { - SASSERT(s.hi > cut); SASSERT(cut >= s.lo); - split(s.idx, cut - s.lo); - } - void slicing::undo_split_slice() { slice_idx i = m_split_trail.back(); m_split_trail.pop_back(); @@ -147,7 +115,7 @@ namespace polysat { } void slicing::merge(slice_idx s1, slice_idx s2) { - SASSERT_EQ(m_slice_width[s1], m_slice_width[s2]); + SASSERT_EQ(width(s1), width(s2)); SASSERT(!has_sub(s1)); SASSERT(!has_sub(s2)); slice_idx r1 = find(s1); @@ -174,109 +142,114 @@ namespace polysat { std::swap(m_next[r1], m_next[r2]); } - void slicing::merge(slice_vector& xs, slice_vector& ys) { + void slicing::merge(slice_idx_vector& xs, slice_idx_vector& ys) { // LOG_H2("Merging " << xs << " with " << ys); while (!xs.empty()) { SASSERT(!ys.empty()); - slice x = xs.back(); - slice y = ys.back(); + slice_idx x = xs.back(); + slice_idx y = ys.back(); xs.pop_back(); ys.pop_back(); SASSERT(!has_sub(x)); SASSERT(!has_sub(y)); - if (x.width() == y.width()) { + if (width(x) == width(y)) { // LOG("Match " << x << " and " << y); - merge(x.idx, y.idx); + merge(x, y); } - else if (x.width() > y.width()) { + else if (width(x) > width(y)) { // need to split x according to y // LOG("Splitting " << x << " to fit " << y); - mk_slice(x, y.hi - y.lo + x.lo, x.lo, xs, true); + mk_slice(x, width(y) - 1, 0, xs, true); ys.push_back(y); } else { - SASSERT(y.width() > x.width()); + SASSERT(width(y) > width(x)); // need to split y according to x // LOG("Splitting " << y << " to fit " << x); - mk_slice(y, x.hi - x.lo + y.lo, y.lo, ys, true); + mk_slice(y, width(x) - 1, 0, ys, true); xs.push_back(x); } } SASSERT(ys.empty()); } - void slicing::merge(slice_vector& xs, slice y) { - slice_vector tmp; + void slicing::merge(slice_idx_vector& xs, slice_idx y) { + slice_idx_vector tmp; tmp.push_back(y); merge(xs, tmp); } - void slicing::find_base(slice src, slice_vector& out_base) const { + void slicing::find_base(slice_idx src, slice_idx_vector& out_base) const { // splits are only stored for the representative - SASSERT_EQ(src.idx, find(src.idx)); + SASSERT_EQ(src, find(src)); if (!has_sub(src)) { out_base.push_back(src); return; } - slice_vector& todo = m_tmp1; + slice_idx_vector& todo = m_tmp1; SASSERT(todo.empty()); todo.push_back(src); while (!todo.empty()) { - slice s = todo.back(); + slice_idx s = todo.back(); todo.pop_back(); if (!has_sub(s)) out_base.push_back(s); else { - todo.push_back(sub_lo(s)); - todo.push_back(sub_hi(s)); + todo.push_back(find_sub_lo(s)); + todo.push_back(find_sub_hi(s)); } } SASSERT(todo.empty()); } - 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 - SASSERT(src.hi >= hi); SASSERT(hi >= lo); SASSERT(lo >= src.lo); - if (src.hi == hi && src.lo == lo) { + void slicing::mk_slice(slice_idx src, unsigned const hi, unsigned const lo, slice_idx_vector& out_base, bool output_full_src) { + SASSERT(hi >= lo); + SASSERT_EQ(src, find(src)); // splits are only stored for the representative + SASSERT(width(src) > hi); // extracted range must be fully contained inside the src slice + if (lo == 0 && width(src) - 1 == hi) { find_base(src, out_base); return; } if (has_sub(src)) { - // src is split into [src.hi, cut+1] and [cut, src.lo] - unsigned const cut = m_slice_cut[src.idx] + src.lo; // adjust cut to current bounds - if (lo >= cut + 1) - return mk_slice(sub_hi(src), hi, lo, out_base); - else if (cut >= hi) - return mk_slice(sub_lo(src), hi, lo, out_base); + // src is split into [src.width-1, cut+1] and [cut, 0] + unsigned const cut = m_slice_cut[src]; + if (lo >= cut + 1) { + // target slice falls into upper subslice + mk_slice(find_sub_hi(src), hi - cut - 1, lo - cut - 1, out_base); + if (output_full_src) + out_base.push_back(find_sub_lo(src)); + return; + } + else if (cut >= hi) { + // target slice falls into lower subslice + if (output_full_src) + out_base.push_back(find_sub_hi(src)); + mk_slice(find_sub_lo(src), hi, lo, out_base); + return; + } else { SASSERT(hi > cut && cut >= lo); // desired range spans over the cutpoint, so we get multiple slices in the result - mk_slice(sub_hi(src), hi, cut + 1, out_base); - mk_slice(sub_lo(src), cut, lo, out_base); + mk_slice(find_sub_hi(src), hi - cut - 1, 0, out_base); + mk_slice(find_sub_lo(src), cut, lo, out_base); return; } } else { - // [src.hi, src.lo] has no subdivision yet - if (src.hi > hi) { + // [src.width-1, 0] has no subdivision yet + if (width(src) - 1 > hi) { split(src, hi); if (output_full_src) - out_base.push_back(sub_hi(src)); - mk_slice(sub_lo(src), hi, lo, out_base); + out_base.push_back(find_sub_hi(src)); + mk_slice(find_sub_lo(src), hi, lo, out_base); // recursive call to take care of case lo > 0 return; } else { - SASSERT(src.hi == hi); - SASSERT(lo > src.lo); + SASSERT(lo > 0); split(src, lo - 1); - slice s = sub_hi(src); - SASSERT_EQ(s.hi, hi); - SASSERT_EQ(s.lo, lo); - out_base.push_back(s); + out_base.push_back(find_sub_hi(src)); if (output_full_src) - out_base.push_back(sub_lo(src)); + out_base.push_back(find_sub_lo(src)); return; } } @@ -284,7 +257,7 @@ namespace polysat { } pvar slicing::mk_extract_var(pvar src, unsigned hi, unsigned lo) { - slice_vector slices; + slice_idx_vector slices; mk_slice(var2slice(src), hi, lo, slices); // src[hi:lo] is the concatenation of the returned slices // TODO: for each slice, set_extract @@ -364,16 +337,20 @@ namespace polysat { } std::ostream& slicing::display(std::ostream& out) const { - slice_vector base; + slice_idx_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() << "}"; + for (slice_idx s : base) + display(out << " ", s); out << "\n"; } return out; } + std::ostream& slicing::display(std::ostream& out, slice_idx s) const { + return out << "{id:" << s << ",w:" << width(s) << "}"; + } + } diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h index 65574694d..5ecff86f5 100644 --- a/src/math/polysat/slicing.h +++ b/src/math/polysat/slicing.h @@ -75,7 +75,6 @@ namespace polysat { static constexpr unsigned null_cut = std::numeric_limits::max(); // number of bits in the slice - // TODO: slice width is useful for debugging but we can probably drop it in release mode? unsigned_vector m_slice_width; // Cut point: if slice represents bit-vector x, then x has been sliced into x[|x|-1:cut+1] and x[cut:0]. // The cut point is relative to the parent slice (rather than a root variable, which might not be unique) @@ -91,34 +90,24 @@ namespace polysat { slice_idx alloc_slice(); - // track slice range while traversing sub-slices - // (reference point of hi/lo is user-defined, e.g., relative to entry point of traversal) - struct slice { - 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; - // 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); } - slice sub_hi(slice const& s) const; - slice sub_lo(slice const& s) const; - // Split a slice into two; the cut is relative to |s|...0 + slice_idx var2slice(pvar v) const { return find(m_var2slice[v]); } + unsigned width(slice_idx s) const { return m_slice_width[s]; } + bool has_sub(slice_idx s) const { return m_slice_sub[s] != null_slice_idx; } + + /// Split slice s into s[|s|-1:cut+1] and s[cut:0] void split(slice_idx s, unsigned cut); - // Split a slice into two; NOTE: the cut point here is relative to hi/lo in s - void split(slice const& s, unsigned cut); - // 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 base slices s_1,...,s_n such that src == s_1 ++ ... + s_n + void find_base(slice_idx src, slice_idx_vector& out_base) const; // Retrieve (or create) base slices s_1,...,s_n such that src[hi:lo] == s_1 ++ ... ++ s_n // 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); + void mk_slice(slice_idx src, unsigned hi, unsigned lo, slice_idx_vector& out_base, bool output_full_src = false); - // Find representative - slice_idx find(slice_idx i) const; + /// Find representative + slice_idx find(slice_idx s) const; + /// Find representative of upper subslice + slice_idx find_sub_hi(slice_idx s) const; + /// Find representative of lower subslice + slice_idx find_sub_lo(slice_idx s) const; // Merge equivalence classes of two base slices void merge(slice_idx s1, slice_idx s2); @@ -128,8 +117,8 @@ namespace polysat { // Precondition: // - sequence of base slices (equal total width) // - ordered from msb to lsb - void merge(slice_vector& xs, slice_vector& ys); - void merge(slice_vector& xs, slice y); + void merge(slice_idx_vector& xs, slice_idx_vector& ys); + void merge(slice_idx_vector& xs, slice_idx y); void set_extract(pvar v, pvar src, unsigned hi_bit, unsigned lo_bit); @@ -151,7 +140,7 @@ namespace polysat { void undo_merge_class(); - mutable slice_vector m_tmp1; + mutable slice_idx_vector m_tmp1; public: @@ -190,6 +179,7 @@ namespace polysat { void propagate(pvar v); std::ostream& display(std::ostream& out) const; + std::ostream& display(std::ostream& out, slice_idx s) const; }; inline std::ostream& operator<<(std::ostream& out, slicing const& s) { return s.display(out); } diff --git a/src/test/slicing.cpp b/src/test/slicing.cpp index e5a8dc32a..3a0f22106 100644 --- a/src/test/slicing.cpp +++ b/src/test/slicing.cpp @@ -29,26 +29,24 @@ namespace polysat { pvar b = s.add_var(6); std::cout << sl << "\n"; - slicing::slice_vector x_7_3; + slicing::slice_idx_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; + slicing::slice_idx_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; + slicing::slice_idx_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; + slicing::slice_idx_vector x_base; sl.find_base(sl.var2slice(x), x_base); - std::cout << "v" << x << "_base: " << x_base << "\n"; - slicing::slice_vector y_base; + slicing::slice_idx_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"; }