Package de.upb.swt.mcie.robdds

This package implements reduced ordered binary decision diagrams (ROBDDs).

See:
          Description

Interface Summary
Assignment This interface defines the basic methods of an assignment of values to some variables of a Context.
 

Class Summary
BinOp This class implements binary operations on ROBDDs.
ChangeSet This class represents a set of variables, which restrict the changed variables in a transition relation.
Context Implements the context for an ROBDD, which comprises the set of variables and the order on these variables.
HashAssignment This class implements an Assignment.
InnerNode Represents the inner nodes of an ROBDD.
NodePair This class represents a pair of nodes.
ROBDD This abstract class represents the nodes of an ROBDD.
TerminalNode This class represents a terminal Node of an ROBDD.
Variable Implements a variable within an ROBDD's context.
 

Exception Summary
IncorrectUseException Exception that results from an incorrect use of the API.
InternalError This exception indicates that some internal error has occurred.
 

Package de.upb.swt.mcie.robdds Description

This package implements reduced ordered binary decision diagrams (ROBDDs). It should demonstrate the implementation of ROBDDs for teaching purposes. So its main focus is not on efficiency, but on a clear structure and an API that allows a safe use. The principle techniques for gaining performance, however, are implemented. In the code, comments at some positions indicate how performance could be improved (by sacrificing clarity or safe use).

Still missing

Note that ROBBD could be represented even more efficiently, by exploiting the effect that the negated ROBDD is exactly the same except for exchanging the terminal nodes. The procedures, however, become a little bit more complicated. Therefore, this optimization is not built into this implementation of ROBDDs.