lava::LVBDD< L, F > Class Template Reference

The LVBDD class template represents a Lattice-Valued Binary Decision Diagram. More...

#include <lavabdd.h>

List of all members.

Public Member Functions

 LVBDD ()
 Default constructor. Is equal to L::bot().
 ~LVBDD ()
 Destructor.
 LVBDD (const LVBDD &other)
 Copy constructor.
LVBDDoperator= (const LVBDD &other)
 Assignment operator.
bool operator== (const LVBDD &other) const
 Equality operator. This tests only for pointer equality of the roots and runs thus in O(1).
bool operator!= (const LVBDD &other) const
 Inequality operator. Same remark as LVBDD::operator==.
LVBDD join (const LVBDD &other) const
 Computes the join of two LVBDD. Runtime complexity depends on the chosen normal form.
LVBDD operator| (const LVBDD &other) const
 Syntactic sugar for LVBDD::join.
LVBDD meet (const LVBDD &other) const
 Computes the meet of two LVBDD. Runtime complexity depends on the chosen normal form.
LVBDD operator& (const LVBDD &other) const
 Syntactic sugar for LVBDD::meet.
int size () const
 Returns the number of nodes in the LVBDD.
int nonterminal_size () const
 Returns the number of non-terminal nodes in the LVBDD.
int terminal_size () const
 Returns the number of terminal nodes in the LVBDD.
int values_size () const
 Returns Lattice<V>::list_size() on the list of all values labeling the LVBDD.
void print_graphviz (ostream &out=cout) const
 Prints a DOT diagram of the LVBDD.
void exists (V &result) const
 Quantifies all decision variables existentially.
exists () const
 Quantifies all decision variables existentially.
void forall (V &result) const
 Quantifies all decision variables universally.
forall () const
 Quantifies all decision variables universally.
LVBDD lo () const
 Returns the low-child of the LVBDD. T Throws std::logic_error on terminal LVBDD.
LVBDD hi () const
 Returns the high-child of the LVBDD. T Throws std::logic_error on terminal LVBDD.
int index () const
 Returns the index (strictly positive) of the node's proposition for nonterminal LVBDD; returns 0 for terminal LVBDD.
void root_value (V &result) const
 Returns the lattice value labeling the root.
root_value () const
 Returns the lattice value labeling the root.
void evaluate (const vector< bool > &valuation, V &result) const
 Evaluate the LVBDD with a single propositional valuation. Throws std::logic_error if the valuation is incomplete.
evaluate (const vector< bool > &valuation) const
 Evaluate the LVBDD with a single propositional valuation. Throws std::logic_error if the valuation is incomplete.

Static Public Member Functions

static LVBDD terminal (const V &value)
 Creates a terminal LVBDD labeled by a chosen value.
static LVBDD literal (int index, bool positive)
 Creates a three-node LVBDD representing a positive or negative literal.
static LVBDD top ()
 Creates an LVBDD representing the "top" lattice constant.
static LVBDD bot ()
 Creates an LVBDD representing the "bottom" lattice constant.
static LVBDD _mk_unsafe (int index, V value, LVBDD lo, LVBDD hi)
 Creates an *non-terminal* LVBDD "by hand". Do not use unless you know what you're doing. Wrong use of this fonction leads to normal form violation.
static int orphan_count ()
 Returns the number of orphaned nodes (reference count = 0) in the hash map.
static void print_hashmap_debug (ostream &out=cout)
 Prints a complete dump of the hash map. Use for debugging.
static void print_hashmap_stats (ostream &out=cout)
 Prints various satistics about the hash map.
static void free_orphaned_nodes ()
 Deallocates all memory used by orphaned nodes.
static void clear_memoization_tables ()
 Clears the memoization tables of join and meet operations.
static int memoization_tables_size ()
 Returns the number of entries in the memoization tables.
static size_t total_node_count ()
 Returns the total number of allocated nodes (orphans included). Always equal to orphan_count() + node_count().
static size_t node_count ()
 Returns the number of nodes in use (non orphaned) in the hash map.
static void init ()
 Initialises the hash map. You MUST call this function before calling any other in the package.
static void print_graphviz_debug (ostream &out=cout)
 Prints a DOT diagram of the entire hash map. Use for debugging.

Friends

ostream & operator<< (ostream &out, const LVBDD &dd)
 Prints the memory address of an LVBDD's root node on an output stream.

Detailed Description

template<class L, int F>
class lava::LVBDD< L, F >

The LVBDD class template represents a Lattice-Valued Binary Decision Diagram.

See lava::UNF, lava::SNF_JOIN and and laval::SNF_MEET.


Member Function Documentation

template<class L , int F>
static LVBDD lava::LVBDD< L, F >::_mk_unsafe ( int  index,
value,
LVBDD< L, F >  lo,
LVBDD< L, F >  hi 
) [inline, static]

Creates an *non-terminal* LVBDD "by hand". Do not use unless you know what you're doing. Wrong use of this fonction leads to normal form violation.

Parameters:
[in] index : The proposition index of the root node. Must be strictly positive.
[in] value : The lattice value labeling the root node.
[in] lo : The node's low-child.
[in] hi : The node's high-child.
template<class L , int F>
V lava::LVBDD< L, F >::evaluate ( const vector< bool > &  valuation  )  const [inline]

Evaluate the LVBDD with a single propositional valuation. Throws std::logic_error if the valuation is incomplete.

Parameters:
[in] valuation : The valuation. Proposition i is indexed at valuation[i-1].
Returns:
The resulting lattice value.
template<class L , int F>
void lava::LVBDD< L, F >::evaluate ( const vector< bool > &  valuation,
V &  result 
) const [inline]

Evaluate the LVBDD with a single propositional valuation. Throws std::logic_error if the valuation is incomplete.

Parameters:
[in] valuation : The valuation. Proposition i is indexed at valuation[i-1].
[out] result : The resulting lattice value.
template<class L , int F>
static LVBDD lava::LVBDD< L, F >::literal ( int  index,
bool  positive 
) [inline, static]

Creates a three-node LVBDD representing a positive or negative literal.

Parameters:
[in] index : The proposition index of the literal. Must be strictly positive.
[in] positive : The polarity of the literal (positive or negative).

The documentation for this class was generated from the following file:
Generated on Tue Apr 20 10:34:30 2010 for LaVaBDD by  doxygen 1.6.3