public class MergeAppIntermediate extends BuiltInAppIntermediate
MergeRule
application.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 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.
|
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() |
getBuiltInIfInsts, getContract, getNewNames, getPosInfo, getRuleName
getLineNr, setLineNr
private int id
private java.lang.String mergeProc
private java.lang.String distinguishingFormula
private int nrPartners
private java.lang.String abstractionPredicates
private java.lang.String userChoices
private java.lang.Class<? extends AbstractPredicateAbstractionLattice> predAbstrLatticeType
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)
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
- public int getId()
public java.lang.String getJoinProc()
public int getNrPartners()
public java.lang.String getDistinguishingFormula()
public java.lang.Class<? extends AbstractPredicateAbstractionLattice> getPredAbstrLatticeType()
public java.lang.String getAbstractionPredicates()
public java.lang.String getUserChoices()