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.

Each node of the diagram represents a single boolean entry with variable value and part of a Boolean function. T is the type with which a variable is represented. In the context of a formula, variables for which the compareTo method returns 0 indicate the same Boolean variable.

Each BDD node has a directed edge to two sub-BDDs: the "high" BDD that leads to a true Terminal, and the "low" BDD that leads to a false Terminal.

Author

Jason Dellaluce

Types

Companion

object Companion

Terminal

interface Terminal<T : Comparable<T>> : BinaryDecisionDiagram<T>

A Terminal is a BDD mode that has no edges to other BDDs, and represent a non-variable known Boolean value (either True or False)

Variable

interface Variable<T : Comparable<T>> : BinaryDecisionDiagram<T>

A Variable is a BDD node representing a Boolean variable.

Functions

abstract fun <E> accept(visitor: BinaryDecisionDiagramVisitor<T, E>): E

Accepts an instance of BinaryDecisionDiagramVisitor as for the visitor pattern.

Properties

isTerminal

abstract val isTerminal: Boolean

Returns true if this node is a Terminal node.

isVariable

abstract val isVariable: Boolean

Returns true if this node is a Variable node.

Inheritors

BinaryDecisionDiagram

Extensions

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(predicate: (T) -> Boolean): Boolean

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

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

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

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.

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/).