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. |

class lava::Lattice< V >

The Lattice class template represents a finite distributive lattice.

The documentation for this class was generated from the following file:

- /Users/nmaquet/Documents/Workspace/lavabdd/src/lavabdd.h

Generated on Sun Mar 28 22:39:33 2010 for LaVaBDD by 1.6.3