mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

Don't track arbitrary hi/lo reference points and just store the slice width

Browse source
This commit is contained in:
Jakob Rath 2023-06-15 16:55:26 +02:00
parent 8ce85da881
commit 2a3006cce3
3 changed files with 86 additions and 121 deletions
Download patch file Download diff file Expand all files Collapse all files

149
src/math/polysat/slicing.cpp
View file

@ -73,62 +73,30 @@ namespace polysat {
m_next.pop_back(); m_next.pop_back();
} }
slicing::slice slicing::var2slice(pvar v) const { slicing::slice_idx slicing::find_sub_hi(slice_idx parent) const {
slice_idx const idx = find(m_var2slice[v]); SASSERT(has_sub(parent));
slice s; return find(m_slice_sub[parent]);
s.idx = idx;
s.hi = m_slice_width[idx] - 1;
// s.hi = m_solver.size(v) - 1;
s.lo = 0;
return s;
} }
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(has_sub(parent));
SASSERT(parent.hi >= parent.lo); return find(m_slice_sub[parent] + 1);
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;
} }
void slicing::split(slice_idx s, unsigned cut) { void slicing::split(slice_idx s, unsigned cut) {
SASSERT(!has_sub(s)); SASSERT(!has_sub(s));
SASSERT(width(s) - 1 >= cut + 1);
slice_idx const sub1 = alloc_slice(); slice_idx const sub1 = alloc_slice();
slice_idx const sub2 = alloc_slice(); slice_idx const sub2 = alloc_slice();
m_slice_cut[s] = cut; m_slice_cut[s] = cut;
m_slice_sub[s] = sub1; m_slice_sub[s] = sub1;
SASSERT_EQ(sub2, sub1 + 1); 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_slice_width[sub2] = cut + 1;
m_trail.push_back(trail_item::split_slice); m_trail.push_back(trail_item::split_slice);
m_split_trail.push_back(s); 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() { void slicing::undo_split_slice() {
slice_idx i = m_split_trail.back(); slice_idx i = m_split_trail.back();
m_split_trail.pop_back(); m_split_trail.pop_back();
@ -147,7 +115,7 @@ namespace polysat {
} }
void slicing::merge(slice_idx s1, slice_idx s2) { 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(s1));
SASSERT(!has_sub(s2)); SASSERT(!has_sub(s2));
slice_idx r1 = find(s1); slice_idx r1 = find(s1);
@ -174,109 +142,114 @@ namespace polysat {
std::swap(m_next[r1], m_next[r2]); 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); // LOG_H2("Merging " << xs << " with " << ys);
while (!xs.empty()) { while (!xs.empty()) {
SASSERT(!ys.empty()); SASSERT(!ys.empty());
slice x = xs.back(); slice_idx x = xs.back();
slice y = ys.back(); slice_idx y = ys.back();
xs.pop_back(); xs.pop_back();
ys.pop_back(); ys.pop_back();
SASSERT(!has_sub(x)); SASSERT(!has_sub(x));
SASSERT(!has_sub(y)); SASSERT(!has_sub(y));
if (x.width() == y.width()) { if (width(x) == width(y)) {
// LOG("Match " << x << " and " << 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 // need to split x according to y
// LOG("Splitting " << x << " to fit " << 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); ys.push_back(y);
} }
else { else {
SASSERT(y.width() > x.width()); SASSERT(width(y) > width(x));
// need to split y according to x // need to split y according to x
// LOG("Splitting " << y << " to fit " << 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); xs.push_back(x);
} }
} }
SASSERT(ys.empty()); SASSERT(ys.empty());
} }
void slicing::merge(slice_vector& xs, slice y) { void slicing::merge(slice_idx_vector& xs, slice_idx y) {
slice_vector tmp; slice_idx_vector tmp;
tmp.push_back(y); tmp.push_back(y);
merge(xs, tmp); 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 // splits are only stored for the representative
SASSERT_EQ(src.idx, find(src.idx)); SASSERT_EQ(src, find(src));
if (!has_sub(src)) { if (!has_sub(src)) {
out_base.push_back(src); out_base.push_back(src);
return; return;
} }
slice_vector& todo = m_tmp1; slice_idx_vector& todo = m_tmp1;
SASSERT(todo.empty()); SASSERT(todo.empty());
todo.push_back(src); todo.push_back(src);
while (!todo.empty()) { while (!todo.empty()) {
slice s = todo.back(); slice_idx s = todo.back();
todo.pop_back(); todo.pop_back();
if (!has_sub(s)) if (!has_sub(s))
out_base.push_back(s); out_base.push_back(s);
else { else {
todo.push_back(sub_lo(s)); todo.push_back(find_sub_lo(s));
todo.push_back(sub_hi(s)); todo.push_back(find_sub_hi(s));
} }
} }
SASSERT(todo.empty()); SASSERT(todo.empty());
} }
void slicing::mk_slice(slice src, unsigned const hi, unsigned const lo, slice_vector& out_base, bool output_full_src) { void slicing::mk_slice(slice_idx src, unsigned const hi, unsigned const lo, slice_idx_vector& out_base, bool output_full_src) {
// splits are only stored for the representative SASSERT(hi >= lo);
SASSERT_EQ(src.idx, find(src.idx)); SASSERT_EQ(src, find(src)); // splits are only stored for the representative
// extracted range must be fully contained inside the src slice SASSERT(width(src) > hi); // extracted range must be fully contained inside the src slice
SASSERT(src.hi >= hi); SASSERT(hi >= lo); SASSERT(lo >= src.lo); if (lo == 0 && width(src) - 1 == hi) {
if (src.hi == hi && src.lo == lo) {
find_base(src, out_base); find_base(src, out_base);
return; return;
} }
if (has_sub(src)) { if (has_sub(src)) {
// src is split into [src.hi, cut+1] and [cut, src.lo] // src is split into [src.width-1, cut+1] and [cut, 0]
unsigned const cut = m_slice_cut[src.idx] + src.lo; // adjust cut to current bounds unsigned const cut = m_slice_cut[src];
if (lo >= cut + 1) if (lo >= cut + 1) {
return mk_slice(sub_hi(src), hi, lo, out_base); // target slice falls into upper subslice
else if (cut >= hi) mk_slice(find_sub_hi(src), hi - cut - 1, lo - cut - 1, out_base);
return mk_slice(sub_lo(src), hi, lo, 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 { else {
SASSERT(hi > cut && cut >= lo); SASSERT(hi > cut && cut >= lo);
// desired range spans over the cutpoint, so we get multiple slices in the result // 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(find_sub_hi(src), hi - cut - 1, 0, out_base);
mk_slice(sub_lo(src), cut, lo, out_base); mk_slice(find_sub_lo(src), cut, lo, out_base);
return; return;
} }
} }
else { else {
// [src.hi, src.lo] has no subdivision yet // [src.width-1, 0] has no subdivision yet
if (src.hi > hi) { if (width(src) - 1 > hi) {
split(src, hi); split(src, hi);
if (output_full_src) if (output_full_src)
out_base.push_back(sub_hi(src)); out_base.push_back(find_sub_hi(src));
mk_slice(sub_lo(src), hi, lo, out_base); mk_slice(find_sub_lo(src), hi, lo, out_base); // recursive call to take care of case lo > 0
return; return;
} }
else { else {
SASSERT(src.hi == hi); SASSERT(lo > 0);
SASSERT(lo > src.lo);
split(src, lo - 1); split(src, lo - 1);
slice s = sub_hi(src); out_base.push_back(find_sub_hi(src));
SASSERT_EQ(s.hi, hi);
SASSERT_EQ(s.lo, lo);
out_base.push_back(s);
if (output_full_src) if (output_full_src)
out_base.push_back(sub_lo(src)); out_base.push_back(find_sub_lo(src));
return; return;
} }
} }
@ -284,7 +257,7 @@ namespace polysat {
} }
pvar slicing::mk_extract_var(pvar src, unsigned hi, unsigned lo) { 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); mk_slice(var2slice(src), hi, lo, slices);
// src[hi:lo] is the concatenation of the returned slices // src[hi:lo] is the concatenation of the returned slices
// TODO: for each slice, set_extract // TODO: for each slice, set_extract
@ -364,16 +337,20 @@ namespace polysat {
} }
std::ostream& slicing::display(std::ostream& out) const { std::ostream& slicing::display(std::ostream& out) const {
slice_vector base; slice_idx_vector base;
for (pvar v = 0; v < m_var2slice.size(); ++v) { for (pvar v = 0; v < m_var2slice.size(); ++v) {
out << "v" << v << ":"; out << "v" << v << ":";
base.reset(); base.reset();
find_base(var2slice(v), base); find_base(var2slice(v), base);
for (slice s : base) for (slice_idx s : base)
out << " {id:" << s.idx << ",w:" << s.width() << "}"; display(out << " ", s);
out << "\n"; out << "\n";
} }
return out; return out;
} }
std::ostream& slicing::display(std::ostream& out, slice_idx s) const {
return out << "{id:" << s << ",w:" << width(s) << "}";
}
} }

46
src/math/polysat/slicing.h
View file

@ -75,7 +75,6 @@ namespace polysat {
static constexpr unsigned null_cut = std::numeric_limits<unsigned>::max(); static constexpr unsigned null_cut = std::numeric_limits<unsigned>::max();
// number of bits in the slice // 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; 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]. // 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) // 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(); slice_idx alloc_slice();
// track slice range while traversing sub-slices slice_idx var2slice(pvar v) const { return find(m_var2slice[v]); }
// (reference point of hi/lo is user-defined, e.g., relative to entry point of traversal) unsigned width(slice_idx s) const { return m_slice_width[s]; }
struct slice { bool has_sub(slice_idx s) const { return m_slice_sub[s] != null_slice_idx; }
slice_idx idx = null_slice_idx;
unsigned hi = UINT_MAX; /// Split slice s into s[|s|-1:cut+1] and s[cut:0]
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); }
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
void split(slice_idx s, unsigned cut); void split(slice_idx s, unsigned cut);
// Split a slice into two; NOTE: the cut point here is relative to hi/lo in s /// Retrieve base slices s_1,...,s_n such that src == s_1 ++ ... + s_n
void split(slice const& s, unsigned cut); void find_base(slice_idx src, slice_idx_vector& out_base) const;
// 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 // 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 // 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 /// Find representative
slice_idx find(slice_idx i) const; 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 // Merge equivalence classes of two base slices
void merge(slice_idx s1, slice_idx s2); void merge(slice_idx s1, slice_idx s2);
@ -128,8 +117,8 @@ namespace polysat {
// Precondition: // Precondition:
// - sequence of base slices (equal total width) // - sequence of base slices (equal total width)
// - ordered from msb to lsb // - ordered from msb to lsb
void merge(slice_vector& xs, slice_vector& ys); void merge(slice_idx_vector& xs, slice_idx_vector& ys);
void merge(slice_vector& xs, slice y); void merge(slice_idx_vector& xs, slice_idx y);
void set_extract(pvar v, pvar src, unsigned hi_bit, unsigned lo_bit); void set_extract(pvar v, pvar src, unsigned hi_bit, unsigned lo_bit);
@ -151,7 +140,7 @@ namespace polysat {
void undo_merge_class(); void undo_merge_class();
mutable slice_vector m_tmp1; mutable slice_idx_vector m_tmp1;
public: public:
@ -190,6 +179,7 @@ namespace polysat {
void propagate(pvar v); void propagate(pvar v);
std::ostream& display(std::ostream& out) const; 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); } inline std::ostream& operator<<(std::ostream& out, slicing const& s) { return s.display(out); }

12
src/test/slicing.cpp
View file

@ -29,26 +29,24 @@ namespace polysat {
pvar b = s.add_var(6); pvar b = s.add_var(6);
std::cout << sl << "\n"; 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); sl.mk_slice(sl.var2slice(x), 7, 3, x_7_3);
std::cout << sl << "\n"; 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); sl.mk_slice(sl.var2slice(a), 4, 0, a_4_0);
std::cout << sl << "\n"; std::cout << sl << "\n";
sl.merge(x_7_3, a_4_0); sl.merge(x_7_3, a_4_0);
std::cout << sl << "\n"; 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.mk_slice(sl.var2slice(y), 5, 0, y_5_0);
sl.merge(y_5_0, sl.var2slice(b)); sl.merge(y_5_0, sl.var2slice(b));
std::cout << sl << "\n"; std::cout << sl << "\n";
slicing::slice_vector x_base; slicing::slice_idx_vector x_base;
sl.find_base(sl.var2slice(x), x_base); sl.find_base(sl.var2slice(x), x_base);
std::cout << "v" << x << "_base: " << x_base << "\n"; slicing::slice_idx_vector y_base;
slicing::slice_vector y_base;
sl.find_base(sl.var2slice(y), y_base); sl.find_base(sl.var2slice(y), y_base);
std::cout << "v" << y << "_base: " << y_base << "\n";
sl.merge(x_base, y_base); sl.merge(x_base, y_base);
std::cout << sl << "\n"; std::cout << sl << "\n";
} }