de.uka.ilkd.key.rule.match.vm

Class TermNavigator.MutablePair

java.lang.Object

de.uka.ilkd.key.rule.match.vm.TermNavigator.MutablePair

Enclosing class:

TermNavigator

private static class TermNavigator.MutablePair
extends java.lang.Object

A mutable tuple of two types

Field Summary

Fields

Modifier and Type	Field and Description
(package private) Term	first
private static java.util.ArrayDeque<TermNavigator.MutablePair>	PAIR_POOL TERM_NAVIGATOR_POOL of TermNavigator.MutablePair as these are created very often and short-living we reuse them as far as possible The used TermNavigator have to be explicitly released by the user via release()
private static int	PAIR_POOL_SIZE
(package private) java.lang.Integer	second

Constructor Summary

Constructors

Constructor and Description
MutablePair(Term first, java.lang.Integer second)

Method Summary

Modifier and Type	Method and Description
(package private) static TermNavigator.MutablePair	get(Term first, java.lang.Integer second) returns a pooled TermNavigator.MutablePair or a new one if the TERM_NAVIGATOR_POOL is currently empty The used MutablePair have to be explicitly released by the user via release()
void	release()
void	set(Term first, java.lang.Integer second)
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

PAIR_POOL_SIZE

private static final int PAIR_POOL_SIZE

See Also:

Constant Field Values

PAIR_POOL

private static java.util.ArrayDeque<TermNavigator.MutablePair> PAIR_POOL

TERM_NAVIGATOR_POOL of TermNavigator.MutablePair as these are created very often and short-living we reuse them as far as possible The used TermNavigator have to be explicitly released by the user via release()

first

Term first

second

java.lang.Integer second

Constructor Detail

MutablePair

public MutablePair(Term first,
                   java.lang.Integer second)

Method Detail

get

static TermNavigator.MutablePair get(Term first,
                                     java.lang.Integer second)

returns a pooled TermNavigator.MutablePair or a new one if the TERM_NAVIGATOR_POOL is currently empty The used MutablePair have to be explicitly released by the user via release()

Returns:

a pooled TermNavigator.MutablePair or a new one if the TERM_NAVIGATOR_POOL is currently empty

set

public final void set(Term first,
                      java.lang.Integer second)

release

public final void release()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object