Package it.unibo.tuprolog.bdd

Types

interface BinaryDecisionDiagram<T : Comparable<T>>

A Binary Decision Diagram (BDD) is a rooted, directed, acyclic graph, which consists of several decision nodes and terminal nodes and uses the concept of Shannon Expansion to represent and encode complex Boolean Formulas.

BinaryDecisionDiagramBuilder

interface BinaryDecisionDiagramBuilder<T : Comparable<T>>

This interfaces hides the strategy with which instances of BinaryDecisionDiagram are created. Platform-specific optimized representations of BDDs can be introduced by providing new implementations of this interface.

BinaryDecisionDiagramVisitor

interface BinaryDecisionDiagramVisitor<T : Comparable<T>, E>

Implements the Visitor pattern over a BinaryDecisionDiagram to its hierarchy, which only includes instances of BinaryDecisionDiagram.Terminal and BinaryDecisionDiagram.Variable. This abstraction is the method of choice to explore the internal structure of a BDD.

Functions

and

infix fun <T : Comparable<T>> BinaryDecisionDiagram<T>.and(that: BinaryDecisionDiagram<T>): BinaryDecisionDiagram<T>

Performs the "And" unary boolean operation over two BinaryDecisionDiagrams. The result is a Reduced Ordered Binary Decision Diagram (ROBDD).

andThenExpansion

fun <T : Comparable<T>, E> BinaryDecisionDiagram<T>.andThenExpansion( that: BinaryDecisionDiagram<T>, expansionFalseTerminal: E, expansionTrueTerminal: E, expansionOperator: (node: T, low: E, high: E) -> E): Pair<BinaryDecisionDiagram<T>, E>

Performs the "And" unary boolean operation over two BinaryDecisionDiagrams and computes a value using the Shannon Expansion over the result. The result is an instance of Pair of which Pair.first is the Reduced Ordered Binary Decision Diagram (ROBDD) produced by the operation, and Pair.second is the value of type T computed with the Shannon Expansion.

any

fun <T : Comparable<T>> BinaryDecisionDiagram<T>.any(): Boolean

Returns true if the BinaryDecisionDiagram has at least one variable element.

fun <T : Comparable<T>> BinaryDecisionDiagram<T>.any(predicate: (T) -> Boolean): Boolean

Returns true if the BinaryDecisionDiagram has at least one variable element matching the given predicate.

apply

fun <T : Comparable<T>> BinaryDecisionDiagram<T>.apply(unaryOp: (Boolean) -> Boolean): BinaryDecisionDiagram<T>

Applies the "Apply" construction algorithm over BinaryDecisionDiagrams using a given boolean operator. The result is a Reduced Ordered Binary Decision Diagram (ROBDD).

fun <T : Comparable<T>> BinaryDecisionDiagram<T>.apply(that: BinaryDecisionDiagram<T>, binaryOp: (Boolean, Boolean) -> Boolean): BinaryDecisionDiagram<T>

Applies the "Apply" construction algorithm over two BinaryDecisionDiagrams using a given boolean operator. The result is a Reduced Ordered Binary Decision Diagram (ROBDD).

applyThenExpansion

fun <T : Comparable<T>, E> BinaryDecisionDiagram<T>.applyThenExpansion( unaryOp: (Boolean) -> Boolean, expansionFalseTerminal: E, expansionTrueTerminal: E, expansionOperator: (node: T, low: E, high: E) -> E): Pair<BinaryDecisionDiagram<T>, E>

Applies the "Apply" construction algorithm over BinaryDecisionDiagrams using a given boolean operator, and computes a value using the Shannon Expansion over the result. The result is an instance of Pair of which Pair.first is the Reduced Ordered Binary Decision Diagram (ROBDD) produced by the operation, and Pair.second is the value of type T computed with the Shannon Expansion.

