bdd/it.unibo.tuprolog.bdd/BinaryDecisionDiagram/Terminal

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)

Properties

isTerminal

open override val isTerminal: Boolean

Returns true if this node is a Terminal node.

isVariable

open override val isVariable: Boolean

Returns true if this node is a Variable node.

truth

abstract val truth: Boolean

Boolean value of the terminal

Functions

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

Accepts an instance of BinaryDecisionDiagramVisitor as for the visitor pattern. This is the method of preference for exploring the inner structure of the diagram, since it distinguishes between Terminal and Variable nodes without runtime type checks by the caller.

and

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

Performs the "And" binary boolean operation over two BinaryDecisionDiagrams. The result is a Reduced Ordered Binary Decision Diagram (ROBDD) representing the logical conjunction of the Boolean formulas encoded by the two diagrams.

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" binary 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 E 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, i.e. it is not just a Terminal.

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. Used e.g. by it.unibo.tuprolog.solve.problog.lib.knowledge.impl.BinaryDecisionDiagramExplanation.containsAnyNotGroundTerm as diagram.any { !it.isGround }, to detect explanations that still contain unbound Prolog terms.

apply

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

Applies the "Apply" construction algorithm over BinaryDecisionDiagrams using a given unary 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 binary 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 unary 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 E 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 binary 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 E computed with the Shannon Expansion.

countVariableNodes

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

Returns the number of Variable nodes contained in a BinaryDecisionDiagram. Note that, since a node can be shared by multiple parents (e.g. in a reduced diagram built by BinaryDecisionDiagramBuilder.reducedOf), a shared node is counted once for every path that reaches it, not once overall.

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: each Terminal is mapped to falseTerminal/trueTerminal, and each Variable is folded with operator, receiving the already-computed E values of its low/high sub-diagrams.

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. Used e.g. by it.unibo.tuprolog.solve.problog.lib.knowledge.impl.BinaryDecisionDiagramExplanation.apply to rewrite the Prolog terms held by every variable of an explanation (e.g. after applying a substitution), as diagram.map { transformation(it) }.

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) representing the logical negation of the Boolean formula encoded by this diagram.

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 E computed with the Shannon Expansion.

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

Performs the "Or" binary boolean operation over two BinaryDecisionDiagrams. The result is a Reduced Ordered Binary Decision Diagram (ROBDD) representing the logical disjunction of the Boolean formulas encoded by the two diagrams.

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" binary 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 E 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.