sdd

Class SDDConstant

java.lang.Object

buffer.CanonicalWatched

sdd.SDDTree

sdd.SDDConstant

All Implemented Interfaces:

java.lang.Comparable<SDDTree>

public final class SDDConstant
extends SDDTree

An SDD Constant is an SDD Tree that represents a boolean constant, i.e., either true or false.

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.
protected boolean	equivalent(java.lang.Object obj) Indicates whether the specified object is equivalent to this object.
static SDDConstant	get(boolean b) Returns the SDD tree corresponding to the specified boolean.
java.util.List<Assignment>	getAssignmentList(Vtree tree) Returns the list of assignments of this SDD tree.
protected java.util.Map<java.lang.Object,SDDConstant>	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.
static SDDConstant	getFalse() Returns the SDD tree corresponding to the constant false.
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.
static SDDConstant	getTrue() Returns the SDD tree corresponding to the constant true.
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.
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 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.

Methods inherited from class sdd.SDDTree

compareTo, DEBUG_VERIFY_VTREE, isNot, isTrue

Methods inherited from class buffer.CanonicalWatched

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

Methods inherited from class java.lang.Object

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

Method Detail

getTrue

public static SDDConstant getTrue()

Returns the SDD tree corresponding to the constant true.

Returns:

the true SDDConstant.

getFalse

public static SDDConstant getFalse()

Returns the SDD tree corresponding to the constant false.

Returns:

the false SDDConstant.

get

public static SDDConstant get(boolean b)

Returns the SDD tree corresponding to the specified boolean.

Parameters:

b - the boolean constant whose SDD tree is requested.

Returns:

the SDDConstant of b.

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

getBuffer

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

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.

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)

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.