mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-10 13:10:50 +00:00
Code Activity

slice2var

Browse source
This commit is contained in:
Jakob Rath 2023-06-15 17:12:19 +02:00
parent 862707baa0
commit 982170e6e0
2 changed files with 16 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -42,9 +42,10 @@ 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 const s = alloc_slice(); slice const s = alloc_slice();
m_slice_width[s] = bit_width; m_slice_width[s] = bit_width;
m_slice2var[s] = v;
m_var2slice.push_back(s); m_var2slice.push_back(s);
} }
@ -60,6 +61,7 @@ namespace polysat {
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);
m_slice2var.push_back(null_var);
m_trail.push_back(trail_item::alloc_slice); m_trail.push_back(trail_item::alloc_slice);
return s; return s;
} }
@ -71,6 +73,7 @@ namespace polysat {
m_find.pop_back(); m_find.pop_back();
m_size.pop_back(); m_size.pop_back();
m_next.pop_back(); m_next.pop_back();
m_slice2var.pop_back();
} }
slicing::slice slicing::find_sub_hi(slice parent) const { slicing::slice slicing::find_sub_hi(slice parent) const {
@ -128,6 +131,12 @@ namespace polysat {
m_find[r1] = r2; m_find[r1] = r2;
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]);
if (m_slice2var[r2] == null_var)
m_slice2var[r2] = m_slice2var[r1];
else {
// otherwise the classes should have been merged already
SASSERT(m_slice2var[r2] != m_slice2var[r1]);
}
m_trail.push_back(trail_item::merge_class); m_trail.push_back(trail_item::merge_class);
m_merge_trail.push_back(r1); m_merge_trail.push_back(r1);
} }
@ -140,6 +149,8 @@ namespace polysat {
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]);
if (m_slice2var[r2] == m_slice2var[r1])
m_slice2var[r2] = null_var;
} }
void slicing::merge(slice_vector& xs, slice_vector& ys) { void slicing::merge(slice_vector& xs, slice_vector& ys) {

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

@ -75,22 +75,24 @@ 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
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)
// (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 if no subdivision) // The sub-slices are at indices sub and sub+1 (null_slice if no subdivision)
slice_vector m_slice_sub; slice_vector m_slice_sub;
slice_vector m_find; // representative of equivalence class slice_vector m_find; // representative of equivalence class
slice_vector m_size; // number of elements in equivalence class slice_vector m_size; // number of elements in equivalence class
slice_vector m_next; // next element of the equivalence class slice_vector m_next; // next element of the equivalence class
unsigned_vector m_slice2var; // slice -> pvar, or null_var if slice is not equivalent to a variable
slice_vector m_var2slice; // pvar -> slice slice_vector m_var2slice; // pvar -> slice
slice alloc_slice(); slice alloc_slice();
slice var2slice(pvar v) const { return find(m_var2slice[v]); } slice var2slice(pvar v) const { return find(m_var2slice[v]); }
pvar slice2var(slice s) const { return m_slice2var[find(s)]; }
unsigned width(slice s) const { return m_slice_width[s]; } unsigned width(slice s) const { return m_slice_width[s]; }
bool has_sub(slice s) const { return m_slice_sub[s] != null_slice; } bool has_sub(slice s) const { return m_slice_sub[s] != null_slice; }