10#ifndef CPROVER_UTIL_UNION_FIND_H
11#define CPROVER_UTIL_UNION_FIND_H
41 mutable std::vector<nodet>
nodes;
68 INVARIANT(
false,
"we don't implement shrinking yet");
87 return nodes[a].parent==a;
136template <
typename T,
typename hasht = std::hash<T>>
159 uuf.make_union(na, nb);
168 uuf.make_union(na, nb);
175 const std::optional<number_type> na =
numbers.get_number(a);
176 const std::optional<number_type> nb =
numbers.get_number(b);
179 return uuf.same_set(*na, *nb);
218 return uuf.is_root(a);
227 return uuf.is_root(na);
unsignedbv_typet size_type()
typename data_typet::size_type size_type
typename data_typet::const_iterator const_iterator
typename data_typet::iterator iterator
size_type number(const T &a)
T & operator[](size_type t)
void isolate(const_iterator it)
const T & find(const_iterator it) const
bool make_union(const T &a, const T &b)
size_type find_number(const T &a)
const_iterator cbegin() const
const_iterator cend() const
bool make_union(const_iterator it_a, const_iterator it_b)
typename numbering_typet::number_type number_type
const_iterator begin() const
numberingt< irep_idt, std::hash< irep_idt > > numbering_typet
size_type find_number(size_type a) const
const_iterator end() const
size_type find_number(const_iterator it) const
bool same_set(const T &a, const T &b) const
typename numbering_typet::size_type size_type
typename numbering_typet::const_iterator const_iterator
const T & operator[](size_type t) const
typename numbering_typet::iterator iterator
bool is_root(const T &a) const
std::optional< number_type > get_number(const T &a) const
bool same_set(const_iterator it_a, const_iterator it_b) const
bool is_root_number(size_type a) const
bool is_root(const_iterator it) const
const T & find(const T &a)
void intersection(const unsigned_union_find &other)
void resize(size_type size)
std::vector< nodet > nodes
void check_index(size_type a)
void re_root(size_type old, size_type new_root)
size_type find(size_type a) const
size_type count(size_type a) const
void swap(unsigned_union_find &other)
size_type count_roots() const
bool is_root(size_type a) const
size_type get_other(size_type a)
void make_union(size_type a, size_type b)
bool same_set(size_type a, size_type b) const
void isolate(size_type a)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.