| Package | Description |
|---|---|
| sdd | |
| sdd.ope | |
| sdd.opt |
| Modifier and Type | Class and Description |
|---|---|
class |
SDDConstant
An SDD Constant is an SDD Tree that represents a boolean constant,
i.e., either true or false.
|
class |
SDDTreeDisjunction
A
SDDTreeDisjunction, i.e., an SDD tree disjunction,
aka a decomposition, is a set of
disjunction elements,
where the primes of the elements form a partition of their respective variables
(their pair-wise conjunction logically evaluates to false,
their disjunction evaluates to true) and the subs are all different. |
class |
SDDVariable
An SDD Variable is an SDD Tree which depends only on the value of a variable.
|
| Modifier and Type | Method and Description |
|---|---|
SDDTree |
SDDMemory.and(SDDTreeDisjunction t1,
SDDTreeDisjunction t2)
Returns the result of the AND operation
between the two specified SDDTreeDisjunction
if this result is known, null otherwise.
|
static SDDTree |
SDDTrees.and(SDDTree tr1,
SDDTree tr2,
SDDMemory mem)
Computes the conjunction of the two specified SDD trees.
|
static SDDTree |
SDDTrees.ban_and(SDDTree tr1,
SDDTree tr2,
SDDMemory mem)
Computes the conjunction of the two specified SDD trees.
|
static SDDTree |
SDDTrees.ban_exists(SDDTree sdd,
Variable var,
SDDMemory mem,
VtreePath path)
Computes the result of the exists operation on the specified sdd
for the specified variable.
|
static SDDTree |
SDDTrees.ban_forall(SDDTree sdd,
Variable var,
SDDMemory mem,
VtreePath path)
Computes the result of the forall operation on the specified sdd
for the specified variable.
|
static SDDTree |
SDDTrees.ban_not(SDDTree sdd,
SDDMemory mem)
Computes the negation of the specified SDD tree.
|
static SDDTree |
SDDTrees.ban_or(SDDTree tr1,
SDDTree tr2,
SDDMemory mem)
Computes the disjunction of the two specified SDD trees.
|
static SDDTree |
SDDTrees.buildSimpleSDDNode(SDDTree prime,
SDDTree sub,
SDDMemory mem) |
SDDTree |
SDDMemory.exists(SDDTreeDisjunction t)
Returns the result of the EXISTS operation
on the specified SDDTreeDisjunction
if this result is known, null otherwise.
|
static SDDTree |
SDDTrees.exists(SDDTree sdd,
Variable var,
SDDMemory mem,
VtreePath path)
Computes the result of the exists operation on the specified sdd
for the specified variable.
|
SDDTree |
SDDMemory.forall(SDDTreeDisjunction t)
Returns the result of the FORALL operation
on the specified SDDTreeDisjunction
if this result is known, null otherwise.
|
static SDDTree |
SDDTrees.forall(SDDTree sdd,
Variable var,
SDDMemory mem,
VtreePath path)
Computes the result of the forall operation on the specified sdd
for the specified variable.
|
SDDTree |
SDDTreeDisjunctionConstructor.get()
Returns the result of this construction.
|
SDDTree |
SDDTreeConjunction.getPrime()
Returns the prime of this conjunction.
|
SDDTree |
SDD.getSDDTree()
Returns the SDDTree of this SDD.
|
SDDTree |
SDDTreeConjunction.getSub()
Returns the sub of this conjunction.
|
SDDTree |
SDDMemory.not(SDDTreeDisjunction t)
Returns the result of the NOT operation
on the specified SDDTreeDisjunction
if this result is known, null otherwise.
|
static SDDTree |
SDDTrees.not(SDDTree sdd,
SDDMemory mem)
Computes the negation of the specified SDD tree.
|
SDDTree |
SDDMemory.or(SDDTreeDisjunction t1,
SDDTreeDisjunction t2)
Returns the result of the OR operation
between the two specified SDDTreeDisjunction
if this result is known, null otherwise.
|
static SDDTree |
SDDTrees.or(SDDTree tr1,
SDDTree tr2,
SDDMemory mem)
Computes the disjunction of the two specified SDD trees.
|
SDDTree |
SDDMemory.tree(SDDTreeDisjunction t)
Returns the result of the tree-based operation
on the specified SDDTreeDisjunction
if this result is known, null otherwise.
|
| Modifier and Type | Method and Description |
|---|---|
void |
SDDTreeDisjunctionConstructor.add(SDDTree prime,
SDDTree sub)
Adds the specified disjunction element to the constructor.
|
void |
SDDMemory.addAnd(SDDTreeDisjunction c1,
SDDTreeDisjunction c2,
SDDTree c)
Stores the specified result of the conjunction of the two specified SDDTree.
|
void |
SDDMemory.addOr(SDDTreeDisjunction d1,
SDDTreeDisjunction d2,
SDDTree d)
Stores the specified result of the disjunction of the two specified SDDTree.
|
static SDDTree |
SDDTrees.and(SDDTree tr1,
SDDTree tr2,
SDDMemory mem)
Computes the conjunction of the two specified SDD trees.
|
static SDDTree |
SDDTrees.ban_and(SDDTree tr1,
SDDTree tr2,
SDDMemory mem)
Computes the conjunction of the two specified SDD trees.
|
static SDDTree |
SDDTrees.ban_exists(SDDTree sdd,
Variable var,
SDDMemory mem,
VtreePath path)
Computes the result of the exists operation on the specified sdd
for the specified variable.
|
static SDDTree |
SDDTrees.ban_forall(SDDTree sdd,
Variable var,
SDDMemory mem,
VtreePath path)
Computes the result of the forall operation on the specified sdd
for the specified variable.
|
static SDDTree |
SDDTrees.ban_not(SDDTree sdd,
SDDMemory mem)
Computes the negation of the specified SDD tree.
|
static SDDTree |
SDDTrees.ban_or(SDDTree tr1,
SDDTree tr2,
SDDMemory mem)
Computes the disjunction of the two specified SDD trees.
|
static SDDTree |
SDDTrees.buildSimpleSDDNode(SDDTree prime,
SDDTree sub,
SDDMemory mem) |
static int |
SDDTrees.compare(SDDTree t1,
SDDTree t2)
Gives a total order on the SDD tree.
|
int |
SDDTree.compareTo(SDDTree t) |
static SDDTreeConjunction |
SDDTreeConjunction.create(SDDTree prime,
SDDTree sub)
Creates the SDD tree conjunction
corresponding to the specified primes and subs.
|
static SDD |
SDD.create(SDDTree sdd,
Vtree tree)
Creates an SDD defined as the specified SDD tree on the specified vtree.
|
static void |
SDDTree.DEBUG_VERIFY_VTREE(Vtree tree,
SDDTree sdd) |
static SDDTree |
SDDTrees.exists(SDDTree sdd,
Variable var,
SDDMemory mem,
VtreePath path)
Computes the result of the exists operation on the specified sdd
for the specified variable.
|
static SDDTree |
SDDTrees.forall(SDDTree sdd,
Variable var,
SDDMemory mem,
VtreePath path)
Computes the result of the forall operation on the specified sdd
for the specified variable.
|
static SDDTree |
SDDTrees.not(SDDTree sdd,
SDDMemory mem)
Computes the negation of the specified SDD tree.
|
static SDDTree |
SDDTrees.or(SDDTree tr1,
SDDTree tr2,
SDDMemory mem)
Computes the disjunction of the two specified SDD trees.
|
| Modifier and Type | Method and Description |
|---|---|
<X> X |
SDDConstant.apply(SDDFunction<X> f,
Vtree tree,
java.util.Map<SDDTree,X> m) |
abstract <X> X |
SDDTree.apply(SDDFunction<X> f,
Vtree tree,
java.util.Map<SDDTree,X> m)
Applies the specified function on this SDD tree.
|
<X> X |
SDDTreeDisjunction.apply(SDDFunction<X> f,
Vtree tree,
java.util.Map<SDDTree,X> m) |
<X> X |
SDDVariable.apply(SDDFunction<X> f,
Vtree tree,
java.util.Map<SDDTree,X> m) |
void |
SDDConstant.saveToDot(DotStream out,
java.util.Map<SDDTree,java.lang.String> sddTrees,
java.util.Map<SDDTreeConjunction,java.lang.String> conjs,
NameGenerator gen) |
abstract void |
SDDTree.saveToDot(DotStream out,
java.util.Map<SDDTree,java.lang.String> sddTrees,
java.util.Map<SDDTreeConjunction,java.lang.String> conjs,
NameGenerator gen)
Prints a dot representation of this SDD tree in the specified string builder
given the specified names for SDDTrees and SDDTreeConjunction,
as well as a counter to create more names.
|
void |
SDDTreeConjunction.saveToDot(DotStream out,
java.util.Map<SDDTree,java.lang.String> sddTrees,
java.util.Map<SDDTreeConjunction,java.lang.String> conjs,
NameGenerator gen)
Prints a dot representation of this tree conjunction in the specified string builder
given the specified names for SDDTrees and SDDTreeConjunction,
as well as a counter to create more names.
|
void |
SDDTreeDisjunction.saveToDot(DotStream out,
java.util.Map<SDDTree,java.lang.String> sddTrees,
java.util.Map<SDDTreeConjunction,java.lang.String> conjs,
NameGenerator gen) |
void |
SDDVariable.saveToDot(DotStream out,
java.util.Map<SDDTree,java.lang.String> sddTrees,
java.util.Map<SDDTreeConjunction,java.lang.String> conjs,
NameGenerator gen) |
int |
SDDConstant.saveToString(java.lang.StringBuilder bui,
java.util.Map<SDDTree,java.lang.String> sddTrees,
java.util.Map<SDDTreeConjunction,java.lang.String> conjs,
int counter) |
abstract int |
SDDTree.saveToString(java.lang.StringBuilder bui,
java.util.Map<SDDTree,java.lang.String> sddTrees,
java.util.Map<SDDTreeConjunction,java.lang.String> conjs,
int counter)
Prints a string representation of this SDD tree in the specified string builder,
given the specified names for SDDTrees and SDDTreeConjunction,
as well as a counter to create more names.
|
int |
SDDTreeConjunction.saveToString(java.lang.StringBuilder bui,
java.util.Map<SDDTree,java.lang.String> sddTrees,
java.util.Map<SDDTreeConjunction,java.lang.String> conjs,
int counter)
Prints a string representation of this tree conjunction in the specified string builder,
given the specified names for SDDTrees and SDDTreeConjunction,
as well as a counter to create more names.
|
int |
SDDTreeDisjunction.saveToString(java.lang.StringBuilder bui,
java.util.Map<SDDTree,java.lang.String> sddTrees,
java.util.Map<SDDTreeConjunction,java.lang.String> conjs,
int counter) |
int |
SDDVariable.saveToString(java.lang.StringBuilder bui,
java.util.Map<SDDTree,java.lang.String> sddTrees,
java.util.Map<SDDTreeConjunction,java.lang.String> conjs,
int counter) |
| Modifier and Type | Method and Description |
|---|---|
SDDTree |
ChildrenOperation.applyToSDD(SDDTree sdd,
SDDMemory mem) |
SDDTree |
ConsecutiveOperations.applyToSDD(SDDTree sdd,
SDDMemory mem) |
SDDTree |
Identity.applyToSDD(SDDTree sdd,
SDDMemory mem) |
SDDTree |
LeftRotation.applyToSDD(SDDTree sdd,
SDDMemory mem) |
SDDTree |
RightRotation.applyToSDD(SDDTree sdd,
SDDMemory mem) |
SDDTree |
Swap.applyToSDD(SDDTree sdd,
SDDMemory mem) |
SDDTree |
VtreeOperation.applyToSDD(SDDTree sdd,
SDDMemory mem)
Computes the SDD tree (associated with the vtree on which this operation is applied)
that are equivalent to the specified SDD tree defined for the specified vtree.
|
static SDDTree |
LeftRotation.leftRotation(SDDTree sdd,
SDDMemory mem,
VtreePath path)
Applies the left rotation operation on the specified SDD tree
at the leaf of the specified path.
|
static SDDTree |
LeftRotation.leftRotationOnCurrentNode(SDDMemory mem,
SDDTreeDisjunction sdd)
Applies the left rotation operation on the specified SDD tree
at the current node.
|
static SDDTree |
RightRotation.rightRotation(SDDTree sdd,
SDDMemory mem,
VtreePath path)
Applies the right rotation operation on the specified SDD tree
at the leaf of the specified path.
|
static SDDTree |
RightRotation.rightRotationOnCurrentNode(SDDMemory mem,
SDDTreeDisjunction sdd)
Applies the right rotation operation on the specified SDD tree
at the current node.
|
static SDDTree |
RightRotation.rightRotationOnCurrentNode2(SDDMemory mem,
SDDTreeDisjunction sdd) |
static SDDTree |
Swap.swapVnodeOnCurrentNode(SDDMemory mem,
SDDTreeDisjunction sdd)
Applies the swap operation on the specified SDD tree
at the current node.
|
| Modifier and Type | Method and Description |
|---|---|
SDDTree |
ChildrenOperation.applyToSDD(SDDTree sdd,
SDDMemory mem) |
SDDTree |
ConsecutiveOperations.applyToSDD(SDDTree sdd,
SDDMemory mem) |
SDDTree |
Identity.applyToSDD(SDDTree sdd,
SDDMemory mem) |
SDDTree |
LeftRotation.applyToSDD(SDDTree sdd,
SDDMemory mem) |
SDDTree |
RightRotation.applyToSDD(SDDTree sdd,
SDDMemory mem) |
SDDTree |
Swap.applyToSDD(SDDTree sdd,
SDDMemory mem) |
SDDTree |
VtreeOperation.applyToSDD(SDDTree sdd,
SDDMemory mem)
Computes the SDD tree (associated with the vtree on which this operation is applied)
that are equivalent to the specified SDD tree defined for the specified vtree.
|
static SDDTree |
LeftRotation.leftRotation(SDDTree sdd,
SDDMemory mem,
VtreePath path)
Applies the left rotation operation on the specified SDD tree
at the leaf of the specified path.
|
static SDDTree |
RightRotation.rightRotation(SDDTree sdd,
SDDMemory mem,
VtreePath path)
Applies the right rotation operation on the specified SDD tree
at the leaf of the specified path.
|
| Modifier and Type | Field and Description |
|---|---|
java.util.Map<SDDTree,SDDTree> |
OptimisationReport._replacementMap
A map that indicates how each SDDTree has been replaced.
|
java.util.Map<SDDTree,SDDTree> |
OptimisationReport._replacementMap
A map that indicates how each SDDTree has been replaced.
|
| Modifier and Type | Method and Description |
|---|---|
java.util.Map<SDDTree,SDDTree> |
OptimisationReport.getNonNullMap() |
java.util.Map<SDDTree,SDDTree> |
OptimisationReport.getNonNullMap() |
java.util.Collection<SDDTree> |
ExplicitOptimisationProblem.getSDDs() |
java.util.Collection<SDDTree> |
OptimisationProblem.getSDDs() |
java.util.Collection<SDDTree> |
OptimisationReport.getSDDs()
Returns the collection of SDDTrees after this optimisation was performed.
|
| Modifier and Type | Method and Description |
|---|---|
static OptimisationReport |
OptimisationReport.optimisationChange(java.util.Map<SDDTree,SDDTree> replacementMap,
java.util.Set<CanonicalWatched> subnodes,
Vtree tree,
java.util.Collection<SDDTree> newSDDs) |
static OptimisationReport |
OptimisationReport.optimisationChange(java.util.Map<SDDTree,SDDTree> replacementMap,
java.util.Set<CanonicalWatched> subnodes,
Vtree tree,
java.util.Collection<SDDTree> newSDDs) |
static OptimisationReport |
OptimisationReport.optimisationChange(java.util.Map<SDDTree,SDDTree> replacementMap,
java.util.Set<CanonicalWatched> subnodes,
Vtree tree,
java.util.Collection<SDDTree> newSDDs) |
| Constructor and Description |
|---|
ExplicitOptimisationProblem(java.util.Collection<SDDTree> sdds,
Vtree tree)
Creates an optimisation problem
of the specified collection of SDD
defined on the specified vtree.
|