public class ExecutionVariable extends AbstractExecutionVariable
IExecutionVariable
.Modifier and Type | Field and Description |
---|---|
private ExecutionValue |
lengthValue
The
ExecutionValue from which the array length was computed. |
private IExecutionNode<?> |
parentNode
The parent
IExecutionNode which provides this ExecutionVariable . |
private ExecutionValue[] |
values
The possible values of this
IExecutionValue . |
Constructor and Description |
---|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
IProgramVariable programVariable,
Term additionalCondition)
Constructor for a "normal" child value.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
Term arrayIndex,
ExecutionValue lengthValue,
Term additionalCondition)
Constructor for an array cell value.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
IProgramVariable programVariable,
Term additionalCondition)
Constructor for a "normal" value.
|
Modifier and Type | Method and Description |
---|---|
protected Term |
computeValueCondition(TermBuilder tb,
java.util.List<Goal> valueGoals,
InitConfig initConfig)
|
Term |
createSelectTerm()
Creates recursive a term which can be used to determine the value
of
IExecutionVariable.getProgramVariable() . |
ExecutionValue |
getLengthValue()
Returns the
ExecutionValue from which the array length was computed. |
IExecutionNode<?> |
getParentNode()
Returns the parent
IExecutionNode which provides this ExecutionVariable . |
ExecutionValue |
getParentValue()
Returns the parent
IExecutionValue if available. |
ExecutionValue[] |
getValues()
Returns the possible values of this
IExecutionVariable . |
protected void |
groupGoalsByValue(ImmutableList<Goal> goals,
Operator operator,
Term siteProofSelectTerm,
Term siteProofCondition,
java.util.Map<Term,java.util.List<Goal>> valueMap,
java.util.List<Goal> unknownValues,
Services services)
Groups all
Goal s which provides the same value. |
protected ExecutionValue[] |
instantiateValuesFromSideProof(InitConfig initConfig,
Services services,
TermBuilder tb,
ApplyStrategyInfo info,
Operator resultOperator,
Term siteProofSelectTerm,
Term siteProofCondition)
Analyzes the side proof defined by the
ApplyStrategyInfo
and creates ExecutionValue s from it. |
protected boolean |
isValidValue(Term value)
Checks if the given
Term represents a valid value. |
protected ExecutionValue[] |
lazyComputeValues()
Computes the value for
getValues()
lazily when the method is called the first time. |
getAdditionalCondition, getArrayIndex, getArrayIndexString, getElementType, getModalityPIO, getProgramVariable, isArrayIndex, lazyComputeName
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 IExecutionNode<?> parentNode
IExecutionNode
which provides this ExecutionVariable
.private final ExecutionValue lengthValue
ExecutionValue
from which the array length was computed.private ExecutionValue[] values
IExecutionValue
.public ExecutionVariable(IExecutionNode<?> parentNode, Node proofNode, PosInOccurrence modalityPIO, IProgramVariable programVariable, Term additionalCondition)
parentNode
- The parent IExecutionNode
which provides this ExecutionVariable
.programVariable
- The represented IProgramVariable
which value is shown.additionalCondition
- An optional additional condition to consider.public ExecutionVariable(IExecutionNode<?> parentNode, Node proofNode, PosInOccurrence modalityPIO, ExecutionValue parentValue, IProgramVariable programVariable, Term additionalCondition)
settings
- The ITreeSettings
to use.parentNode
- The parent IExecutionNode
which provides this ExecutionVariable
.parentValue
- The parent ExecutionValue
or null
if not available.programVariable
- The represented IProgramVariable
which value is shown.additionalCondition
- An optional additional condition to consider.public ExecutionVariable(IExecutionNode<?> parentNode, Node proofNode, PosInOccurrence modalityPIO, ExecutionValue parentValue, Term arrayIndex, ExecutionValue lengthValue, Term additionalCondition)
parentNode
- The parent IExecutionNode
which provides this ExecutionVariable
.parentValue
- The parent ExecutionValue
or null
if not available.arrayIndex
- The index in the parent array.lengthValue
- The ExecutionValue
from which the array length was computed.additionalCondition
- An optional additional condition to consider.public ExecutionValue[] getValues() throws ProofInputException
IExecutionVariable
.IExecutionVariable
.ProofInputException
protected ExecutionValue[] lazyComputeValues() throws ProofInputException
getValues()
lazily when the method is called the first time.ProofInputException
- Occurred Exception.protected ExecutionValue[] instantiateValuesFromSideProof(InitConfig initConfig, Services services, TermBuilder tb, ApplyStrategyInfo info, Operator resultOperator, Term siteProofSelectTerm, Term siteProofCondition) throws ProofInputException
ApplyStrategyInfo
and creates ExecutionValue
s from it.initConfig
- The InitConfig
of the side proof.services
- The Services
of the side proof.tb
- The TermBuilder
of the side proof.info
- The side proof.resultOperator
- The Operator
of the result predicate.siteProofSelectTerm
- The queried value.siteProofCondition
- The condition under which the value is queried.ExecutionValue
instances.ProofInputException
- Occurred Exception.protected boolean isValidValue(Term value)
Term
represents a valid value.value
- The value to check.true
valid value, false
invalid value to be ignored.protected void groupGoalsByValue(ImmutableList<Goal> goals, Operator operator, Term siteProofSelectTerm, Term siteProofCondition, java.util.Map<Term,java.util.List<Goal>> valueMap, java.util.List<Goal> unknownValues, Services services) throws ProofInputException
Goal
s which provides the same value.goals
- All available Goal
s to group.operator
- The Operator
of the Term
which provides the value.services
- The Services
to use.ProofInputException
protected Term computeValueCondition(TermBuilder tb, java.util.List<Goal> valueGoals, InitConfig initConfig) throws ProofInputException
Goal
s which is the
or combination of each path condition per Goal
.tb
- The TermBuilder
to use passed to ensure that it is still available even if the Proof
is disposed in between.valueGoals
- The Goal
s to compute combined path condition for.initConfig
- The InitConfig
to use.ProofInputException
- Occurred Exception.public Term createSelectTerm()
IExecutionVariable.getProgramVariable()
.public ExecutionValue getParentValue()
IExecutionValue
if available.getParentValue
in interface IExecutionVariable
getParentValue
in class AbstractExecutionVariable
IExecutionValue
if available and null
otherwise.public IExecutionNode<?> getParentNode()
IExecutionNode
which provides this ExecutionVariable
.IExecutionNode
which provides this ExecutionVariable
.public ExecutionValue getLengthValue()
ExecutionValue
from which the array length was computed.ExecutionValue
from which the array length was computed.