de.uka.ilkd.key.proof.io.intermediate

Class MergePartnerAppIntermediate

java.lang.Object

de.uka.ilkd.key.proof.io.intermediate.AppIntermediate

de.uka.ilkd.key.proof.io.intermediate.BuiltInAppIntermediate

de.uka.ilkd.key.proof.io.intermediate.MergePartnerAppIntermediate

public class MergePartnerAppIntermediate
extends BuiltInAppIntermediate

Encapsulates intermediate information for constructing a close-join-partner rule application.

Author:

Dominic Scheurer

Field Summary

Fields

Modifier and Type	Field and Description
private int	mergeNodeId

Constructor Summary

Constructors

Constructor and Description
MergePartnerAppIntermediate(java.lang.String ruleName, Pair<java.lang.Integer,PosInTerm> pos, int mergeNodeId, ImmutableList<Name> newNames) Constructs a new close-merge-partner intermediate application.

Method Summary

Modifier and Type	Method and Description
int	getMergeNodeId()

Methods inherited from class de.uka.ilkd.key.proof.io.intermediate.BuiltInAppIntermediate

getBuiltInIfInsts, getContract, getNewNames, getPosInfo, getRuleName

Methods inherited from class de.uka.ilkd.key.proof.io.intermediate.AppIntermediate

getLineNr, setLineNr

Methods inherited from class java.lang.Object

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

Field Detail

mergeNodeId

private int mergeNodeId

Constructor Detail

MergePartnerAppIntermediate

public MergePartnerAppIntermediate(java.lang.String ruleName,
                                   Pair<java.lang.Integer,PosInTerm> pos,
                                   int mergeNodeId,
                                   ImmutableList<Name> newNames)

Constructs a new close-merge-partner intermediate application.

Parameters:

ruleName - The name of the rule; should be "MergeAfterJoin".

pos - Position information for the merge rule application (Symbolic State - Program Counter formula).

mergeNodeId - The ID of the corresponding merge node.

newNames - New names registered in the course of partner goal closing.

Method Detail

getMergeNodeId

public int getMergeNodeId()

Returns:

The ID of the corresponding merge node.