public class ExecutionAllArrayIndicesVariable extends ExecutionVariable
IExecutionVariable
used to query
all array indices at the same time. This supports also arrays where
the length is symbolic and not a concrete number.Modifier and Type | Field and Description |
---|---|
static java.lang.String |
ARRAY_INDEX_CONSTANT_NAME
The name of the constant used to query the value of all array indices.
|
private Term |
constant
The constant representing an arbitrary array index.
|
static java.lang.String |
NOT_A_VALUE_NAME
The name used to represent the fact that a value is not available.
|
private Term |
notAValue
The constant representing the fact that no value is available.
|
Constructor and Description |
---|
ExecutionAllArrayIndicesVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
IProgramVariable arrayProgramVariable,
Term additionalCondition)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
Term |
createArrayTerm()
Creates a
Term to access the array. |
Term |
createSelectTerm()
Creates recursive a term which can be used to determine the value
of
IExecutionVariable.getProgramVariable() . |
Term |
getConstant()
Returns the constant representing an arbitrary array index.
|
Term |
getNotAValue()
Returns the constant representing the fact that no value is available.
|
protected boolean |
isValidValue(Term value)
Checks if the given
Term represents a valid value. |
protected java.lang.String |
lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected ExecutionValue[] |
lazyComputeValues()
Computes the value for
ExecutionVariable.getValues()
lazily when the method is called the first time. |
computeValueCondition, getLengthValue, getParentNode, getParentValue, getValues, groupGoalsByValue, instantiateValuesFromSideProof
getAdditionalCondition, getArrayIndex, getArrayIndexString, getElementType, getModalityPIO, 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
public static final java.lang.String ARRAY_INDEX_CONSTANT_NAME
public static final java.lang.String NOT_A_VALUE_NAME
private Term constant
private final Term notAValue
public ExecutionAllArrayIndicesVariable(IExecutionNode<?> parentNode, Node proofNode, PosInOccurrence modalityPIO, ExecutionValue parentValue, IProgramVariable arrayProgramVariable, Term additionalCondition)
parentNode
- The parent IExecutionNode
.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.modalityPIO
- The PosInOccurrence
of the modality of interest.parentValue
- The parent IExecutionValue
representing the array.arrayProgramVariable
- The IProgramVariable
of the array.additionalCondition
- An optional additional condition to consider.protected java.lang.String lazyComputeName() throws ProofInputException
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionVariable
IExecutionNode
.ProofInputException
protected ExecutionValue[] lazyComputeValues() throws ProofInputException
ExecutionVariable.getValues()
lazily when the method is called the first time.lazyComputeValues
in class ExecutionVariable
ProofInputException
- Occurred Exception.protected boolean isValidValue(Term value)
Term
represents a valid value.isValidValue
in class ExecutionVariable
value
- The value to check.true
valid value, false
invalid value to be ignored.public Term createArrayTerm()
Term
to access the array.Term
to access the array.public Term createSelectTerm()
IExecutionVariable.getProgramVariable()
.createSelectTerm
in interface IExecutionVariable
createSelectTerm
in class ExecutionVariable
public Term getConstant()
public Term getNotAValue()