sdd

Class SDDTreeConjunction

java.lang.Object

buffer.CanonicalWatched

sdd.SDDTreeConjunction

All Implemented Interfaces:

java.lang.Comparable<SDDTreeConjunction>

public final class SDDTreeConjunction
extends CanonicalWatched
implements java.lang.Comparable<SDDTreeConjunction>

A SDDTreeConjunction, i.e., an SDD Tree Conjunction, aka a decomposition element, is a pair of SDDs defined as a conjunction and that are defined on two different (non overlapping) sets of variables. These sets of variables are chosen according to a Vtree that is implicit at the creation of the element.

The first SDD of the decomposition element is called the prime and cannot be SDDConstant.getFalse(); the second one is the sub. Decomposition elements are generally gathered around an SDD Tree Disjunction that has the following properties:

• the logical disjunction of all the primes in the disjunction evaluates to true;
• the logical conjunction of any pair of primes in the disjunction evaluates to false.

Consequently, each element can also be seen as an implication: if the prime is true, then the sub should be true.

Method Summary

Methods

Modifier and Type	Method and Description
int	compareTo(SDDTreeConjunction t)
static SDDTreeConjunction	create(SDDTree prime, SDDTree sub) Creates the SDD tree conjunction corresponding to the specified primes and subs.
protected 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.
protected java.util.Map<java.lang.Object,SDDTreeConjunction>	getBuffer() Returns the buffer that is used to decide the canonical objects.
SDDTree	getPrime() Returns the prime of this conjunction.
SDDTree	getSub() Returns the sub of this conjunction.
int	hashCode()
static void	printBuffer(java.io.PrintStream out) Prints in the specified print stream the current state of the buffer for SDDConstant.
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 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	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.
java.lang.String	toString()

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 SDDTreeConjunction create(SDDTree prime,
                        SDDTree sub)

Creates the SDD tree conjunction corresponding to the specified primes and subs. In other word, the resulting structure represents the conjunction of prime and sub.

Parameters:

prime - the prime of the conjunction.

sub - the sub of the conjunction.

Returns:

the conjunction prime AND sub.

hashCode

public int hashCode()

Specified by:

hashCode in class CanonicalWatched

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.

getBuffer

protected java.util.Map<java.lang.Object,SDDTreeConjunction> 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.

destroy

protected 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

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

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)

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.

Parameters:

bui - the string building where this tree conjunction 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)

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.

Parameters:

out - the dot stream where this tree conjunction 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).

getPrime

public SDDTree getPrime()

Returns the prime of this conjunction.

Returns:

the prime of this conjunction.

getSub

public SDDTree getSub()

Returns the sub of this conjunction.

Returns:

the sub of this conjunction.

printBuffer

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

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

Parameters:

out - the print stream.

See Also:

CanonicalWatched.print(java.io.PrintStream)

compareTo

public int compareTo(SDDTreeConjunction t)

Specified by:

compareTo in interface java.lang.Comparable<SDDTreeConjunction>