de.uka.ilkd.key.symbolic_execution

Class TruthValueTracingUtil

java.lang.Object

de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil

public final class TruthValueTracingUtil
extends java.lang.Object

Provides functionality to evaluate the truth value of labeled formulas (predicates and junctors).

Author:

Martin Hentschel

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	TruthValueTracingUtil.BranchResult Represents the unmodifiable predicate results of a leaf Node (Goal).
private static class	TruthValueTracingUtil.LabelOccurrence Utility class which specifies the occurrence of a FormulaTermLabel.
static class	TruthValueTracingUtil.MultiEvaluationResult Instances of this unmodifyable class are used to store the found evaluation results.
static class	TruthValueTracingUtil.TruthValue Represents the possible truth values.
static class	TruthValueTracingUtil.TruthValueTracingResult Represents the final predicate evaluation result returned by {@link TruthValueEvaluationUtil#evaluate(Node, Name, boolean, boolean).

Constructor Summary

Constructors

Modifier	Constructor and Description
private	TruthValueTracingUtil() Forbid instances.

Method Summary

Modifier and Type	Method and Description
protected static void	analyzeTacletGoal(Node parent, TacletApp tacletApp, TacletGoalTemplate tacletGoal, java.util.List<TruthValueTracingUtil.LabelOccurrence> labels, Services services, java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results) Analyzes the given TacletGoalTemplate.
protected static Term	checkForNewMinorIds(Node childNode, FormulaTermLabel label, boolean antecedentRuleApplication, TermBuilder tb) Checks if new minor IDs are available.
protected static void	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 Term	checkForNewMinorIdsOSS(SequentFormula onlyChangedChildSF, FormulaTermLabel label, boolean antecedentRuleApplication, TermBuilder tb) Checks if new minor IDs are available in case of OneStepSimplifier usage.
protected static void	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.
protected static Term	computeInstructionTerm(java.util.List<Term> antecedentReplacements, java.util.List<Term> succedentReplacements, boolean antecedentRuleApplication, TermBuilder tb) Computes the Term with the instruction how to compute the truth value based on the found replacements.
static TruthValueTracingUtil.TruthValueTracingResult	evaluate(Node node, Name termLabelName, boolean useUnicode, boolean usePrettyPrinting) Evaluates the truth values in the subtree of the given Node for predicates labeled with the given TermLabel name.
protected static void	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) Evaluates the truth statuses changed from the parent Node to its child Node.
protected static java.util.List<TruthValueTracingUtil.LabelOccurrence>	findInvolvedLabels(Sequent sequent, TacletApp tacletApp, Name termLabelName) Computes the occurrences of all involved FormulaTermLabels.
protected static boolean	isClosingRule(Taclet taclet) Checks if the Taclet is a closing rule.
static boolean	isIfThenElseFormula(Operator operator, ImmutableArray<Term> subs) Checks if the given Operator and its sub Terms specify an if-then-else formula.
static boolean	isIfThenElseFormula(Term term) Checks if the given Term is an if-then-else formula.
static boolean	isLogicOperator(Operator operator, ImmutableArray<Term> subs) Checks if the given Operator and its sub Terms specify a logical operator.
static boolean	isLogicOperator(Term term) Checks if the given Term is a logical operator
static boolean	isPredicate(Operator operator) Checks if the given Operator is a predicate.
static boolean	isPredicate(SequentFormula sequentFormula) Checks if the given SequentFormula is a predicate.
static boolean	isPredicate(Term term) Checks if the given Term is a predicate.
protected static void	listLabelReplacements(SequentFormula sf, Name labelName, java.lang.String labelId, java.util.List<Term> resultToFill) Lists all label replacements in the given SequentFormula.
protected static void	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	updatePredicateResult(FormulaTermLabel label, Term instructionTerm, java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results) Updates the instruction Term for the given FormulaTermLabel in the result Map.
protected static void	updatePredicateResultBasedOnNewMinorIds(Node childNode, Name termLabelName, TermBuilder tb, java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results) Updates the PredicateResults based on minor ID changes if available.
protected static void	updatePredicateResultBasedOnNewMinorIdsOSS(PosInOccurrence childPio, PosInOccurrence parentPio, Name termLabelName, TermBuilder tb, java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results) Updates the PredicateResults based on minor ID changes if available in case of OneStepSimplifier usage.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

TruthValueTracingUtil

private TruthValueTracingUtil()

Forbid instances.

Method Detail

isPredicate

public static boolean isPredicate(SequentFormula sequentFormula)

