Hi,
The Value Analysis plugin of Frama-C uses hash-consing of Patricial trees extensively. In fact, some analyses would not run without it at all. See Section 9 of
cristal.inria.fr/~doligez/publications/cuoq-doligez-mlw-2008.ps for more details. Unfortunately, as mentioned there, no figures exist for with hash-consing vs. without hash-consing -- but most of the examples would have failed without it.
Although I'm not sure what was implemented exactly at the time, one important feature when using hash-consed Patricia trees is the possibility of using caches. Alain mentioned this in this mail:
> Also, you get a nice unique integer for each tree. This allow you to
> memoize efficiently set operations (like union, intersection, for which
> you can use memoization in the inner loop, not only at toplevel), and to
> build sets of sets (and so on).
I should stress that the possibility of memoizing *in the inner loop*, is crucial. When performing e.g. unions or map2 operations, it is possible to return a result in constant time when either
- the two trees is equivalent (because e.g. union s s == s)