bdd/it.unibo.tuprolog.bdd/andThenExpansion

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.

By definition, invoking and and then expansion should produce the same result as calling this function directly. This is used e.g. by it.unibo.tuprolog.solve.problog.lib.knowledge.impl.BinaryDecisionDiagramExplanation.and to compute the probability of a conjunction of explanations in one pass.

Return

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

Parameters

that

the other diagram to combine this one with.

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.