de.uka.ilkd.key.proof.init

Class AbstractPO.Vertex

java.lang.Object

de.uka.ilkd.key.proof.init.AbstractPO.Vertex

Enclosing class:

AbstractPO

static class AbstractPO.Vertex
extends java.lang.Object

Represents a vertex and additional information required by the Tarjan algorithm. Two vertices are equal if the observer function and the target sort are identical.

Field Summary

Fields

Modifier and Type	Field and Description
private ClassAxiom	axiom
private Pair<Sort,IObserverFunction>	core
(package private) int	index the index (number of already visited nodes) and -1 if not yet visited
(package private) int	lowLink an SCC is identified by the node that was visited first
(package private) boolean	onStack to avoid linear lookup in the stack

Constructor Summary

Constructors

Constructor and Description
Vertex(Pair<Sort,IObserverFunction> vertexCore, ClassAxiom axiom, boolean onStack, int index, int lowLink)

Method Summary

Modifier and Type	Method and Description
boolean	equals(java.lang.Object o)
(package private) ClassAxiom	getAxiom()
int	hashCode()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait

Field Detail

onStack

boolean onStack

to avoid linear lookup in the stack

index

int index

the index (number of already visited nodes) and -1 if not yet visited

lowLink

int lowLink

an SCC is identified by the node that was visited first

axiom

private final ClassAxiom axiom

core

private final Pair<Sort,IObserverFunction> core

Constructor Detail

Vertex

public Vertex(Pair<Sort,IObserverFunction> vertexCore,
              ClassAxiom axiom,
              boolean onStack,
              int index,
              int lowLink)

Method Detail

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

getAxiom

ClassAxiom getAxiom()