sdd

Class SDDVariable

java.lang.Object

buffer.CanonicalWatched

sdd.SDDTree

sdd.SDDVariable

All Implemented Interfaces:

java.lang.Comparable<SDDTree>

public final class SDDVariable
extends SDDTree

An SDD Variable is an SDD Tree which depends only on the value of a variable. A more appropriate name may be SDDLiteral and it will possibly changed in the future.

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 SDDVariable	create(Variable var, boolean val)
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,SDDVariable>	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.
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.
boolean	getSign() Returns the sign of this literal.
Variable	getVariable() Returns the variable of this literal.
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.
java.math.BigInteger	nbModels(Vtree tree, java.util.Map<SDDTreeDisjunction,java.math.BigInteger> records) Returns the number of models of this SDD tree.
SDDVariable	not() Returns the negation of this literal.
static void	printBuffer(java.io.PrintStream out) Prints in the specified print stream the current state of the buffer for SDDVariable.
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 SDDVariable create(Variable var,
                 boolean val)

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.

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).

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,SDDVariable> 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.

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()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

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.

not

public SDDVariable not()

Returns the negation of this literal.

Returns:

the negation of this literal.

getVariable

public Variable getVariable()

Returns the variable of this literal.

Returns:

the variable upon which this literal is defined.

getSign

public boolean getSign()

Returns the sign of this literal.

Returns:

true if this literal corresponds to getVariable(), false if it corresponds to NOT getVariable().

printBuffer

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

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

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.