SymbolicExecutionUtil (KeY API Documentation)

java.lang.Object
- de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil

```
public final class SymbolicExecutionUtil
extends java.lang.Object
```
Provides utility methods for symbolic execution with KeY.

Author:

Martin Hentschel

Nested Class Summary

Nested Classes
Modifier and Type	Class and Description
`static class`	`SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult` The result of `searchContractPostOrExcPostExceptionVariable(Node, Services)`.
`private static class`	`SymbolicExecutionUtil.FindModalityWithSymbolicExecutionLabelId` Utility class used to find the maximal modality Term used by `findModalityWithMaxSymbolicExecutionLabelId(Term)`.
`static class`	`SymbolicExecutionUtil.SiteProofVariableValueInput` Helper class which represents the return value of `ExecutionMethodReturn#createExtractReturnVariableValueSequent(TypeReference, ReferencePrefix, Node, IProgramVariable)` and `ExecutionMethodReturn#createExtractVariableValueSequent(IExecutionContext, Node, IProgramVariable)`.

Field Summary

Fields
Modifier and Type	Field and Description
`static java.lang.String`	`CHOICE_SETTING_RUNTIME_EXCEPTIONS` Key for the choice option "runtimeExceptions".
`static java.lang.String`	`CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_ALLOW` Value in choice option "runtimeExceptions" to allow exceptions.
`static java.lang.String`	`CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_BAN` Value in choice option "runtimeExceptions" to ban exceptions.
`static TermLabel`	`LOOP_BODY_LABEL` Label attached to the modality which executes a loop body in branch "Body Preserves Invariant" of applied "Loop Invariant" rules.
`static Name`	`LOOP_BODY_LABEL_NAME` Name of `LOOP_BODY_LABEL`.
`static TermLabel`	`LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL` Label attached to the implication when a loop body execution terminated normally without any exceptions, returns or breaks in branch "Body Preserves Invariant" of applied "Loop Invariant" rules to show the loop invariant.
`static Name`	`LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL_NAME` Name of `LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL`.
`static TermLabel`	`RESULT_LABEL` Label attached to a `Term` to evaluate in a side proof.
`static Name`	`RESULT_LABEL_NAME` Name of `RESULT_LABEL`.

Constructor Summary

Constructors
Modifier Constructor and Description

private SymbolicExecutionUtil()
Forbid instances.

Constructors
Modifier	Constructor and Description
`private`	`SymbolicExecutionUtil()` Forbid instances.

Method Summary

