public class ExecutionConstraint extends AbstractExecutionElement implements IExecutionConstraint
IExecutionConstraint
.Modifier and Type | Field and Description |
---|---|
private PosInOccurrence |
modalityPIO
The
PosInOccurrence of the modality of interest. |
private Term |
term
The
Term representing the constraint. |
Constructor and Description |
---|
ExecutionConstraint(ITreeSettings settings,
Node proofNode,
PosInOccurrence modalityPIO,
Term term)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getElementType()
Returns a human readable element type name.
|
PosInOccurrence |
getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
Term |
getTerm()
Returns the
Term representing the constraint. |
protected java.lang.String |
lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, setName, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final PosInOccurrence modalityPIO
PosInOccurrence
of the modality of interest.public ExecutionConstraint(ITreeSettings settings, Node proofNode, PosInOccurrence modalityPIO, Term term)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.term
- The Term
representing the constraint.protected java.lang.String lazyComputeName() throws ProofInputException
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionElement
IExecutionNode
.ProofInputException
public java.lang.String getElementType()
getElementType
in interface IExecutionElement
public Term getTerm()
Term
representing the constraint.getTerm
in interface IExecutionConstraint
Term
representing the constraint.public PosInOccurrence getModalityPIO()
PosInOccurrence
of the modality of interest including updates.getModalityPIO
in interface IExecutionElement
PosInOccurrence
of the modality of interest including updates.