Package | Description |
---|---|
de.uka.ilkd.key.symbolic_execution |
Modifier and Type | Method and Description |
---|---|
TruthValueTracingUtil.MultiEvaluationResult |
TruthValueTracingUtil.BranchResult.getResult(FormulaTermLabel termLabel)
Returns the
TruthValueTracingUtil.MultiEvaluationResult for the given FormulaTermLabel . |
TruthValueTracingUtil.MultiEvaluationResult |
TruthValueTracingUtil.MultiEvaluationResult.newEvaluatesToFalse(boolean newEvaluatesToFalse)
Creates a new
TruthValueTracingUtil.MultiEvaluationResult based on the current once
but with an update evaluates to false state. |
TruthValueTracingUtil.MultiEvaluationResult |
TruthValueTracingUtil.MultiEvaluationResult.newEvaluatesToTrue(boolean newEvaluatesToTrue)
Creates a new
TruthValueTracingUtil.MultiEvaluationResult based on the current once
but with an update evaluates to true state. |
TruthValueTracingUtil.MultiEvaluationResult |
TruthValueTracingUtil.MultiEvaluationResult.newEvaluationResult(boolean evaluationResult)
Creates a new
TruthValueTracingUtil.MultiEvaluationResult based on the current once
but with an updated evaluation result. |
TruthValueTracingUtil.MultiEvaluationResult |
TruthValueTracingUtil.MultiEvaluationResult.newInstructionTerm(Term newInstructionTerm)
Creates a new
TruthValueTracingUtil.MultiEvaluationResult based on the current once
but with an update instruction term. |
Modifier and Type | Method and Description |
---|---|
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> |
TruthValueTracingUtil.BranchResult.getResults()
Returns all found results.
|
Modifier and Type | Method and Description |
---|---|
void |
TruthValueTracingUtil.BranchResult.updateResult(FormulaTermLabel termLabel,
TruthValueTracingUtil.MultiEvaluationResult result)
Updates a result.
|
Modifier and Type | Method and Description |
---|---|
protected static void |
TruthValueTracingUtil.analyzeTacletGoal(Node parent,
TacletApp tacletApp,
TacletGoalTemplate tacletGoal,
java.util.List<de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil.LabelOccurrence> labels,
Services services,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Analyzes the given
TacletGoalTemplate . |
protected static void |
TruthValueTracingUtil.checkForNewMinorIds(Node childNode,
Term term,
Name termLabelName,
PosInOccurrence parentPio,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Checks if new minor IDs are available.
|
protected static void |
TruthValueTracingUtil.checkForNewMinorIdsOSS(SequentFormula onlyChangedChildSF,
Term term,
Name termLabelName,
PosInOccurrence parentPio,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Checks if new minor IDs are available in case of
OneStepSimplifier usage. |
TruthValueTracingUtil.TruthValue |
TruthValueTracingUtil.MultiEvaluationResult.evaluate(Name termLabelName,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Computes the final truth value.
|
protected static void |
TruthValueTracingUtil.evaluateNode(Node evaluationNode,
boolean useUnicode,
boolean usePrettyPrinting,
Node child,
int childIndexOnParent,
Name termLabelName,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> nodeResult,
TruthValueTracingUtil.TruthValueTracingResult result,
Services services)
|
protected static void |
TruthValueTracingUtil.updatePredicateResult(FormulaTermLabel label,
boolean evaluationResult,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Updates the evaluation result for the given
FormulaTermLabel
in the result Map . |
protected static void |
TruthValueTracingUtil.updatePredicateResult(FormulaTermLabel label,
Term instructionTerm,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
|
protected static void |
TruthValueTracingUtil.updatePredicateResultBasedOnNewMinorIds(Node childNode,
Name termLabelName,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Updates the
PredicateResult s based on minor ID changes if available. |
protected static void |
TruthValueTracingUtil.updatePredicateResultBasedOnNewMinorIdsOSS(PosInOccurrence childPio,
PosInOccurrence parentPio,
Name termLabelName,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Updates the
PredicateResult s based on minor ID changes if
available in case of OneStepSimplifier usage. |
Constructor and Description |
---|
BranchResult(Node leafNode,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results,
Term condition,
java.lang.String conditionString,
Name termLabelName)
Constructor.
|
Copyright © 2003-2019 The KeY-Project.