All Methods Static Methods Concrete Methods
Modifier and Type	Method and Description
`private static Term`	`addLabelRecursiveToNonSkolem(TermFactory tf, Term term, TermLabel label)` Adds the given `TermLabel` to the given `Term` and to all of its children.
`static boolean`	`canComputeVariables(IExecutionNode<?> node, Services services)` Checks if it is right now possible to compute the variables of the given `IExecutionNode` via `IExecutionNode.getVariables()`.
`private static boolean`	`checkNull(Node node, Term additionalAntecedent, Term newSuccedent, boolean nullExpected)` Checks if the given `Term` is null or not in the `Sequent` of the given `Node`.
`private static boolean`	`checkReplaceTerm(Term toCheck, PosInOccurrence posInOccurrence, Term replaceTerm)` Checks if the given replace `Term` is equal module labels to the `Term` to check.
`static int`	`checkSkolemEquality(SequentFormula sf)` Checks if the given `SequentFormula` is a skolem equality.
`static int`	`checkSkolemEquality(Term term)` Checks if the given `Term` is a skolem equality.
`static java.util.List<IProgramVariable>`	`collectAllElementaryUpdateTerms(Node node)` Collects all `IProgramVariable` used in `ElementaryUpdate`s.
`private static void`	`collectContractPreconditions(Services services, SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult search, java.util.List<Term> normalConditions, java.util.List<Term> exceptinalConditions)` Collects the preconditions of an applied operation contract.
`static ImmutableList<Term>`	`collectElementaryUpdates(Term term)` Collects the `ElementaryUpdate`s in the given `Term`.
`static ImmutableList<Goal>`	`collectGoalsInSubtree(IExecutionElement executionElement)` Collects all `Goal`s in the subtree of the given `IExecutionElement`.
`static ImmutableList<Goal>`	`collectGoalsInSubtree(Node node)` Collects all `Goal`s in the subtree of the given `Node`.
`private static java.util.Set<Term>`	`collectSkolemConstants(Sequent sequent, Term term)` Collects all contained skolem `Term`s which fulfill `isSkolemConstant(Term)` as well as the skolem constants used in the find once recursive.
`private static java.util.Set<Term>`	`collectSkolemConstantsNonRecursive(Term term)` Collects all contained skolem `Term`s which fulfill `isSkolemConstant(Term)`.
`private static void`	`collectSpecifcationCasesPreconditions(Term normalExcDefinition, Term exceptionalExcDefinition, Term term, java.util.List<Term> normalConditions, java.util.List<Term> exceptinalConditions)` Collects recursively the preconditions of specification cases.
`private static Term`	`computeBlockContractBuiltInRuleAppBranchCondition(Node parent, Node node, boolean simplify, boolean improveReadability)` Computes the branch condition of the given `Node` which was constructed by an `AbstractBlockContractBuiltInRuleApp`.
`static Term`	`computeBranchCondition(Node node, boolean simplify, boolean improveReadability)` Computes the branch condition of the given `Node`.
`private static Term`	`computeContractRuleAppBranchCondition(Node parent, Node node, boolean simplify, boolean improveReadability)` Computes the branch condition of the given `Node` which was constructed by a `ContractRuleApp`.
`private static Term`	`computeLoopInvariantBuiltInRuleAppBranchCondition(Node parent, Node node, boolean simplify, boolean improveReadability)` Computes the branch condition of the given `Node` which was constructed by a `LoopInvariantBuiltInRuleApp`.
`static Term`	`computePathCondition(Node node, boolean simplify, boolean improveReadability)` Computes the path condition of the given `Node`.
`static Term`	`computePathCondition(Node parentNode, Node childNode, boolean simplify, boolean improveReadability)` Computes the path condition between the given `Node`s.
`static ImmutableList<Term>`	`computeRootElementaryUpdates(Node root)` Computes the initial `ElementaryUpdate`s on the given root `Node`.
`static Pair<java.lang.Integer,SourceElement>`	`computeSecondStatement(RuleApp ruleApp)` Computes the call stack size and the second statement similar to `NodeInfo.computeActiveStatement(SourceElement)`.
`static int`	`computeStackSize(RuleApp ruleApp)` Compute the stack size of the given `Term` described by the given `RuleApp`.
`private static Term`	`computeTacletAppBranchCondition(Node parent, Node node, boolean simplify, boolean improveReadability)` Computes the branch condition of the given `Node` which was constructed by a `TacletApp`.
`static boolean`	`containsStatement(ProgramElement toSearchIn, SourceElement toSearch, Services services)` Checks if the given `ProgramElement` contains the given `SourceElement`.
`static boolean`	`containsSymbolicExecutionLabel(Term term)` Checks if the `Term` or one of its sub terms contains a symbolic execution label.
`static IExecutionVariable[]`	`createAllExecutionVariables(IExecutionNode<?> node, Node proofNode, PosInOccurrence modalityPIO, Term condition)` Creates for the given `IExecutionNode` the contained root `IExecutionVariable`s.
`static IExecutionConstraint[]`	`createExecutionConstraints(IExecutionNode<?> node)` Creates for the given `IExecutionNode` the contained `IExecutionConstraint`s.
`static IExecutionVariable[]`	`createExecutionVariables(IExecutionNode<?> node)` Creates for the given `IExecutionNode` the contained root `IExecutionVariable`s.
`static IExecutionVariable[]`	`createExecutionVariables(IExecutionNode<?> node, Node proofNode, PosInOccurrence modalityPIO, Term condition)` Creates for the given `IExecutionNode` the contained root `IExecutionVariable`s.
`static IExecutionVariable[]`	`createExecutionVariables(IExecutionNode<?> node, Term condition)` Creates for the given `IExecutionNode` the contained root `IExecutionVariable`s.
`static SymbolicExecutionUtil.SiteProofVariableValueInput`	`createExtractReturnVariableValueSequent(Services services, IExecutionContext context, Node methodReturnNode, Node methodCallEmptyNode, IProgramVariable variable)` Creates a `Sequent` which can be used in site proofs to extract the return value of the given `IProgramVariable` from the sequent of the given `Node`.
`static SymbolicExecutionUtil.SiteProofVariableValueInput`	`createExtractReturnVariableValueSequent(Services services, TypeReference contextObjectType, IProgramMethod contextMethod, ReferencePrefix contextObject, Node methodReturnNode, Node methodCallEmptyNode, IProgramVariable variable)` Creates a `Sequent` which can be used in site proofs to extract the return value of the given `IProgramVariable` from the sequent of the given `Node`.
`static SymbolicExecutionUtil.SiteProofVariableValueInput`	`createExtractTermSequent(Services sideProofServices, Node node, PosInOccurrence pio, Term additionalConditions, Term term, boolean keepUpdates)` Creates a `Sequent` which can be used in site proofs to extract the value of the given `IProgramVariable` from the sequent of the given `Node`.
`static SymbolicExecutionUtil.SiteProofVariableValueInput`	`createExtractVariableValueSequent(Services services, Node node, PosInOccurrence pio, Term additionalConditions, IProgramVariable variable)` Creates a `Sequent` which can be used in site proofs to extract the value of the given `IProgramVariable` from the sequent of the given `Node`.
`static NotationInfo`	`createNotationInfo(IExecutionElement element)` Creates the `NotationInfo` for the given `IExecutionElement`.
`static NotationInfo`	`createNotationInfo(Node node)` Creates the `NotationInfo` for the given `Node`.
`static NotationInfo`	`createNotationInfo(Proof proof)` Creates the `NotationInfo` for the given `Proof`.
`static Term`	`createSelectTerm(IExecutionVariable variable)` Creates recursive a term which can be used to determine the value of `#getProgramVariable()`.
`static Sequent`	`createSequentToProveWithNewSuccedent(Node node, PosInOccurrence pio, Term newSuccedent)` Creates a new `Sequent` which is a modification from the `Sequent` of the given `Node` which contains the same information but a different succedent.
`static Sequent`	`createSequentToProveWithNewSuccedent(Node node, PosInOccurrence pio, Term additionalAntecedent, Term newSuccedent, boolean addResultLabel)` Creates a new `Sequent` which is a modification from the `Sequent` of the given `Node` which contains the same information but a different succedent.
`static Sequent`	`createSequentToProveWithNewSuccedent(Node node, PosInOccurrence pio, Term additionalAntecedent, Term newSuccedent, ImmutableList<Term> updates, boolean addResultLabel)` Creates a new `Sequent` which is a modification from the `Sequent` of the given `Node` which contains the same information but a different succedent.
`static Sequent`	`createSequentToProveWithNewSuccedent(Node node, Term additionalAntecedent, Term newSuccedent, boolean addResultLabel)` Creates a new `Sequent` which is a modification from the `Sequent` of the given `Node` which contains the same information but a different succedent.
`static Sequent`	`createSequentToProveWithNewSuccedent(Node node, Term additionalAntecedent, Term newSuccedent, ImmutableList<Term> updates, boolean addResultLabel)` Creates a new `Sequent` which is a modification from the `Sequent` of the given `Node` which contains the same information but a different succedent.
`static boolean`	`equalsWithPosition(SourceElement first, SourceElement second)` Compares the given `SourceElement`s including their `PositionInfo`s.
`private static Term`	`evaluateInSideProof(Services services, Proof proof, ProofEnvironment sideProofEnvironment, Sequent sequentToProve, TermLabel label, java.lang.String description, java.lang.String splittingOption)` Starts the side proof and evaluates the `Sequent` to prove into a single `Term`.
`static IProgramVariable`	`extractExceptionVariable(Proof proof)` Extracts the exception variable which is used to check if the executed program in proof terminates normally.
`protected static ImmutableArray<Term>`	`extractValueFromUpdate(Term term, IProgramVariable variable)` Utility method to extract the value of the `IProgramVariable` from the given update term.
`private static Term`	`findInnerMostSelect(Term term, Services services)`
`static Node`	`findMethodCallNode(Node node, PosInOccurrence pio)` Searches for the given `Node` the parent node which also represents a symbolic execution tree node (checked via `isSymbolicExecutionTreeNode(Node, RuleApp)`).
`static PosInOccurrence`	`findModalityWithMaxSymbolicExecutionLabelId(Semisequent semisequent, boolean inAntec)` Searches the modality `Term` with the maximal `SymbolicExecutionTermLabel` ID `SymbolicExecutionTermLabel.getId()` in the given `Semisequent`.
`static PosInOccurrence`	`findModalityWithMaxSymbolicExecutionLabelId(Sequent sequent)` Searches the modality `PosInOccurrence` with the maximal `SymbolicExecutionTermLabel` ID `SymbolicExecutionTermLabel.getId()` in the given `Sequent`.
`static PosInTerm`	`findModalityWithMaxSymbolicExecutionLabelId(Term term)` Searches the modality `PosInTerm` with the maximal `SymbolicExecutionTermLabel` ID `SymbolicExecutionTermLabel.getId()` in the given `Term`.
`static PosInOccurrence`	`findModalityWithMinSymbolicExecutionLabelId(Semisequent semisequent, boolean inAntec)` Searches the modality `PosInOccurrence` with the minimal `SymbolicExecutionTermLabel` ID `SymbolicExecutionTermLabel.getId()` in the given `Semisequent`.
`static PosInOccurrence`	`findModalityWithMinSymbolicExecutionLabelId(Sequent sequent)` Searches the modality `PosInOccurrence` with the minimal `SymbolicExecutionTermLabel` ID `SymbolicExecutionTermLabel.getId()` in the given `Sequent`.
`static PosInTerm`	`findModalityWithMinSymbolicExecutionLabelId(Term term)` Searches the modality `PosInTerm` with the minimal `SymbolicExecutionTermLabel` ID `SymbolicExecutionTermLabel.getId()` in the given `Term`.
`static Node`	`findParentSetNode(Node node)` Searches for the given `Node` the parent node which also represents a symbolic execution tree node (checked via `isSymbolicExecutionTreeNode(Node, RuleApp)`).
`private static Term`	`findReplacement(Semisequent semisequent, PosInOccurrence posInOccurrence, Term replaceTerm)` Searches the by `Rule` application instantiated replace `Term` which is equal modulo labels to the given replace `Term`.
`static IProgramVariable`	`findSelfTerm(Node node, PosInOccurrence pio)` Searches the `IProgramVariable` of the current `this`/`self` reference.
`private static java.util.List<Term>`	`findSkolemReplacements(Sequent sequent, Term skolemConstant, Term skolemEquality)` Utility method of `replaceSkolemConstants(Sequent, Term, Services)` to find all equality parts of the given skolem constant.
`static Term`	`followPosInOccurrence(PosInOccurrence posInOccurrence, Term term)` Returns the sub `Term` at the given `PosInOccurrence` but on the given `Term` instead of the one contained in the `PosInOccurrence`.
`static java.lang.String`	`formatTerm(Term term, Services services, boolean useUnicode, boolean usePrettyPrinting)` Converts the given `Term` into a `String` respecting `#isUsePretty()`.
`static Term`	`getArrayIndex(Services services, HeapLDT heapLDT, Term arrayIndexTerm)` Returns the array index defined by the given `Term`.
`static java.lang.String`	`getChoiceSetting(java.lang.String key)` Returns the default choice value.
`static java.util.HashMap<java.lang.String,java.lang.String>`	`getDefaultTacletOptions()` Returns the default taclet options for symbolic execution.
`static java.lang.String`	`getDisplayString(IProgramVariable pv)` Returns the human readable name of the given `IProgramVariable`.
`static ProgramVariable`	`getProgramVariable(Services services, HeapLDT heapLDT, Term locationTerm)` Returns the `ProgramVariable` defined by the given `Term`.
`static java.util.Set<IProgramVariable>`	`getProgramVariables(FieldDeclaration fd)` Collects all `IProgramVariable`s of the given `FieldDeclaration`.
`static IExecutionNode<?>`	`getRoot(IExecutionNode<?> executionNode)` Returns the root of the given `IExecutionNode`.
`static java.lang.String`	`getSourcePath(PositionInfo posInfo)` Returns the path to the source file defined by the given `PositionInfo`.
`static SymbolicExecutionTermLabel`	`getSymbolicExecutionLabel(RuleApp ruleApp)` Returns the contained `SymbolicExecutionTermLabel` if available.
`static SymbolicExecutionTermLabel`	`getSymbolicExecutionLabel(Term term)` Returns the contained `SymbolicExecutionTermLabel` if available.
`static boolean`	`hasApplicableRules(Goal goal)` Checks if the `Goal` has applicable rules.
`static boolean`	`hasLoopBodyLabel(RuleApp ruleApp)` Checks if the `Term` on which the `RuleApp` was applied contains a `SymbolicExecutionTermLabel`.
`static boolean`	`hasLoopBodyTerminationLabel(RuleApp ruleApp)` Checks if the `Term` on which the `RuleApp` was applied contains a `SymbolicExecutionTermLabel`.
`static boolean`	`hasLoopCondition(Node node, RuleApp ruleApp, SourceElement statement)` Checks if the given `Node` has a loop condition.
`static boolean`	`hasReferenceSort(Services services, IProgramVariable var)` Checks if the `Sort` of the given `IProgramVariable` is a reference type.
`static boolean`	`hasReferenceSort(Services services, Sort sort)` Checks if the `Sort` is a reference type.
`static boolean`	`hasReferenceSort(Services services, Term term)` Checks if the `Sort` of the given `Term` is a reference type.
`static boolean`	`hasSymbolicExecutionLabel(RuleApp ruleApp)` Checks if the `Term` on which the `RuleApp` was applied contains a `SymbolicExecutionTermLabel`.
`static boolean`	`hasSymbolicExecutionLabel(Term term)` Checks if the given `Term` contains a `SymbolicExecutionTermLabel`.
`static Term`	`improveReadability(Term term, Services services)` Improves the `Term` to increase its readability.
`private static Term`	`improveReadabilityRecursive(Term term, Services services, IntegerLDT integerLDT)` Helper method of `improveReadability(Term, Services)`.
`static void`	`initializeStrategy(SymbolicExecutionTreeBuilder builder)` Initializes the `Proof` of the given `SymbolicExecutionTreeBuilder` so that the correct `Strategy` is used.
`static Term`	`instantiateTerm(Node node, Term term, TacletApp tacletApp, Services services)` Instantiates the given `Term` of the applied `TacletApp`.
`private static void`	`internalCollectAllElementaryUpdateTerms(Services services, java.util.List<IProgramVariable> result, Term term)` Utility method of `collectAllElementaryUpdateTerms(Node)` which collects all `IProgramVariable`s of `ElementaryUpdate`s and static field manipulations.
`private static void`	`internalCollectStaticProgramVariablesOnHeap(Services services, java.util.Set<IProgramVariable> result, Term term)` Utility method of `internalCollectAllElementaryUpdateTerms(Services, List, Term)` which collects static field manipulations on the given heap update.
`static boolean`	`isBaseHeap(Operator op, HeapLDT heapLDT)` Checks if the given `Operator` is the base heap.
`static boolean`	`isBlockContractValidityBranch(PosInOccurrence pio)` Checks if the modality at the given `PosInOccurrence` represents the validity branch of an applied block contract.
`static boolean`	`isBlockContractValidityBranch(RuleApp appliedRuleApp)` Checks if the modality at the applied rule represents the validity branch of an applied block contract.
`static boolean`	`isBlockSpecificationElement(Node node, RuleApp ruleApp)` Checks if the given node should be represented as block/loop contract.
`static boolean`	`isBoolean(Services services, Operator op)` Checks if the given `Operator` is a boolean.
`static boolean`	`isBranchStatement(Node node, RuleApp ruleApp, SourceElement statement, PositionInfo posInfo)` Checks if the given node should be represented as branch statement.
`static boolean`	`isChoiceSettingInitialised()` Checks if the choice settings are initialized.
`static boolean`	`isCloseAfterJoin(RuleApp ruleApp)` Checks if the `CloseAfterMergeRuleBuiltInRuleApp` is applied.
`static boolean`	`isDoWhileLoopCondition(Node node, SourceElement statement)` Checks if the given `SourceElement` is a do while loop.
`static boolean`	`isExceptionalMethodReturnNode(Node node, RuleApp ruleApp)` Checks if the given node should be represented as exceptional method return.
`static boolean`	`isForLoopCondition(Node node, SourceElement statement)` Checks if the given `SourceElement` is a for loop.
`static boolean`	`isHeap(Operator op, HeapLDT heapLDT)` Checks if the given `Operator` is a heap.
`static boolean`	`isHeapUpdate(Services services, Term term)` Checks if the given `Term` represents a heap update, in particular a store or create operation on a heap.
`static boolean`	`isInImplicitMethod(Node node, RuleApp ruleApp)` Checks if the currently executed code is in an implicit method (`IProgramMethod.isImplicit()` is `true`).
`static boolean`	`isJoin(RuleApp ruleApp)` Checks if the `MergeRuleBuiltInRuleApp` is applied.
`static boolean`	`isLoopBodyTermination(Node node, RuleApp ruleApp)` Checks if the given node should be represented as loop body termination.
`static boolean`	`isLoopInvariant(Node node, RuleApp ruleApp)` Checks if the given node should be represented as loop invariant.
`static boolean`	`isLoopStatement(Node node, RuleApp ruleApp, SourceElement statement, PositionInfo posInfo)` Checks if the given node should be represented as loop statement.
`static boolean`	`isMethodCallNode(Node node, RuleApp ruleApp, SourceElement statement)` Checks if the given node should be represented as method call.
`static boolean`	`isMethodCallNode(Node node, RuleApp ruleApp, SourceElement statement, boolean allowImpliciteMethods)` Checks if the given node should be represented as method call.
`static boolean`	`isMethodReturnNode(Node node, RuleApp ruleApp)` Checks if the given node should be represented as method return.
`private static boolean`	`isMinusOne(Term term, IntegerLDT integerLDT)` Checks if the given `Term` represents the integer constant `-1`.
`static boolean`	`isNotImplicit(Services services, IProgramMethod pm)` Checks if the given `IProgramMethod` is not implicit.
`static boolean`	`isNotNull(Node node, Term additionalAntecedent, Term newSuccedent)` Checks if the given `Term` is not null in the `Sequent` of the given `Node`.
`static boolean`	`isNull(Node node, Term additionalAntecedent, Term newSuccedent)` Checks if the given `Term` is null in the `Sequent` of the given `Node`.
`static boolean`	`isNullSort(Sort sort, Services services)` Checks if the given `Sort` represents a `null` value in the given `Services`.
`static boolean`	`isNumber(Operator op)` Checks if the given `Operator` is a number.
`private static boolean`	`isOne(Term subOne, IntegerLDT integerLDT)` Checks if the given term represent the number one
`static boolean`	`isOperationContract(Node node, RuleApp ruleApp)` Checks if the given node should be represented as operation contract.
`static boolean`	`isRuleAppToIgnore(RuleApp ruleApp)` Checks if the given `RuleApp` should be ignored or checked for possible symbolic execution tree node representation.
`static boolean`	`isSelect(Services services, Term term)` Checks if the given `Term` is a select on a heap.
`static boolean`	`isSkolemConstant(Term term)` Checks if the given `Term` is a skolem `Term` meaning that it has the `SelectSkolemConstantTermLabel`.
`static boolean`	`isStatementNode(Node node, RuleApp ruleApp, SourceElement statement, PositionInfo posInfo)` Checks if the given node should be represented as statement.
`static boolean`	`isStaticVariable(IProgramVariable programVariable)` Checks if the given `IProgramVariable` is static or not.
`static boolean`	`isSymbolicExecutionTreeNode(Node node, RuleApp ruleApp)` Checks if the given `Node` in KeY's proof tree represents also a `Node` in a symbolic execution tree.
`static boolean`	`isTerminationNode(Node node, RuleApp ruleApp)` Checks if the given node should be represented as termination.
`static boolean`	`isUsePrettyPrinting()` Checks if pretty printing is enabled or not.
`static boolean`	`isWeakeningGoalEnabled(Proof proof)` Checks if the weakening goal is enabled or not.
`protected static Sequent`	`labelSkolemConstants(Sequent sequent, java.util.Set<Term> constantsToLabel, TermFactory factory)` Labels all specified skolem equalities with the `RESULT_LABEL`.
`static Sort`	`lazyComputeExceptionSort(Node node, IProgramVariable exceptionVariable)` Computes the exception `Sort` lazily when `#getExceptionSort()` is called the first time.
`static boolean`	`lazyComputeIsAdditionalBranchVerified(Node node)` Checks if this branch would be closed without the uninterpreted predicate and thus be treated as valid/closed in a regular proof.
`static boolean`	`lazyComputeIsExceptionalTermination(Node node, IProgramVariable exceptionVariable)` Checks if is an exceptional termination.
`static boolean`	`lazyComputeIsMainBranchVerified(Node node)` Checks if this branch would be closed without the uninterpreted predicate and thus be treated as valid/closed in a regular proof.
`private static ImmutableList<Term>`	`listNewSemisequentTerms(Semisequent parent, Semisequent child)` Lists the `Term`s of all new `SequentFormula` in the child `Semisequent`.
`static ImmutableList<Term>`	`listSemisequentTerms(Semisequent semisequent)` Lists the `Term`s contained in the given `Semisequent`.
`static Term`	`posInOccurrenceInOtherNode(Node original, PosInOccurrence pio, Node toApplyOn)` Returns the `Term` described by the given `PosInOccurrence` of the original `Node` in the `Node` to apply on.
`static Term`	`posInOccurrenceInOtherNode(Sequent original, PosInOccurrence pio, Sequent toApplyOn)` Returns the `Term` described by the given `PosInOccurrence` of the original `Sequent` in the `Sequent` to apply on.
`static PosInOccurrence`	`posInOccurrenceToOtherSequent(Node original, PosInOccurrence pio, Node toApplyTo)` Returns the `PosInOccurrence` described by the given `PosInOccurrence` of the original `Node` in the `Node` to apply too.
`static PosInOccurrence`	`posInOccurrenceToOtherSequent(Sequent original, PosInOccurrence pio, Sequent toApplyTo)` Returns the `PosInOccurrence` described by the given `PosInOccurrence` of the original `Sequent` in the `Sequent` to apply too.
`private static Sequent`	`removeAllUnusedSkolemEqualities(Sequent sequent, java.util.Collection<Term> skolemConstants)` Removes all `SequentFormula`s with a skolem equality from the given `Sequent` if the skolem `Term` is not contained in the given `Collection`.
`private static Sequent`	`removeAllUnusedSkolemEqualities(Sequent sequent, SequentFormula sf, boolean antecedent, java.util.Collection<Term> skolemConstants)` Helper method of `removeAllUnusedSkolemEqualities(Sequent, Collection)` which removes the given `SequentFormula` if required.
`static Term`	`removeLabelRecursive(TermFactory tf, Term term, TermLabel label)` Removes the given `TermLabel` from the given `Term` and from all of its children.
`static Term`	`replaceSkolemConstants(Sequent sequent, Term term, Services services)` Replaces all skolem constants in the given `Term`.
`static SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult`	`searchContractPostOrExcPostExceptionVariable(Node node, Services services)` Searches the used exception variable in the post or exceptional post branch of an applied `ContractRuleApp` on the parent of the given `Node`.
`private static Term`	`searchExceptionDefinition(Term term, Services services)` Searches the exception definition.
`static Term`	`sequentToImplication(Sequent sequent, Services services)` Converts the given `Sequent` into an implication.
`static void`	`setChoiceSetting(java.lang.String key, java.lang.String value)` Sets the default choice value.
`static void`	`setUsePrettyPrinting(boolean usePrettyPrinting)` Defines if pretty printing is enabled or not.
`static Term`	`simplify(InitConfig initConfig, Proof parentProof, Term term)` Simplifies the given `Term` in a side proof.
`static Term`	`simplify(InitConfig initConfig, Term term)` Simplifies the given `Term` in a side proof.
`static Term`	`simplify(Proof parentProof, Term term)` Simplifies the given `Term` in a side proof.
`static void`	`updateStrategySettings(Proof proof, boolean useOperationContracts, boolean useLoopInvariants, boolean nonExecutionBranchHidingSideProofs, boolean aliasChecksImmediately)` Configures the proof to use the given settings.
`static void`	`updateStrategySettings(Proof proof, StrategyProperties sp)` Configures the proof to use the given `StrategyProperties`.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Field Detail
  - CHOICE_SETTING_RUNTIME_EXCEPTIONS
