diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc index 6f6aef0df..f5755408a 100644 --- a/spot/ltsmin/ltsmin.cc +++ b/spot/ltsmin/ltsmin.cc @@ -42,6 +42,8 @@ #include #include #include +#include +#include using namespace std::string_literals; @@ -1115,12 +1117,36 @@ namespace spot } }; - typedef std::unordered_map cspins_state_map; + struct both + { + cspins_state first; + int second; + }; - typedef std::unordered_set cspins_state_set; + struct cspins_state_hasher + { + cspins_state_hasher(cspins_state&) + { } + cspins_state_hasher() = default; + + brick::hash::hash128_t + hash(cspins_state t) const + { + // FIXME we should compute a better hash value for this particular + // case. Shall we use two differents hash functions? + return std::make_pair(t[0], t[0]); + } + + bool equal(cspins_state lhs, cspins_state rhs) const + { + return 0 == memcmp(lhs, rhs, (2+rhs[1])* sizeof(int)); + } + }; + + //brick::hashset::FastConcurrent ht2; + typedef brick::hashset::FastConcurrent cspins_state_map; //////////////////////////////////////////////////////////////////////// // A manager for Cspins states. @@ -1255,12 +1281,10 @@ namespace spot cspins_state s = inner->manager->alloc_setup(dst, inner->compressed_, inner->manager->size() * 2); - auto it = inner->map->insert({s, inner->default_value_}); - inner->succ->push_back((*(it.first)).first); - if (!it.second) - { - inner->manager->dealloc(s); - } + auto it = inner->map->insert({s}); + inner->succ->push_back(*it); + if (!it.isnew()) + inner->manager->dealloc(s); }, &inner); if (!n && selfloopize) @@ -1306,9 +1330,9 @@ namespace spot cspins_state s = inner->manager->alloc_setup(dst, inner->compressed_, inner->manager->size() * 2); - auto it = inner->map->insert({s, inner->default_value_}); - inner->succ->push_back((*(it.first)).first); - if (!it.second) + auto it = inner->map->insert({s}); + inner->succ->push_back(*it); + if (!it.isnew()) inner->manager->dealloc(s); }, &inner); @@ -1387,7 +1411,7 @@ namespace spot compress_(compress), cubeset_(visible_aps.size()), selfloopize_(selfloopize), aps_(visible_aps) { - map_.reserve(2000000); + map_.setSize(2000000); recycle_.reserve(2000000); inner_.compressed_ = new int[d_->get_state_size() * 2]; inner_.uncompressed_ = new int[d_->get_state_size()+30]; @@ -1396,13 +1420,6 @@ namespace spot } ~kripkecube() { - typename cspins_state_map::const_iterator s = map_.begin(); - while (s != map_.end()) - { - manager_.dealloc(s->first); - ++s; - } - map_.clear(); for (auto i: recycle_) { cubeset_.release(i->condition());