Package it.unibo.tuprolog.bdd

Types

BinaryDecisionDiagram

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.

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.

Functions

and

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

Performs the "And" unary boolean operation over two BinaryDecisionDiagrams.

andThenExpansion

fun <T : Comparable<T>, E> BinaryDecisionDiagram<T>.andThenExpansion(that: BinaryDecisionDiagram<T>, expansionFalseTerminal: E, expansionTrueTerminal: E, expansionOperator: (T, E, 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.

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.

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.

applyThenExpansion

fun <T : Comparable<T>, E> BinaryDecisionDiagram<T>.applyThenExpansion(unaryOp: (Boolean) -> Boolean, expansionFalseTerminal: E, expansionTrueTerminal: E, expansionOperator: (T, E, 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.

fun <T : Comparable<T>, E> BinaryDecisionDiagram<T>.applyThenExpansion(that: BinaryDecisionDiagram<T>, binaryOp: (Boolean, Boolean) -> Boolean, expansionFalseTerminal: E, expansionTrueTerminal: E, expansionOperator: (T, E, 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.

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: (T, E, E) -> E): E

Applies a given operation over a BinaryDecisionDiagram using the Shannon Expansion.

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.

not

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

Performs the "Not" unary boolean operation over a BinaryDecisionDiagram.

notThenExpansion

fun <T : Comparable<T>, E> BinaryDecisionDiagram<T>.notThenExpansion(expansionFalseTerminal: E, expansionTrueTerminal: E, expansionOperator: (T, E, 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.

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

Performs the "Or" unary boolean operation over two BinaryDecisionDiagrams.

orThenExpansion

fun <T : Comparable<T>, E> BinaryDecisionDiagram<T>.orThenExpansion(that: BinaryDecisionDiagram<T>, expansionFalseTerminal: E, expansionTrueTerminal: E, expansionOperator: (T, E, 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.

toDotString

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

Formats a BinaryDecisionDiagram using Graphviz DOT notation (https://graphviz.org/).