bdd/it.unibo.tuprolog.bdd/notThenExpansion

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.

By definition, invoking not and then expansion should produce the same result as calling this function directly.

Return

a Pair of the negated ROBDD and the Shannon-Expansion result.

Parameters

expansionFalseTerminal

the E value associated to a false Terminal.

expansionTrueTerminal

the E value associated to a true Terminal.

expansionOperator

combines a BinaryDecisionDiagram.Variable's value with the already computed E values of its low and high sub-diagrams.

Throws

it.unibo.tuprolog.bdd.exception.BinaryDecisionDiagramOperationException

if construction fails, e.g. because expansionOperator throws.