Checks if the given SequentFormula is a predicate.

Parameters:

sequentFormula - The SequentFormula to check.

Returns:

true is predicate, false is something else.

isPredicate

public static boolean isPredicate(Term term)

Checks if the given Term is a predicate.

Parameters:

term - The Term to check.

Returns:

true is predicate, false is something else.

isPredicate

public static boolean isPredicate(Operator operator)

Checks if the given Operator is a predicate.

Parameters:

operator - The Operator to check.

Returns:

true is predicate, false is something else.

isLogicOperator

public static boolean isLogicOperator(Term term)

Checks if the given Term is a logical operator

Parameters:

operator - The Term to check.

Returns:

true is logical operator, false is something else.

isLogicOperator

public static boolean isLogicOperator(Operator operator,
                                      ImmutableArray<Term> subs)

Checks if the given Operator and its sub Terms specify a logical operator.

Parameters:

operator - The Operator.

subs - The sub Terms.

Returns:

true is logical operator, false is something else.

isIfThenElseFormula

public static boolean isIfThenElseFormula(Term term)

Checks if the given Term is an if-then-else formula.

Parameters:

term - The Term to check.

Returns:

true is if-then-else formula, false is something else.

isIfThenElseFormula

public static boolean isIfThenElseFormula(Operator operator,
                                          ImmutableArray<Term> subs)

Checks if the given Operator and its sub Terms specify an if-then-else formula.

Parameters:

operator - The Operator.

subs - The sub Terms.

Returns:

true is if-then-else formula, false is something else.

evaluate

public static TruthValueTracingUtil.TruthValueTracingResult evaluate(Node node,
                                                                     Name termLabelName,
                                                                     boolean useUnicode,
                                                                     boolean usePrettyPrinting)
                                                              throws ProofInputException

Evaluates the truth values in the subtree of the given Node for predicates labeled with the given TermLabel name.

Parameters:

node - The Node to start evaluation at.

termLabelName - The Name of the TermLabel to consider.

useUnicode - true use unicode characters, false do not use unicode characters.

usePrettyPrinting - true use pretty printing, false do not use pretty printing.

Returns:

The result.

Throws:

ProofInputException - Occurred Exception

evaluateNode

protected static void 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)
                            throws ProofInputException

Evaluates the truth statuses changed from the parent Node to its child Node.

Parameters:

evaluationNode - The Node where the truth status tracing started.

useUnicode - true use unicode characters, false do not use unicode characters.

usePrettyPrinting - true use pretty printing, false do not use pretty printing.

child - The current child Node to analyze.

childIndexOnParent - The index of the child Node on its parent Node.

termLabelName - The Name of the TermLabel to consider.

nodeResult - The to child Node related result Map to update.

result - The overall TruthValueTracingUtil.TruthValueTracingResult to update.

services - The Services to use.

Throws:

ProofInputException - Occurred exception.

isClosingRule

protected static boolean isClosingRule(Taclet taclet)

Checks if the Taclet is a closing rule.

Parameters:

taclet - The Taclet to check.

Returns:

true is closing, false is not closing.

findInvolvedLabels

protected static java.util.List<TruthValueTracingUtil.LabelOccurrence> findInvolvedLabels(Sequent sequent,
                                                                                          TacletApp tacletApp,
                                                                                          Name termLabelName)

Computes the occurrences of all involved FormulaTermLabels.

Parameters:

sequent - The Sequent on which the given TacletApp was applied.

tacletApp - The applied TacletApp.

termLabelName - The Name of the TermLabel to consider.

Returns:

The found TruthValueTracingUtil.LabelOccurrences.

analyzeTacletGoal

protected static void analyzeTacletGoal(Node parent,
                                        TacletApp tacletApp,
                                        TacletGoalTemplate tacletGoal,
                                        java.util.List<TruthValueTracingUtil.LabelOccurrence> labels,
                                        Services services,
                                        java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)

Analyzes the given TacletGoalTemplate.

Parameters:

parent - The current Node on which the rule was applied.

tacletApp - The TacletApp.

tacletGoal - The TacletGoalTemplate.

labels - The FormulaTermLabels.

servies - The Services to use.

results - The Map with all available TruthValueTracingUtil.MultiEvaluationResults.

updatePredicateResultBasedOnNewMinorIdsOSS

protected static void updatePredicateResultBasedOnNewMinorIdsOSS(PosInOccurrence childPio,
                                                                 PosInOccurrence parentPio,
                                                                 Name termLabelName,
                                                                 TermBuilder tb,
                                                                 java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)

