mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
adding hash/eq to uint_set
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
1239c8f8e8
commit
0997eba700
|
@ -131,6 +131,32 @@ static void tst4() {
|
|||
SASSERT(!s.contains(0));
|
||||
}
|
||||
|
||||
#include "map.h"
|
||||
|
||||
template <typename Value>
|
||||
struct uint_map : public map<uint_set, Value, uint_set::hash, uint_set::eq> {};
|
||||
|
||||
static void tst5() {
|
||||
uint_set s;
|
||||
std::cout << s.get_hash() << "\n";
|
||||
s.insert(1);
|
||||
std::cout << s.get_hash() << "\n";
|
||||
s.insert(2);
|
||||
std::cout << s.get_hash() << "\n";
|
||||
s.insert(44);
|
||||
std::cout << s.get_hash() << "\n";
|
||||
|
||||
uint_map<unsigned> m;
|
||||
m.insert(s, 1);
|
||||
s.insert(4);
|
||||
m.insert(s, 3);
|
||||
uint_map<unsigned>::iterator it = m.begin(), end = m.end();
|
||||
for (; it != end; ++it) {
|
||||
std::cout << it->m_key << " : " << it->m_value << "\n";
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
void tst_uint_set() {
|
||||
for (unsigned i = 0; i < 100; i++) {
|
||||
tst1(1 + rand()%31);
|
||||
|
@ -146,5 +172,6 @@ void tst_uint_set() {
|
|||
tst3(12);
|
||||
tst3(100);
|
||||
tst4();
|
||||
tst5();
|
||||
}
|
||||
|
||||
|
|
|
@ -218,6 +218,18 @@ public:
|
|||
|
||||
iterator const begin() const { return iterator(*this, false); }
|
||||
iterator const end() const { return iterator(*this, true); }
|
||||
|
||||
unsigned get_hash() const {
|
||||
unsigned h = 0;
|
||||
for (unsigned i = 0; i < size(); ++i) {
|
||||
h += (i+1)*((*this)[i]);
|
||||
}
|
||||
return h;
|
||||
}
|
||||
|
||||
struct eq { bool operator()(uint_set const& s1, uint_set const& s2) const { return s1 == s2; } };
|
||||
struct hash { unsigned operator()(uint_set const& s) const { return s.get_hash(); } };
|
||||
|
||||
};
|
||||
|
||||
inline std::ostream & operator<<(std::ostream & target, const uint_set & s) {
|
||||
|
|
Loading…
Reference in a new issue