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

Class MergeAppIntermediate

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.MergeAppIntermediate

public class MergeAppIntermediate
extends BuiltInAppIntermediate

Encapsulates intermediate information for constructing a MergeRule application.

Author:

Dominic Scheurer

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.String	abstractionPredicates
private java.lang.String	distinguishingFormula
private int	id
private java.lang.String	mergeProc
private int	nrPartners
private java.lang.Class<? extends AbstractPredicateAbstractionLattice>	predAbstrLatticeType
private java.lang.String	userChoices

Constructor Summary

Constructors

Constructor and Description
MergeAppIntermediate(java.lang.String ruleName, Pair<java.lang.Integer,PosInTerm> pos, int id, java.lang.String joinProc, int nrPartners, ImmutableList<Name> newNames, java.lang.String distinguishingFormula, java.lang.Class<? extends AbstractPredicateAbstractionLattice> predAbstrLatticeType, java.lang.String abstractionPredicates, java.lang.String userChoices) Constructs a new join rule.

Method Summary

Modifier and Type	Method and Description
java.lang.String	getAbstractionPredicates()
java.lang.String	getDistinguishingFormula()
int	getId()
java.lang.String	getJoinProc()
int	getNrPartners()
java.lang.Class<? extends AbstractPredicateAbstractionLattice>	getPredAbstrLatticeType()
java.lang.String	getUserChoices()

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

id

private int id

mergeProc

private java.lang.String mergeProc

distinguishingFormula

private java.lang.String distinguishingFormula

nrPartners

private int nrPartners

abstractionPredicates

private java.lang.String abstractionPredicates

userChoices

private java.lang.String userChoices

predAbstrLatticeType

private java.lang.Class<? extends AbstractPredicateAbstractionLattice> predAbstrLatticeType

Constructor Detail

MergeAppIntermediate

public MergeAppIntermediate(java.lang.String ruleName,
                            Pair<java.lang.Integer,PosInTerm> pos,
                            int id,
                            java.lang.String joinProc,
                            int nrPartners,
                            ImmutableList<Name> newNames,
                            java.lang.String distinguishingFormula,
                            java.lang.Class<? extends AbstractPredicateAbstractionLattice> predAbstrLatticeType,
                            java.lang.String abstractionPredicates,
                            java.lang.String userChoices)

Constructs a new join rule.

Parameters:

ruleName - Name of the rule; should be "JoinRule".

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

id - ID of the join rule application (should have been stored during proof saving and should match the joinNodeId fields of the corresponding partner nodes).

joinProc - The name of the join procedure used during joining.

nrPartners - Number of involved join partners.

newNames - New names registered in the course of the join rule application.

distinguishingFormula - The user-supplied distinguishing formula for the join.

predAbstrLatticeType - The type for the used predicate abstraction lattice which determines how abstract domain elements are generated from predicates.

abstractionPredicates - The abstraction predicates, if predicate abstraction is used as a join technique.

currAbstractionPredicates -

Method Detail

getId

public int getId()

Returns:

ID of the join rule application (should have been stored during proof saving and should match the joinNodeId fields of the corresponding partner nodes).

getJoinProc

public java.lang.String getJoinProc()

Returns:

The name of the join procedure used during joining.

getNrPartners

public int getNrPartners()

Returns:

Number of involved join partners.

getDistinguishingFormula

public java.lang.String getDistinguishingFormula()

Returns:

The user-supplied distinguishing formula; null if none given.

getPredAbstrLatticeType

public java.lang.Class<? extends AbstractPredicateAbstractionLattice> getPredAbstrLatticeType()

Returns:

The abstraction predicates, if predicate abstraction is used as a join technique.

getAbstractionPredicates

public java.lang.String getAbstractionPredicates()

Returns:

The abstraction predicates for predicate abstraction; null if none given.

getUserChoices

public java.lang.String getUserChoices()

Returns:

The abstraction predicates for program variables involved in a join that are manually chosen by the user.