public static class ExecutionVariableExtractor.ExtractedExecutionVariable extends AbstractExecutionVariable
IExecutionVariable
instantiated by the ExecutionVariableExtractor
.Modifier and Type | Field and Description |
---|---|
private Term |
arrayEndIndex
The array end index or
null if not used. |
private Term |
arrayStartIndex
The array start index or
null if not used. |
private java.util.List<IExecutionValue> |
values
The contained
IExecutionValue s. |
Constructor and Description |
---|
ExtractedExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
IProgramVariable programVariable,
Term arrayIndex,
Term arrayStartIndex,
Term arrayEndIndex,
Term additionalCondition,
ExecutionVariableExtractor.ExtractedExecutionValue parentValue)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
Term |
createSelectTerm()
Creates recursive a term which can be used to determine the value
of
IExecutionVariable.getProgramVariable() . |
Term |
getArrayEndIndex()
Returns the array end index.
|
java.lang.String |
getArrayEndIndexString()
Returns the human readable array end index.
|
Term |
getArrayStartIndex()
Returns the array start index.
|
java.lang.String |
getArrayStartIndexString()
Returns the human readable array start index.
|
IExecutionValue[] |
getValues()
Returns the possible values of this
IExecutionVariable . |
protected java.lang.String |
lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
private void |
setValues(java.util.List<IExecutionValue> values)
Sets the
IExecutionValue s. |
getAdditionalCondition, getArrayIndex, getArrayIndexString, getElementType, getModalityPIO, getParentValue, getProgramVariable, isArrayIndex
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 java.util.List<IExecutionValue> values
IExecutionValue
s.private final Term arrayStartIndex
null
if not used.private final Term arrayEndIndex
null
if not used.public ExtractedExecutionVariable(IExecutionNode<?> parentNode, Node proofNode, PosInOccurrence modalityPIO, IProgramVariable programVariable, Term arrayIndex, Term arrayStartIndex, Term arrayEndIndex, Term additionalCondition, ExecutionVariableExtractor.ExtractedExecutionValue parentValue)
parentNode
- The IExecutionNode
providing relevant information.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.modalityPIO
- The PosInOccurrence
of the modality of interest.programVariable
- The represented IProgramVariable
which value is shown.arrayIndex
- The index in the parent array.additionalCondition
- An optional additional condition to consider.parentValue
- The parent IExecutionValue
or null
if not available.private void setValues(java.util.List<IExecutionValue> values)
IExecutionValue
s.values
- The IExecutionValue
s to set.public IExecutionValue[] getValues() throws ProofInputException
IExecutionVariable
.IExecutionVariable
.ProofInputException
public Term createSelectTerm()
IExecutionVariable.getProgramVariable()
.public Term getArrayStartIndex()
public java.lang.String getArrayStartIndexString()
public Term getArrayEndIndex()
public java.lang.String getArrayEndIndexString()
protected java.lang.String lazyComputeName() throws ProofInputException
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionVariable
IExecutionNode
.ProofInputException