The LVBDD class template represents a Lattice-Valued Binary Decision Diagram. More...
#include <lavabdd.h>
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. |
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
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.
[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. |
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.
[in] | valuation | : The valuation. Proposition i is indexed at valuation[i-1]. |
[out] | result | : The resulting lattice value. |
static LVBDD lava::LVBDD< L, F >::literal | ( | int | index, | |
bool | positive | |||
) | [inline, static] |
Creates a three-node LVBDD representing a positive or negative literal.
[in] | index | : The proposition index of the literal. Must be strictly positive. |
[in] | positive | : The polarity of the literal (positive or negative). |