Skip to content

Commit f91394b

Browse files
committed
Make numbering use unordered_map if numbering ireps
This avoids slow lookups into `std::map` caused by long running `irept::operator<` calls.
1 parent a46f12d commit f91394b

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

src/util/numbering.h

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,12 @@ Author: Daniel Kroening, [email protected]
1010
#define CPROVER_UTIL_NUMBERING_H
1111

1212
#include <map>
13+
#include <type_traits>
1314
#include <unordered_map>
1415
#include <vector>
1516

1617
#include "invariant.h"
18+
#include "irep.h"
1719
#include "optional.h"
1820

1921
/// \tparam Map: a map from a key type to some numeric type
@@ -110,7 +112,10 @@ class template_numberingt final
110112
};
111113

112114
template <typename Key>
113-
using numbering = template_numberingt<std::map<Key, std::size_t>>; // NOLINT
115+
using numbering = typename std::conditional<
116+
std::is_base_of<irept, Key>::value,
117+
template_numberingt<std::unordered_map<Key, std::size_t, irep_hash>>,
118+
template_numberingt<std::map<Key, std::size_t>>>::type;
114119

115120
template <typename Key, typename Hash>
116121
using hash_numbering = // NOLINT

0 commit comments

Comments
 (0)