Package | Description |
---|---|
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.rule.label | |
de.uka.ilkd.key.symbolic_execution |
Modifier and Type | Method and Description |
---|---|
FormulaTermLabel |
FormulaTermLabelFactory.parseInstance(java.util.List<java.lang.String> parameters,
TermServices services)
Parses the arguments and produces a term label.
|
Modifier and Type | Method and Description |
---|---|
static int |
FormulaTermLabel.newLabelSubID(Services services,
FormulaTermLabel label)
Creates a new label sub ID.
|
Modifier and Type | Method and Description |
---|---|
static FormulaTermLabel |
StayOnFormulaTermLabelPolicy.searchFormulaTermLabel(ImmutableArray<TermLabel> labels)
Searches the
FormulaTermLabel in the given TermLabel s. |
Modifier and Type | Method and Description |
---|---|
FormulaTermLabel |
TruthValueTracingUtil.BranchResult.getPredicateLabel(Term term)
|
Modifier and Type | Method and Description |
---|---|
protected static Term |
TruthValueTracingUtil.checkForNewMinorIds(Node childNode,
FormulaTermLabel label,
boolean antecedentRuleApplication,
TermBuilder tb)
Checks if new minor IDs are available.
|
protected static Term |
TruthValueTracingUtil.checkForNewMinorIdsOSS(SequentFormula onlyChangedChildSF,
FormulaTermLabel label,
boolean antecedentRuleApplication,
TermBuilder tb)
Checks if new minor IDs are available in case of
OneStepSimplifier usage. |
TruthValueTracingUtil.TruthValue |
TruthValueTracingUtil.BranchResult.evaluate(FormulaTermLabel termLabel)
Evaluates the given
FormulaTermLabel . |
TruthValueTracingUtil.MultiEvaluationResult |
TruthValueTracingUtil.BranchResult.getResult(FormulaTermLabel termLabel)
Returns the
TruthValueTracingUtil.MultiEvaluationResult for the given FormulaTermLabel . |
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)
|
void |
TruthValueTracingUtil.BranchResult.updateResult(FormulaTermLabel termLabel,
TruthValueTracingUtil.MultiEvaluationResult result)
Updates a result.
|
Copyright © 2003-2019 The KeY-Project.