* src/misc/hashfunc.hh (knuth32_hash): New function.

* src/misc/hash.hh (ptr_hash): Use knuth32_hash.
* src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory): Use
ltl::formula_ptr_hash for acc_map_.
This commit is contained in:
Alexandre Duret-Lutz 2005-05-04 16:09:41 +00:00
parent 9063c5abb4
commit 814ec7c2d0
4 changed files with 26 additions and 5 deletions

View file

@ -1,5 +1,10 @@
2005-05-04 Alexandre Duret-Lutz <adl@src.lip6.fr> 2005-05-04 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/misc/hashfunc.hh (knuth32_hash): New function.
* src/misc/hash.hh (ptr_hash): Use knuth32_hash.
* src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory): Use
ltl::formula_ptr_hash for acc_map_.
* src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_fm.cc: Add * src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_fm.cc: Add
the reduce_ltl argument. the reduce_ltl argument.
* src/tgbatest/ltl2tgba.cc: Add options -fr1, -fr2, -fr3, and -fr4. * src/tgbatest/ltl2tgba.cc: Add options -fr1, -fr2, -fr3, and -fr4.

View file

@ -1,4 +1,4 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -24,6 +24,7 @@
# include <string> # include <string>
# include <functional> # include <functional>
# include "hashfunc.hh"
// See the G++ FAQ for details about the following. // See the G++ FAQ for details about the following.
# ifdef __GNUC__ # ifdef __GNUC__
@ -62,7 +63,8 @@ namespace spot
{ {
size_t operator()(const T* p) const size_t operator()(const T* p) const
{ {
return reinterpret_cast<const char*>(p) - static_cast<const char*>(0); return knuth32_hash(reinterpret_cast<const char*>(p)
- static_cast<const char*>(0));
} }
}; };

View file

@ -1,4 +1,4 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -45,6 +45,20 @@ namespace spot
key ^= (key >> 16); key ^= (key >> 16);
return key; return key;
} }
/// \brief Knuth's Multiplicative hash function.
///
/// This function is suitable for hashing values whose
/// high order bits do not vary much (ex. addresses of
/// memory objects). Prefer spot::wang32_hash() otherwise.
/// http://www.concentric.net/~Ttwang/tech/addrhash.htm
inline size_t
knuth32_hash(size_t key)
{
// 2654435761 is the golden ratio of 2^32. The right shift of 3
// bits assumes that all objects are aligned on a 8 byte boundary.
return (key >> 3) * 2654435761U;
}
/// @} /// @}
} }

View file

@ -1,4 +1,4 @@
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -86,7 +86,7 @@ namespace spot
tgba_bdd_core_data data_; ///< Core data for the new automata. tgba_bdd_core_data data_; ///< Core data for the new automata.
typedef Sgi::hash_map<const ltl::formula*, bdd, typedef Sgi::hash_map<const ltl::formula*, bdd,
ptr_hash<ltl::formula> > acc_map_; ltl::formula_ptr_hash> acc_map_;
acc_map_ acc_; ///< BDD associated to each acceptance condition acc_map_ acc_; ///< BDD associated to each acceptance condition
}; };