sdd

Class SDDTreeDisjunction

java.lang.Object

buffer.CanonicalWatched

sdd.SDDTree

sdd.SDDTreeDisjunction

All Implemented Interfaces:

java.lang.Comparable<SDDTree>

public final class SDDTreeDisjunction
extends SDDTree

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.

Field Summary

Fields inherited from class sdd.SDDTree

CONSTANT_TYPE, DISJUNCTION_TYPE, LITERAL_TYPE

Method Summary

Methods

Modifier and Type	Method and Description
<X> X	apply(SDDFunction<X> f, Vtree tree, java.util.Map<SDDTree,X> m) Applies the specified function on this SDD tree.
static SDDTreeDisjunction	create(java.util.Set<SDDTreeConjunction> conjuncts)
void	destroy() Notifies this object that it is no longer referenced.
protected boolean	equivalent(java.lang.Object obj) Indicates whether the specified object is equivalent to this object.
java.util.List<Assignment>	getAssignmentList(Vtree tree) Returns the list of assignments of this SDD tree.
protected java.util.Map<java.lang.Object,SDDTreeDisjunction>	getBuffer() Returns the buffer that is used to decide the canonical objects.
SDDConstant	getConstant() Returns the constant associated with this SDD tree.
SDDTreeDisjunction	getDisjunction() Returns the disjunction associated with this SDD tree.
java.util.Collection<SDDTreeConjunction>	getDisjuncts() Returns an iterable on the SDDTreeDisjunct of this disjunction.
SDDVariable	getLiteral() Returns the literal associated with this SDD tree.
Assignment	getOneAssignment(Vtree tree) Returns one assignment for this SDDTree defined on the specified vtree.
int	hashCode()
void	insertSubSDDTrees(java.util.Set<CanonicalWatched> set) Adds all the sub SDD trees (including this one) of this SDD tree to the specified set.
boolean	isConstant() Indicates whether this SDD tree is a constant.
boolean	isDisjunction() Indicates whether this SDD tree is a disjunction.
boolean	isFalse() Indicates whether this SDD tree is the false constant.
boolean	isLiteral() Indicates whether this SDD tree is a literal.
int	nbDisjuncts() Returns the number of disjuncts of this disjunction.
java.math.BigInteger	nbModels(Vtree tree, java.util.Map<SDDTreeDisjunction,java.math.BigInteger> records) Returns the number of models of this SDD tree.
static void	printBuffer(java.io.PrintStream out) Prints in the specified print stream the current state of the buffer for SDDTreeDisjunction.
void	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.
int	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.
java.lang.String	toString()

Methods inherited from class sdd.SDDTree

compareTo, DEBUG_VERIFY_VTREE, isNot, isTrue

Methods inherited from class buffer.CanonicalWatched

equals, getCanonical, print, unwatch, unwatchAll, verifyValidity, watch

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Method Detail

create

public static SDDTreeDisjunction create(java.util.Set<SDDTreeConjunction> conjuncts)

hashCode

public int hashCode()

Specified by:

hashCode in class CanonicalWatched

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

equivalent

protected boolean equivalent(java.lang.Object obj)

Description copied from class: CanonicalWatched

Indicates whether the specified object is equivalent to this object. There should not be two equivalent objects, so this method is used at the creation of this type of object to verify whether the object create is truly original.

Specified by:

equivalent in class CanonicalWatched

Parameters:

obj - the object compared to this object.

Returns:

true if obj is equivalent to this.

destroy

public void destroy()

Description copied from class: CanonicalWatched

Notifies this object that it is no longer referenced. The object may have some cleaning up to do at this stage. The default implementation is that the object does nothing.

Overrides:

destroy in class CanonicalWatched

getBuffer

protected java.util.Map<java.lang.Object,SDDTreeDisjunction> getBuffer()

Description copied from class: CanonicalWatched

Returns the buffer that is used to decide the canonical objects.

Specified by:

getBuffer in class CanonicalWatched

Returns:

a map that contains the canonical objects.

getDisjuncts

public java.util.Collection<SDDTreeConjunction> getDisjuncts()

Returns an iterable on the SDDTreeDisjunct of this disjunction.

Returns:

an object that allows to recursively look at how this disjunction is defined.

isConstant

public boolean isConstant()

Description copied from class: SDDTree

Indicates whether this SDD tree is a constant.

Specified by:

isConstant in class SDDTree

Returns:

true if this instanceof SDDConstant, false otherwise.

isFalse

public boolean isFalse()

Description copied from class: SDDTree

Indicates whether this SDD tree is the false constant.

Specified by:

isFalse in class SDDTree

Returns:

true if this corresponds to the constant false.

getConstant

public SDDConstant getConstant()

Description copied from class: SDDTree

Returns the constant associated with this SDD tree. This method assumes that this SDD tree is a constant.

Specified by:

