|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectde.upb.swt.mcie.robdds.Context
public class Context
Implements the context for an ROBDD, which comprises the set of variables and the order on these variables. In addition, the context maintains all hash tables for ROBBDs and its operations.
This class provides a public method createVariable
, which can be used
for instantiating new variables in this context. Each variable is
assigned a unique number in ascending order. This is the variable
order used in ROBDDs as defined in package robdds
. When a variable is created, the variable as well as its primed
version are instantiated (where the unprimed version is created first).
From outside this package, variables can only be generated by
method createVariable
, which returns the
unprimed version. The corresponding primed version can
be obtained by the method Variable.getPartner()
.
Field Summary | |
---|---|
BinOp |
and
The and operation in this context. |
BinOp |
equiv
The equivalence operation (equality) in this context. |
TerminalNode |
high
The (in this context) unique terminal node representing true (1). |
BinOp |
impl
The implication operation in this context. |
(package private) java.util.Map |
innerNodesTable
This hash table holds references to all existing inner nodes. |
TerminalNode |
low
The (in this context) unique terminal node representing false (0). |
BinOp |
or
The or operation in this context. |
(package private) java.util.Map |
predecessorTable
This table is used during the calculation of the predecessors of a set with respect to a transition relation. |
(package private) java.util.Map |
relationTable
This table is used during the calculation of the relation product of two relations. |
(package private) java.util.Map |
successorTable
This table is used during the calculation of the successors of a set with respect to a transition relation. |
private int |
variablesCounter
The number of variables (primed and unprimed) instantiated so far in this context. |
private java.util.Map |
variablesTable
The table keeping track of all variables in this context. |
BinOp |
xor
The xor operation in this context. |
Constructor Summary | |
---|---|
Context()
|
Method Summary | |
---|---|
void |
clearHashTables()
Clears the hash tables of all operations in this context. |
(package private) ROBDD |
createInnerNode(Variable variable,
ROBDD low,
ROBDD high)
Creates the inner node, provided that it is not duplicate and not redundant. |
Variable |
createVariable(java.lang.String name)
Creates a pair of new variables for the given name and returns the unprimed version of this pair as a result. |
int |
getSize()
Returns the number of internal nodes currently in use. |
Variable |
getVariable(java.lang.String name)
For the given name, returns the associated variable, if the variable exists. |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
---|
private java.util.Map variablesTable
private int variablesCounter
public final TerminalNode low
public final TerminalNode high
java.util.Map innerNodesTable
WeakHashMaps
and WeakReferences
in this
table. Note that most inner nodes will be referenced from other
hash tables too; therefore, garbage collection will be effective
only after these tables have been cleared.
TODO: Much fine tuning could be done at this point, but this
depends on the particular application.BTW: The other two requirements on ROBDDs, variable order and exclusion of redundant nodes are guaranteed by the implementation of the different algorithms on ROBDDs. The API should be such that these properties cannot be compromised from outside the package.
java.util.Map predecessorTable
java.util.Map successorTable
java.util.Map relationTable
public final BinOp and
public final BinOp or
public final BinOp xor
public final BinOp equiv
public final BinOp impl
Constructor Detail |
---|
public Context()
Method Detail |
---|
public Variable createVariable(java.lang.String name)
Variable.getPartner()
. In principle, the name
could contain special characters and symbols other than letters or
digits. These variables, however, cannot be parsed, and should be
used for special purposes only, when directly generating formulas in
the code.
name
- the name of the variable
public Variable getVariable(java.lang.String name)
Variable.getPartner()
. In principle, the name
could contain special characters and symbols other than letters or
digits. These variables, however, cannot be parsed, and should be
used for special purposes only, when directly generating formulas in
the code.
name
- a String
ROBDD createInnerNode(Variable variable, ROBDD low, ROBDD high)
variable
- the variable of this nodelow
- the successor for 0high
- the successor for 1
IncorrectUseException
- if the contexts of the variable
and the successor nodes do not coincide
InternalError
- if for some reason the requirements of
ROBDDs are compromisedpublic int getSize()
WeakHashMap
, it
returns an upper bound only.
public void clearHashTables()
BinOp.clearHashtable()
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |