de.uka.ilkd.key.logic

Class RenameTable

java.lang.Object

de.uka.ilkd.key.logic.RenameTable

Direct Known Subclasses:

RenameTable.EmptyRenameTable

public class RenameTable
extends java.lang.Object

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	RenameTable.EmptyRenameTable

Field Summary

Fields

Modifier and Type	Field and Description
static RenameTable	EMPTY_TABLE
private ImmutableMap<QuantifiableVariable,java.lang.Integer>	localRenamingTable local map mapping a QuantifiableVariable object to an abstract name.
private int	max the maximal value of an abstract name
private RenameTable	parent the parent renaming table

Constructor Summary

Constructors

Constructor and Description
RenameTable(RenameTable parent, ImmutableMap<QuantifiableVariable,java.lang.Integer> localTable, int newMax)

Method Summary

Modifier and Type	Method and Description
RenameTable	assign(QuantifiableVariable n1, QuantifiableVariable n2) assigns both QuantifiableVariable objects the same abstract name
boolean	contains(QuantifiableVariable n) returns true iff the given variable is mapped to an abstract name.
boolean	containsLocally(QuantifiableVariable n) does nearly the same as contains(QuantifiableVariable) but performs the test only on the local table
private java.lang.Integer	createNewAbstractName()
RenameTable	extend() creates a nested renaming table with this as parent
RenameTable	parent()
boolean	sameAbstractName(QuantifiableVariable n1, QuantifiableVariable n2) tests if both QuantifiableVariables are assigned to the same abstract name (locally or by the parent)
java.lang.String	toString() toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

EMPTY_TABLE

public static final RenameTable EMPTY_TABLE

localRenamingTable

private final ImmutableMap<QuantifiableVariable,java.lang.Integer> localRenamingTable

local map mapping a QuantifiableVariable object to an abstract name. This map is allowed to hide bound renaming of the parent table.

max

private final int max

the maximal value of an abstract name

parent

private final RenameTable parent

the parent renaming table

Constructor Detail

RenameTable

public RenameTable(RenameTable parent,
                   ImmutableMap<QuantifiableVariable,java.lang.Integer> localTable,
                   int newMax)

Method Detail

contains

public boolean contains(QuantifiableVariable n)

returns true iff the given variable is mapped to an abstract name. The test is performed in the local as well as in the parent renaming table.

Parameters:

n - the QuantifiableVariable object the existence of an abstract name is checked.

Returns:

true if n has been already assigned to an abstract name

containsLocally

public boolean containsLocally(QuantifiableVariable n)

does nearly the same as contains(QuantifiableVariable) but performs the test only on the local table

Parameters:

n - the QuantifiableVariable object the existence of an abstract name is checked.

Returns:

true if n has been already locally assigned to an abstract name

sameAbstractName

public boolean sameAbstractName(QuantifiableVariable n1,
                                QuantifiableVariable n2)

tests if both QuantifiableVariables are assigned to the same abstract name (locally or by the parent)

Parameters:

n1 - one of the QuantifiableVariables to be tested iff they have been assigned the same abstract name

n2 - one of the QuantifiableVariables to be tested

Returns:

true iff n1 and n2 are mapped to the same abstract name

createNewAbstractName

private java.lang.Integer createNewAbstractName()

assign

public RenameTable assign(QuantifiableVariable n1,
                          QuantifiableVariable n2)

assigns both QuantifiableVariable objects the same abstract name

extend

public RenameTable extend()

creates a nested renaming table with this as parent

toString

public java.lang.String toString()

toString

Overrides:

toString in class java.lang.Object

parent

public RenameTable parent()