de.upb.swt.mcie.robdds
Class InnerNode

java.lang.Object
  extended by de.upb.swt.mcie.robdds.ROBDD
      extended by de.upb.swt.mcie.robdds.InnerNode

 class InnerNode
extends ROBDD

Represents the inner nodes of an ROBDD. An inner node is represented by a reference to the corresponding variable and its two successor nodes low and high.

Author:
Ekkart Kindler, kindler@upb.de

Field Summary
(package private)  ROBDD high
          Outgoing arc for value 1.
(package private)  ROBDD low
          Outgoing arc for value 0.
private  InnerNode negation
          If defined, this attribute refers to the complement of this ROBDD.
(package private)  Variable variable
          The variable associated with this inner node.
 
Fields inherited from class de.upb.swt.mcie.robdds.ROBDD
context
 
Constructor Summary
InnerNode(Variable variable, ROBDD low, ROBDD high)
          Creates a new inner node.
 
Method Summary
 boolean equals(java.lang.Object o)
          Checks whether this inner node is equal to an other node.
 ROBDD eval(Assignment ass)
          Evaluates the ROBDD in the given assignment, where the result is the ROBDD node at which the evaluation terminates.
 Assignment getAssignment()
          Returns an assignment for which the ROBDD evaluates to true.
 int hashCode()
          Returns the hash code of this inner node.
 boolean isValid()
          Returns true, if the ROBDD is valid (i.e. if it evaluates to true for any assignment).
 ROBDD negate()
          Returns the negation of this ROBDD.
private  ROBDD predecessors(InnerNode n)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD predecessors(InnerNode n, ChangeSet changeset)
          Returns the ROBBD with all the predecessors of a set n.
 ROBDD predecessors(ROBDD n)
          Returns the ROBBD with all the predecessors of a set n.
 ROBDD predecessors(ROBDD n, ChangeSet changeset)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD predecessors(TerminalNode n)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD predecessors(TerminalNode n, ChangeSet changeset)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD relProd(InnerNode n)
          Computes the product of two relations.
 ROBDD relProd(ROBDD n)
          Computes the product of two relations.
private  ROBDD relProd(TerminalNode n)
          Computes the product of two relations.
private  ROBDD successors(InnerNode n)
          Returns the ROBBD with all the successors of a set n.
private  ROBDD successors(InnerNode n, ChangeSet changeset)
          Returns the ROBBD with all the successors of a set n.
 ROBDD successors(ROBDD n)
          Returns the ROBBD with all the successors of a set n.
 ROBDD successors(ROBDD n, ChangeSet changeset)
          Considers this ROBBD as a transition relation and computes the successors of a given set.
private  ROBDD successors(TerminalNode n)
          Returns the ROBBD with all the successors of a set n.
private  ROBDD successors(TerminalNode n, ChangeSet changeset)
          Returns the ROBBD with all the successors of a set n.
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

variable

Variable variable
The variable associated with this inner node.


low

ROBDD low
Outgoing arc for value 0.


high

ROBDD high
Outgoing arc for value 1.


negation

private InnerNode negation
If defined, this attribute refers to the complement of this ROBDD.

Constructor Detail

InnerNode

InnerNode(Variable variable,
          ROBDD low,
          ROBDD high)
Creates a new inner node. In order to avoid creation of duplicate inner nodes (same variable and same successors for low and high), inner nodes can only be created from within this package. The method for this purpose is Context.createInnerNode(Variable,ROBDD,ROBDD). This method also maintains a hash table for all inner nodes.

Parameters:
variable - the variable associated with this inner node
low - outgoing arc for value 0
high - outgoing arc for value 1
Throws:
IncorrectUseException - if context of the variables and successor nodes do not coincide
Method Detail

negate

public ROBDD negate()
Returns the negation of this ROBDD. For efficiency reasons, this method maintains an attribute negate. When defined, this attribute refers to the negated ROBDD.

Specified by:
negate in class ROBDD
Returns:
the negated ROBDD

predecessors

public ROBDD predecessors(ROBDD n)
Returns the ROBBD with all the predecessors of a set n. This class itself plays the role of the transition relation. An invocation with an ROBDD from a different context results in an exception. This method only dispatches the call to more specific private methods.

Specified by:
predecessors in class ROBDD
Parameters:
n - the ROBDD representing the set for which the predecessors should be computed; this ROBDD must not refer to primed variables
Returns:
the set of predecessors represented as an ROBDD
Throws:
IncorrectUseException - if the set n contains a primed variable
InternalError - can occur only, if somebody messed up the implementation of the ROBDD package
See Also:
ROBDD.predecessors(ROBDD), predecessors(InnerNode), predecessors(TerminalNode)

