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.
|
|
V | exists () const |
| | Quantifies all decision variables existentially.
|
|
void | forall (V &result) const |
| | Quantifies all decision variables universally.
|
|
V | 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.
|
|
V | 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.
|
| V | 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.
|
