Commit 2e890dfa authored by Thibault Allançon's avatar Thibault Allançon

mc: bloom_filter: regroup hash function in misc/hashfunc

* spot/mc/bitstate.hh,
  spot/mc/mc.hh,
  tests/ltsmin/modelcheck.cc: use size_t for mem_size
* spot/mc/bloom_filter.hh,
  spot/misc/hashfunc.hh: regroup hash function
parent 64bcc008
...@@ -29,7 +29,7 @@ namespace spot ...@@ -29,7 +29,7 @@ namespace spot
class bitstate class bitstate
{ {
public: public:
bitstate(kripkecube<State, SuccIterator>& sys, uint32_t mem_size): bitstate(kripkecube<State, SuccIterator>& sys, size_t mem_size):
sys_(sys) sys_(sys)
{ {
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys), static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
......
...@@ -19,41 +19,25 @@ ...@@ -19,41 +19,25 @@
#pragma once #pragma once
#include <spot/misc/hashfunc.hh>
#include <functional> #include <functional>
namespace spot namespace spot
{ {
class bloom_filter class bloom_filter
{ {
using hash_t = uint32_t; using hash_t = size_t;
using hash_function_t = std::function<hash_t(hash_t)>; using hash_function_t = std::function<hash_t(hash_t)>;
// https://burtleburtle.net/bob/c/lookup3.c
#define rot(x,k) (((x)<<(k)) | ((x)>>(32-(k))))
static hash_t jenkins_hash_function(hash_t k)
{
hash_t s1, s2;
s1 = s2 = 0xdeadbeef;
s2 ^= s1; s2 -= rot(s1, 14);
k ^= s2; k -= rot(s2, 11);
s1 ^= k; s1 -= rot(k, 25);
s2 ^= s1; s2 -= rot(s1, 16);
k ^= s2; k -= rot(s2, 4);
s1 ^= k; s1 -= rot(k, 14);
s2 ^= s1; s2 -= rot(s1, 24);
return s2;
}
public: public:
bloom_filter(uint32_t mem_size) bloom_filter(size_t mem_size)
: mem_size_(mem_size) : mem_size_(mem_size)
{ {
bitset_.assign(mem_size, false); bitset_.assign(mem_size, false);
// Internal hash functions // Internal hash functions
hash_functions_.push_back(jenkins_hash_function); hash_functions_.push_back(lookup3_hash);
} }
void insert(hash_t elem) void insert(hash_t elem)
...@@ -80,6 +64,6 @@ namespace spot ...@@ -80,6 +64,6 @@ namespace spot
private: private:
std::vector<hash_function_t> hash_functions_; std::vector<hash_function_t> hash_functions_;
std::vector<bool> bitset_; std::vector<bool> bitset_;
uint32_t mem_size_; size_t mem_size_;
}; };
} }
...@@ -418,7 +418,7 @@ namespace spot ...@@ -418,7 +418,7 @@ namespace spot
template<typename kripke_ptr, typename State, template<typename kripke_ptr, typename State,
typename Iterator, typename Hash, typename Equal> typename Iterator, typename Hash, typename Equal>
void bitstate_hashing(kripke_ptr sys, uint32_t mem_size) void bitstate_hashing(kripke_ptr sys, size_t mem_size)
{ {
using algo_name = spot::bitstate<State, Iterator, Hash, Equal>; using algo_name = spot::bitstate<State, Iterator, Hash, Equal>;
auto s = new algo_name(*sys, mem_size); auto s = new algo_name(*sys, mem_size);
......
...@@ -64,6 +64,33 @@ namespace spot ...@@ -64,6 +64,33 @@ namespace spot
return (key >> 3) * 2654435761U; return (key >> 3) * 2654435761U;
} }
/// \brief Jenkins lookup3 hash function.
///
/// https://burtleburtle.net/bob/c/lookup3.c
#define _jenkins_rot(x,k) (((x)<<(k)) | ((x)>>(32-(k))))
inline size_t
lookup3_hash(size_t key)
{
size_t s1, s2;
s1 = s2 = 0xdeadbeef;
s2 ^= s1;
s2 -= _jenkins_rot(s1, 14);
key ^= s2;
key -= _jenkins_rot(s2, 11);
s1 ^= key;
s1 -= _jenkins_rot(key, 25);
s2 ^= s1;
s2 -= _jenkins_rot(s1, 16);
key ^= s2;
key -= _jenkins_rot(s2, 4);
s1 ^= key;
s1 -= _jenkins_rot(key, 14);
s2 ^= s1;
s2 -= _jenkins_rot(s1, 24);
return s2;
}
/// Struct for Fowler-Noll-Vo parameters /// Struct for Fowler-Noll-Vo parameters
template<class T, class Enable = void> template<class T, class Enable = void>
......
...@@ -77,7 +77,7 @@ struct mc_options_ ...@@ -77,7 +77,7 @@ struct mc_options_
bool bloemen = false; bool bloemen = false;
bool bloemen_ec = false; bool bloemen_ec = false;
bool cndfs = false; bool cndfs = false;
unsigned bitstate_mem_size = 0; size_t bitstate_mem_size = 0;
} mc_options; } mc_options;
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment