mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 17:45:32 +00:00
find is now get_root
This commit is contained in:
Jakob Rath
parent
b8d118a558
commit
741e37c2d7
2 changed files with 18 additions and 49 deletions
|
|
@ -249,7 +249,6 @@ namespace polysat {
|
|||
}
|
||||
#endif
|
||||
|
||||
#if 1
|
||||
bool slicing::merge_base(enode* s1, enode* s2, dep_t dep) {
|
||||
SASSERT_EQ(width(s1), width(s2));
|
||||
SASSERT(!has_sub(s1));
|
||||
|
|
@ -262,7 +261,7 @@ namespace polysat {
|
|||
#if 0
|
||||
bool slicing::merge_value(slice s0, rational val0, dep_t dep) {
|
||||
vector<std::pair<slice, rational>> todo;
|
||||
todo.push_back({find(s0), std::move(val0)});
|
||||
todo.push_back({s0->get_root(), std::move(val0)});
|
||||
// check compatibility for sub-slices
|
||||
for (unsigned i = 0; i < todo.size(); ++i) {
|
||||
auto const& [s, val] = todo[i];
|
||||
|
|
@ -278,8 +277,8 @@ namespace polysat {
|
|||
if (has_sub(s)) {
|
||||
// s is split into [s.width-1, cut+1] and [cut, 0]
|
||||
unsigned const cut = m_slice_cut[s];
|
||||
todo.push_back({find_sub_lo(s), mod2k(val, cut + 1)});
|
||||
todo.push_back({find_sub_hi(s), machine_div2k(val, cut + 1)});
|
||||
todo.push_back({sub_lo(s)->get_root(), mod2k(val, cut + 1)});
|
||||
todo.push_back({sub_hi(s)->get_root(), machine_div2k(val, cut + 1)});
|
||||
}
|
||||
}
|
||||
// all succeeded, so apply the values
|
||||
|
|
@ -339,8 +338,8 @@ namespace polysat {
|
|||
if (x == y)
|
||||
continue;
|
||||
if (width(x) == width(y)) {
|
||||
enode* const rx = find(x);
|
||||
enode* const ry = find(y);
|
||||
enode* const rx = x->get_root();
|
||||
enode* const ry = y->get_root();
|
||||
if (rx == ry)
|
||||
explain_class(x, y, out_deps);
|
||||
else {
|
||||
|
|
@ -351,7 +350,7 @@ namespace polysat {
|
|||
}
|
||||
}
|
||||
else if (width(x) > width(y)) {
|
||||
enode* const rx = find(x);
|
||||
enode* const rx = x->get_root();
|
||||
xs.push_back(sub_hi(rx));
|
||||
xs.push_back(sub_lo(rx));
|
||||
ys.push_back(y);
|
||||
|
|
@ -359,7 +358,7 @@ namespace polysat {
|
|||
else {
|
||||
SASSERT(width(x) < width(y));
|
||||
xs.push_back(x);
|
||||
enode* const ry = find(y);
|
||||
enode* const ry = y->get_root();
|
||||
ys.push_back(sub_hi(ry));
|
||||
ys.push_back(sub_lo(ry));
|
||||
}
|
||||
|
|
@ -441,8 +440,8 @@ namespace polysat {
|
|||
enode_vector& ys = m_tmp3;
|
||||
SASSERT(xs.empty());
|
||||
SASSERT(ys.empty());
|
||||
find_base(x, xs);
|
||||
find_base(y, ys);
|
||||
get_root_base(x, xs);
|
||||
get_root_base(y, ys);
|
||||
SASSERT(all_of(xs, [](enode* s) { return s->is_root(); }));
|
||||
SASSERT(all_of(ys, [](enode* s) { return s->is_root(); }));
|
||||
bool result = (xs == ys);
|
||||
|
|
@ -454,7 +453,7 @@ namespace polysat {
|
|||
return result;
|
||||
}
|
||||
|
||||
template <bool should_find>
|
||||
template <bool should_get_root>
|
||||
void slicing::get_base_core(enode* src, enode_vector& out_base) const {
|
||||
enode_vector& todo = m_tmp1;
|
||||
SASSERT(todo.empty());
|
||||
|
|
@ -462,7 +461,7 @@ namespace polysat {
|
|||
while (!todo.empty()) {
|
||||
enode* s = todo.back();
|
||||
todo.pop_back();
|
||||
if constexpr (should_find) {
|
||||
if constexpr (should_get_root) {
|
||||
s = s->get_root();
|
||||
}
|
||||
if (!has_sub(s))
|
||||
|
|
@ -479,7 +478,7 @@ namespace polysat {
|
|||
get_base_core<false>(src, out_base);
|
||||
}
|
||||
|
||||
void slicing::find_base(enode* src, enode_vector& out_base) const {
|
||||
void slicing::get_root_base(enode* src, enode_vector& out_base) const {
|
||||
get_base_core<true>(src, out_base);
|
||||
}
|
||||
|
||||
|
|
@ -659,7 +658,7 @@ namespace polysat {
|
|||
out << "v" << v << ":";
|
||||
base.reset();
|
||||
enode* const vs = var2slice(v);
|
||||
find_base(vs, base);
|
||||
get_root_base(vs, base);
|
||||
for (enode* s : base)
|
||||
display(out << " ", s);
|
||||
// if (has_value(vs)) {
|
||||
|
|
@ -722,12 +721,11 @@ namespace polysat {
|
|||
}
|
||||
// if slice has a value, it should be propagated to its sub-slices
|
||||
// if (has_value(s)) {
|
||||
// VERIFY(has_value(find_sub_hi(s)));
|
||||
// VERIFY(has_value(find_sub_lo(s)));
|
||||
// VERIFY(has_value(sub_hi(s)->get_root()));
|
||||
// VERIFY(has_value(sub_lo(s)->get_root()));
|
||||
// }
|
||||
}
|
||||
return true;
|
||||
}
|
||||
#endif
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -49,7 +49,7 @@ namespace polysat {
|
|||
struct slice_info {
|
||||
unsigned width = 0; // number of bits in the slice
|
||||
unsigned cut = null_cut; // cut point, or null_cut if no subslices
|
||||
pvar var = null_var; // slice is equivalent to this variable, if any
|
||||
pvar var = null_var; // slice is equivalent to this variable, if any (without dependencies)
|
||||
enode* slice = nullptr; // if enode corresponds to a concat(...) expression, this field links to the represented slice.
|
||||
enode* sub_hi = nullptr; // upper subslice s[|s|-1:cut+1]
|
||||
enode* sub_lo = nullptr; // lower subslice s[cut:0]
|
||||
|
|
@ -67,8 +67,6 @@ namespace polysat {
|
|||
ast_manager m_ast;
|
||||
sort_ref m_slice_sort;
|
||||
func_decl_ref_vector m_concat_decls;
|
||||
// expr_ref_vector m_expr_storage;
|
||||
// unsigned_vector m_expr_scopes;
|
||||
|
||||
euf::egraph m_egraph;
|
||||
slice_info_vector m_info; // indexed by enode::get_id()
|
||||
|
|
@ -113,32 +111,8 @@ namespace polysat {
|
|||
unsigned_vector m_slice_cut;
|
||||
// The sub-slices are at indices sub and sub+1 (or null_slice if there is no subdivision)
|
||||
slice_vector m_slice_sub;
|
||||
|
||||
pvar_vector m_slice2var; // slice -> pvar, or null_var if slice is not equivalent to a variable
|
||||
slice_vector m_var2slice; // pvar -> slice
|
||||
|
||||
ptr_vector<euf::enode> m_slice2enode;
|
||||
ptr_addr_map<euf::enode, slice> m_enode2slice;
|
||||
*/
|
||||
|
||||
#if 0
|
||||
unsigned_vector m_mark;
|
||||
unsigned m_mark_timestamp = 0;
|
||||
#if Z3DEBUG
|
||||
bool m_mark_active = false;
|
||||
#endif
|
||||
|
||||
void begin_mark() {
|
||||
DEBUG_CODE({ SASSERT(!m_mark_active); m_mark_active = true; });
|
||||
m_mark_timestamp++;
|
||||
if (!m_mark_timestamp)
|
||||
m_mark_timestamp++;
|
||||
}
|
||||
void end_mark() { DEBUG_CODE({ SASSERT(m_mark_active); m_mark_active = false; }); }
|
||||
bool is_marked(slice s) const { SASSERT(m_mark_active); return m_mark[s] == m_mark_timestamp; }
|
||||
void mark(slice s) { SASSERT(m_mark_active); m_mark[s] = m_mark_timestamp; }
|
||||
#endif
|
||||
|
||||
slice_info& info(euf::enode* n);
|
||||
slice_info const& info(euf::enode* n) const;
|
||||
|
||||
|
|
@ -172,22 +146,19 @@ namespace polysat {
|
|||
void split(enode* s, unsigned cut);
|
||||
void split_core(enode* s, unsigned cut);
|
||||
|
||||
template <bool should_find>
|
||||
template <bool should_get_root>
|
||||
void get_base_core(enode* src, enode_vector& out_base) const;
|
||||
|
||||
/// Retrieve base slices s_1,...,s_n such that src == s_1 ++ ... ++ s_n (actual descendant subslices)
|
||||
void get_base(enode* src, enode_vector& out_base) const;
|
||||
/// Retrieve base slices s_1,...,s_n such that src == s_1 ++ ... ++ s_n (representatives of subslices)
|
||||
void find_base(enode* src, enode_vector& out_base) const;
|
||||
void get_root_base(enode* src, enode_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, return the new base for src, i.e., src == s_1 ++ ... ++ s_n.
|
||||
/// If output_base is false, return coarsest intermediate slices instead of only base slices.
|
||||
void mk_slice(enode* src, unsigned hi, unsigned lo, enode_vector& out, bool output_full_src = false, bool output_base = true);
|
||||
|
||||
/// Find representative
|
||||
enode* find(enode* s) const { return s->get_root(); }
|
||||
|
||||
// Merge equivalence classes of two base slices.
|
||||
// Returns true if merge succeeded without conflict.
|
||||
[[nodiscard]] bool merge_base(enode* s1, enode* s2, dep_t dep);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue