mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00
Code Activity

fix #9815 properly

Browse source
This commit is contained in:
Nuno Lopes 2026-06-16 10:00:45 +01:00
parent c67bb140dc
commit 82777c0092
1 changed files with 6 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/util/obj_hashtable.h
View file

@ -62,10 +62,6 @@ public:
struct key_data {
Key * m_key = nullptr;
Value m_value;
key_data() = default;
key_data(Key* k): m_key(k) {}
key_data(Key* k, Value const& v): m_key(k), m_value(v) {}
key_data(Key* k, Value&& v): m_key(k), m_value(std::move(v)) {}
Value const & get_value() const { return m_value; }
Key & get_key () const { return *m_key; }
unsigned hash() const { return m_key->hash(); }
@ -136,15 +132,15 @@ public:
}
void insert(Key * const k, Value const & v) {
m_table.insert(key_data(k, v));
m_table.insert(key_data{k, v});
}
void insert(Key * const k, Value && v) {
m_table.insert(key_data(k, std::move(v)));
m_table.insert(key_data{k, std::move(v)});
}
Value& insert_if_not_there(Key * k, Value const & v) {
return m_table.insert_if_not_there2(key_data(k, v))->get_data().m_value;
return m_table.insert_if_not_there2(key_data{k, v})->get_data().m_value;
}
Value& insert_if_not_there(Key * k, Value && v) {
@ -194,7 +190,7 @@ public:
}
iterator find_iterator(Key * k) const {
return m_table.find(key_data(k));
return m_table.find(key_data{k});
}
bool contains(Key * k) const {
@ -202,7 +198,7 @@ public:
}
void remove(Key * k) {
m_table.remove(key_data(k));
m_table.remove(key_data{k});
}
void erase(Key * k) {
@ -213,7 +209,7 @@ public:
void get_collisions(Key * k, vector<Key*>& collisions) {
vector<key_data> cs;
m_table.get_collisions(key_data(k), cs);
m_table.get_collisions(key_data{k}, cs);
for (key_data const& kd : cs) {
collisions.push_back(kd.m_key);
}