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.
LVBDD &	operator= (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.
void	forall (V &result) 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.
void	evaluate (vector< bool > valuation, V &result) const
	Evaluate the LVBDD with a single propositional valuation. Throws std::logic_error if the valuation is incomplete.
Static Public Member Functions
static int	hash_int (int key)
	Simple hash function for int values. It is used internally to hash pointers and indexes.
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 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.

---

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. TODO: finish doc

---

Member Function Documentation

template<class L , int F>

static LVBDD lava::LVBDD< L, F >::_mk_unsafe	(	int	index,
		V	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>

void lava::LVBDD< L, F >::evaluate	(	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:

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