```
public static final java.lang.String CHOICE_SETTING_RUNTIME_EXCEPTIONS
```
    Key for the choice option "runtimeExceptions".
    
    See Also:
    
    Constant Field Values
  - CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_BAN
```
public static final java.lang.String CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_BAN
```
    Value in choice option "runtimeExceptions" to ban exceptions.
    
    See Also:
    
    Constant Field Values
  - CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_ALLOW
```
public static final java.lang.String CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_ALLOW
```
    Value in choice option "runtimeExceptions" to allow exceptions.
    
    See Also:
    
    Constant Field Values
  - RESULT_LABEL_NAME
```
public static final Name RESULT_LABEL_NAME
```
    Name of RESULT_LABEL.
  - RESULT_LABEL
```
public static final TermLabel RESULT_LABEL
```
    Label attached to a Term to evaluate in a side proof.
  - LOOP_BODY_LABEL_NAME
```
public static final Name LOOP_BODY_LABEL_NAME
```
    Name of LOOP_BODY_LABEL.
  - LOOP_BODY_LABEL
```
public static final TermLabel LOOP_BODY_LABEL
```
    Label attached to the modality which executes a loop body in branch "Body Preserves Invariant" of applied "Loop Invariant" rules.
  - LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL_NAME
```
public static final Name LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL_NAME
```
    Name of LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL.
  - LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL
```
public static final TermLabel LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL
```
    Label attached to the implication when a loop body execution terminated normally without any exceptions, returns or breaks in branch "Body Preserves Invariant" of applied "Loop Invariant" rules to show the loop invariant.
- Constructor Detail
  - SymbolicExecutionUtil
```
private SymbolicExecutionUtil()
```
    Forbid instances.
- Method Detail
  - simplify
```
public static Term simplify(InitConfig initConfig,
                            Term term)
                     throws ProofInputException
```
    Simplifies the given Term in a side proof.
    
    Parameters:
    
    initConfig - The InitConfig to use.
    
    term - The Term to simplify.
    
    Returns:
    
    The simplified Term.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - simplify
```
public static Term simplify(Proof parentProof,
                            Term term)
                     throws ProofInputException
```
    Simplifies the given Term in a side proof.
    
    Parameters:
    
    parentProof - The parent Proof.
    
    term - The Term to simplify.
    
    Returns:
    
    The simplified Term.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - simplify
```
public static Term simplify(InitConfig initConfig,
                            Proof parentProof,
                            Term term)
                     throws ProofInputException
```
    Simplifies the given Term in a side proof.
    
    Parameters:
    
    initConfig - The InitConfig to use.
    
    parentProof - The parent Proof which provides the StrategySettings.
    
    term - The Term to simplify.
    
    Returns:
    
    The simplified Term.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - sequentToImplication
```
public static Term sequentToImplication(Sequent sequent,
                                        Services services)
```
    Converts the given Sequent into an implication.
    
    Parameters:
    
    sequent - The Sequent to convert.
    
    services - The Services to use.
    
    Returns:
    
    The created implication.
  - listSemisequentTerms
```
public static ImmutableList<Term> listSemisequentTerms(Semisequent semisequent)
```
    Lists the Terms contained in the given Semisequent.
    
    Parameters:
    
    semisequent - The Semisequent to list terms of.
    
    Returns:
    
    The list with all contained Terms.
  - improveReadability
```
public static Term improveReadability(Term term,
                                      Services services)
```
    Improves the Term to increase its readability. The following changes will be performed:
    - a < 1 + b => a <= b
    - a < b + 1 => a <= b
    - a >= 1 + b => a > b
    - a >= b + 1 => a > b
    - a <= -1 + b => a < b
    - a <= b + -1 => a < b
    - a <= b - 1 => a < b
    - a > -1 + b => a >= b
    - a > b + -1 => a >= b
    - a > b - 1 => a >= b
    - a >= 1 + b => a > b
    - a >= b + 1 => a > b
    - !a >= b => a < b
    - !a > b => a <= b
    - !a <= b => a > b
    - !a < b => a >= b
    Parameters:
    
    term - The Term to improve.
    
    services - The Services to use.
    
    Returns:
    
    The improved Term or the Term itself if no improvements are possible.
  - improveReadabilityRecursive
```
private static Term improveReadabilityRecursive(Term term,
                                                Services services,
                                                IntegerLDT integerLDT)
```
    Helper method of improveReadability(Term, Services).
    
    Parameters:
    
    term - The Term to improve.
    
    services - The Services to use.
    
    integerLDT - The IntegerLDT to use.
    
    Returns:
    
    The improved Term or the Term itself if no improvements are possible.
  - isOne
```
private static boolean isOne(Term subOne,
                             IntegerLDT integerLDT)
```
    Checks if the given term represent the number one
    
    Parameters:
    
    subOne - the term to be checked
    
    integerLDT - the LDT for integers
    
    Returns:
    
    true if the term represents the one
  - isMinusOne
```
private static boolean isMinusOne(Term term,
                                  IntegerLDT integerLDT)
```
    Checks if the given Term represents the integer constant -1.
    
    Parameters:
    
    term - The Term to check.
    
    integerLDT - The IntegerLDT to use.
    
    Returns:
    
    true Term represents -1, false Term is something else.
  - createExtractReturnVariableValueSequent
```
public static SymbolicExecutionUtil.SiteProofVariableValueInput createExtractReturnVariableValueSequent(Services services,
                                                                                                        TypeReference contextObjectType,
                                                                                                        IProgramMethod contextMethod,
                                                                                                        ReferencePrefix contextObject,
                                                                                                        Node methodReturnNode,
                                                                                                        Node methodCallEmptyNode,
                                                                                                        IProgramVariable variable)
```
    Creates a Sequent which can be used in site proofs to extract the return value of the given IProgramVariable from the sequent of the given Node.
    
    Parameters:
    
    services - The Services to use.
    
    contextObjectType - The type of the current object (this reference).
    
    contextMethod - The current method.
    
    contextObject - The current object (this reference).
    
    methodReturnNode - The method return Node which provides the sequent to extract updates and return expression from.
    
    methodCallEmptyNode - The method call empty Node which provides the sequent to start site proof in.
    
    variable - The IProgramVariable of the value which is interested.
    
    Returns:
    
    The created SymbolicExecutionUtil.SiteProofVariableValueInput with the created sequent and the predicate which will contain the value.
  - createExtractReturnVariableValueSequent
```
public static SymbolicExecutionUtil.SiteProofVariableValueInput createExtractReturnVariableValueSequent(Services services,
                                                                                                        IExecutionContext context,
                                                                                                        Node methodReturnNode,
                                                                                                        Node methodCallEmptyNode,
                                                                                                        IProgramVariable variable)
```
    Creates a Sequent which can be used in site proofs to extract the return value of the given IProgramVariable from the sequent of the given Node.
    
    Parameters:
    
    services - The Services to use.
    
    context - The IExecutionContext that defines the current object (this reference).
    
    methodReturnNode - The method return Node which provides the sequent to extract updates and return expression from.
    
    methodCallEmptyNode - The method call empty Node which provides the sequent to start site proof in.
    
    variable - The IProgramVariable of the value which is interested.
    
    Returns:
    
    The created SymbolicExecutionUtil.SiteProofVariableValueInput with the created sequent and the predicate which will contain the value.
  - createExtractVariableValueSequent
