de.uka.ilkd.key.rule.merge

Class MergePartner

java.lang.Object

de.uka.ilkd.key.rule.merge.MergePartner

public class MergePartner
extends java.lang.Object

A MergePartner consists of a Goal and a PosInOccurrence; the PosInOccurrence part indicates the portion of the sequent in the Goal which represents the symbolic state-program counter part.

Author:

Dominic Scheurer

Field Summary

Fields

Modifier and Type	Field and Description
private Goal	goal
private PosInOccurrence	pio

Constructor Summary

Constructors

Constructor and Description
MergePartner(Goal goal, PosInOccurrence pio)

Method Summary

Modifier and Type	Method and Description
Goal	getGoal()
PosInOccurrence	getPio()
void	setGoal(Goal goal)
void	setPio(PosInOccurrence pio)

Methods inherited from class java.lang.Object

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

Field Detail

goal

private Goal goal

pio

private PosInOccurrence pio

Constructor Detail

MergePartner

public MergePartner(Goal goal,
                    PosInOccurrence pio)

Method Detail

getGoal

public Goal getGoal()

Returns:

The merge partner goal.

setGoal

public void setGoal(Goal goal)

getPio

public PosInOccurrence getPio()

Returns:

The PosInOccurrence representing the symbolic state-program counter part of the MergePartner.

setPio

public void setPio(PosInOccurrence pio)