lava::Lattice< V > Class Template Reference

The Lattice class template represents a finite distributive lattice. More...

#include <lavabdd.h>

List of all members.

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.

Detailed Description

template<typename V>
class lava::Lattice< V >

The Lattice class template represents a finite distributive lattice.


The documentation for this class was generated from the following file:
Generated on Tue Feb 23 19:27:51 2010 for LaVaBDD by  doxygen 1.6.3