```
public static SymbolicExecutionUtil.SiteProofVariableValueInput createExtractVariableValueSequent(Services services,
                                                                                                  Node node,
                                                                                                  PosInOccurrence pio,
                                                                                                  Term additionalConditions,
                                                                                                  IProgramVariable variable)
```
    Creates a Sequent which can be used in site proofs to extract the value of the given IProgramVariable from the sequent of the given Node.
    
    Parameters:
    
    services - The Services to use.
    
    node - The original Node which provides the sequent to extract from.
    
    pio - The PosInOccurrence of the SE modality.
    
    additionalConditions - Optional additional conditions.
    
    variable - The IProgramVariable of the value which is interested.
    
    Returns:
    
    The created SymbolicExecutionUtil.SiteProofVariableValueInput with the created sequent and the predicate which will contain the value.
  - createExtractTermSequent
```
public static SymbolicExecutionUtil.SiteProofVariableValueInput createExtractTermSequent(Services sideProofServices,
                                                                                         Node node,
                                                                                         PosInOccurrence pio,
                                                                                         Term additionalConditions,
                                                                                         Term term,
                                                                                         boolean keepUpdates)
```
    Creates a Sequent which can be used in site proofs to extract the value of the given IProgramVariable from the sequent of the given Node.
    
    Parameters:
    
    sideProofServices - The Services of the side proof to use.
    
    node - The original Node which provides the sequent to extract from.
    
    pio - The PosInOccurrence of the modality or its updates.
    
    additionalConditions - Additional conditions to add to the antecedent.
    
    term - The new succedent term.
    
    keepUpdates - true keep updates, false throw updates away.
    
    Returns:
    
    The created SymbolicExecutionUtil.SiteProofVariableValueInput with the created sequent and the predicate which will contain the value.
  - isHeapUpdate
```
public static boolean isHeapUpdate(Services services,
                                   Term term)
```
    Checks if the given Term represents a heap update, in particular a store or create operation on a heap.
    
    Parameters:
    
    services - The Services to use.
    
    term - The Term to check.
    
    Returns:
    
    true is heap update, false is something else.
  - canComputeVariables
```
public static boolean canComputeVariables(IExecutionNode<?> node,
                                          Services services)
                                   throws ProofInputException
```
    Checks if it is right now possible to compute the variables of the given IExecutionNode via IExecutionNode.getVariables().
    
    Parameters:
    
    node - The IExecutionNode to check.
    
    services - The Services to use.
    
    Returns:
    
    true right now it is possible to compute variables, false it is not possible to compute variables.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - createExecutionConstraints
```
public static IExecutionConstraint[] createExecutionConstraints(IExecutionNode<?> node)
```
    Creates for the given IExecutionNode the contained IExecutionConstraints.
    
    Parameters:
    
    node - The IExecutionNode to create constraints for.
    
    Returns:
    
    The created IExecutionConstraints.
  - containsSymbolicExecutionLabel
```
public static boolean containsSymbolicExecutionLabel(Term term)
```
    Checks if the Term or one of its sub terms contains a symbolic execution label.
    
    Parameters:
    
    term - The Term to check.
    
    Returns:
    
    true SE label is somewhere contained, false SE label is not contained at all.
  - createExecutionVariables
```
public static IExecutionVariable[] createExecutionVariables(IExecutionNode<?> node)
                                                     throws ProofInputException
```
    Creates for the given IExecutionNode the contained root IExecutionVariables.
    
    Parameters:
    
    node - The IExecutionNode to create variables for.
    
    Returns:
    
    The created IExecutionVariables.
    
    Throws:
    
    ProofInputException
  - createExecutionVariables
```
public static IExecutionVariable[] createExecutionVariables(IExecutionNode<?> node,
                                                            Term condition)
                                                     throws ProofInputException
```
    Creates for the given IExecutionNode the contained root IExecutionVariables.
    
    Parameters:
    
    node - The IExecutionNode to create variables for.
    
    condition - A Term specifying some additional constraints to consider.
    
    Returns:
    
    The created IExecutionVariables.
    
    Throws:
    
    ProofInputException
  - createExecutionVariables
```
public static IExecutionVariable[] createExecutionVariables(IExecutionNode<?> node,
                                                            Node proofNode,
                                                            PosInOccurrence modalityPIO,
                                                            Term condition)
                                                     throws ProofInputException
```
    Creates for the given IExecutionNode the contained root IExecutionVariables.
    
    Parameters:
    
    node - The IExecutionNode to create variables for.
    
    proofNode - The proof Node to work with.
    
    modalityPIO - The PosInOccurrence of the modality of interest.
    
    condition - A Term specifying some additional constraints to consider.
    
    Returns:
    
    The created IExecutionVariables.
    
    Throws:
    
    ProofInputException
  - createAllExecutionVariables
```
public static IExecutionVariable[] createAllExecutionVariables(IExecutionNode<?> node,
                                                               Node proofNode,
                                                               PosInOccurrence modalityPIO,
                                                               Term condition)
```
    Creates for the given IExecutionNode the contained root IExecutionVariables.
    
    Parameters:
    
    node - The IExecutionNode to create variables for.
    
    proofNode - The proof Node to work with.
    
    modalityPIO - The PosInOccurrence of the modality of interest.
    
    condition - A Term specifying some additional constraints to consider.
    
    Returns:
    
    The created IExecutionVariables.
  - collectAllElementaryUpdateTerms
```
public static java.util.List<IProgramVariable> collectAllElementaryUpdateTerms(Node node)
```
    Collects all IProgramVariable used in ElementaryUpdates.
    
    Parameters:
    
    node - The Node to search in.
    
    Returns:
    
    The found IProgramVariable which are used in ElementaryUpdates.
  - internalCollectAllElementaryUpdateTerms
```
private static void internalCollectAllElementaryUpdateTerms(Services services,
                                                            java.util.List<IProgramVariable> result,
                                                            Term term)
```
    Utility method of collectAllElementaryUpdateTerms(Node) which collects all IProgramVariables of ElementaryUpdates and static field manipulations.
    
    Parameters:
    
    services - The Services to use.
    
    result - The result List to fill.
    
    term - The current term to analyze.
  - internalCollectStaticProgramVariablesOnHeap
```
private static void internalCollectStaticProgramVariablesOnHeap(Services services,
                                                                java.util.Set<IProgramVariable> result,
                                                                Term term)
```
    Utility method of internalCollectAllElementaryUpdateTerms(Services, List, Term) which collects static field manipulations on the given heap update.
    
    Parameters:
    
    services - The Services to use.
    
    result - The result List to fill.
    
    term - The current term to analyze.
  - findInnerMostSelect
```
private static Term findInnerMostSelect(Term term,
                                        Services services)
```
  - getProgramVariable
```
public static ProgramVariable getProgramVariable(Services services,
                                                 HeapLDT heapLDT,
                                                 Term locationTerm)
```
    Returns the ProgramVariable defined by the given Term.
    
    Parameters:
    
    services - The Services to use.
    
    heapLDT - The HeapLDT to use.
    
    locationTerm - The Term to extract ProgramVariable from.
    
    Returns:
    
    The Terms ProgramVariable or null if not available.
  - getArrayIndex
```
public static Term getArrayIndex(Services services,
                                 HeapLDT heapLDT,
                                 Term arrayIndexTerm)
```
    Returns the array index defined by the given Term.
    
    Parameters:
    
    services - The Services to use.
    
    heapLDT - The HeapLDT to use.
    
    arrayIndexTerm - The Term to extract the array index from.
    
    Returns:
    
    The array index or null if the term defines no array index.
  - findSelfTerm
```
public static IProgramVariable findSelfTerm(Node node,
                                            PosInOccurrence pio)
```
    Searches the IProgramVariable of the current this/self reference.
    
    Parameters:
    
    node - The Node to search in.
    
    pio - The PosInOccurrence describing the location of the modality of interest.
    
    Returns:
    
    The found IProgramVariable with the current this/self reference or null if no one is available.
  - isMethodCallNode
```
public static boolean isMethodCallNode(Node node,
                                       RuleApp ruleApp,
                                       SourceElement statement)
```
    Checks if the given node should be represented as method call.
    
    Parameters:
    
    node - The current Node in the proof tree of KeY.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    statement - The statement (SourceElement).
    
    Returns:
    
    true represent node as method call, false represent node as something else.
  - isMethodCallNode
```
public static boolean isMethodCallNode(Node node,
                                       RuleApp ruleApp,
                                       SourceElement statement,
                                       boolean allowImpliciteMethods)
```
    Checks if the given node should be represented as method call.
    
    Parameters:
    
    node - The current Node in the proof tree of KeY.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    statement - The statement (SourceElement).
    
    allowImpliciteMethods - true implicit methods are included, false implicit methods are outfiltered.
    
    Returns:
    
    true represent node as method call, false represent node as something else.
  - isNotImplicit
```
public static boolean isNotImplicit(Services services,
                                    IProgramMethod pm)
```
    Checks if the given IProgramMethod is not implicit.
    
    Parameters:
    
    services - The Services to use.
    
    pm - The IProgramMethod to check.
    
    Returns:
    
    true is not implicit, false is implicit
  - isBranchStatement
```
public static boolean isBranchStatement(Node node,
                                        RuleApp ruleApp,
                                        SourceElement statement,
                                        PositionInfo posInfo)
```
    Checks if the given node should be represented as branch statement.
    
    Parameters:
    
    node - The current Node in the proof tree of KeY.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    statement - The statement (SourceElement).
    
    posInfo - The PositionInfo.
    
    Returns:
    
    true represent node as branch statement, false represent node as something else.
  - isLoopStatement
```
public static boolean isLoopStatement(Node node,
                                      RuleApp ruleApp,
                                      SourceElement statement,
                                      PositionInfo posInfo)
```
    Checks if the given node should be represented as loop statement.
    
    Parameters:
    
    node - The current Node in the proof tree of KeY.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    statement - The statement (SourceElement).
    
    posInfo - The PositionInfo.
    
    Returns:
    
    true represent node as loop statement, false represent node as something else.
  - isStatementNode
```
public static boolean isStatementNode(Node node,
                                      RuleApp ruleApp,
                                      SourceElement statement,
                                      PositionInfo posInfo)
```
    Checks if the given node should be represented as statement.
    
    Parameters:
    
    node - The current Node in the proof tree of KeY.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    statement - The statement (SourceElement).
    
    posInfo - The PositionInfo.
    
    Returns:
    
    true represent node as statement, false represent node as something else.
  - isTerminationNode
```
public static boolean isTerminationNode(Node node,
                                        RuleApp ruleApp)
```
    Checks if the given node should be represented as termination.
    
    Parameters:
    
    node - The current Node in the proof tree of KeY.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    Returns:
    
    true represent node as termination, false represent node as something else.
  - isOperationContract
```
public static boolean isOperationContract(Node node,
                                          RuleApp ruleApp)
```
    Checks if the given node should be represented as operation contract.
    
    Parameters:
    
    node - The current Node in the proof tree of KeY.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    Returns:
    
    true represent node as operation contract, false represent node as something else.
  - isBlockSpecificationElement
```
public static boolean isBlockSpecificationElement(Node node,
                                                  RuleApp ruleApp)
```
    Checks if the given node should be represented as block/loop contract.
    
    Parameters:
    
    node - The current Node in the proof tree of KeY.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    Returns:
    
    true represent node as block contract, false represent node as something else.
  - isLoopInvariant
```
public static boolean isLoopInvariant(Node node,
                                      RuleApp ruleApp)
```
    Checks if the given node should be represented as loop invariant.
    
    Parameters:
    
    node - The current Node in the proof tree of KeY.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    Returns:
    
    true represent node as use loop invariant, false represent node as something else.
  - isMethodReturnNode
```
public static boolean isMethodReturnNode(Node node,
                                         RuleApp ruleApp)
```
    Checks if the given node should be represented as method return.
    
    Parameters:
    
    node - The current Node in the proof tree of KeY.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    Returns:
    
    true represent node as method return, false represent node as something else.
  - isExceptionalMethodReturnNode
