CONSTANT_TYPE, DISJUNCTION_TYPE, LITERAL_TYPE| 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.
|
compareTo, DEBUG_VERIFY_VTREE, isNot, isTruedestroy, equals, getCanonical, print, unwatch, unwatchAll, verifyValidity, watchpublic static SDDConstant getTrue()
public static SDDConstant getFalse()
public static SDDConstant get(boolean b)
b - the boolean constant whose SDD tree is requested.public int hashCode()
hashCode in class CanonicalWatchedprotected boolean equivalent(java.lang.Object obj)
CanonicalWatchedequivalent in class CanonicalWatchedobj - the object compared to this object.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)
SDDTreesaveToString in class SDDTreebui - 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.public void saveToDot(DotStream out, java.util.Map<SDDTree,java.lang.String> sddTrees, java.util.Map<SDDTreeConjunction,java.lang.String> conjs, NameGenerator gen)
SDDTreeprotected java.util.Map<java.lang.Object,SDDConstant> getBuffer()
CanonicalWatchedgetBuffer in class CanonicalWatchedpublic boolean isConstant()
SDDTreeisConstant in class SDDTreepublic boolean isFalse()
SDDTreepublic SDDConstant getConstant()
SDDTreegetConstant in class SDDTreeSDDTree.isConstant()public boolean isLiteral()
SDDTreepublic SDDVariable getLiteral()
SDDTreegetLiteral in class SDDTreeSDDTree.isLiteral()public boolean isDisjunction()
SDDTreeisDisjunction in class SDDTreepublic SDDTreeDisjunction getDisjunction()
SDDTreegetDisjunction in class SDDTreeSDDTree.isDisjunction()public java.util.List<Assignment> getAssignmentList(Vtree tree)
SDDTreegetAssignmentList in class SDDTreetree - the vtree upon which this SDD tree is defined.public Assignment getOneAssignment(Vtree tree)
SDDTreegetOneAssignment in class SDDTreetree - the vtree upon which this SDD tree is defined.public static void printBuffer(java.io.PrintStream out)
out - the print stream.CanonicalWatched.print(java.io.PrintStream)public void insertSubSDDTrees(java.util.Set<CanonicalWatched> set)
SDDTreeinsertSubSDDTrees in class SDDTreeset - the set where the sub SDD trees of this SDD tree are to be added.public java.math.BigInteger nbModels(Vtree tree, java.util.Map<SDDTreeDisjunction,java.math.BigInteger> records)
SDDTreenbModels in class SDDTreetree - the vtree upon which this SDDTree is defined.records - a map that records the results already computed.SDDTree.getAssignmentList(sdd.Vtree).public <X> X apply(SDDFunction<X> f, Vtree tree, java.util.Map<SDDTree,X> m)
SDDTree