The Lattice class template represents a finite distributive lattice. More...
#include <lavabdd.h>
Static Public Member Functions | |
| static bool | less (const V &x, const V &y) |
| The partial order of the lattice. It must be antisymmetric, reflexive and transitive. | |
| static bool | equal (const V &x, const V &y) |
| Is equivalent to "less(x,y) and less(y,x)" but ideally more efficient. | |
| static void | join (const V &x, const V &y, V &z) |
| Least upper bound operator of the lattice (or "join"). | |
| static void | meet (const V &x, const V &y, V &z) |
| Greatest lower bound operator of the lattice (or "meet"). | |
| static void | rpc (const V &x, const V &y, V &z) |
| Relative pseudocomplementation. Assumes that less(y, x) is true. Computes the greatest value z such that "x meet z = y". | |
| static void | drpc (const V &x, const V &y, V &z) |
| Dual relative pseudocomplementation. Assumes that less(x, y) is true. Computes the smallest value z such that "x join z = y". | |
| static void | top (V &x) |
| Returns the "top" element of the lattice. | |
| static void | bot (V &x) |
| Returns the "bottom" element of the lattice. | |
| static size_t | hash (const V &x) |
| Computes an approriate hash value for a lattice. It must be the case that "equal(x, y)" implies "hash(x) == hash(y)". Note that you can first compute an integer and then use LVBDD::hash_int. A poor implementation of this function will lead to bad performance due to hash map collisions. See http://www.sgi.com/tech/stl/HashFunction.html for more information. | |
| static void | print (const V &x, ostream &out) |
| Prints a textual representation of a lattice value. | |
| static int | size (const V &x) |
| Returns a reasonable measure of the size of the encoding of a lattice value. For instance, a reasonable measure for the size of a lattice value encoded as an ROBDD is the number of its nodes. | |
| static int | list_size (const list< V > &l) |
| Returns a reasonable measure of the size of a list of lattice values. In many cases, it is valid to simply return the sum of Lattice::size for each value in the list. If memory is shared among lattice values, this is not accurate (e.g. ROBDD), hence the need for this function. | |
The Lattice class template represents a finite distributive lattice.
1.6.3