de.upb.swt.mcie.robdds
Class BinOp

java.lang.Object
  extended by de.upb.swt.mcie.robdds.BinOp

public class BinOp
extends java.lang.Object

This class implements binary operations on ROBDDs. A binary operation is defined by a truth table, which is a two dimensional boolean array passed to the constructor. Each binary operation belongs to a Context and has its own hash table for pairs of nodes for which the operation has already been calculated. The standard binary operations will be instantiated for each context upon creation of a new context and are stored in this context: Context.and, Context.or, Context.xor, Context.equiv and Context.impl.

Author:
Ekkart Kindler, kindler@upb.de

Field Summary
private  Context context
          The context for this binary operation.
private  java.util.Map table
          Hash table for pairs of nodes for which this binary operation has already been applied.
private  boolean[][] truthTable
          The truth table defining the binary operation.
 
Constructor Summary
BinOp(Context context, boolean[][] truthTable)
          Creates a new binary operation from the truth table.
 
Method Summary
private  ROBDD apply(InnerNode n1, InnerNode n2)
          Applies the binary operation to the two ROBDDs.
 ROBDD apply(ROBDD n1, ROBDD n2)
          Applies the binary operation to the two ROBDDs.
private  ROBDD apply(ROBDD n1, TerminalNode n2)
          Applies the binary operation to the two ROBDDs.
private  ROBDD apply(TerminalNode n1, ROBDD n2)
          Applies the binary operation to the two ROBDDs.
 void clearHashtable()
          Clears the hash table keeping track of pairs of ROBDD nodes for which this binary operation has already been computed in this context.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

context

private Context context
The context for this binary operation.


truthTable

private boolean[][] truthTable
The truth table defining the binary operation. In each dimension, this array has length 2.


table

private java.util.Map table
Hash table for pairs of nodes for which this binary operation has already been applied. Once calculated, the result is stored in this table, so that it need not be calculated again. This significantly increases the efficiency of the recursive application of the binary operations and recurrent application of the binary operation to the same arguments. The reference itself is stored as a weak reference. This allows a node to be garbage collected when there are only references from this table.

Constructor Detail

BinOp

public BinOp(Context context,
             boolean[][] truthTable)
Creates a new binary operation from the truth table.

Parameters:
context - The context in which this binary operation is to be applied.
truthTable - The truth table defining the binary operation. It is a two-dimensional array with length two each. The first dimension refers to the first operand and the second to the second operand. In the array, index 0 stands for false and index 1 stands for true. If the length of one dimension is less than two or no truth table is provided at all, the entries not provided are considered to be false.
Method Detail

apply

public ROBDD apply(ROBDD n1,
                   ROBDD n2)
Applies the binary operation to the two ROBDDs. This method dispatches the calls to the more specific operations for the different node types. It is an error if the ROBDDs provided as parameters are from a different context.

Parameters:
n1 - first operand
n2 - second operand
Returns:
the result of the binary operation
Throws:
IncorrectUseException - indicates that the context of the operation is different from the context of the ROBDDs
InternalError - indicates that a node of unknown type was encountered
See Also:
apply(TerminalNode, ROBDD), apply(ROBDD, TerminalNode), apply(InnerNode, InnerNode)

apply

private ROBDD apply(TerminalNode n1,
                    ROBDD n2)
Applies the binary operation to the two ROBDDs. This is the version, when the first operand is a terminal node.

Parameters:
n1 - first operand
n2 - second operand
Returns:
the result of the binary operation
See Also:
apply(ROBDD, ROBDD)

apply

private ROBDD apply(ROBDD n1,
                    TerminalNode n2)
Applies the binary operation to the two ROBDDs. This is the version, when the second operand is a terminal node.

Parameters:
n1 - first operand
n2 - second operand
Returns:
the result of the binary operation
See Also:
apply(ROBDD, ROBDD)

apply

private ROBDD apply(InnerNode n1,
                    InnerNode n2)
Applies the binary operation to the two ROBDDs. This is the version, when both operands are inner nodes.

Parameters:
n1 - first operand
n2 - second operand
Returns:
the result of the binary operation
See Also:
apply(ROBDD, ROBDD)

clearHashtable

public void clearHashtable()
Clears the hash table keeping track of pairs of ROBDD nodes for which this binary operation has already been computed in this context. This method can be called any time without compromising the correctness. But, calling it can significantly reduce the efficiency. So, it should not be called without need. On the other hand, not calling it in time can result in an OutOfMemoryError.