diff --git a/src/util/map.h b/src/util/map.h index f6fe38ec2..849c3d24a 100644 --- a/src/util/map.h +++ b/src/util/map.h @@ -115,7 +115,7 @@ public: } entry * find_core(key const & k) const { - return m_table.find_core(key_data{k, value()}); + return m_table.find_core(key_data{k, value{}}); } bool find(key const & k, value & v) const { @@ -137,7 +137,7 @@ public: } iterator find_iterator(key const & k) const { - return m_table.find(key_data{k, value()}); + return m_table.find(key_data{k, value{}}); } value const & find(key const& k) const { @@ -161,8 +161,8 @@ public: return find_core(k) != nullptr; } - void remove(key const &k) { - m_table.remove(key_data{k, value()}); + void remove(key const & k) { + m_table.remove(key_data{k, value{}}); } void erase(key const & k) { @@ -184,7 +184,7 @@ public: } return true; } - + #ifdef Z3DEBUG bool check_invariant() { diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index ae2a54f04..e158d09cb 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -65,7 +65,7 @@ public: key_data() : m_key(nullptr), m_value(Value()) {} key_data(Key * key) : m_key(key), m_value(Value()) {} - key_data(Key * key, const Value& value) : m_key(key), m_value(value) {} + key_data(Key * key, const Value & value) : m_key(key), m_value(value) {} Value const & get_value() const { return m_value; } Key & get_key () const { return *m_key; } @@ -162,7 +162,7 @@ public: return m_table.insert_if_not_there2({k, v}); } - obj_map_entry *find_core(Key *k) const { + obj_map_entry *find_core(Key * k) const { return m_table.find_core({k}); } @@ -194,7 +194,7 @@ public: return find(k); } - iterator find_iterator(Key *k) const { + iterator find_iterator(Key * k) const { return m_table.find(key_data{k}); } @@ -202,7 +202,7 @@ public: return find_core(k) != nullptr; } - void remove(Key *k) { + void remove(Key * k) { m_table.remove(key_data{k, value()}); } diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 079f6357c..59301f4b2 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -32,8 +32,8 @@ class symbol_table { T m_data; key_data() {} - key_data(const symbol &key) : m_key(key) {} - key_data(const symbol &key, const T &data) : m_key(key), m_data(data) {} + key_data(const symbol & key) : m_key(key) {} + key_data(const symbol & key, const T & data) : m_key(key), m_data(data) {} }; struct key_data_hash_proc { @@ -120,7 +120,7 @@ public: result = e->get_data().m_data; return true; } - + bool contains(symbol key) const { return m_sym_table.contains(key_data{key}); }