de.upb.swt.mcie.robdds
Class Variable

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

public class Variable
extends java.lang.Object

Implements a variable within an ROBDD's context. A variable is a name that can be primed or unprimed. Each variable is assigned a unique number, which defines the variable order (currently, the order is the order in which the variables are created in the context). When a variable is created in the context, the variable as well as its primed or unprimed version are instantiated, where the unprimed version is created first (see Context).

Author:
Ekkart Kindler, kindler@upb.de

Field Summary
(package private)  Context context
          The context in which this variable is defined.
(package private)  boolean isprimed
          Field indicating whether the variable is primed or unprimed.
(package private)  java.lang.String name
          The identifier of this variable.
(package private)  int number
          The number of the variable.
(package private)  Variable partner
          The partner variable.
(package private)  ROBDD repr
          The ROBDD representing the formula that consists of this variable only.
 
Constructor Summary
Variable(Context context, java.lang.String name, int number, boolean isprimed)
          Constructs a variable.
 
Method Summary
 java.lang.String getName()
          Returns the name of the variable.
 Variable getPartner()
          Returns the partner variable.
 boolean isPrimed()
          Checks whether the variable is a primed variable.
 boolean precedes(Variable v)
          Checks whether this variable precedes the given variable v in the variable order.
 ROBDD toROBDD()
          Returns the ROBDD representation for this variable (considered as a formula).
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

context

Context context
The context in which this variable is defined.


number

int number
The number of the variable.


name

java.lang.String name
The identifier of this variable.


isprimed

boolean isprimed
Field indicating whether the variable is primed or unprimed.


partner

Variable partner
The partner variable. If the variable is unprimed, this field refers to the primed version of the variable. If the variable is primed, this field refers to the unprimed version.


repr

ROBDD repr
The ROBDD representing the formula that consists of this variable only.

Constructor Detail

Variable

Variable(Context context,
         java.lang.String name,
         int number,
         boolean isprimed)
Constructs a variable. This constructor is only available from inside the package, in order to achieve proper instantiation of pairs of primed and unprimed variables (partner variables). It should be called from the class Context only.

Parameters:
name - the identifier of the variable
isprimed - true if the primed version should be instantiated
Method Detail

getName

public java.lang.String getName()
Returns the name of the variable.

Returns:
the name of the variable

isPrimed

public boolean isPrimed()
Checks whether the variable is a primed variable.

Returns:
true, if the variable is primed; false otherwise

getPartner

public Variable getPartner()
Returns the partner variable. For a primed variable, this is the unprimed variable; for an unprimed variable, this is the primed variable.

Returns:
the partner variable

toROBDD

public ROBDD toROBDD()
Returns the ROBDD representation for this variable (considered as a formula).

Returns:
the ROBDD

precedes

public boolean precedes(Variable v)
Checks whether this variable precedes the given variable v in the variable order. This represents the variable order, which is an irreflexive and total order. It is an error if the variables are from a different context.

Parameters:
v - the variable to be compared with.
Returns:
true if this variable precedes variable v
Throws:
IncorrectUseException - if variables are from a different context