Skip to content

Commit 15a6759

Browse files
committed
Make union_find use hashes for numbering
This avoids slow lookups into `std::map` caused by long running `irept::operator<` calls. The type of hash to use is included as a template parameter in order to make the data structure used to implement `union_find` more explicit.
1 parent 908ef78 commit 15a6759

File tree

2 files changed

+5
-3
lines changed

2 files changed

+5
-3
lines changed

src/solvers/flattening/arrays.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ class arrayst:public equalityt
6868
array_equalitiest array_equalities;
6969

7070
// this is used to find the clusters of arrays being compared
71-
union_find<exprt> arrays;
71+
union_find<exprt, irep_hash> arrays;
7272

7373
// this tracks the array indicies for each array
7474
typedef std::set<exprt> index_sett;

src/util/union_find.h

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -132,11 +132,13 @@ class unsigned_union_find
132132
size_type get_other(size_type a);
133133
};
134134

135-
template <typename T>
135+
/// \tparam T: The type of values stored.
136+
/// \tparam hasht: The type of hash used for looking up the value numbering.
137+
template <typename T, typename hasht = std::hash<T>>
136138
// NOLINTNEXTLINE(readability/identifiers)
137139
class union_find final
138140
{
139-
using numbering_typet = numbering<T>;
141+
using numbering_typet = numberingt<T, hasht>;
140142
numbering_typet numbers;
141143

142144
// NOLINTNEXTLINE(readability/identifiers)

0 commit comments

Comments
 (0)