```
public static boolean isExceptionalMethodReturnNode(Node node,
                                                    RuleApp ruleApp)
```
    Checks if the given node should be represented as exceptional method return.
    
    Parameters:
    
    node - The current Node in the proof tree of KeY.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    Returns:
    
    true represent node as exceptional method return, false represent node as something else.
  - hasLoopCondition
```
public static boolean hasLoopCondition(Node node,
                                       RuleApp ruleApp,
                                       SourceElement statement)
```
    Checks if the given Node has a loop condition.
    
    Parameters:
    
    node - The Node to check.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    statement - The actual statement (SourceElement).
    
    Returns:
    
    true has loop condition, false has no loop condition.
  - hasLoopBodyLabel
```
public static boolean hasLoopBodyLabel(RuleApp ruleApp)
```
    Checks if the Term on which the RuleApp was applied contains a SymbolicExecutionTermLabel.
    
    Parameters:
    
    ruleApp - The RuleApp to check.
    
    Returns:
    
    true contains a SymbolicExecutionTermLabel, false does not contain a SymbolicExecutionTermLabel or the given RuleApp is null.
  - hasLoopBodyTerminationLabel
```
public static boolean hasLoopBodyTerminationLabel(RuleApp ruleApp)
```
    Checks if the Term on which the RuleApp was applied contains a SymbolicExecutionTermLabel.
    
    Parameters:
    
    ruleApp - The RuleApp to check.
    
    Returns:
    
    true contains a SymbolicExecutionTermLabel, false does not contain a SymbolicExecutionTermLabel or the given RuleApp is null.
  - hasSymbolicExecutionLabel
```
public static boolean hasSymbolicExecutionLabel(RuleApp ruleApp)
```
    Checks if the Term on which the RuleApp was applied contains a SymbolicExecutionTermLabel.
    
    Parameters:
    
    ruleApp - The RuleApp to check.
    
    Returns:
    
    true contains a SymbolicExecutionTermLabel, false does not contain a SymbolicExecutionTermLabel or the given RuleApp is null.
  - getSymbolicExecutionLabel
```
public static SymbolicExecutionTermLabel getSymbolicExecutionLabel(RuleApp ruleApp)
```
    Returns the contained SymbolicExecutionTermLabel if available.
    
    Parameters:
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    Returns:
    
    The first found SymbolicExecutionTermLabel or null if no SymbolicExecutionTermLabel is provided.
  - hasSymbolicExecutionLabel
```
public static boolean hasSymbolicExecutionLabel(Term term)
```
    Checks if the given Term contains a SymbolicExecutionTermLabel.
    
    Parameters:
    
    term - The Term to check.
    
    Returns:
    
    true contains a SymbolicExecutionTermLabel, false does not contain a SymbolicExecutionTermLabel or the given Term is null.
  - getSymbolicExecutionLabel
```
public static SymbolicExecutionTermLabel getSymbolicExecutionLabel(Term term)
```
    Returns the contained SymbolicExecutionTermLabel if available.
    
    Parameters:
    
    term - The Term to search in.
    
    Returns:
    
    The first found SymbolicExecutionTermLabel or null if no SymbolicExecutionTermLabel is provided.
  - findModalityWithMaxSymbolicExecutionLabelId
```
public static PosInOccurrence findModalityWithMaxSymbolicExecutionLabelId(Sequent sequent)
```
    Searches the modality PosInOccurrence with the maximal SymbolicExecutionTermLabel ID SymbolicExecutionTermLabel.getId() in the given Sequent.
    
    Parameters:
    
    sequent - The Sequent to search in.
    
    Returns:
    
    The modality PosInOccurrence with the maximal ID if available or null otherwise.
  - findModalityWithMaxSymbolicExecutionLabelId
```
public static PosInOccurrence findModalityWithMaxSymbolicExecutionLabelId(Semisequent semisequent,
                                                                          boolean inAntec)
```
    Searches the modality Term with the maximal SymbolicExecutionTermLabel ID SymbolicExecutionTermLabel.getId() in the given Semisequent.
    
    Parameters:
    
    semisequent - The Semisequent to search in.
    
    inAntec - true antecedent, false succedent.
    
    Returns:
    
    The modality Term with the maximal ID if available or null otherwise.
  - findModalityWithMaxSymbolicExecutionLabelId
```
public static PosInTerm findModalityWithMaxSymbolicExecutionLabelId(Term term)
```
    Searches the modality PosInTerm with the maximal SymbolicExecutionTermLabel ID SymbolicExecutionTermLabel.getId() in the given Term.
    
    Parameters:
    
    term - The Term to search in.
    
    Returns:
    
    The modality PosInTerm with the maximal ID if available or null otherwise.
  - findModalityWithMinSymbolicExecutionLabelId
```
public static PosInOccurrence findModalityWithMinSymbolicExecutionLabelId(Sequent sequent)
```
    Searches the modality PosInOccurrence with the minimal SymbolicExecutionTermLabel ID SymbolicExecutionTermLabel.getId() in the given Sequent.
    
    Parameters:
    
    sequent - The Sequent to search in.
    
    Returns:
    
    The modality PosInOccurrence with the maximal ID if available or null otherwise.
  - findModalityWithMinSymbolicExecutionLabelId
```
public static PosInOccurrence findModalityWithMinSymbolicExecutionLabelId(Semisequent semisequent,
                                                                          boolean inAntec)
```
    Searches the modality PosInOccurrence with the minimal SymbolicExecutionTermLabel ID SymbolicExecutionTermLabel.getId() in the given Semisequent.
    
    Parameters:
    
    semisequent - The Semisequent to search in.
    
    inAntec - true antecedent, false succedent.
    
    Returns:
    
    The modality PosInOccurrence with the minimal ID if available or null otherwise.
  - findModalityWithMinSymbolicExecutionLabelId
```
public static PosInTerm findModalityWithMinSymbolicExecutionLabelId(Term term)
```
    Searches the modality PosInTerm with the minimal SymbolicExecutionTermLabel ID SymbolicExecutionTermLabel.getId() in the given Term.
    
    Parameters:
    
    term - The Term to search in.
    
    Returns:
    
    The modality PosInTerm with the maximal ID if available or null otherwise.
  - isSymbolicExecutionTreeNode
```
public static boolean isSymbolicExecutionTreeNode(Node node,
                                                  RuleApp ruleApp)
```
    Checks if the given Node in KeY's proof tree represents also a Node in a symbolic execution tree.
    
    Parameters:
    
    node - The Node of KeY's proof tree to check.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    Returns:
    
    true is also symbolic execution tree node, false is no node in a symbolic execution tree.
  - isRuleAppToIgnore
```
public static boolean isRuleAppToIgnore(RuleApp ruleApp)
```
    Checks if the given RuleApp should be ignored or checked for possible symbolic execution tree node representation.
    
    Parameters:
    
    ruleApp - The RuleApp to check.
    
    Returns:
    
    true ignore RuleApp, false check if the RuleApp represents a symbolic execution tree node.
  - isInImplicitMethod
```
public static boolean isInImplicitMethod(Node node,
                                         RuleApp ruleApp)
```
    Checks if the currently executed code is in an implicit method (IProgramMethod.isImplicit() is true).
    
    Parameters:
    
    node - The Node of KeY's proof tree to check.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    Returns:
    
    true is in implicit method, false is not in implicit method.
  - computeStackSize
```
public static int computeStackSize(RuleApp ruleApp)
```
    Compute the stack size of the given Term described by the given RuleApp.
    
    Parameters:
    
    ruleApp - The RuleApp which defines the Term to compute its stack size.
    
    Returns:
    
    The stack size.
  - isDoWhileLoopCondition
```
public static boolean isDoWhileLoopCondition(Node node,
                                             SourceElement statement)
```
    Checks if the given SourceElement is a do while loop.
    
    Parameters:
    
    node - The Node to check.
    
    statement - The actual statement (SourceElement).
    
    Returns:
    
    true is do while loop, false is something else.
  - isForLoopCondition
```
public static boolean isForLoopCondition(Node node,
                                         SourceElement statement)
```
    Checks if the given SourceElement is a for loop.
    
    Parameters:
    
    node - The Node to check.
    
    statement - The actual statement (SourceElement).
    
    Returns:
    
    true is for loop, false is something else.
  - collectGoalsInSubtree
```
public static ImmutableList<Goal> collectGoalsInSubtree(IExecutionElement executionElement)
```
    Collects all Goals in the subtree of the given IExecutionElement.
    
    Parameters:
    
    executionElement - The IExecutionElement to collect Goals in.
    
    Returns:
    
    The found Goals.
  - collectGoalsInSubtree
```
public static ImmutableList<Goal> collectGoalsInSubtree(Node node)
```
    Collects all Goals in the subtree of the given Node.
    
    Parameters:
    
    node - The Node to collect Goals in.
    
    Returns:
    
    The found Goals.
  - findMethodCallNode
```
public static Node findMethodCallNode(Node node,
                                      PosInOccurrence pio)
```
    Searches for the given Node the parent node which also represents a symbolic execution tree node (checked via isSymbolicExecutionTreeNode(Node, RuleApp)).
    
    Parameters:
    
    node - The Node to start search in.
    
    pio - The PosInOccurrence of the modality.
    
    Returns:
    
    The parent Node of the given Node which is also a set node or null if no parent node was found.
  - findParentSetNode
```
public static Node findParentSetNode(Node node)
```
    Searches for the given Node the parent node which also represents a symbolic execution tree node (checked via isSymbolicExecutionTreeNode(Node, RuleApp)).
    
    Parameters:
    
    node - The Node to start search in.
    
    Returns:
    
    The parent Node of the given Node which is also a set node or null if no parent node was found.
  - computeBranchCondition
```
public static Term computeBranchCondition(Node node,
                                          boolean simplify,
                                          boolean improveReadability)
                                   throws ProofInputException
```
    Computes the branch condition of the given Node.
    
    Parameters:
    
    node - The Node to compute its branch condition.
    
    simplify - true simplify condition in a side proof, false do not simplify condition.
    
    improveReadability - true improve readability, false do not improve readability.
    
    Returns:
    
    The computed branch condition.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - computeContractRuleAppBranchCondition
```
private static Term computeContractRuleAppBranchCondition(Node parent,
                                                          Node node,
                                                          boolean simplify,
                                                          boolean improveReadability)
                                                   throws ProofInputException
```
    Computes the branch condition of the given Node which was constructed by a ContractRuleApp.
    
    The branch conditions are:
    - Post: caller != null & exc_0 = null & (pre1 | .. | preN)
    - ExcPost: caller != null & exc_0 != null & (excPre1 | ... | excPreM)
    - Pre: caller != null & !(pre1 | ... | preN | excPre1 | ... | excPreM) because the branch is only open if all conditions are false
    - NPE: caller = null
    Idea:
    - Last semisequent in antecedent contains contract
    - Contract is defined as exc_0 = null and pre -> post/excPre -> !exc_0 = null & signals terms
    - Find exc_0 = null Term
    - List all implications
    - Filter implications for post/exceptional post branch based on the negation of exc_0 = null
    - Return disjunction of all filtered implication conditions or return true if no implications were found
    Parameters:
    
    parent - The parent Node of the given one.
    
    node - The Node to compute its branch condition.
    
    simplify - true simplify condition in a side proof, false do not simplify condition.
    
    improveReadability - true improve readability, false do not improve readability.
    
    Returns:
    
    The computed branch condition.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - collectContractPreconditions
```
private static void collectContractPreconditions(Services services,
                                                 SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult search,
                                                 java.util.List<Term> normalConditions,
                                                 java.util.List<Term> exceptinalConditions)
                                          throws ProofInputException
```
    Collects the preconditions of an applied operation contract.
    
    Parameters:
    
    services - The Services to use.
    
    search - The SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult.
    
    normalConditions - The List with the normal case conditions to fill.
    
    exceptinalConditions - The List with the exceptional case conditions to fill.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - collectSpecifcationCasesPreconditions
