mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-19 09:40:20 +00:00
Code Activity

get rid of _idx suffix

Browse source
This commit is contained in:
Jakob Rath 2023-06-15 16:58:39 +02:00
parent 2a3006cce3
commit cddfcc1658
3 changed files with 67 additions and 67 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -43,7 +43,7 @@ namespace polysat {
void slicing::add_var(unsigned bit_width) { 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(); slice const s = alloc_slice();
m_slice_width[s] = bit_width; m_slice_width[s] = bit_width;
m_var2slice.push_back(s); m_var2slice.push_back(s);
} }
@ -52,11 +52,11 @@ namespace polysat {
m_var2slice.pop_back(); m_var2slice.pop_back();
} }
slicing::slice_idx slicing::alloc_slice() { slicing::slice slicing::alloc_slice() {
slice_idx const s = m_slice_cut.size(); slice const s = m_slice_cut.size();
m_slice_width.push_back(0); m_slice_width.push_back(0);
m_slice_cut.push_back(null_cut); m_slice_cut.push_back(null_cut);
m_slice_sub.push_back(null_slice_idx); m_slice_sub.push_back(null_slice);
m_find.push_back(s); m_find.push_back(s);
m_size.push_back(1); m_size.push_back(1);
m_next.push_back(s); m_next.push_back(s);
@ -73,21 +73,21 @@ namespace polysat {
m_next.pop_back(); m_next.pop_back();
} }
slicing::slice_idx slicing::find_sub_hi(slice_idx parent) const { slicing::slice slicing::find_sub_hi(slice parent) const {
SASSERT(has_sub(parent)); SASSERT(has_sub(parent));
return find(m_slice_sub[parent]); return find(m_slice_sub[parent]);
} }
slicing::slice_idx slicing::find_sub_lo(slice_idx parent) const { slicing::slice slicing::find_sub_lo(slice parent) const {
SASSERT(has_sub(parent)); SASSERT(has_sub(parent));
return find(m_slice_sub[parent] + 1); return find(m_slice_sub[parent] + 1);
} }
void slicing::split(slice_idx s, unsigned cut) { void slicing::split(slice s, unsigned cut) {
SASSERT(!has_sub(s)); SASSERT(!has_sub(s));
SASSERT(width(s) - 1 >= cut + 1); SASSERT(width(s) - 1 >= cut + 1);
slice_idx const sub1 = alloc_slice(); slice const sub1 = alloc_slice();
slice_idx const sub2 = alloc_slice(); slice 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);
@ -98,28 +98,28 @@ namespace polysat {
} }
void slicing::undo_split_slice() { void slicing::undo_split_slice() {
slice_idx i = m_split_trail.back(); slice s = m_split_trail.back();
m_split_trail.pop_back(); m_split_trail.pop_back();
m_slice_cut[i] = null_cut; m_slice_cut[s] = null_cut;
m_slice_sub[i] = null_slice_idx; m_slice_sub[s] = null_slice;
} }
slicing::slice_idx slicing::find(slice_idx i) const { slicing::slice slicing::find(slice s) const {
while (true) { while (true) {
SASSERT(i < m_find.size()); SASSERT(s < m_find.size());
slice_idx const new_i = m_find[i]; slice const new_s = m_find[s];
if (new_i == i) if (new_s == s)
return i; return s;
i = new_i; s = new_s;
} }
} }
void slicing::merge(slice_idx s1, slice_idx s2) { void slicing::merge(slice s1, slice s2) {
SASSERT_EQ(width(s1), 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 r1 = find(s1);
slice_idx r2 = find(s2); slice r2 = find(s2);
if (r1 == r2) if (r1 == r2)
return; return;
if (m_size[r1] > m_size[r2]) if (m_size[r1] > m_size[r2])
@ -133,21 +133,21 @@ namespace polysat {
} }
void slicing::undo_merge_class() { void slicing::undo_merge_class() {
slice_idx r1 = m_merge_trail.back(); slice r1 = m_merge_trail.back();
m_merge_trail.pop_back(); m_merge_trail.pop_back();
slice_idx r2 = m_find[r1]; slice r2 = m_find[r1];
SASSERT(find(r2) == r2); SASSERT(find(r2) == r2);
m_find[r1] = r1; m_find[r1] = r1;
m_size[r2] -= m_size[r1]; m_size[r2] -= m_size[r1];
std::swap(m_next[r1], m_next[r2]); std::swap(m_next[r1], m_next[r2]);
} }
void slicing::merge(slice_idx_vector& xs, slice_idx_vector& ys) { void slicing::merge(slice_vector& xs, slice_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_idx x = xs.back(); slice x = xs.back();
slice_idx y = ys.back(); slice y = ys.back();
xs.pop_back(); xs.pop_back();
ys.pop_back(); ys.pop_back();
SASSERT(!has_sub(x)); SASSERT(!has_sub(x));
@ -173,24 +173,24 @@ namespace polysat {
SASSERT(ys.empty()); SASSERT(ys.empty());
} }
void slicing::merge(slice_idx_vector& xs, slice_idx y) { void slicing::merge(slice_vector& xs, slice y) {
slice_idx_vector tmp; slice_vector tmp;
tmp.push_back(y); tmp.push_back(y);
merge(xs, tmp); merge(xs, tmp);
} }
void slicing::find_base(slice_idx src, slice_idx_vector& out_base) const { void slicing::find_base(slice src, slice_vector& out_base) const {
// splits are only stored for the representative // splits are only stored for the representative
SASSERT_EQ(src, find(src)); 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_idx_vector& todo = m_tmp1; slice_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_idx s = todo.back(); slice 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);
@ -202,7 +202,7 @@ namespace polysat {
SASSERT(todo.empty()); SASSERT(todo.empty());
} }
void slicing::mk_slice(slice_idx src, unsigned const hi, unsigned const lo, slice_idx_vector& out_base, bool output_full_src) { void slicing::mk_slice(slice src, unsigned const hi, unsigned const lo, slice_vector& out_base, bool output_full_src) {
SASSERT(hi >= lo); SASSERT(hi >= lo);
SASSERT_EQ(src, find(src)); // splits are only stored for the representative 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 SASSERT(width(src) > hi); // extracted range must be fully contained inside the src slice
@ -257,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_idx_vector slices; slice_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
@ -337,19 +337,19 @@ namespace polysat {
} }
std::ostream& slicing::display(std::ostream& out) const { std::ostream& slicing::display(std::ostream& out) const {
slice_idx_vector base; slice_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_idx s : base) for (slice s : base)
display(out << " ", s); display(out << " ", s);
out << "\n"; out << "\n";
} }
return out; return out;
} }
std::ostream& slicing::display(std::ostream& out, slice_idx s) const { std::ostream& slicing::display(std::ostream& out, slice s) const {
return out << "{id:" << s << ",w:" << width(s) << "}"; return out << "{id:" << s << ",w:" << width(s) << "}";
} }

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

@ -68,9 +68,9 @@ namespace polysat {
// need src -> [v] and v -> [src] for propagation? // need src -> [v] and v -> [src] for propagation?
#endif #endif
using slice_idx = unsigned; using slice = unsigned;
using slice_idx_vector = unsigned_vector; using slice_vector = unsigned_vector;
static constexpr slice_idx null_slice_idx = std::numeric_limits<slice_idx>::max(); static constexpr slice null_slice = std::numeric_limits<slice>::max();
static constexpr unsigned null_cut = std::numeric_limits<unsigned>::max(); static constexpr unsigned null_cut = std::numeric_limits<unsigned>::max();
@ -80,45 +80,45 @@ namespace polysat {
// 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)
// (UINT_MAX for leaf slices) // (UINT_MAX for leaf slices)
unsigned_vector m_slice_cut; unsigned_vector m_slice_cut;
// The sub-slices are at indices sub and sub+1 (null_slice_idx if no subdivision) // The sub-slices are at indices sub and sub+1 (null_slice if no subdivision)
slice_idx_vector m_slice_sub; slice_vector m_slice_sub;
slice_idx_vector m_find; // representative of equivalence class slice_vector m_find; // representative of equivalence class
slice_idx_vector m_size; // number of elements in equivalence class slice_vector m_size; // number of elements in equivalence class
slice_idx_vector m_next; // next element of the equivalence class slice_vector m_next; // next element of the equivalence class
slice_idx_vector m_var2slice; // pvar -> slice_idx slice_vector m_var2slice; // pvar -> slice
slice_idx alloc_slice(); slice alloc_slice();
slice_idx var2slice(pvar v) const { return find(m_var2slice[v]); } slice var2slice(pvar v) const { return find(m_var2slice[v]); }
unsigned width(slice_idx s) const { return m_slice_width[s]; } unsigned width(slice s) const { return m_slice_width[s]; }
bool has_sub(slice_idx s) const { return m_slice_sub[s] != null_slice_idx; } bool has_sub(slice s) const { return m_slice_sub[s] != null_slice; }
/// Split slice s into s[|s|-1:cut+1] and s[cut:0] /// Split slice s into s[|s|-1:cut+1] and s[cut:0]
void split(slice_idx s, unsigned cut); void split(slice s, unsigned cut);
/// Retrieve base slices s_1,...,s_n such that src == s_1 ++ ... + s_n /// 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; 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_idx src, unsigned hi, unsigned lo, slice_idx_vector& out_base, bool output_full_src = false); void mk_slice(slice src, unsigned hi, unsigned lo, slice_vector& out_base, bool output_full_src = false);
/// Find representative /// Find representative
slice_idx find(slice_idx s) const; slice find(slice s) const;
/// Find representative of upper subslice /// Find representative of upper subslice
slice_idx find_sub_hi(slice_idx s) const; slice find_sub_hi(slice s) const;
/// Find representative of lower subslice /// Find representative of lower subslice
slice_idx find_sub_lo(slice_idx s) const; slice find_sub_lo(slice 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 s1, slice s2);
// Merge equality x_1 ++ ... ++ x_n == y_1 ++ ... ++ y_k // Merge equality x_1 ++ ... ++ x_n == y_1 ++ ... ++ y_k
// //
// 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_idx_vector& xs, slice_idx_vector& ys); void merge(slice_vector& xs, slice_vector& ys);
void merge(slice_idx_vector& xs, slice_idx y); void merge(slice_vector& xs, slice 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);
@ -130,8 +130,8 @@ namespace polysat {
merge_class, merge_class,
}; };
svector<trail_item> m_trail; svector<trail_item> m_trail;
slice_idx_vector m_split_trail; slice_vector m_split_trail;
slice_idx_vector m_merge_trail; slice_vector m_merge_trail;
unsigned_vector m_scopes; unsigned_vector m_scopes;
void undo_add_var(); void undo_add_var();
@ -140,7 +140,7 @@ namespace polysat {
void undo_merge_class(); void undo_merge_class();
mutable slice_idx_vector m_tmp1; mutable slice_vector m_tmp1;
public: public:
@ -179,7 +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; std::ostream& display(std::ostream& out, slice 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); }

10
src/test/slicing.cpp
View file

@ -29,23 +29,23 @@ namespace polysat {
pvar b = s.add_var(6); pvar b = s.add_var(6);
std::cout << sl << "\n"; std::cout << sl << "\n";
slicing::slice_idx_vector x_7_3; slicing::slice_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_idx_vector a_4_0; slicing::slice_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_idx_vector y_5_0; slicing::slice_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_idx_vector x_base; slicing::slice_vector x_base;
sl.find_base(sl.var2slice(x), x_base); sl.find_base(sl.var2slice(x), x_base);
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);
sl.merge(x_base, y_base); sl.merge(x_base, y_base);
std::cout << sl << "\n"; std::cout << sl << "\n";