getConstant in class SDDTree

Returns:

this SDD tree as a constant.

See Also:

SDDTree.isConstant()

isLiteral

public boolean isLiteral()

Description copied from class: SDDTree

Indicates whether this SDD tree is a literal.

Specified by:

isLiteral in class SDDTree

Returns:

true if this instanceof SDDVariable, false otherwise.

getLiteral

public SDDVariable getLiteral()

Description copied from class: SDDTree

Returns the literal associated with this SDD tree. This method assumes that this SDD tree is a literal.

Specified by:

getLiteral in class SDDTree

Returns:

this SDD tree as a literal.

See Also:

SDDTree.isLiteral()

isDisjunction

public boolean isDisjunction()

Description copied from class: SDDTree

Indicates whether this SDD tree is a disjunction.

Specified by:

isDisjunction in class SDDTree

Returns:

true if this instanceof SDDTreeDisjunction, false otherwise.

getDisjunction

public SDDTreeDisjunction getDisjunction()

Description copied from class: SDDTree

Returns the disjunction associated with this SDD tree. This method assumes that this SDD tree is a disjunction.

Specified by:

getDisjunction in class SDDTree

Returns:

this SDD tree as a disjunction.

See Also:

SDDTree.isDisjunction()

saveToString

public int saveToString(java.lang.StringBuilder bui,
               java.util.Map<SDDTree,java.lang.String> sddTrees,
               java.util.Map<SDDTreeConjunction,java.lang.String> conjs,
               int counter)

Description copied from class: SDDTree

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.

Specified by:

saveToString in class SDDTree

Parameters:

bui - the string building where this SDD tree must be written.

sddTrees - the names of the SDD Trees.

conjs - the names of the SDD tree conjunctions.

counter - the number of names already created.

Returns:

an updated number of names.

saveToDot

public void saveToDot(DotStream out,
             java.util.Map<SDDTree,java.lang.String> sddTrees,
             java.util.Map<SDDTreeConjunction,java.lang.String> conjs,
             NameGenerator gen)

Description copied from class: SDDTree

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.

Specified by:

saveToDot in class SDDTree

Parameters:

out - the dot stream where this SDD tree must be written.

sddTrees - the names of the SDD Trees.

conjs - the names of the SDD tree conjunctions.

gen - the name generator (to generate dot node names).

getAssignmentList

public java.util.List<Assignment> getAssignmentList(Vtree tree)

Description copied from class: SDDTree

Returns the list of assignments of this SDD tree.

Specified by:

getAssignmentList in class SDDTree

Parameters:

tree - the vtree upon which this SDD tree is defined.

Returns:

the list of assignments that satisfy this SDD tree.

getOneAssignment

public Assignment getOneAssignment(Vtree tree)

Description copied from class: SDDTree

Returns one assignment for this SDDTree defined on the specified vtree.

Specified by:

getOneAssignment in class SDDTree

Parameters:

tree - the vtree upon which this SDD tree is defined.

Returns:

an assignment that satisfies this SDD tree if existing, null otherwise.

nbDisjuncts

public int nbDisjuncts()

Returns the number of disjuncts of this disjunction.

Returns:

how many disjuncts this disjunction relies on.

printBuffer

public static void printBuffer(java.io.PrintStream out)

Prints in the specified print stream the current state of the buffer for SDDTreeDisjunction.

Parameters:

out - the print stream.

See Also:

CanonicalWatched.print(java.io.PrintStream)

insertSubSDDTrees

public void insertSubSDDTrees(java.util.Set<CanonicalWatched> set)

Description copied from class: SDDTree

Adds all the sub SDD trees (including this one) of this SDD tree to the specified set. The input is a set of canonical watched object because we expect SDDTreeDisjunction, SDDTreeConjunction, SDDVariable, and SDDConstant objects.

Specified by:

insertSubSDDTrees in class SDDTree

Parameters:

set - the set where the sub SDD trees of this SDD tree are to be added.

nbModels

public java.math.BigInteger nbModels(Vtree tree,
                            java.util.Map<SDDTreeDisjunction,java.math.BigInteger> records)

Description copied from class: SDDTree

Returns the number of models of this SDD tree.

Specified by:

nbModels in class SDDTree

Parameters:

tree - the vtree upon which this SDDTree is defined.

records - a map that records the results already computed.

Returns:

the number of elements in SDDTree.getAssignmentList(sdd.Vtree).

apply

public <X> X apply(SDDFunction<X> f,
          Vtree tree,
          java.util.Map<SDDTree,X> m)

Description copied from class: SDDTree

Applies the specified function on this SDD tree.

Specified by:

apply in class SDDTree

Type Parameters:

X - the type of object returned by the function.

Parameters:

f - the function to apply.

tree - the tree on which this SDD tree is defined.

m - a map that stores the results.

Returns:

the result of the function.