```
private static void collectSpecifcationCasesPreconditions(Term normalExcDefinition,
                                                          Term exceptionalExcDefinition,
                                                          Term term,
                                                          java.util.List<Term> normalConditions,
                                                          java.util.List<Term> exceptinalConditions)
                                                   throws ProofInputException
```
    Collects recursively the preconditions of specification cases.
    
    Parameters:
    
    normalExcDefinition - The normal exception equality.
    
    exceptionalExcDefinition - The exceptional equality.
    
    term - The current Term.
    
    normalConditions - The List with the normal case conditions to fill.
    
    exceptinalConditions - The List with the exceptional case conditions to fill.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - searchContractPostOrExcPostExceptionVariable
```
public static SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult searchContractPostOrExcPostExceptionVariable(Node node,
                                                                                                                              Services services)
                                                                                                                       throws ProofInputException
```
    Searches the used exception variable in the post or exceptional post branch of an applied ContractRuleApp on the parent of the given Node.
    
    Parameters:
    
    node - The Node which is the post or exceptional post branch of an applied ContractRuleApp.
    
    services - The Services to use.
    
    Returns:
    
    The result.
    
    Throws:
    
    ProofInputException - Occurred exception if something is not as expected.
  - searchExceptionDefinition
```
private static Term searchExceptionDefinition(Term term,
                                              Services services)
```
    Searches the exception definition.
    
    Parameters:
    
    term - The Term to start search in.
    
    services - the Services to use.
    
    Returns:
    
    The found exception definition or null if not available.
  - computeLoopInvariantBuiltInRuleAppBranchCondition
```
private static Term computeLoopInvariantBuiltInRuleAppBranchCondition(Node parent,
                                                                      Node node,
                                                                      boolean simplify,
                                                                      boolean improveReadability)
                                                               throws ProofInputException
```
    Computes the branch condition of the given Node which was constructed by a LoopInvariantBuiltInRuleApp.
    
    The branch conditions are:
    - Preserves Branch: Invariant + LoopCondition
    - Use Branch: Invariant + !LoopCondition
    Parameters:
    
    parent - The parent Node of the given one.
    
    node - The Node to compute its branch condition.
    
    simplify - true simplify condition in a side proof, false do not simplify condition.
    
    improveReadability - true improve readability, false do not improve readability.
    
    Returns:
    
    The computed branch condition.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - computeBlockContractBuiltInRuleAppBranchCondition
```
private static Term computeBlockContractBuiltInRuleAppBranchCondition(Node parent,
                                                                      Node node,
                                                                      boolean simplify,
                                                                      boolean improveReadability)
                                                               throws ProofInputException
```
    Computes the branch condition of the given Node which was constructed by an AbstractBlockContractBuiltInRuleApp.
    
    The branch conditions are:
    - Validity: true
    - Usage: Postcondition (added antecedent top level formula)
    Parameters:
    
    parent - The parent Node of the given one.
    
    node - The Node to compute its branch condition.
    
    simplify - true simplify condition in a side proof, false do not simplify condition.
    
    improveReadability - true improve readability, false do not improve readability.
    
    Returns:
    
    The computed branch condition.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - posInOccurrenceInOtherNode
```
public static Term posInOccurrenceInOtherNode(Node original,
                                              PosInOccurrence pio,
                                              Node toApplyOn)
```
    Returns the Term described by the given PosInOccurrence of the original Node in the Node to apply on.
    
    Parameters:
    
    original - The original Node on which the given PosInOccurrence works.
    
    pio - The given PosInOccurrence.
    
    toApplyOn - The new Node to apply the PosInOccurrence on.
    
    Returns:
    
    The Term in the other Node described by the PosInOccurrence or null if not available.
  - posInOccurrenceInOtherNode
```
public static Term posInOccurrenceInOtherNode(Sequent original,
                                              PosInOccurrence pio,
                                              Sequent toApplyOn)
```
    Returns the Term described by the given PosInOccurrence of the original Sequent in the Sequent to apply on.
    
    Parameters:
    
    original - The original Sequent on which the given PosInOccurrence works.
    
    pio - The given PosInOccurrence.
    
    toApplyOn - The new Sequent to apply the PosInOccurrence on.
    
    Returns:
    
    The Term in the other Sequent described by the PosInOccurrence or null if not available.
  - posInOccurrenceToOtherSequent
```
public static PosInOccurrence posInOccurrenceToOtherSequent(Node original,
                                                            PosInOccurrence pio,
                                                            Node toApplyTo)
```
    Returns the PosInOccurrence described by the given PosInOccurrence of the original Node in the Node to apply too.
    
    Parameters:
    
    original - The original Node on which the given PosInOccurrence works.
    
    pio - The given PosInOccurrence.
    
    toApplyTo - The new Node to apply the PosInOccurrence to.
    
    Returns:
    
    The PosInOccurrence in the other Node described by the PosInOccurrence or null if not available.
  - posInOccurrenceToOtherSequent
```
public static PosInOccurrence posInOccurrenceToOtherSequent(Sequent original,
                                                            PosInOccurrence pio,
                                                            Sequent toApplyTo)
```
    Returns the PosInOccurrence described by the given PosInOccurrence of the original Sequent in the Sequent to apply too.
    
    Parameters:
    
    original - The original Sequent on which the given PosInOccurrence works.
    
    pio - The given PosInOccurrence.
    
    toApplyTo - The new Sequent to apply the PosInOccurrence to.
    
    Returns:
    
    The PosInOccurrence in the other Sequent described by the PosInOccurrence or null if not available.
  - computeTacletAppBranchCondition
```
private static Term computeTacletAppBranchCondition(Node parent,
                                                    Node node,
                                                    boolean simplify,
                                                    boolean improveReadability)
                                             throws ProofInputException
```
    Computes the branch condition of the given Node which was constructed by a TacletApp.
    
    Parameters:
    
    parent - The parent Node of the given one.
    
    node - The Node to compute its branch condition.
    
    simplify - true simplify condition in a side proof, false do not simplify condition.
    
    improveReadability - true improve readability, false do not improve readability.
    
    Returns:
    
    The computed branch condition.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - listNewSemisequentTerms
```
private static ImmutableList<Term> listNewSemisequentTerms(Semisequent parent,
                                                           Semisequent child)
```
    Lists the Terms of all new SequentFormula in the child Semisequent.
    
    Parameters:
    
    parent - The parent Semisequent.
    
    child - The child Semisequent.
    
    Returns:
    
    An ImmutableList with all new Terms.
  - findReplacement
```
private static Term findReplacement(Semisequent semisequent,
                                    PosInOccurrence posInOccurrence,
                                    Term replaceTerm)
```
    Searches the by Rule application instantiated replace Term which is equal modulo labels to the given replace Term.
    
    Parameters:
    
    terms - The available candidates created by Rule application.
    
    posInOccurrence - The PosInOccurrence on which the rule was applied.
    
    replaceTerm - The Term to find.
    
    Returns:
    
    The found Term or null if not available.
  - checkReplaceTerm
```
private static boolean checkReplaceTerm(Term toCheck,
                                        PosInOccurrence posInOccurrence,
                                        Term replaceTerm)
```
    Checks if the given replace Term is equal module labels to the Term to check.
    
    Parameters:
    
    toCheck - The Term to check.
    
    posInOccurrence - The PosInOccurrence of the Rule application.
    
    replaceTerm - The Term to compare with.
    
    Returns:
    
    true equal modulo labels, false not equal at all.
  - followPosInOccurrence
```
public static Term followPosInOccurrence(PosInOccurrence posInOccurrence,
                                         Term term)
```
    Returns the sub Term at the given PosInOccurrence but on the given Term instead of the one contained in the PosInOccurrence.
    
    Parameters:
    
    posInOccurrence - The PosInOccurrence which defines the sub term position.
    
    term - The Term to work with.
    
    Returns:
    
    The found sub Term or null if the PosInOccurrence is not compatible.
  - instantiateTerm
```
public static Term instantiateTerm(Node node,
                                   Term term,
                                   TacletApp tacletApp,
                                   Services services)
```
    Instantiates the given Term of the applied TacletApp.
    
    Parameters:
    
    node - The current Node.
    
    term - The Term to instantiate.
    
    tacletApp - The TacletApp to consider.
    
    services - The Services to use.
    
    Returns:
    
    The instantiated Term or null if no Term was given.
  - evaluateInSideProof
```
private static Term evaluateInSideProof(Services services,
                                        Proof proof,
                                        ProofEnvironment sideProofEnvironment,
                                        Sequent sequentToProve,
                                        TermLabel label,
                                        java.lang.String description,
                                        java.lang.String splittingOption)
                                 throws ProofInputException
```
    Starts the side proof and evaluates the Sequent to prove into a single Term.
    
    Parameters:
    
    services - The Services to use.
    
    proof - The Proof from on which the side proof si performed.
    
    sequentToProve - The Sequent to prove in a side proof.
    
    label - The TermLabel which is used to compute the result.
    
    description - The side proof description.
    
    splittingOption - The splitting options to use.
    
    Returns:
    
    The result Term.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - getChoiceSetting
```
public static java.lang.String getChoiceSetting(java.lang.String key)
```
    Returns the default choice value. Attention: This method returns null if it is called before a proof is instantiated the first time. It can be checked via isChoiceSettingInitialised().
    
    Parameters:
    
    key - The choice key.
    
    Returns:
    
    The choice value.
  - setChoiceSetting
```
public static void setChoiceSetting(java.lang.String key,
                                    java.lang.String value)
```
    Sets the default choice value. Attention: Settings should not be changed before the first proof is instantiated in KeY. Otherwise the default settings are not loaded. If default settings are defined can be checked via isChoiceSettingInitialised().
    
    Parameters:
    
    key - The choice key to modify.
    
    value - The new choice value to set.
  - isNull
```
public static boolean isNull(Node node,
                             Term additionalAntecedent,
                             Term newSuccedent)
                      throws ProofInputException
```
    Checks if the given Term is null in the Sequent of the given Node.
    
    Parameters:
    
    node - The Node which provides the original Sequent
    
    additionalAntecedent - An additional antecedent.
    
    newSuccedent - The Term to check.
    
    Returns:
    
    true Term was evaluated to null, false Term was not evaluated to null.
    
    Throws:
    
    ProofInputException - Occurred Exception
  - isNotNull
```
public static boolean isNotNull(Node node,
                                Term additionalAntecedent,
                                Term newSuccedent)
                         throws ProofInputException
```
    Checks if the given Term is not null in the Sequent of the given Node.
    
    Parameters:
    
    node - The Node which provides the original Sequent
    
    additionalAntecedent - An additional antecedent.
    
    newSuccedent - The Term to check.
    
    Returns:
    
    true Term was evaluated to not null, false Term was not evaluated to not null.
    
    Throws:
    
    ProofInputException - Occurred Exception
  - checkNull
```
private static boolean checkNull(Node node,
                                 Term additionalAntecedent,
                                 Term newSuccedent,
                                 boolean nullExpected)
                          throws ProofInputException
```
    Checks if the given Term is null or not in the Sequent of the given Node.
    
    Parameters:
    
    node - The Node which provides the original Sequent
    
    additionalAntecedent - An additional antecedent.
    
    newSuccedent - The Term to check.
    
    nullExpected - true expect that Term is null, false expect that term is not null.
    
    Returns:
    
    true term is null value matches the expected nullExpected value, false otherwise.
    
    Throws:
    
    ProofInputException - Occurred Exception
  - createSequentToProveWithNewSuccedent
```
public static Sequent createSequentToProveWithNewSuccedent(Node node,
                                                           PosInOccurrence pio,
                                                           Term newSuccedent)
```
    Creates a new Sequent which is a modification from the Sequent of the given Node which contains the same information but a different succedent.
    
    Parameters:
    
    node - The Node which provides the original Sequent.
    
    newSuccedent - The new succedent.
    
    Returns:
    
    The created Sequent.
  - createSequentToProveWithNewSuccedent
```
public static Sequent createSequentToProveWithNewSuccedent(Node node,
                                                           Term additionalAntecedent,
                                                           Term newSuccedent,
                                                           boolean addResultLabel)
```
    Creates a new Sequent which is a modification from the Sequent of the given Node which contains the same information but a different succedent.
    
    Parameters:
    
    node - The Node which provides the original Sequent.
    
    additionalAntecedent - An optional additional antecedents.
    
    newSuccedent - The new succedent.
    
    Returns:
    
    The created Sequent.
  - createSequentToProveWithNewSuccedent