predecessors

private ROBDD predecessors(InnerNode n)
Returns the ROBBD with all the predecessors of a set n. This class itself plays the role of the transition relation. This method implements the case where the set is represented by an inner node.

Parameters:
n - the ROBDD representing the set for which the predecessors should be computed; this ROBDD must not refer to primed variables
Returns:
the set of predecessors represented as an ROBDD
Throws:
IncorrectUseException - if the set n contains a primed variable
InternalError - can occur only, if somebody messed up the implementation of the ROBDD package
See Also:
ROBDD.predecessors(ROBDD)

predecessors

private ROBDD predecessors(TerminalNode n)
Returns the ROBBD with all the predecessors of a set n. This class itself plays the role of the transition relation. This method implements the case where the set is represented by a terminal node.

Parameters:
n - the ROBDD representing the set for which the predecessors should be computed
Returns:
the set of predecessors represented as ROBDD
See Also:
ROBDD.predecessors(ROBDD)

predecessors

public ROBDD predecessors(ROBDD n,
                          ChangeSet changeset)
Returns the ROBBD with all the predecessors of a set n. This class itself plays the role of the transition relation, where only the variables from changeset change. An invocation with an ROBDD from a different context results in an exception. If the transition relation contains a primed variable that is not in the changeset, an exception will be thrown. This method only dispatches the call to more specific private methods.

Specified by:
predecessors in class ROBDD
Parameters:
n - the ROBDD representing the set for which the predecessors should be computed
changeset - the set of variables that can change
Returns:
the set of predecessors represented as an ROBDD
Throws:
IncorrectUseException - if the set n contains a primed variable or the transition relation contains a primed variable that is not in the changeset
InternalError - can occur only, if somebody messed up the implementation of the ROBDD package
See Also:
ROBDD.predecessors(ROBDD, ChangeSet), predecessors(InnerNode, ChangeSet), predecessors(TerminalNode, ChangeSet)

predecessors

private ROBDD predecessors(InnerNode n,
                           ChangeSet changeset)
Returns the ROBBD with all the predecessors of a set n. This class itself plays the role of the transition relation, where only the variables from changeset change. An invocation with an ROBDD from a different context results in an exception. If the transition relation contains a primed variable that is not in the changeset, an exception will be thrown. This method implements the case where the set is represented by an inner node.

Parameters:
n - the ROBDD representing the set for which the predecessors should be computed
changeset - the set of variables that can change
Returns:
the set of predecessors represented as an ROBDD
Throws:
IncorrectUseException - if the set n contains a primed variable or the transition relation contains a primed variable that is not in the changeset
See Also:
ROBDD.predecessors(ROBDD, ChangeSet)

predecessors

private ROBDD predecessors(TerminalNode n,
                           ChangeSet changeset)
Returns the ROBBD with all the predecessors of a set n. This class itself plays the role of the transition relation, where only the variables from changeset change. An invocation with an ROBDD from a different context results in an exception. If the transition relation contains a primed variable that is not in the changeset, an exception will be thrown. This method implements the case where the set is represented by a terminal node.

Parameters:
n - the ROBDD representing the set for which the predecessors should be computed
changeset - the set of variables that can change
Returns:
the set of predecessors represented as an ROBDD
Throws:
IncorrectUseException - if the transition relation contains a primed variable that is not in the changeset
See Also:
ROBDD.predecessors(ROBDD, ChangeSet)

successors

public ROBDD successors(ROBDD n)
Returns the ROBBD with all the successors of a set n. This class itself plays the role of the transition relation. An invocation with an ROBDD from a different context results in an exception. This method only dispatches the call to more specific private methods.

Specified by:
successors in class ROBDD
Parameters:
n - the set, this ROBDD must not refer to primed variables
Returns:
the successors
Throws:
IncorrectUseException - if the set n contains a primed variable
InternalError - if somebody messed up the implementation of this package
See Also:
ROBDD.successors(ROBDD), successors(InnerNode), successors(TerminalNode)

successors

private ROBDD successors(InnerNode n)
Returns the ROBBD with all the successors of a set n. This class itself plays the role of the transition relation. This method implements the case where the set is represented by an inner node.

Parameters:
n - the set, this ROBDD must not refer to primed variables
Returns:
the successors
Throws:
IncorrectUseException - if the set n contains a primed variable
See Also:
ROBDD.successors(ROBDD)

successors

private ROBDD successors(TerminalNode n)
Returns the ROBBD with all the successors of a set n. This class itself plays the role of the transition relation. This method implements the case where the set is represented by a terminal node.