fun <T : Comparable<T>, E> BinaryDecisionDiagram<T>.applyThenExpansion( that: BinaryDecisionDiagram<T>, binaryOp: (Boolean, Boolean) -> Boolean, expansionFalseTerminal: E, expansionTrueTerminal: E, expansionOperator: (node: T, low: E, high: E) -> E): Pair<BinaryDecisionDiagram<T>, E>

Applies the "Apply" construction algorithm over two BinaryDecisionDiagrams using a given boolean operator, and computes a value using the Shannon Expansion over the result. The result is an instance of Pair of which Pair.first is the Reduced Ordered Binary Decision Diagram (ROBDD) produced by the operation, and Pair.second is the value of type T computed with the Shannon Expansion.

bddOf

fun <T : Comparable<T>> bddOf(value: T): BinaryDecisionDiagram<T>

Shortcut for the BinaryDecisionDiagram.variableOf method.

bddTerminalOf

fun <T : Comparable<T>> bddTerminalOf(value: Boolean): BinaryDecisionDiagram<T>

Shortcut for the BinaryDecisionDiagram.terminalOf method.

countVariableNodes

fun <T : Comparable<T>> BinaryDecisionDiagram<T>.countVariableNodes(): Int

Returns the number of variable nodes contained in a BinaryDecisionDiagram.

expansion

fun <T : Comparable<T>, E> BinaryDecisionDiagram<T>.expansion( falseTerminal: E, trueTerminal: E, operator: (node: T, low: E, high: E) -> E): E

Applies a given operation over a BinaryDecisionDiagram using the Shannon Expansion. The result is a reduction of a given diagram, determined by applying an operation recursively over a BDD with bottom-up order.

map

fun <T : Comparable<T>, E : Comparable<E>> BinaryDecisionDiagram<T>.map(mapper: (T) -> E): BinaryDecisionDiagram<E>

Returns a BinaryDecisionDiagram containing nodes of applying the given transform function to each element in the original BinaryDecisionDiagram. The internal structure of the diagram is maintained.

not

fun <T : Comparable<T>> BinaryDecisionDiagram<T>.not(): BinaryDecisionDiagram<T>

Performs the "Not" unary boolean operation over a BinaryDecisionDiagram. The result is a Reduced Ordered Binary Decision Diagram (ROBDD).

notThenExpansion

fun <T : Comparable<T>, E> BinaryDecisionDiagram<T>.notThenExpansion( expansionFalseTerminal: E, expansionTrueTerminal: E, expansionOperator: (node: T, low: E, high: E) -> E): Pair<BinaryDecisionDiagram<T>, E>

Performs the "Not" unary boolean operation over a BinaryDecisionDiagram and computes a value using the Shannon Expansion over the result. The result is an instance of Pair of which Pair.first is the Reduced Ordered Binary Decision Diagram (ROBDD) produced by the operation, and Pair.second is the value of type T computed with the Shannon Expansion.

infix fun <T : Comparable<T>> BinaryDecisionDiagram<T>.or(that: BinaryDecisionDiagram<T>): BinaryDecisionDiagram<T>

Performs the "Or" unary boolean operation over two BinaryDecisionDiagrams. The result is a Reduced Ordered Binary Decision Diagram (ROBDD).

orThenExpansion

fun <T : Comparable<T>, E> BinaryDecisionDiagram<T>.orThenExpansion( that: BinaryDecisionDiagram<T>, expansionFalseTerminal: E, expansionTrueTerminal: E, expansionOperator: (node: T, low: E, high: E) -> E): Pair<BinaryDecisionDiagram<T>, E>

Performs the "Or" unary boolean operation over two BinaryDecisionDiagrams and computes a value using the Shannon Expansion over the result. The result is an instance of Pair of which Pair.first is the Reduced Ordered Binary Decision Diagram (ROBDD) produced by the operation, and Pair.second is the value of type T computed with the Shannon Expansion.

toDotString

fun <T : Comparable<T>> BinaryDecisionDiagram<T>.toDotString(): String

Formats a BinaryDecisionDiagram using Graphviz DOT notation (https://graphviz.org/). This provides a fast and widely supported solution to visualize the contents of a BDD.