Updates the PredicateResults based on minor ID changes if available in case of OneStepSimplifier usage.

Parameters:

childNode - The child Node.

termLabelName - The name of the TermLabel which is added to predicates.

tb - The TermBuilder to use.

results - The Map with all available TruthValueTracingUtil.MultiEvaluationResults.

checkForNewMinorIdsOSS

protected static void 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.

Parameters:

onlyChangedChildSF - The only changed SequentFormula in the child Node.

term - The Term contained in the child Node to check.

termLabelName - The name of the TermLabel which is added to predicates.

parentPio - The PosInOccurrence of the applied rule of the parent Node.

tb - The TermBuilder to use.

results - The Map with all available TruthValueTracingUtil.MultiEvaluationResults.

checkForNewMinorIdsOSS

protected static Term checkForNewMinorIdsOSS(SequentFormula onlyChangedChildSF,
                                             FormulaTermLabel label,
                                             boolean antecedentRuleApplication,
                                             TermBuilder tb)

Checks if new minor IDs are available in case of OneStepSimplifier usage.

Parameters:

onlyChangedChildSF - The only changed SequentFormula in the child Node.

label - The FormulaTermLabel of interest.

antecedentRuleApplication - true rule applied on antecedent, false rule applied on succedent.

tb - The TermBuilder to use.

Returns:

The computed instruction Term or null if not available.

updatePredicateResultBasedOnNewMinorIds

protected static void updatePredicateResultBasedOnNewMinorIds(Node childNode,
                                                              Name termLabelName,
                                                              TermBuilder tb,
                                                              java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)

Updates the PredicateResults based on minor ID changes if available.

Parameters:

childNode - The child Node.

termLabelName - The name of the TermLabel which is added to predicates.

tb - The TermBuilder to use.

results - The Map with all available TruthValueTracingUtil.MultiEvaluationResults.

checkForNewMinorIds

protected static void 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.

Parameters:

childNode - The child Node.

term - The Term contained in the child Node to check.

termLabelName - The name of the TermLabel which is added to predicates.

parentPio - The PosInOccurrence of the applied rule of the parent Node.

tb - The TermBuilder to use.

results - The Map with all available TruthValueTracingUtil.MultiEvaluationResults.

checkForNewMinorIds

protected static Term checkForNewMinorIds(Node childNode,
                                          FormulaTermLabel label,
                                          boolean antecedentRuleApplication,
                                          TermBuilder tb)

Checks if new minor IDs are available.

Parameters:

childNode - The child Node.

label - The FormulaTermLabel of interest.

antecedentRuleApplication - true rule applied on antecedent, false rule applied on succedent.

tb - The TermBuilder to use.

Returns:

The computed instruction Term or null if not available.

listLabelReplacements

protected static void listLabelReplacements(SequentFormula sf,
                                            Name labelName,
                                            java.lang.String labelId,
                                            java.util.List<Term> resultToFill)

Lists all label replacements in the given SequentFormula.

Parameters:

sf - The SequentFormula to analyze.

labelName - The name of the TermLabel which is added to predicates.

labelId - The label ID of interest.

resultToFill - The result List to fill.

computeInstructionTerm

protected static Term computeInstructionTerm(java.util.List<Term> antecedentReplacements,
                                             java.util.List<Term> succedentReplacements,
                                             boolean antecedentRuleApplication,
                                             TermBuilder tb)

Computes the Term with the instruction how to compute the truth value based on the found replacements.

Parameters:

antecedentReplacements - The replacements found in the antecedent.

succedentReplacements - The replacements found in the succedent.

antecedentRuleApplication - true rule applied on antecedent, false rule applied on succedent.

tb - The TermBuilder to use.

Returns:

The computed instruction Term or null if not available.

updatePredicateResult

protected static void updatePredicateResult(FormulaTermLabel label,
                                            Term instructionTerm,
                                            java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)

Updates the instruction Term for the given FormulaTermLabel in the result Map.

Parameters:

label - The FormulaTermLabel to update its instruction Term.

instructionTerm - The new instruction Term to set.

results - The Map with all available TruthValueTracingUtil.MultiEvaluationResults.

updatePredicateResult

protected static void 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.

Parameters:

label - The FormulaTermLabel to update its instruction Term.

evaluationResult - true label evaluates at least once to true, false label evaluates at least once to false.

results - The Map with all available TruthValueTracingUtil.MultiEvaluationResults.