```
public static Sequent createSequentToProveWithNewSuccedent(Node node,
                                                           PosInOccurrence pio,
                                                           Term additionalAntecedent,
                                                           Term newSuccedent,
                                                           boolean addResultLabel)
```
    Creates a new Sequent which is a modification from the Sequent of the given Node which contains the same information but a different succedent.
    
    Parameters:
    
    node - The Node which provides the original Sequent.
    
    additionalAntecedent - An optional additional antecedents.
    
    newSuccedent - The new succedent.
    
    Returns:
    
    The created Sequent.
  - computeRootElementaryUpdates
```
public static ImmutableList<Term> computeRootElementaryUpdates(Node root)
```
    Computes the initial ElementaryUpdates on the given root Node.
    
    Parameters:
    
    root - The root Node of the Proof.
    
    Returns:
    
    The found initial ElementaryUpdates.
  - collectElementaryUpdates
```
public static ImmutableList<Term> collectElementaryUpdates(Term term)
```
    Collects the ElementaryUpdates in the given Term.
    
    Parameters:
    
    term - The Term to collect its updates.
    
    Returns:
    
    The found ElementaryUpdates.
  - createSequentToProveWithNewSuccedent
```
public static Sequent createSequentToProveWithNewSuccedent(Node node,
                                                           Term additionalAntecedent,
                                                           Term newSuccedent,
                                                           ImmutableList<Term> updates,
                                                           boolean addResultLabel)
```
    Creates a new Sequent which is a modification from the Sequent of the given Node which contains the same information but a different succedent.
    
    Parameters:
    
    node - The Node which provides the original Sequent.
    
    additionalAntecedent - An optional additional antecedents.
    
    newSuccedent - The new succedent.
    
    updates - The updates to use.
    
    Returns:
    
    The created Sequent.
  - createSequentToProveWithNewSuccedent
```
public static Sequent createSequentToProveWithNewSuccedent(Node node,
                                                           PosInOccurrence pio,
                                                           Term additionalAntecedent,
                                                           Term newSuccedent,
                                                           ImmutableList<Term> updates,
                                                           boolean addResultLabel)
```
    Creates a new Sequent which is a modification from the Sequent of the given Node which contains the same information but a different succedent.
    
    Parameters:
    
    node - The Node which provides the original Sequent.
    
    additionalAntecedent - An optional additional antecedents.
    
    newSuccedent - The new succedent.
    
    updates - The updates to use.
    
    Returns:
    
    The created Sequent.
  - labelSkolemConstants
```
protected static Sequent labelSkolemConstants(Sequent sequent,
                                              java.util.Set<Term> constantsToLabel,
                                              TermFactory factory)
```
    Labels all specified skolem equalities with the RESULT_LABEL.
    
    Parameters:
    
    sequent - The Sequent to modify.
    
    constantsToLabel - The skolem constants to label.
    
    factory - The TermFactory to use.
    
    Returns:
    
    The modified Sequent.
  - addLabelRecursiveToNonSkolem
```
private static Term addLabelRecursiveToNonSkolem(TermFactory tf,
                                                 Term term,
                                                 TermLabel label)
```
    Adds the given TermLabel to the given Term and to all of its children.
    
    Parameters:
    
    tf - The TermFactory to use.
    
    term - The Term to add label to.
    
    label - The TermLabel to add.
    
    Returns:
    
    A new Term with the given TermLabel.
  - removeLabelRecursive
```
public static Term removeLabelRecursive(TermFactory tf,
                                        Term term,
                                        TermLabel label)
```
    Removes the given TermLabel from the given Term and from all of its children.
    
    Parameters:
    
    tf - The TermFactory to use.
    
    term - The Term to remove label from.
    
    label - The TermLabel to remove.
    
    Returns:
    
    A new Term without the given TermLabel.
  - collectSkolemConstants
```
private static java.util.Set<Term> collectSkolemConstants(Sequent sequent,
                                                          Term term)
```
    Collects all contained skolem Terms which fulfill isSkolemConstant(Term) as well as the skolem constants used in the find once recursive.
    
    Parameters:
    
    sequent - The Sequent which provides the skolem equalities.
    
    term - The Term to start collection in.
    
    Returns:
    
    The found skolem Terms.
  - collectSkolemConstantsNonRecursive
```
private static java.util.Set<Term> collectSkolemConstantsNonRecursive(Term term)
```
    Collects all contained skolem Terms which fulfill isSkolemConstant(Term).
    
    Parameters:
    
    term - The Term to collect in.
    
    Returns:
    
    The found skolem Terms.
  - isSkolemConstant
```
public static boolean isSkolemConstant(Term term)
```
    Checks if the given Term is a skolem Term meaning that it has the SelectSkolemConstantTermLabel.
    
    Parameters:
    
    term - The Term to check.
    
    Returns:
    
    true is skolem Term, false is not a skolem Term.
  - removeAllUnusedSkolemEqualities
```
private static Sequent removeAllUnusedSkolemEqualities(Sequent sequent,
                                                       java.util.Collection<Term> skolemConstants)
```
    Removes all SequentFormulas with a skolem equality from the given Sequent if the skolem Term is not contained in the given Collection.
    
    Parameters:
    
    sequent - The Sequent to modify.
    
    skolemConstants - The allowed skolem Terms.
    
    Returns:
    
    The modified Sequent in which all not listed skolem Term equalites are removed.
  - removeAllUnusedSkolemEqualities
```
private static Sequent removeAllUnusedSkolemEqualities(Sequent sequent,
                                                       SequentFormula sf,
                                                       boolean antecedent,
                                                       java.util.Collection<Term> skolemConstants)
```
    Helper method of removeAllUnusedSkolemEqualities(Sequent, Collection) which removes the given SequentFormula if required.
    
    Parameters:
    
    sequent - The Sequent to modify.
    
    sf - The SequentFormula to remove if its skolem Term is not listed.
    
    antecedent - true antecedent, false succedent.
    
    skolemConstants - The allowed skolem Terms.
    
    Returns:
    
    The modified Sequent in which the SequentFormula might be removed.
  - checkSkolemEquality
```
public static int checkSkolemEquality(SequentFormula sf)
```
    Checks if the given SequentFormula is a skolem equality.
    
    Parameters:
    
    sf - The SequentFormula to check.
    
    Returns:
    
    -1 left side of skolem equality, 0 no skolem equality, 1 right side of skolem equality.
  - checkSkolemEquality
```
public static int checkSkolemEquality(Term term)
```
    Checks if the given Term is a skolem equality.
    
    Parameters:
    
    sf - The Term to check.
    
    Returns:
    
    -1 left side of skolem equality, 0 no skolem equality, 1 right side of skolem equality.
  - replaceSkolemConstants
```
public static Term replaceSkolemConstants(Sequent sequent,
                                          Term term,
                                          Services services)
```
    Replaces all skolem constants in the given Term.
    
    Parameters:
    
    sequent - The Sequent which provides the skolem equalities.
    
    term - The Term to replace its skolem constants.
    
    services - The Services to use.
    
    Returns:
    
    The skolem constant free Term.
  - findSkolemReplacements
```
private static java.util.List<Term> findSkolemReplacements(Sequent sequent,
                                                           Term skolemConstant,
                                                           Term skolemEquality)
```
    Utility method of replaceSkolemConstants(Sequent, Term, Services) to find all equality parts of the given skolem constant.
    
    Parameters:
    
    sequent - The Sequent which provides the skolem equalities.
    
    skolemConstant - The skolem constant to solve.
    
    skolemEquality - The optional skolem equality to ignore.
    
    Returns:
    
    The equality parts of the given skolem equality.
  - isNullSort
```
public static boolean isNullSort(Sort sort,
                                 Services services)
```
    Checks if the given Sort represents a null value in the given Services.
    
    Parameters:
    
    sort - The Sort to check.
    
    services - The Services to use.
    
    Returns:
    
    true is Null-Sort, false is something else.
  - isStaticVariable
```
public static boolean isStaticVariable(IProgramVariable programVariable)
```
    Checks if the given IProgramVariable is static or not.
    
    Returns:
    
    true is static, false is not static or is array cell.
  - getProgramVariables
```
public static java.util.Set<IProgramVariable> getProgramVariables(FieldDeclaration fd)
```
    Collects all IProgramVariables of the given FieldDeclaration.
    
    Parameters:
    
    fd - The given FieldDeclaration.
    
    Returns:
    
    The found IProgramVariables for the given FieldDeclaration.
  - computePathCondition
```
public static Term computePathCondition(Node node,
                                        boolean simplify,
                                        boolean improveReadability)
                                 throws ProofInputException
```
    Computes the path condition of the given Node.
    
    Parameters:
    
    node - The Node to compute its path condition.
    
    simplify - true simplify each branch condition in a side proof, false do not simplify branch conditions.
    
    improveReadability - true improve readability, false do not improve readability.
    
    Returns:
    
    The computed path condition.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - computePathCondition
```
public static Term computePathCondition(Node parentNode,
                                        Node childNode,
                                        boolean simplify,
                                        boolean improveReadability)
                                 throws ProofInputException
```
    Computes the path condition between the given Nodes.
    
    Parameters:
    
    parentNode - The Node to stop path condition computation at.
    
    childNode - The Node to compute its path condition back to the parent.
    
    simplify - true simplify each branch condition in a side proof, false do not simplify branch conditions.
    
    improveReadability - true improve readability, false do not improve readability.
    
    Returns:
    
    The computed path condition.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - hasReferenceSort
```
public static boolean hasReferenceSort(Services services,
                                       Term term)
```
    Checks if the Sort of the given Term is a reference type.
    
    Parameters:
    
    services - The Services to use.
    
    term - The Term to check.
    
    Returns:
    
    true is reference sort, false is no reference sort.
  - hasReferenceSort
```
public static boolean hasReferenceSort(Services services,
                                       IProgramVariable var)
```
    Checks if the Sort of the given IProgramVariable is a reference type.
    
    Parameters:
    
    services - The Services to use.
    
    var - The IProgramVariable to check.
    
    Returns:
    
    true is reference sort, false is no reference sort.
  - hasReferenceSort
```
public static boolean hasReferenceSort(Services services,
                                       Sort sort)
```
    Checks if the Sort is a reference type.
    
    Parameters:
    
    services - The Services to use.
    
    sort - The Sort to check.
    
    Returns:
    
    true is reference sort, false is no reference sort.
  - getDisplayString
```
public static java.lang.String getDisplayString(IProgramVariable pv)
```
    Returns the human readable name of the given IProgramVariable.
    
    Parameters:
    
    pv - The IProgramVariable to get its name.
    
    Returns:
    
    The human readable name of the given IProgramVariable.
  - getRoot
```
public static IExecutionNode<?> getRoot(IExecutionNode<?> executionNode)
```
    Returns the root of the given IExecutionNode.
    
    Parameters:
    
    executionNode - The IExecutionNode to get the root of its symbolic execution tree.
    
    Returns:
    
    The root of the given IExecutionNode.
  - extractExceptionVariable
```
public static IProgramVariable extractExceptionVariable(Proof proof)
```
    Extracts the exception variable which is used to check if the executed program in proof terminates normally.
    
    Parameters:
    
    proof - The Proof to extract variable from.
    
    Returns:
    
    The extract variable.
  - updateStrategySettings
```
public static void updateStrategySettings(Proof proof,
                                          boolean useOperationContracts,
                                          boolean useLoopInvariants,
                                          boolean nonExecutionBranchHidingSideProofs,
                                          boolean aliasChecksImmediately)
```
    Configures the proof to use the given settings.
    
    Parameters:
    
    proof - The Proof to configure.
    
    useOperationContracts - true use operation contracts, false expand methods.
    
    useLoopInvariants - true use loop invariants, false expand loops.
    
    nonExecutionBranchHidingSideProofs - true hide non execution branch labels by side proofs, false do not hide execution branch labels.
    
    useLoopInvariants - true immediately alias checks, false alias checks never.
  - updateStrategySettings