Parameters:
n - the set
Returns:
the successors
See Also:
ROBDD.successors(ROBDD)

successors

public ROBDD successors(ROBDD n,
                        ChangeSet changeset)
Considers this ROBBD as a transition relation and computes the successors of a given set. Only the variables in the set changeable can be changed by the transition relation.

Specified by:
successors in class ROBDD
Parameters:
n - the set, this ROBDD must not refer to primed variables
changeset - variables that may change in the transition relation
Returns:
the set of successors of the set
Throws:
IncorrectUseException - if the set n contains a primed variable or the transition relation contains a primed variable that is not in the changeset
InternalError - if somebody messed up the implementation of this package
See Also:
ROBDD.successors(ROBDD, ChangeSet), successors(InnerNode, ChangeSet), successors(TerminalNode, ChangeSet)

successors

private ROBDD successors(InnerNode n,
                         ChangeSet changeset)
Returns the ROBBD with all the successors of a set n. This class itself plays the role of the transition relation. This method implements the case where the set is represented by an inner node.

Parameters:
n - the set, this ROBDD may not refer to primed variables
changeset - variables that may change in the transition relation
Returns:
the successors
Throws:
IncorrectUseException - if the set n contains a primed variable or the transition relation contains a primed variable that is not in the changeset
See Also:
ROBDD.successors(ROBDD, ChangeSet)

successors

private ROBDD successors(TerminalNode n,
                         ChangeSet changeset)
Returns the ROBBD with all the successors of a set n. This class itself plays the role of the transition relation. This method implements the case where the set is represented by a terminal node.

Parameters:
n - the set
changeset - variables that may change in the transition relation
Returns:
the successors
Throws:
IncorrectUseException - if the transition relation contains a primed variable that is not in the changeset
See Also:
ROBDD.successors(ROBDD, ChangeSet)

isValid

public boolean isValid()
Returns true, if the ROBDD is valid (i.e. if it evaluates to true for any assignment). This is false for every inner node!

Specified by:
isValid in class ROBDD
Returns:
false

getAssignment

public Assignment getAssignment()
Returns an assignment for which the ROBDD evaluates to true.

Specified by:
getAssignment in class ROBDD
Returns:
assignment that evaluates to true; null, if no such assignment exists

hashCode

public int hashCode()
Returns the hash code of this inner node. This method must be implemented in order to map identical inner nodes to the same hash value. This method will be used in the hash tables (see HashMap and WeakHashMap). Here, we use a simple minded calculation that tries not to compromise the randomness of the hash codes of its parts. Moreover, the calculation guarantees that a symmetric pair has a different hash code. But, there may be better ways to calculate the hash code.

Overrides:
hashCode in class java.lang.Object
Returns:
the hash code of this inner node

equals

public boolean equals(java.lang.Object o)
Checks whether this inner node is equal to an other node. This method must be implemented in order to guarantee proper operation of the hash tables (see HashMap and WeakHashMap).

Overrides:
equals in class java.lang.Object
Parameters:
o - object to be compared with
Returns:
true if the object is an identical inner node; false otherwise

relProd

public ROBDD relProd(ROBDD n)
Computes the product of two relations. This object is considered as the first relation, argument n is considered as the second relation. An invocation with an ROBDD from a different context results in an exception. This method dispatches the call to the more specific private methods only.

This method is not fully tested yet!

Specified by:
relProd in class ROBDD
Parameters:
n - the set second relation
Returns:
the product of the two relations

relProd

private ROBDD relProd(InnerNode n)
Computes the product of two relations. This object is considered as the first relation, argument n is considered as the second relation. This method implements the case, where the second argument is an inner node (i.e. it is neither the empty nor the fully connected relation).

This method is not fully tested yet!

Parameters:
n - the set second relation
Returns:
the product of the two relations

relProd

private ROBDD relProd(TerminalNode n)
Computes the product of two relations. This object is considered as the first relation, argument n is considered as the second relation. This method implements the case, where the second argument is a terminal node (i.e. it is either the full relation or the empty relation).

This method is not fully tested yet!

Parameters:
n - the set second relation
Returns:
the product of the two relations

eval

public ROBDD eval(Assignment ass)
Evaluates the ROBDD in the given assignment, where the result is the ROBDD node at which the evaluation terminates. If the evaluation is successful, it is the corresponding TerminalNode; if the evaluation is stuck due to an undefined value for some inner node, this node is returned. It is an error, if the assignment is from a different context.

Specified by:
eval in class ROBDD
Parameters:
ass - for which the ROBDD should be evaluated
Returns:
the final node
Throws:
IncorrectUseException - if the assignment and the ROBDD are from a different context