sdd

Class SDDTree

java.lang.Object

buffer.CanonicalWatched

sdd.SDDTree

All Implemented Interfaces:

java.lang.Comparable<SDDTree>

Direct Known Subclasses:

SDDConstant, SDDTreeDisjunction, SDDVariable

public abstract class SDDTree
extends CanonicalWatched
implements java.lang.Comparable<SDDTree>

An SDD tree is a node of the SDD (but not the conjunction).

Field Summary

Fields

Modifier and Type	Field and Description
protected java.lang.String	CONSTANT_TYPE
protected java.lang.String	DISJUNCTION_TYPE
protected java.lang.String	LITERAL_TYPE

Constructor Summary

Constructors

Constructor and Description
SDDTree()

Method Summary

Methods

Modifier and Type	Method and Description
abstract <X> X	apply(SDDFunction<X> f, Vtree tree, java.util.Map<SDDTree,X> m) Applies the specified function on this SDD tree.
int	compareTo(SDDTree t)
static void	DEBUG_VERIFY_VTREE(Vtree tree, SDDTree sdd)
abstract java.util.List<Assignment>	getAssignmentList(Vtree tree) Returns the list of assignments of this SDD tree.
abstract SDDConstant	getConstant() Returns the constant associated with this SDD tree.
abstract SDDTreeDisjunction	getDisjunction() Returns the disjunction associated with this SDD tree.
abstract SDDVariable	getLiteral() Returns the literal associated with this SDD tree.
abstract Assignment	getOneAssignment(Vtree tree) Returns one assignment for this SDDTree defined on the specified vtree.
abstract void	insertSubSDDTrees(java.util.Set<CanonicalWatched> set) Adds all the sub SDD trees (including this one) of this SDD tree to the specified set.
abstract boolean	isConstant() Indicates whether this SDD tree is a constant.
abstract boolean	isDisjunction() Indicates whether this SDD tree is a disjunction.
abstract boolean	isFalse() Indicates whether this SDD tree is the false constant.
abstract boolean	isLiteral() Indicates whether this SDD tree is a literal.
protected void	isNot(java.lang.String type) Throws an error saying that this object is not of specified type.
boolean	isTrue() Indicates whether this SDD tree is the true constant.
abstract java.math.BigInteger	nbModels(Vtree tree, java.util.Map<SDDTreeDisjunction,java.math.BigInteger> records) Returns the number of models of this SDD tree.
abstract 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.
abstract 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 buffer.CanonicalWatched

destroy, equals, equivalent, getBuffer, getCanonical, hashCode, print, unwatch, unwatchAll, verifyValidity, watch

Methods inherited from class java.lang.Object

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

Field Detail

CONSTANT_TYPE

protected final java.lang.String CONSTANT_TYPE

See Also:

Constant Field Values

DISJUNCTION_TYPE

protected final java.lang.String DISJUNCTION_TYPE

See Also:

Constant Field Values

LITERAL_TYPE

protected final java.lang.String LITERAL_TYPE

See Also:

Constant Field Values

Constructor Detail

SDDTree

public SDDTree()

Method Detail

isConstant

public abstract boolean isConstant()

Indicates whether this SDD tree is a constant.

Returns:

true if this instanceof SDDConstant, false otherwise.

isFalse

public abstract boolean isFalse()

Indicates whether this SDD tree is the false constant.

Returns:

true if this corresponds to the constant false.

isTrue

public final boolean isTrue()

Indicates whether this SDD tree is the true constant.

Returns:

true if this corresponds to the constant true.

getConstant

public abstract SDDConstant getConstant()

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

Returns:

this SDD tree as a constant.

See Also:

isConstant()

isLiteral

public abstract boolean isLiteral()

Indicates whether this SDD tree is a literal.

Returns:

true if this instanceof SDDVariable, false otherwise.

getLiteral

public abstract SDDVariable getLiteral()

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

Returns:

this SDD tree as a literal.

See Also:

isLiteral()

isDisjunction

public abstract boolean isDisjunction()

Indicates whether this SDD tree is a disjunction.

Returns:

true if this instanceof SDDTreeDisjunction, false otherwise.

getDisjunction

public abstract SDDTreeDisjunction getDisjunction()

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

Returns:

this SDD tree as a disjunction.

See Also:

isDisjunction()

isNot

protected void isNot(java.lang.String type)

Throws an error saying that this object is not of specified type.

Parameters:

type - the type that this object is not.

getAssignmentList

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

Returns the list of assignments of this SDD tree.

Parameters:

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

Returns:

the list of assignments that satisfy this SDD tree.

getOneAssignment

public abstract Assignment getOneAssignment(Vtree tree)

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

Parameters:

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

Returns:

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

nbModels

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

Returns the number of models of this SDD tree.

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 getAssignmentList(sdd.Vtree).

insertSubSDDTrees

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

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.

Parameters:

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

saveToString

public abstract 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.

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

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

compareTo

public int compareTo(SDDTree t)

Specified by:

compareTo in interface java.lang.Comparable<SDDTree>

DEBUG_VERIFY_VTREE

public static void DEBUG_VERIFY_VTREE(Vtree tree,
                      SDDTree sdd)

apply

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

Applies the specified function on this SDD tree.

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.