public final class TruthValueTracingUtil
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
TruthValueTracingUtil.BranchResult
|
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).
|
Modifier | Constructor and Description |
---|---|
private |
TruthValueTracingUtil()
Forbid instances.
|
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)
|
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)
|
protected static java.util.List<TruthValueTracingUtil.LabelOccurrence> |
findInvolvedLabels(Sequent sequent,
TacletApp tacletApp,
Name termLabelName)
Computes the occurrences of all involved
FormulaTermLabel s. |
protected static boolean |
isClosingRule(Taclet taclet)
Checks if the
Taclet is a closing rule. |
static boolean |
isIfThenElseFormula(Operator operator,
ImmutableArray<Term> subs)
|
static boolean |
isIfThenElseFormula(Term term)
Checks if the given
Term is an if-then-else formula. |
static boolean |
isLogicOperator(Operator operator,
ImmutableArray<Term> subs)
|
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)
|
protected static void |
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 |
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. |
public static boolean isPredicate(SequentFormula sequentFormula)
SequentFormula
is a predicate.sequentFormula
- The SequentFormula
to check.true
is predicate, false
is something else.public static boolean isPredicate(Term term)
Term
is a predicate.term
- The Term
to check.true
is predicate, false
is something else.public static boolean isPredicate(Operator operator)
Operator
is a predicate.operator
- The Operator
to check.true
is predicate, false
is something else.public static boolean isLogicOperator(Term term)
Term
is a logical operatoroperator
- The Term
to check.true
is logical operator, false
is something else.public static boolean isLogicOperator(Operator operator, ImmutableArray<Term> subs)
public static boolean isIfThenElseFormula(Term term)
Term
is an if-then-else formula.term
- The Term
to check.true
is if-then-else formula, false
is something else.public static boolean isIfThenElseFormula(Operator operator, ImmutableArray<Term> subs)
public static TruthValueTracingUtil.TruthValueTracingResult evaluate(Node node, Name termLabelName, boolean useUnicode, boolean usePrettyPrinting) throws ProofInputException
Node
for predicates labeled with the given TermLabel
name.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.ProofInputException
- Occurred Exceptionprotected 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
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.ProofInputException
- Occurred exception.protected static boolean isClosingRule(Taclet taclet)
Taclet
is a closing rule.taclet
- The Taclet
to check.true
is closing, false
is not closing.protected static java.util.List<TruthValueTracingUtil.LabelOccurrence> findInvolvedLabels(Sequent sequent, TacletApp tacletApp, Name termLabelName)
FormulaTermLabel
s.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)
TacletGoalTemplate
.parent
- The current Node
on which the rule was applied.tacletApp
- The TacletApp
.tacletGoal
- The TacletGoalTemplate
.labels
- The FormulaTermLabel
s.servies
- The Services
to use.results
- The Map
with all available TruthValueTracingUtil.MultiEvaluationResult
s.protected static void updatePredicateResultBasedOnNewMinorIdsOSS(PosInOccurrence childPio, PosInOccurrence parentPio, Name termLabelName, TermBuilder tb, java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
PredicateResult
s based on minor ID changes if
available in case of OneStepSimplifier
usage.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.MultiEvaluationResult
s.protected static void checkForNewMinorIdsOSS(SequentFormula onlyChangedChildSF, Term term, Name termLabelName, PosInOccurrence parentPio, TermBuilder tb, java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
OneStepSimplifier
usage.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.MultiEvaluationResult
s.protected static Term checkForNewMinorIdsOSS(SequentFormula onlyChangedChildSF, FormulaTermLabel label, boolean antecedentRuleApplication, TermBuilder tb)
OneStepSimplifier
usage.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.Term
or null
if not available.protected static void updatePredicateResultBasedOnNewMinorIds(Node childNode, Name termLabelName, TermBuilder tb, java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
PredicateResult
s based on minor ID changes if available.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.MultiEvaluationResult
s.protected static void checkForNewMinorIds(Node childNode, Term term, Name termLabelName, PosInOccurrence parentPio, TermBuilder tb, java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
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.MultiEvaluationResult
s.protected static Term checkForNewMinorIds(Node childNode, FormulaTermLabel label, boolean antecedentRuleApplication, TermBuilder tb)
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.Term
or null
if not available.protected static void listLabelReplacements(SequentFormula sf, Name labelName, java.lang.String labelId, java.util.List<Term> resultToFill)
SequentFormula
.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.protected static Term computeInstructionTerm(java.util.List<Term> antecedentReplacements, java.util.List<Term> succedentReplacements, boolean antecedentRuleApplication, TermBuilder tb)
Term
with the instruction how to compute the truth
value based on the found replacements.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.Term
or null
if not available.protected static void updatePredicateResult(FormulaTermLabel label, Term instructionTerm, java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
label
- The FormulaTermLabel
to update its instruction Term
.instructionTerm
- The new instruction Term
to set.results
- The Map
with all available TruthValueTracingUtil.MultiEvaluationResult
s.protected static void updatePredicateResult(FormulaTermLabel label, boolean evaluationResult, java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
FormulaTermLabel
in the result Map
.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.MultiEvaluationResult
s.