```
public static void updateStrategySettings(Proof proof,
                                          StrategyProperties sp)
```
    Configures the proof to use the given StrategyProperties.
    
    Parameters:
    
    proof - The Proof to configure.
    
    sb - The StrategyProperties to set.
  - isChoiceSettingInitialised
```
public static boolean isChoiceSettingInitialised()
```
    Checks if the choice settings are initialized.
    
    Returns:
    
    true settings are initialized, false settings are not initialized.
  - isLoopBodyTermination
```
public static boolean isLoopBodyTermination(Node node,
                                            RuleApp ruleApp)
```
    Checks if the given node should be represented as loop body termination.
    
    Parameters:
    
    node - The current Node in the proof tree of KeY.
    
    ruleApp - The RuleApp may used or not used in the rule.
    
    Returns:
    
    true represent node as loop body termination, false represent node as something else.
  - isHeap
```
public static boolean isHeap(Operator op,
                             HeapLDT heapLDT)
```
    Checks if the given Operator is a heap.
    
    Parameters:
    
    op - The Operator to check.
    
    heapLDT - The HeapLDT which provides the available heaps.
    
    Returns:
    
    true Operator is heap, false Operator is something else.
  - isBaseHeap
```
public static boolean isBaseHeap(Operator op,
                                 HeapLDT heapLDT)
```
    Checks if the given Operator is the base heap.
    
    Parameters:
    
    op - The Operator to check.
    
    heapLDT - The HeapLDT which provides the available heaps.
    
    Returns:
    
    true Operator is the base heap, false Operator is something else.
  - getSourcePath
```
public static java.lang.String getSourcePath(PositionInfo posInfo)
```
    Returns the path to the source file defined by the given PositionInfo.
    
    Parameters:
    
    posInfo - The PositionInfo to extract source file from.
    
    Returns:
    
    The source file name or null if not available.
  - isSelect
```
public static boolean isSelect(Services services,
                               Term term)
```
    Checks if the given Term is a select on a heap.
    
    Parameters:
    
    services - The Services to use.
    
    term - The Term to check.
    
    Returns:
    
    true is select, false is something else.
  - isNumber
```
public static boolean isNumber(Operator op)
```
    Checks if the given Operator is a number.
    
    Parameters:
    
    op - The Operator to check.
    
    Returns:
    
    true is number, false is something else.
  - isBoolean
```
public static boolean isBoolean(Services services,
                                Operator op)
```
    Checks if the given Operator is a boolean.
    
    Parameters:
    
    op - The Operator to check.
    
    Returns:
    
    true is boolean, false is something else.
  - getDefaultTacletOptions
```
public static java.util.HashMap<java.lang.String,java.lang.String> getDefaultTacletOptions()
```
    Returns the default taclet options for symbolic execution.
    
    Returns:
    
    The default taclet options for symbolic execution.
  - formatTerm
```
public static java.lang.String formatTerm(Term term,
                                          Services services,
                                          boolean useUnicode,
                                          boolean usePrettyPrinting)
```
    Converts the given Term into a String respecting #isUsePretty().
    
    The functionality is similar to OutputStreamProofSaver.printTerm(Term, Services, boolean) but allows to set custom settings.
    
    Parameters:
    
    term - The Term to convert.
    
    services - The Services to use.
    
    useUnicode - true use unicode characters, false do not use unicode characters.
    
    usePrettyPrinting - true use pretty printing, false do not use pretty printing.
    
    Returns:
    
    The String representation of the given Term.
  - isUsePrettyPrinting
```
public static boolean isUsePrettyPrinting()
```
    Checks if pretty printing is enabled or not.
    
    Returns:
    
    true pretty printing is enabled, false pretty printing is disabled.
  - setUsePrettyPrinting
```
public static void setUsePrettyPrinting(boolean usePrettyPrinting)
```
    Defines if pretty printing is enabled or not.
    
    Parameters:
    
    usePrettyPrinting - true pretty printing is enabled, false pretty printing is disabled.
  - hasApplicableRules
```
public static boolean hasApplicableRules(Goal goal)
```
    Checks if the Goal has applicable rules.
    
    Parameters:
    
    goal - The Goal to check.
    
    Returns:
    
    true has applicable rules, false no rules are applicable.
  - computeSecondStatement
```
public static Pair<java.lang.Integer,SourceElement> computeSecondStatement(RuleApp ruleApp)
```
    Computes the call stack size and the second statement similar to NodeInfo.computeActiveStatement(SourceElement).
    
    Parameters:
    
    ruleApp - The RuleApp.
    
    Returns:
    
    The computed call stack size and the second statement if available.
  - equalsWithPosition
```
public static boolean equalsWithPosition(SourceElement first,
                                         SourceElement second)
```
    Compares the given SourceElements including their PositionInfos.
    
    Parameters:
    
    first - The first SourceElement.
    
    second - The second SourceElement.
    
    Returns:
    
    true both are equal and at the same PositionInfo, false otherwise.
  - containsStatement
```
public static boolean containsStatement(ProgramElement toSearchIn,
                                        SourceElement toSearch,
                                        Services services)
```
    Checks if the given ProgramElement contains the given SourceElement.
    
    Parameters:
    
    toSearchIn - The ProgramElement to search in.
    
    toSearch - The SourceElement to search.
    
    services - The Services to use.
    
    Returns:
    
    true contained, false not contained.
  - createSelectTerm
```
public static Term createSelectTerm(IExecutionVariable variable)
```
    Creates recursive a term which can be used to determine the value of #getProgramVariable().
    
    Parameters:
    
    services - The Services to use.
    
    Returns:
    
    The created term.
  - createNotationInfo
```
public static NotationInfo createNotationInfo(IExecutionElement element)
```
    Creates the NotationInfo for the given IExecutionElement.
    
    Parameters:
    
    element - The IExecutionElement to create its NotationInfo.
    
    Returns:
    
    The created NotationInfo.
  - createNotationInfo
```
public static NotationInfo createNotationInfo(Node node)
```
    Creates the NotationInfo for the given Node.
    
    Parameters:
    
    node - The Node to create its NotationInfo.
    
    Returns:
    
    The created NotationInfo.
  - createNotationInfo
```
public static NotationInfo createNotationInfo(Proof proof)
```
    Creates the NotationInfo for the given Proof.
    
    Parameters:
    
    proof - The Proof to create its NotationInfo.
    
    Returns:
    
    The created NotationInfo.
  - lazyComputeIsMainBranchVerified
```
public static boolean lazyComputeIsMainBranchVerified(Node node)
```
    Checks if this branch would be closed without the uninterpreted predicate and thus be treated as valid/closed in a regular proof.
    
    Returns:
    
    true verified/closed, false not verified/still open
  - lazyComputeIsAdditionalBranchVerified
```
public static boolean lazyComputeIsAdditionalBranchVerified(Node node)
```
    Checks if this branch would be closed without the uninterpreted predicate and thus be treated as valid/closed in a regular proof.
    
    Returns:
    
    true verified/closed, false not verified/still open
  - lazyComputeIsExceptionalTermination
```
public static boolean lazyComputeIsExceptionalTermination(Node node,
                                                          IProgramVariable exceptionVariable)
```
    Checks if is an exceptional termination.
    
    Parameters:
    
    node - the node which is used for computation.
    
    exceptionVariable - the exception variable which is used to check if the executed program in proof terminates normally.
    
    Returns:
    
    true exceptional termination, false normal termination.
  - lazyComputeExceptionSort
```
public static Sort lazyComputeExceptionSort(Node node,
                                            IProgramVariable exceptionVariable)
```
    Computes the exception Sort lazily when #getExceptionSort() is called the first time.
    
    Parameters:
    
    node - the node which is user for computation.
    
    exceptionVariable - the exception variable which is used to check if the executed program in proof terminates normally.
    
    Returns:
    
    The exception Sort.
  - extractValueFromUpdate
```
protected static ImmutableArray<Term> extractValueFromUpdate(Term term,
                                                             IProgramVariable variable)
```
    Utility method to extract the value of the IProgramVariable from the given update term.
    
    Parameters:
    
    term - The given update term.
    
    variable - The IProgramVariable for that the value is needed.
    
    Returns:
    
    The found value or null if it is not defined in the given update term.
  - initializeStrategy
```
public static void initializeStrategy(SymbolicExecutionTreeBuilder builder)
```
    Initializes the Proof of the given SymbolicExecutionTreeBuilder so that the correct Strategy is used.
    
    Parameters:
    
    builder - The SymbolicExecutionTreeBuilder to initialize.
  - isBlockContractValidityBranch
```
public static boolean isBlockContractValidityBranch(RuleApp appliedRuleApp)
```
    Checks if the modality at the applied rule represents the validity branch of an applied block contract.
    
    Parameters:
    
    appliedRuleApp - The RuleApp to check.
    
    Returns:
    
    true validitiy branch, false otherwise.
  - isBlockContractValidityBranch
```
public static boolean isBlockContractValidityBranch(PosInOccurrence pio)
```
    Checks if the modality at the given PosInOccurrence represents the validity branch of an applied block contract.
    
    Parameters:
    
    pio - The PosInOccurrence to check.
    
    Returns:
    
    validitiy branch, false otherwise.
  - isJoin
```
public static boolean isJoin(RuleApp ruleApp)
```
    Checks if the MergeRuleBuiltInRuleApp is applied.
    
    Parameters:
    
    ruleApp - The RuleApp to check.
    
    Returns:
    
    true is MergeRuleBuiltInRuleApp, false otherwise.
  - isCloseAfterJoin
```
public static boolean isCloseAfterJoin(RuleApp ruleApp)
```
    Checks if the CloseAfterMergeRuleBuiltInRuleApp is applied.
    
    Parameters:
    
    ruleApp - The RuleApp to check.
    
    Returns:
    
    true is CloseAfterMergeRuleBuiltInRuleApp, false otherwise.
  - isWeakeningGoalEnabled
```
public static boolean isWeakeningGoalEnabled(Proof proof)
```
    Checks if the weakening goal is enabled or not.
    
    Parameters:
    
    proof - The Proof to check.
    
    Returns:
    
    true enabled, false disabled.

Class SymbolicExecutionUtil

Nested Class Summary

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

CHOICE_SETTING_RUNTIME_EXCEPTIONS

CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_BAN

CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_ALLOW

RESULT_LABEL_NAME

RESULT_LABEL

LOOP_BODY_LABEL_NAME

LOOP_BODY_LABEL

LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL_NAME

LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL

Constructor Detail

SymbolicExecutionUtil

Method Detail

simplify

simplify

simplify

sequentToImplication

listSemisequentTerms

improveReadability

improveReadabilityRecursive

isOne

isMinusOne

createExtractReturnVariableValueSequent

createExtractReturnVariableValueSequent

createExtractVariableValueSequent

createExtractTermSequent

isHeapUpdate

canComputeVariables

createExecutionConstraints

containsSymbolicExecutionLabel

createExecutionVariables

createExecutionVariables

createExecutionVariables

createAllExecutionVariables

collectAllElementaryUpdateTerms

internalCollectAllElementaryUpdateTerms

internalCollectStaticProgramVariablesOnHeap

findInnerMostSelect

getProgramVariable

getArrayIndex

findSelfTerm

isMethodCallNode

isMethodCallNode

isNotImplicit

isBranchStatement

isLoopStatement

isStatementNode

isTerminationNode

isOperationContract

isBlockSpecificationElement

isLoopInvariant

isMethodReturnNode

isExceptionalMethodReturnNode

hasLoopCondition

hasLoopBodyLabel

hasLoopBodyTerminationLabel

hasSymbolicExecutionLabel

getSymbolicExecutionLabel

hasSymbolicExecutionLabel

getSymbolicExecutionLabel

findModalityWithMaxSymbolicExecutionLabelId

findModalityWithMaxSymbolicExecutionLabelId

findModalityWithMaxSymbolicExecutionLabelId

findModalityWithMinSymbolicExecutionLabelId

findModalityWithMinSymbolicExecutionLabelId

findModalityWithMinSymbolicExecutionLabelId

isSymbolicExecutionTreeNode

isRuleAppToIgnore

isInImplicitMethod

computeStackSize

isDoWhileLoopCondition

isForLoopCondition

collectGoalsInSubtree

collectGoalsInSubtree