Modifier and Type | Method and Description |
---|---|
protected ImmutableSet<TacletApp> |
AbstractProofControl.getAppsForName(Goal goal,
java.lang.String name,
PosInOccurrence pos)
collects all Taclet applications at the given position of the specified
taclet
|
protected ImmutableSet<TacletApp> |
AbstractProofControl.getAppsForName(Goal goal,
java.lang.String name,
PosInOccurrence pos,
TacletFilter filter)
collects all taclet applications for the given position and taclet
(identified by its name) matching the filter condition
|
ImmutableList<BuiltInRule> |
AbstractProofControl.getBuiltInRule(Goal focusedGoal,
PosInOccurrence pos) |
ImmutableList<BuiltInRule> |
ProofControl.getBuiltInRule(Goal focusedGoal,
PosInOccurrence pos)
collects all built-in rules that are applicable at the given sequent
position 'pos'.
|
ImmutableSet<IBuiltInRuleApp> |
AbstractProofControl.getBuiltInRuleApp(Goal focusedGoal,
BuiltInRule rule,
PosInOccurrence pos)
collects all built-in rule applications for the given rule that are
applicable at position 'pos' and the current user constraint
|
protected ImmutableSet<IBuiltInRuleApp> |
AbstractProofControl.getBuiltInRuleAppsForName(Goal focusedGoal,
java.lang.String name,
PosInOccurrence pos)
collects all applications of a rule given by its name at a give position
in the sequent
|
ImmutableList<TacletApp> |
AbstractProofControl.getFindTaclet(Goal focusedGoal,
PosInOccurrence pos) |
ImmutableList<TacletApp> |
ProofControl.getFindTaclet(Goal focusedGoal,
PosInOccurrence pos)
collects all applicable FindTaclets of the current goal (called by the
SequentViewer)
|
ImmutableList<TacletApp> |
AbstractProofControl.getRewriteTaclet(Goal focusedGoal,
PosInOccurrence pos) |
ImmutableList<TacletApp> |
ProofControl.getRewriteTaclet(Goal focusedGoal,
PosInOccurrence pos)
collects all applicable RewriteTaclets of the current goal (called by the
SequentViewer)
|
void |
InteractionListener.runBuiltInRule(Goal goal,
IBuiltInRuleApp app,
BuiltInRule rule,
PosInOccurrence pos,
boolean forced) |
void |
DefaultProofControl.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc)
|
void |
ProofControl.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc)
|
void |
InteractionListener.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc,
ProofMacroFinishedInfo info) |
void |
AbstractProofControl.selectedBuiltInRule(Goal goal,
BuiltInRule rule,
PosInOccurrence pos,
boolean forced) |
void |
ProofControl.selectedBuiltInRule(Goal goal,
BuiltInRule rule,
PosInOccurrence pos,
boolean forced)
selected rule to apply
|
boolean |
AbstractProofControl.selectedTaclet(Taclet taclet,
Goal goal,
PosInOccurrence pos) |
boolean |
ProofControl.selectedTaclet(Taclet taclet,
Goal goal,
PosInOccurrence pos) |
void |
AbstractProofControl.startFocussedAutoMode(PosInOccurrence focus,
Goal goal)
starts the execution of rules with active strategy.
|
void |
ProofControl.startFocussedAutoMode(PosInOccurrence focus,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
static PosInOccurrence |
DependencyContractCompletion.findCorrespondingStep(java.util.List<PosInOccurrence> steps,
Term[] resultHeaps) |
Modifier and Type | Method and Description |
---|---|
protected void |
ProofMacroWorker.emitProofMacroFinished(Node node,
ProofMacro macro,
PosInOccurrence posInOcc,
ProofMacroFinishedInfo info) |
Modifier and Type | Method and Description |
---|---|
static void |
DependencyContractCompletion.extractHeaps(java.util.List<LocationVariable> heapContext,
java.util.List<PosInOccurrence> steps,
DependencyContractCompletion.TermStringWrapper[] heaps,
LogicPrinter lp) |
static PosInOccurrence |
DependencyContractCompletion.findCorrespondingStep(java.util.List<PosInOccurrence> steps,
Term[] resultHeaps) |
Constructor and Description |
---|
ProofMacroMenu(KeYMediator mediator,
PosInOccurrence posInOcc)
Instantiates a new proof macro menu.
|
ProofMacroWorker(Node node,
ProofMacro macro,
KeYMediator mediator,
PosInOccurrence posInOcc)
Instantiates a new proof macro worker.
|
Modifier and Type | Method and Description |
---|---|
abstract C |
MergeProcedureCompletion.complete(C proc,
Pair<Goal,PosInOccurrence> mergeGoalPio,
java.util.Collection<MergePartner> partners)
Completes the given merge procedure either automatically (if the procedure
is already complete) or by demanding input from the user in a GUI.
|
Constructor and Description |
---|
MergePartnerSelectionDialog(Goal mergeGoal,
PosInOccurrence pio,
ImmutableList<MergePartner> candidates,
Services services)
Creates a new merge partner selection dialog.
|
MergeRuleMenuItem(Goal goal,
PosInOccurrence pio,
KeYMediator mediator)
Creates a new menu item for the join rule.
|
Modifier and Type | Method and Description |
---|---|
MergeWithPredicateAbstraction |
PredicateAbstractionCompletion.complete(MergeWithPredicateAbstraction proc,
Pair<Goal,PosInOccurrence> joinGoalPio,
java.util.Collection<MergePartner> partners) |
Constructor and Description |
---|
OriginTermLabelVisualizer(PosInOccurrence pos,
Node node,
Services services)
Creates a new
OriginTermLabelVisualizer . |
Modifier and Type | Method and Description |
---|---|
ProofMacroFinishedInfo |
StartAuxiliaryLoopComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
FinishAuxiliaryLoopComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
StartAuxiliaryBlockComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
FinishAuxiliaryBlockComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
StartAuxiliaryMethodComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
ExhaustiveProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
FinishAuxiliaryMethodComputationMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
boolean |
StartAuxiliaryLoopComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
SelfcompositionStateExpansionMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
FinishAuxiliaryLoopComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
StartAuxiliaryBlockComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
StateExpansionAndInfFlowContractApplicationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
FullUseInformationFlowContractMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
FullInformationFlowAutoPilotMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
FinishAuxiliaryBlockComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
StartAuxiliaryMethodComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
ExhaustiveProofMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
FinishAuxiliaryMethodComputationMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
RuleAppCost |
UseInformationFlowContractMacro.PropExpansionStrategy.computeCost(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal) |
protected Strategy |
SelfcompositionStateExpansionMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected UseInformationFlowContractMacro.PropExpansionStrategy |
UseInformationFlowContractMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
void |
UseInformationFlowContractMacro.PropExpansionStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal,
RuleAppCostCollector collector) |
boolean |
UseInformationFlowContractMacro.PropExpansionStrategy.isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
protected boolean |
SelfcompositionStateExpansionMacro.ruleApplicationInContextAllowed(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal) |
protected boolean |
UseInformationFlowContractMacro.ruleApplicationInContextAllowed(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal)
Checks whether the application of the passed rule is ok in the given
context.
|
Modifier and Type | Method and Description |
---|---|
protected void |
InfFlowContractAppTacletExecutor.addToAntec(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services) |
Modifier and Type | Method and Description |
---|---|
java.util.Map<Node,PosInOccurrence> |
ServiceCaches.getExhaustiveMacroCache() |
LRUCache<PosInOccurrence,RuleAppCost> |
ServiceCaches.getIfThenElseMalusCache() |
Modifier and Type | Method and Description |
---|---|
PosInOccurrence |
PosInOccurrence.down(int i)
creates a new PosInOccurrence that has exactly the same state as this
object except the PosInTerm is new and walked down the specified
subterm, as specified in method down of
PosInTerm . |
static PosInOccurrence |
PosInOccurrence.findInSequent(Sequent seq,
int formulaNumber,
PosInTerm pos) |
PosInOccurrence |
PIOPathIterator.getPosInOccurrence() |
PosInOccurrence |
FormulaChangeInfo.getPositionOfModification() |
PosInOccurrence |
PosInOccurrence.replaceConstrainedFormula(SequentFormula p_newFormula)
Replace the formula this object points to with the new formula given
|
PosInOccurrence |
PosInOccurrence.topLevel()
Ascend to the top node of the formula this object points to
|
PosInOccurrence |
PosInOccurrence.up()
Ascend to the parent node
|
Modifier and Type | Method and Description |
---|---|
SequentChangeInfo |
Sequent.addFormula(ImmutableList<SequentFormula> insertions,
PosInOccurrence p)
adds the formulas of list insertions to the sequent starting at position p.
|
SequentChangeInfo |
Sequent.addFormula(SequentFormula cf,
PosInOccurrence p)
adds a formula to the sequent at the given position.
|
SequentChangeInfo |
Sequent.changeFormula(ImmutableList<SequentFormula> replacements,
PosInOccurrence p)
replaces the formula at position p with the head of the given list and adds
the remaining list elements to the sequent (NOTICE:Sequent determines index
using identity (==) not equality.)
|
SequentChangeInfo |
Sequent.changeFormula(SequentFormula newCF,
PosInOccurrence p)
replaces the formula at the given position with another one (NOTICE:Sequent
determines index using identity (==) not equality.)
|
static SequentChangeInfo |
SequentChangeInfo.createSequentChangeInfo(PosInOccurrence pos,
SemisequentChangeInfo semiCI,
Sequent result,
Sequent original)
creates a new sequent change info whose semisequent described by position
pos has changed.
|
protected ProgramElementName |
VariableNamer.getNameProposalForSchemaVariable(java.lang.String basename,
SchemaVariable sv,
PosInOccurrence posOfFind,
PosInProgram posOfDeclaration,
ImmutableList<java.lang.String> previousProposals)
proposes a unique name for the instantiation of a schema variable
(like getProposal(), but somewhat less nicely)
|
protected ProgramElement |
VariableNamer.getProgramFromPIO(PosInOccurrence pio)
returns the program contained in a PosInOccurrence
|
boolean |
VariableNamer.isUniqueNameForSchemaVariable(java.lang.String name,
SchemaVariable sv,
PosInOccurrence posOfFind,
PosInProgram posOfDeclaration)
tells whether a name for instantiating a schema variable is unique
within its scope
|
SequentChangeInfo |
Sequent.removeFormula(PosInOccurrence p)
removes the formula at position p (NOTICE:Sequent determines index using
identity (==) not equality.)
|
abstract ProgramVariable |
VariableNamer.rename(ProgramVariable var,
Goal goal,
PosInOccurrence posOfFind)
intended to be called when symbolically executing a variable declaration;
resolves any naming conflicts between the new variable and other global
variables by renaming the new variable and / or other variables
|
ProgramVariable |
InnerVariableNamer.rename(ProgramVariable var,
Goal goal,
PosInOccurrence posOfFind) |
SemisequentChangeInfo |
Semisequent.replace(PosInOccurrence pos,
ImmutableList<SequentFormula> replacements)
replaces the element at place idx with the first element of the
given list and adds the rest of the list to the semisequent
behind the replaced formula
|
SemisequentChangeInfo |
Semisequent.replace(PosInOccurrence pos,
SequentFormula sequentFormula)
replaces the element at place idx with sequentFormula
|
Constructor and Description |
---|
FormulaChangeInfo(PosInOccurrence positionOfModification,
SequentFormula newFormula) |
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<Name,ChildTermLabelPolicy> |
TermLabelManager.computeActiveChildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificPolicies,
java.util.Map<Name,ChildTermLabelPolicy> ruleIndependentPolicies)
Computes active
ChildTermLabelPolicy instances which have to be executed during the given rule application. |
protected TermLabelManager.RefactoringsContainer |
TermLabelManager.computeRefactorings(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Computes the
TermLabelRefactoring to consider. |
static TermLabel |
TermLabelManager.findInnerMostParentLabel(PosInOccurrence pio,
Name termLabelName)
Searches the inner most
TermLabel wit the given Name in the parent hierarchy of the PosInOccurrence . |
static OriginTermLabel.Origin |
OriginTermLabel.getOrigin(PosInOccurrence pio)
Find a term's origin.
|
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static Term |
TermLabelManager.label(Services services,
TermLabelState state,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
TermLabelManager.instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp,
Goal, Object, Term, Operator, ImmutableArray, ImmutableArray,
JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
TermLabelManager.refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object,
Rule, Term) . |
static Term |
TermLabelManager.label(Services services,
TermLabelState state,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
TermLabelManager.instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp,
Goal, Object, Term, Operator, ImmutableArray, ImmutableArray,
JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
TermLabelManager.refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object,
Rule, Term) . |
Term |
TermLabelManager.label(TermLabelState state,
Services services,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
TermLabelManager.instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp,
Goal, Object, Term, Operator, ImmutableArray, ImmutableArray,
JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
TermLabelManager.refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object,
Rule, Term) . |
protected void |
TermLabelManager.performChildAndGrandchildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,ChildTermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild
ChildTermLabelPolicy instances. |
protected void |
TermLabelManager.performDirectChildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,ChildTermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given direct
ChildTermLabelPolicy instances. |
protected ImmutableArray<TermLabel> |
TermLabelManager.performRefactoring(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
ImmutableList<TermLabelRefactoring> activeRefactorings)
Computes the new labels as part of the refactoring for the given
Term . |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given
TermLabelPolicy instances. |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels,
TermLabel label)
Performs the given
TermLabelPolicy instances. |
protected void |
TermLabelManager.performUpdater(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableList<TermLabelUpdate> updater,
java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild
TermLabelUpdate instances. |
protected Term |
TermLabelManager.refactorApplicationTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
TermLabelManager.RefactoringsContainer refactorings,
TermFactory tf)
Refactors the labels of the application term.
|
static void |
TermLabelManager.refactorGoal(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
void |
TermLabelManager.refactorGoal(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
protected Term |
TermLabelManager.refactorLabelsRecursive(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
ImmutableList<TermLabelRefactoring> activeRefactorings)
|
protected void |
TermLabelManager.refactorSemisequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Semisequent semisequent,
boolean inAntec,
ImmutableList<TermLabelRefactoring> activeRefactorings)
Performs a
TermLabel refactoring on the given Semisequent . |
static void |
TermLabelManager.refactorSequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
void |
TermLabelManager.refactorSequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
Term |
TermLabelManager.refactorSequentFormula(TermLabelState state,
Services services,
Term sequentFormula,
PosInOccurrence applicationPosInOccurrence,
Goal goal,
java.lang.Object hint,
Rule rule,
Term tacletTerm)
|
static Term |
TermLabelManager.refactorSequentFormula(TermLabelState state,
Services services,
Term sequentFormula,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
|
Term |
TermLabelManager.refactorTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Goal goal,
java.lang.Object hint,
Rule rule,
Term tacletTerm)
Refactors all labels in the given application
Term . |
static Term |
TermLabelManager.refactorTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
protected Term |
TermLabelManager.replaceTerm(TermLabelState state,
PosInOccurrence pio,
Term newTerm,
TermFactory tf,
ImmutableList<TermLabelRefactoring> parentRefactorings,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Replaces the
Term at the specified PosInOccurrence . |
Modifier and Type | Method and Description |
---|---|
static Transformer |
Transformer.getTransformer(PosInOccurrence pio)
Examines a position for whether it is inside a term transformer.
|
static boolean |
Transformer.inTransformer(PosInOccurrence pio)
Examines a position for whether it is inside a term transformer.
|
Modifier and Type | Method and Description |
---|---|
ProofMacroFinishedInfo |
ProofMacro.applyTo(UserInterfaceControl uic,
Node node,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given node.
|
ProofMacroFinishedInfo |
AbstractProofMacro.applyTo(UserInterfaceControl uic,
Node node,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
FinishSymbolicExecutionUntilMergePointMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
SequentialOnLastGoalProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
ProofMacroFinishedInfo |
SequentialProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
ProofMacroFinishedInfo |
ProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
ProofMacroFinishedInfo |
AlternativeMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
ProofMacroFinishedInfo |
TryCloseMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
StrategyProofMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
DoWhileFinallyMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
AbstractBlastingMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
ProofMacroFinishedInfo |
SkipMacro.applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
boolean |
ProofMacro.canApplyTo(Node node,
PosInOccurrence posInOcc)
Can this macro be applied on the given node?
This method should not make any changes but check if the macro can be
applied or not on the given node.
|
boolean |
AbstractProofMacro.canApplyTo(Node node,
PosInOccurrence posInOcc) |
boolean |
WellDefinednessMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
SequentialProofMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
ProofMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
AlternativeMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
TryCloseMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
StrategyProofMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
boolean |
DoWhileFinallyMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
boolean |
SkipMacro.canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc) |
RuleAppCost |
FilterStrategy.computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal) |
RuleAppCost |
PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy.computeCost(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal) |
protected Strategy |
FinishSymbolicExecutionMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
AbstractPropositionalExpansionMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
PrepareInfFlowContractPreBranchesMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
FinishSymbolicExecutionUntilMergePointMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
WellDefinednessMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
AutoPilotPrepareProofMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected abstract Strategy |
StrategyProofMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
AutoMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
OneStepProofMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
AbstractBlastingMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
TestGenMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected RuleAppCost |
PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
void |
FilterStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal,
RuleAppCostCollector collector) |
boolean |
FilterStrategy.isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
boolean |
PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy.isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
protected boolean |
AbstractPropositionalExpansionMacro.ruleApplicationInContextAllowed(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal)
Checks whether the application of the passed rule is ok in the given
context.
|
Modifier and Type | Method and Description |
---|---|
static PosInOccurrence |
MacroCommand.extractMatchingPio(Sequent sequent,
java.lang.String matchRegEx,
Services services)
TODO
|
Modifier and Type | Method and Description |
---|---|
Term |
RewriteCommand.getTermAtPos(SequentFormula sf,
PosInOccurrence pio)
Calculates term at the PosInOccurrence pio
|
Modifier and Type | Method and Description |
---|---|
PosInOccurrence |
PosInSequent.getPosInOccurrence()
returns the PosInOccurrence if the PosInSequent marks a
SequentFormula or parts of it, null otherwise.
|
Modifier and Type | Method and Description |
---|---|
static PosInSequent |
PosInSequent.createCfmaPos(PosInOccurrence posInOcc)
creates a PosInSequent that points to a SequentFormula described by
a PosInOccurrence.
|
ImmutableList<java.lang.Integer> |
InitialPositionTable.pathForPosition(PosInOccurrence pio,
SequentPrintFilter filter)
Returns the path for a given PosInOccurrence.
|
Constructor and Description |
---|
ShowSelectedSequentPrintFilter(PosInOccurrence pos)
Create a new
ShowSelectedSequentPrintFilter . |
Modifier and Type | Method and Description |
---|---|
PosInOccurrence |
FormulaTagManager.getPosForTag(FormulaTag p_tag) |
Modifier and Type | Method and Description |
---|---|
void |
Goal.addFormula(SequentFormula cf,
PosInOccurrence p)
adds a formula to the sequent before the given position
and informs the rule application index about this change
|
TermTacletAppIndex |
TermTacletAppIndex.addTaclets(RuleFilter filter,
PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Create a new tree of indices that additionally contain the taclets that
are selected by
filter |
void |
Goal.changeFormula(SequentFormula cf,
PosInOccurrence p)
replaces a formula at the given position
and informs the rule application index about this change
|
static TermTacletAppIndex |
TermTacletAppIndex.create(PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
RuleFilter filter,
TermTacletAppIndexCacheSet indexCaches)
Create an index for the given term
|
ImmutableList<NoPosTacletApp> |
TacletIndex.getAntecedentTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Taclets for the antecedent.
|
ImmutableList<IBuiltInRuleApp> |
BuiltInRuleAppIndex.getBuiltInRule(Goal goal,
PosInOccurrence pos)
returns a list of built-in rules application applicable
for the given goal and position
|
ImmutableList<IBuiltInRuleApp> |
RuleAppIndex.getBuiltInRules(Goal g,
PosInOccurrence pos)
returns a list of built-in rule applications applicable
for the given goal, user defined constraint and position
|
ImmutableList<NoPosTacletApp> |
TacletAppIndex.getFindTaclet(PosInOccurrence pos,
TacletFilter filter,
TermServices services)
collects all FindTaclets with instantiations and position
|
ImmutableList<NoPosTacletApp> |
RuleAppIndex.getFindTaclet(TacletFilter filter,
PosInOccurrence pos,
TermServices services)
collects all FindTacletInstantiations for the given
heuristics and position
|
ImmutableList<NoPosTacletApp> |
TacletIndex.getRewriteTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Rewrite-Taclets.
|
ImmutableList<NoPosTacletApp> |
TacletAppIndex.getRewriteTaclet(PosInOccurrence pos,
TacletFilter filter,
TermServices services)
collects all RewriteTacletInstantiations in a subterm of the
constrainedFormula described by a PosInOccurrence.
|
ImmutableList<NoPosTacletApp> |
RuleAppIndex.getRewriteTaclet(TacletFilter filter,
PosInOccurrence pos,
TermServices services)
collects all RewriteTacletInstantiations for the given
heuristics in a subterm of the constraintformula described by a
PosInOccurrence
|
ImmutableList<NoPosTacletApp> |
TacletIndex.getSuccedentTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Taclets for the succedent.
|
ImmutableList<NoPosTacletApp> |
TermTacletAppIndex.getTacletAppAt(PosInOccurrence pos,
RuleFilter p_filter) |
ImmutableList<NoPosTacletApp> |
SemisequentTacletAppIndex.getTacletAppAt(PosInOccurrence pos,
RuleFilter filter) |
ImmutableList<TacletApp> |
TacletAppIndex.getTacletAppAt(PosInOccurrence pos,
TacletFilter filter,
Services services)
returns the set of rule applications
at the given position of the given sequent.
|
ImmutableList<TacletApp> |
RuleAppIndex.getTacletAppAt(TacletFilter filter,
PosInOccurrence pos,
Services services)
returns the set of rule applications for
the given heuristics
at the given position of the given sequent.
|
ImmutableList<TacletApp> |
TermTacletAppIndex.getTacletAppAtAndBelow(PosInOccurrence pos,
RuleFilter filter,
Services services) |
ImmutableList<TacletApp> |
SemisequentTacletAppIndex.getTacletAppAtAndBelow(PosInOccurrence pos,
RuleFilter filter,
Services services) |
ImmutableList<TacletApp> |
TacletAppIndex.getTacletAppAtAndBelow(PosInOccurrence pos,
TacletFilter filter,
Services services)
returns the rule applications at the given PosInOccurrence and at all
Positions below this.
|
ImmutableList<TacletApp> |
RuleAppIndex.getTacletAppAtAndBelow(TacletFilter filter,
PosInOccurrence pos,
Services services)
returns the rule applications at the given PosInOccurrence and at all
Positions below this.
|
FormulaTag |
FormulaTagManager.getTagForPos(PosInOccurrence p_pio) |
protected abstract ImmutableList<NoPosTacletApp> |
TacletIndex.matchTaclets(ImmutableList<NoPosTacletApp> tacletApps,
RuleFilter p_filter,
PosInOccurrence pos,
Services services)
Filter the given list of taclet apps, and match their find
parts at the given position of the sequent
|
void |
Goal.removeFormula(PosInOccurrence p)
removes a formula at the given position from the sequent
and informs the rule appliccation index about this change
|
void |
NewRuleListener.ruleAdded(RuleApp rule,
PosInOccurrence pos)
Called when a new RuleApp is added
|
void |
NullNewRuleListener.ruleAdded(RuleApp rule,
PosInOccurrence pos) |
void |
NewRuleListener.rulesAdded(ImmutableList<? extends RuleApp> rule,
PosInOccurrence pos)
Called when a collection of new RuleApps is added
|
void |
NullNewRuleListener.rulesAdded(ImmutableList<? extends RuleApp> rule,
PosInOccurrence pos) |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
OutputStreamProofSaver.posInOccurrence2Proof(Sequent seq,
PosInOccurrence pos) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
OutputStreamProofSaver.builtinRuleIfInsts(Node node,
ImmutableList<PosInOccurrence> ifInsts) |
Modifier and Type | Method and Description |
---|---|
java.util.List<ProspectivePartner> |
JoinIsApplicable.computeProspecitvePartner(Goal goal,
PosInOccurrence pio)
Computes the partners for the given selection.
|
java.util.List<ProspectivePartner> |
JoinIsApplicable.isApplicable(Goal goal,
PosInOccurrence pio) |
Modifier and Type | Method and Description |
---|---|
PosInOccurrence |
NodeRedundantAddChange.getPos()
returns the PosInOccurrence of the formula that has been tried to add
|
PosInOccurrence |
NodeChange.getPos()
provides position information about the change
|
PosInOccurrence |
NodeChangeARFormula.getPos() |
Constructor and Description |
---|
NodeChangeAddFormula(PosInOccurrence p_pos) |
NodeChangeARFormula(PosInOccurrence p_pos) |
NodeChangeRemoveFormula(PosInOccurrence p_pos) |
NodeRedundantAddChange(PosInOccurrence pio)
creates an instance
|
Modifier and Type | Field and Description |
---|---|
protected PosInOccurrence |
SyntacticalReplaceVisitor.applicationPosInOccurrence |
protected PosInOccurrence |
AbstractBuiltInRuleApp.pio |
Modifier and Type | Field and Description |
---|---|
protected ImmutableList<PosInOccurrence> |
AbstractBuiltInRuleApp.ifInsts |
Modifier and Type | Method and Description |
---|---|
static PosInOccurrence |
UseDependencyContractRule.findStepInIfInsts(java.util.List<PosInOccurrence> steps,
UseDependencyContractApp app,
TermServices services) |
PosInOccurrence |
NoPosTacletApp.posInOccurrence()
returns the PositionInOccurrence (representing a SequentFormula and
a position in the corresponding formula)
|
PosInOccurrence |
AbstractBuiltInRuleApp.posInOccurrence()
returns the PositionInOccurrence (representing a SequentFormula and
a position in the corresponding formula) of this rule application
|
PosInOccurrence |
PosTacletApp.posInOccurrence()
returns the PositionInOccurrence (representing a SequentFormula and
a position in the corresponding formula)
|
PosInOccurrence |
RuleApp.posInOccurrence()
returns the PositionInOccurrence (representing a SequentFormula and
a position in the corresponding formula) of this rule application
|
PosInOccurrence |
UseDependencyContractApp.step(Sequent seq,
TermServices services) |
PosInOccurrence |
IfFormulaInstSeq.toPosInOccurrence() |
Modifier and Type | Method and Description |
---|---|
static java.util.List<PosInOccurrence> |
UseDependencyContractRule.getSteps(java.util.List<LocationVariable> heapContext,
PosInOccurrence pos,
Sequent seq,
Services services) |
ImmutableList<PosInOccurrence> |
IBuiltInRuleApp.ifInsts() |
ImmutableList<PosInOccurrence> |
AbstractBuiltInRuleApp.ifInsts() |
Modifier and Type | Method and Description |
---|---|
protected static ImmutableSet<QuantifiableVariable> |
TacletApp.boundAtOccurrenceSet(TacletPrefix prefix,
SVInstantiations instantiations,
PosInOccurrence pos)
collects all bound variables above the occurrence of the schemavariable
whose prefix is given
|
MatchConditions |
RewriteTaclet.checkPrefix(PosInOccurrence p_pos,
MatchConditions p_mc)
For taclets with
getSameUpdatePrefix () , collect
the updates above p_pos and add them to the update
context of the instantiations object p_mc . |
static boolean |
TacletApp.checkVarCondNotFreeIn(Taclet taclet,
SVInstantiations instantiations,
PosInOccurrence pos)
checks if the variable conditions of type 'x not free in y' are hold by
the found instantiations.
|
protected static ImmutableSet<QuantifiableVariable> |
TacletApp.collectBoundVarsAbove(PosInOccurrence pos)
collects all bound vars that are bound above the subterm described by the
given term position information
|
UseDependencyContractApp |
UseDependencyContractRule.createApp(PosInOccurrence pos) |
ContractRuleApp |
UseOperationContractRule.createApp(PosInOccurrence pos) |
IBuiltInRuleApp |
BlockContractExternalRule.createApp(PosInOccurrence pos,
TermServices services) |
DefaultBuiltInRuleApp |
QueryExpand.createApp(PosInOccurrence pos,
TermServices services) |
OneStepSimplifierRuleApp |
OneStepSimplifier.createApp(PosInOccurrence pos,
TermServices services) |
LoopInvariantBuiltInRuleApp |
WhileInvariantRule.createApp(PosInOccurrence pos,
TermServices services) |
BlockContractInternalBuiltInRuleApp |
BlockContractInternalRule.createApp(PosInOccurrence occurrence,
TermServices services) |
IBuiltInRuleApp |
LoopContractExternalRule.createApp(PosInOccurrence pos,
TermServices services) |
IBuiltInRuleApp |
BuiltInRule.createApp(PosInOccurrence pos,
TermServices services) |
LoopContractInternalBuiltInRuleApp |
LoopContractInternalRule.createApp(PosInOccurrence occurrence,
TermServices services) |
UseDependencyContractApp |
UseDependencyContractRule.createApp(PosInOccurrence pos,
TermServices services) |
IBuiltInRuleApp |
LoopApplyHeadRule.createApp(PosInOccurrence pos,
TermServices services) |
ContractRuleApp |
UseOperationContractRule.createApp(PosInOccurrence pos,
TermServices services) |
IBuiltInRuleApp |
AbstractLoopInvariantRule.createApp(PosInOccurrence pos,
TermServices services) |
static PosTacletApp |
PosTacletApp.createPosTacletApp(FindTaclet taclet,
MatchConditions matchCond,
PosInOccurrence pos,
Services services) |
static PosTacletApp |
PosTacletApp.createPosTacletApp(FindTaclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
PosInOccurrence pos,
Services services) |
static PosTacletApp |
PosTacletApp.createPosTacletApp(FindTaclet taclet,
SVInstantiations instantiations,
PosInOccurrence pos,
Services services)
creates a PosTacletApp for the given taclet with some known instantiations
and a position information
and CHECKS variable conditions as well as it resolves
collisions
The ifInstantiations parameter is not
matched against the if sequence, but only stored.
|
static java.util.List<PosInOccurrence> |
UseDependencyContractRule.getSteps(java.util.List<LocationVariable> heapContext,
PosInOccurrence pos,
Sequent seq,
Services services) |
boolean |
BlockContractExternalRule.isApplicable(Goal goal,
PosInOccurrence occurrence) |
boolean |
QueryExpand.isApplicable(Goal goal,
PosInOccurrence pio) |
boolean |
OneStepSimplifier.isApplicable(Goal goal,
PosInOccurrence pio) |
boolean |
WhileInvariantRule.isApplicable(Goal goal,
PosInOccurrence pio) |
boolean |
AbstractBlockContractRule.isApplicable(Goal goal,
PosInOccurrence occurrence) |
boolean |
BlockContractInternalRule.isApplicable(Goal goal,
PosInOccurrence occurrence) |
boolean |
LoopContractExternalRule.isApplicable(Goal goal,
PosInOccurrence occurrence) |
boolean |
BuiltInRule.isApplicable(Goal goal,
PosInOccurrence pio)
returns true iff a rule is applicable at the given
position.
|
boolean |
UseDependencyContractRule.isApplicable(Goal goal,
PosInOccurrence pio) |
boolean |
LoopApplyHeadRule.isApplicable(Goal goal,
PosInOccurrence pio) |
boolean |
UseOperationContractRule.isApplicable(Goal goal,
PosInOccurrence pio) |
boolean |
AbstractLoopInvariantRule.isApplicable(Goal goal,
PosInOccurrence pio) |
boolean |
AbstractLoopContractRule.isApplicable(Goal goal,
PosInOccurrence occurrence) |
boolean |
LoopScopeInvariantRule.isApplicable(Goal goal,
PosInOccurrence pio)
NOTE: The
LoopScopeInvariantRule currently
doesn't support Java Card transactions and information flow proof
obligations. |
NoPosTacletApp |
NoPosTacletApp.matchFind(PosInOccurrence pos,
Services services)
PRECONDITION: ifFormulaInstantiations () == null &&
( pos == null || termConstraint.isSatisfiable () )
|
NoPosTacletApp |
NoPosTacletApp.matchFind(PosInOccurrence pos,
Services services,
Term t) |
protected static boolean |
AbstractAuxiliaryContractRule.occursNotAtTopLevelInSuccedent(PosInOccurrence occurrence) |
LoopInvariantBuiltInRuleApp |
LoopInvariantBuiltInRuleApp.replacePos(PosInOccurrence newPos) |
IBuiltInRuleApp |
IBuiltInRuleApp.replacePos(PosInOccurrence newPos) |
abstract AbstractBuiltInRuleApp |
AbstractBuiltInRuleApp.replacePos(PosInOccurrence newPos) |
DefaultBuiltInRuleApp |
DefaultBuiltInRuleApp.replacePos(PosInOccurrence newPos) |
AbstractBuiltInRuleApp |
LoopApplyHeadBuiltInRuleApp.replacePos(PosInOccurrence newPos) |
LoopContractExternalBuiltInRuleApp |
LoopContractExternalBuiltInRuleApp.replacePos(PosInOccurrence newOccurrence) |
UseDependencyContractApp |
UseDependencyContractApp.replacePos(PosInOccurrence newPos) |
BlockContractInternalBuiltInRuleApp |
BlockContractInternalBuiltInRuleApp.replacePos(PosInOccurrence newOccurrence) |
ContractRuleApp |
ContractRuleApp.replacePos(PosInOccurrence newPos) |
BlockContractExternalBuiltInRuleApp |
BlockContractExternalBuiltInRuleApp.replacePos(PosInOccurrence newOccurrence) |
LoopContractInternalBuiltInRuleApp |
LoopContractInternalBuiltInRuleApp.replacePos(PosInOccurrence newOccurrence) |
PosTacletApp |
TacletApp.setPosInOccurrence(PosInOccurrence pos,
Services services)
returns a new PosTacletApp that is equal to this TacletApp except that
the position is set to the given PosInOccurrence.
|
UseDependencyContractApp |
UseDependencyContractApp.setStep(PosInOccurrence p_step) |
protected MatchConditions |
NoPosTacletApp.setupMatchConditions(PosInOccurrence pos,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
static PosInOccurrence |
UseDependencyContractRule.findStepInIfInsts(java.util.List<PosInOccurrence> steps,
UseDependencyContractApp app,
TermServices services) |
LoopInvariantBuiltInRuleApp |
LoopInvariantBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
IBuiltInRuleApp |
IBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
abstract IBuiltInRuleApp |
AbstractBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
DefaultBuiltInRuleApp |
DefaultBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
IBuiltInRuleApp |
LoopApplyHeadBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
LoopContractExternalBuiltInRuleApp |
LoopContractExternalBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInstantiations) |
UseDependencyContractApp |
UseDependencyContractApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
BlockContractInternalBuiltInRuleApp |
BlockContractInternalBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInstantiations) |
ContractRuleApp |
ContractRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
BlockContractExternalBuiltInRuleApp |
BlockContractExternalBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInstantiations) |
LoopContractInternalBuiltInRuleApp |
LoopContractInternalBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInstantiations) |
void |
AbstractBuiltInRuleApp.setMutable(ImmutableList<PosInOccurrence> ifInsts)
HACK: but strategies do not work otherwise in the moment; I need to have a closer look on what is going on there
This restores the behaviour as it was before my previous commit for the moment
|
Modifier and Type | Method and Description |
---|---|
protected void |
TacletExecutor.addToAntec(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
adds SequentFormula to antecedent depending on
position information (if none is handed over it is added at the
head of the antecedent).
|
protected void |
TacletExecutor.addToSucc(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
adds SequentFormula to succedent depending on
position information (if none is handed over it is added at the
head of the succedent).
|
protected void |
RewriteTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
adds the sequent of the add part of the Taclet to the goal sequent
|
protected void |
SuccTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected abstract void |
FindTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected void |
AntecTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected void |
TacletExecutor.applyAddProgVars(ImmutableSet<SchemaVariable> pvs,
SequentChangeInfo currentSequent,
Goal goal,
PosInOccurrence posOfFind,
Services services,
MatchConditions matchCond) |
protected void |
RewriteTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
SuccTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected abstract void |
FindTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
AntecTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected ImmutableList<SequentFormula> |
TacletExecutor.instantiateSemisequent(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
instantiates the given semisequent with the instantiations found in
Matchconditions
|
protected void |
TacletExecutor.replaceAtPos(Semisequent semi,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
MatchConditions matchCond,
Taclet.TacletLabelHint labelHint,
Goal goal,
RuleApp ruleApp,
Services services)
replaces the constrained formula at the given position with the first
formula in the given semisequent and adds possible other formulas of the
semisequent starting at the position
|
protected Term |
TacletExecutor.syntacticalReplace(Term term,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
MatchConditions mc,
Goal goal,
RuleApp ruleApp,
Services services)
a new term is created by replacing variables of term whose replacement is
found in the given SVInstantiations
|
Modifier and Type | Method and Description |
---|---|
boolean |
ChildTermLabelPolicy.addLabel(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
Term childTerm,
TermLabel label)
|
TermLabelRefactoring.RefactoringScope |
TermLabelRefactoring.defineRefactoringScope(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Defines if a refactoring is required and if so in which
TermLabelRefactoring.RefactoringScope . |
TermLabelRefactoring.RefactoringScope |
OriginTermLabelRefactoring.defineRefactoringScope(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm) |
TermLabelRefactoring.RefactoringScope |
FormulaTermLabelRefactoring.defineRefactoringScope(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Defines if a refactoring is required and if so in which
TermLabelRefactoring.RefactoringScope . |
TermLabelRefactoring.RefactoringScope |
RemoveInCheckBranchesTermLabelRefactoring.defineRefactoringScope(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Defines if a refactoring is required and if so in which
TermLabelRefactoring.RefactoringScope . |
boolean |
ChildTermLabelPolicy.isRuleApplicationSupported(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock)
Decides if the currently active
Rule application is supported or not. |
TermLabel |
OriginTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label) |
TermLabel |
TermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
TermLabel |
PerpetualTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label) |
TermLabel |
StayOnOperatorTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
TermLabel |
StayOnFormulaTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
protected void |
FormulaTermLabelRefactoring.refactorBewlowUpdates(PosInOccurrence applicationPosInOccurrence,
Term term,
java.util.List<TermLabel> labels)
Refactors the
Term below its update. |
void |
TermLabelRefactoring.refactorLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
java.util.List<TermLabel> labels)
This method is used to refactor the labels of the given
Term . |
void |
OriginTermLabelRefactoring.refactorLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
java.util.List<TermLabel> labels) |
void |
FormulaTermLabelRefactoring.refactorLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
java.util.List<TermLabel> labels)
This method is used to refactor the labels of the given
Term . |
void |
RemoveInCheckBranchesTermLabelRefactoring.refactorLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
java.util.List<TermLabel> labels)
This method is used to refactor the labels of the given
Term . |
void |
TermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
FormulaTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
LoopBodyTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
BlockContractValidityTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
SymbolicExecutionTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
LoopInvariantNormalBehaviorTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
Modifier and Type | Method and Description |
---|---|
PosInOccurrence |
MergePartner.getPio() |
Modifier and Type | Method and Description |
---|---|
CloseAfterMergeRuleBuiltInRuleApp |
CloseAfterMerge.createApp(PosInOccurrence pio,
Node thePartnerNode,
Node correspondingMergeNode,
SymbolicExecutionState mergeNodeState,
SymbolicExecutionState partnerState,
Term pc,
java.util.Set<Name> newNames)
Creates a complete CloseAfterMergeBuiltInRuleApp.
|
IBuiltInRuleApp |
MergeRule.createApp(PosInOccurrence pio,
TermServices services) |
IBuiltInRuleApp |
CloseAfterMerge.createApp(PosInOccurrence pos,
TermServices services) |
static ImmutableList<MergePartner> |
MergeRule.findPotentialMergePartners(Goal goal,
PosInOccurrence pio)
Finds all suitable merge partners
|
boolean |
MergeRule.isApplicable(Goal goal,
PosInOccurrence pio)
We admit top level formulas of the form \<{ ...
|
boolean |
CloseAfterMerge.isApplicable(Goal goal,
PosInOccurrence pio) |
static boolean |
MergeRule.isOfAdmissibleForm(Goal goal,
PosInOccurrence pio,
boolean doMergePartnerCheck)
We admit top level formulas of the form \<{ ...
|
AbstractBuiltInRuleApp |
CloseAfterMergeRuleBuiltInRuleApp.replacePos(PosInOccurrence newPos) |
AbstractBuiltInRuleApp |
MergeRuleBuiltInRuleApp.replacePos(PosInOccurrence newPos) |
void |
MergePartner.setPio(PosInOccurrence pio) |
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
CloseAfterMergeRuleBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
IBuiltInRuleApp |
MergeRuleBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
Constructor and Description |
---|
MergeRuleBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts) |
MergeRuleBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
Node mergeNode,
ImmutableList<MergePartner> mergePartners,
MergeProcedure concreteRule,
SymbolicExecutionStateWithProgCnt thisSEState,
ImmutableList<SymbolicExecutionState> mergePartnerStates,
Term distForm,
java.util.ArrayList<MergeRule.MergeRuleProgressListener> progressListeners) |
Modifier and Type | Method and Description |
---|---|
Term |
WhileInvariantTransformer.transform(TermLabelState termLabelState,
Rule rule,
RuleApp ruleApp,
Goal goal,
Sequent applicationSequent,
PosInOccurrence applicationPos,
Term initialPost,
Term invariantFramingTermination,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Modifier and Type | Method and Description |
---|---|
PosInOccurrence |
RuleAppSMT.posInOccurrence() |
Modifier and Type | Method and Description |
---|---|
RuleAppSMT |
RuleAppSMT.SMTRule.createApp(PosInOccurrence pos) |
RuleAppSMT |
RuleAppSMT.SMTRule.createApp(PosInOccurrence pos,
TermServices services) |
boolean |
RuleAppSMT.SMTRule.isApplicable(Goal goal,
PosInOccurrence pio) |
RuleAppSMT |
RuleAppSMT.replacePos(PosInOccurrence newPos) |
Modifier and Type | Method and Description |
---|---|
RuleAppSMT |
RuleAppSMT.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
Modifier and Type | Method and Description |
---|---|
protected PosInOccurrence |
FindTacletAppContainer.getPosInOccurrence(Goal p_goal) |
protected PosInOccurrence |
TacletAppContainer.getPosInOccurrence(Goal p_goal) |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
SimpleFilteredStrategy.computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal)
Evaluate the cost of a
RuleApp . |
RuleAppCost |
FIFOStrategy.computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal)
Evaluate the cost of a
RuleApp . |
RuleAppCost |
IsInRangeProvable.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
JavaCardDLStrategy.computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal)
Evaluate the cost of a
RuleApp . |
static RuleAppContainer |
RuleAppContainer.createAppContainer(RuleApp p_app,
PosInOccurrence p_pio,
Goal p_goal)
Create container for a RuleApp.
|
static ImmutableList<RuleAppContainer> |
RuleAppContainer.createAppContainers(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos,
Goal goal)
Create containers for RuleApps.
|
protected Term |
IsInRangeProvable.createConsequence(PosInOccurrence pos,
Services services)
creates the term to be proven to follow from a (possibly empty) set of axioms
|
protected static TacletAppContainer |
TacletAppContainer.createContainer(NoPosTacletApp p_app,
PosInOccurrence p_pio,
Goal p_goal,
boolean p_initial) |
protected static ImmutableList<RuleAppContainer> |
TacletAppContainer.createInitialAppContainers(ImmutableList<NoPosTacletApp> p_app,
PosInOccurrence p_pio,
Goal p_goal) |
protected boolean |
IntroducedSymbolBy.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected abstract RuleAppCost |
AbstractFeatureStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
protected RuleAppCost |
JavaCardDLStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
void |
SimpleFilteredStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal,
RuleAppCostCollector collector) |
void |
Strategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal,
RuleAppCostCollector collector)
Instantiate an incomplete
RuleApp . |
void |
FIFOStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal,
RuleAppCostCollector collector) |
void |
AbstractFeatureStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal,
RuleAppCostCollector collector) |
boolean |
SimpleFilteredStrategy.isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal)
Re-Evaluate a
RuleApp . |
boolean |
Strategy.isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal)
Re-Evaluate a
RuleApp . |
boolean |
FIFOStrategy.isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal)
Re-Evaluate a
RuleApp . |
boolean |
JavaCardDLStrategy.isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal)
Re-Evaluate a
RuleApp . |
protected boolean |
FocussedRuleApplicationManager.isRuleApplicationForFocussedFormula(RuleApp rule,
PosInOccurrence pos) |
void |
FocussedBreakpointRuleApplicationManager.ruleAdded(RuleApp rule,
PosInOccurrence pos) |
void |
FocussedRuleApplicationManager.ruleAdded(RuleApp rule,
PosInOccurrence pos) |
void |
QueueRuleApplicationManager.ruleAdded(RuleApp rule,
PosInOccurrence pos)
Implementation of the method from
NewRuleListener . |
void |
FocussedBreakpointRuleApplicationManager.rulesAdded(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos) |
void |
FocussedRuleApplicationManager.rulesAdded(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos) |
void |
QueueRuleApplicationManager.rulesAdded(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos)
Implementation of the method from
NewRuleListener . |
Constructor and Description |
---|
FocussedRuleApplicationManager(AutomatedRuleApplicationManager delegate,
Goal goal,
PosInOccurrence focussedSubterm) |
Constructor and Description |
---|
FocussedBreakpointRuleApplicationManager(AutomatedRuleApplicationManager delegate,
Goal goal,
java.util.Optional<PosInOccurrence> focussedSubterm,
java.util.Optional<java.lang.String> breakpoint) |
Modifier and Type | Method and Description |
---|---|
protected abstract boolean |
TopLevelFindFeature.checkPosition(PosInOccurrence pos) |
protected boolean |
NonDuplicateAppFeature.comparePio(TacletApp newApp,
TacletApp oldApp,
PosInOccurrence newPio,
PosInOccurrence oldPio) |
protected boolean |
NonDuplicateAppModPositionFeature.comparePio(TacletApp newApp,
TacletApp oldApp,
PosInOccurrence newPio,
PosInOccurrence oldPio) |
protected boolean |
EqNonDuplicateAppFeature.comparePio(TacletApp newApp,
TacletApp oldApp,
PosInOccurrence newPio,
PosInOccurrence oldPio) |
protected boolean |
InfFlowContractAppFeature.comparePio(TacletApp newApp,
TacletApp oldApp,
PosInOccurrence newPio,
PosInOccurrence oldPio)
Compare whether two
PosInOccurrence s are equal. |
protected abstract boolean |
AbstractNonDuplicateAppFeature.comparePio(TacletApp newApp,
TacletApp oldApp,
PosInOccurrence newPio,
PosInOccurrence oldPio)
Compare whether two
PosInOccurrence s are equal. |
RuleAppCost |
CountBranchFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Compute the cost of a RuleApp.
|
RuleAppCost |
AgeFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
BinaryFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ConstFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
FocusIsSubFormulaOfInfFlowContractAppFeature.computeCost(RuleApp ruleApp,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
LetFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
IfThenElseMalusFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
FindDepthFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ComprehendedSumFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
PrintFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
SimplifyReplaceKnownCandidateFeature.computeCost(RuleApp ruleApp,
PosInOccurrence pos,
Goal goal)
Compute the cost of a RuleApp.
|
RuleAppCost |
Feature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Evaluate the cost of a
RuleApp . |
RuleAppCost |
ShannonFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
RuleSetDispatchFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ContainsTermFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
SumFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
FindRightishFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
DeleteMergePointRuleFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ConditionalFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
MergeRuleFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
AbstractBetaFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Compute the cost of a RuleApp.
|
RuleAppCost |
InfFlowContractAppFeature.computeCost(RuleApp ruleApp,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
QueryExpandCost.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ApplyTFFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
NonDuplicateAppFeature.containsRuleApp(ImmutableList<RuleApp> list,
TacletApp rapp,
PosInOccurrence pio) |
protected RuleAppCost |
ContainsQuantifierFeature.doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
protected RuleAppCost |
PurePosDPathFeature.doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
protected RuleAppCost |
CountMaxDPathFeature.doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
protected RuleAppCost |
LeftmostNegAtomFeature.doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
protected RuleAppCost |
SimplifyBetaCandidateFeature.doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
protected RuleAppCost |
CountPosDPathFeature.doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
protected abstract RuleAppCost |
AbstractBetaFeature.doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
protected boolean |
InfFlowContractAppFeature.duplicateFindTaclet(TacletApp app,
PosInOccurrence pos,
Goal goal)
Search for a duplicate of the application
app by walking upwards in the proof tree. |
protected boolean |
SortComparisonFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
FocusInAntecFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
DependencyContractFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected abstract boolean |
BinaryFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal)
Compute whether the result of the feature is zero (
true )
or infinity (false ) |
protected boolean |
ThrownExceptionFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
ImplicitCastNecessary.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
DirectlyBelowFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
SeqContainsExecutableCodeFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
boolean |
FormulaAddedByRuleFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
BinaryTacletAppFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
NotInScopeOfModalityFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
boolean |
AllowedCutPositionFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
boolean |
NotBelowBinderFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
boolean |
NotBelowQuantifierFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
TriggerVarInstantiatedFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
SetsSmallerThanFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
MatchedIfFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
TacletRequiringInstantiationFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
OnlyInScopeOfQuantifiersFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
InEquationMultFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
AutomatedRuleFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
MonomialsSmallerThanFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
ReducibleMonomialsFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
TopLevelFindFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
TermSmallerThanFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
NoSelfApplicationFeature.filter(TacletApp p_app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
DiffFindAndIfFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
AtomsSmallerThanFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected abstract boolean |
BinaryTacletAppFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal)
Compute whether the result of the feature is zero (
true )
or infinity (false ) |
protected boolean |
SVNeedsInstantiation.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
boolean |
NonDuplicateAppFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
PolynomialValuesCmpFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
TrivialMonomialLCRFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
boolean |
NonDuplicateAppModPositionFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
boolean |
EqNonDuplicateAppFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
DiffFindAndReplacewithFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
InstantiatedSVFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
CheckApplyEqFeature.filter(TacletApp p_app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
SmallerThanFeature.lessThan(ImmutableList<Term> list1,
ImmutableList<Term> list2,
PosInOccurrence focus,
Goal currentGoal) |
protected boolean |
MonomialsSmallerThanFeature.lessThan(Term t1,
Term t2,
PosInOccurrence focus,
Goal goal)
this overwrites the method of
SmallerThanFeature |
protected boolean |
SmallerThanFeature.lessThan(Term t1,
Term t2,
PosInOccurrence focus,
Goal currentGoal) |
protected boolean |
AtomsSmallerThanFeature.lessThan(Term t1,
Term t2,
PosInOccurrence focus,
Goal goal)
this overwrites the method of
SmallerThanFeature |
protected boolean |
AbstractNonDuplicateAppFeature.noDuplicateFindTaclet(TacletApp app,
PosInOccurrence pos,
Goal goal)
Search for a duplicate of the application
app by walking
upwards in the proof tree. |
protected boolean |
SetsSmallerThanFeature.origLessThan(Term leftTerm,
Term rightTerm,
PosInOccurrence pos,
Goal goal) |
protected java.lang.Boolean |
AbstractPolarityFeature.polarity(PosInOccurrence pos,
java.lang.Boolean formulaPol) |
protected int |
QueryExpandCost.queryExpandAlreadyAppliedAtPos(RuleApp app,
PosInOccurrence pos,
Goal goal)
The method checks if the same rule has been applied earlier on this branch
at the same position in the sequent.
|
protected boolean |
InfFlowContractAppFeature.sameApplication(RuleApp ruleCmp,
TacletApp newApp,
PosInOccurrence newPio)
Check whether the old rule application
ruleCmp is a duplicate of the new application
newApp at position
newPio .newPio can be
null |
protected boolean |
AbstractNonDuplicateAppFeature.sameApplication(RuleApp ruleCmp,
TacletApp newApp,
PosInOccurrence newPio)
Check whether the old rule application
ruleCmp is a
duplicate of the new application newApp at position
newPio .newPio can be null |
Modifier and Type | Method and Description |
---|---|
PosInOccurrence |
RemoveParentUpdateModifier.modifyPosistion(PosInOccurrence pos) |
Modifier and Type | Method and Description |
---|---|
boolean |
FindPrefixRestrictionFeature.PrefixChecker.check(PosInOccurrence pio) |
protected boolean |
FindPrefixRestrictionFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
PosInOccurrence |
RemoveParentUpdateModifier.modifyPosistion(PosInOccurrence pos) |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
ForEachCP.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
OneOfCP.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
SVInstantiationCP.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
protected boolean |
LiteralsSmallerThanFeature.compareTerms(Term leftTerm,
Term rightTerm,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
InstantiationCostScalerFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
InstantiationCost.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Compute the cost of a RuleApp.
|
int |
QuanEliminationAnalyser.eliminableDefinition(Term definition,
PosInOccurrence envPIO) |
protected boolean |
SplittableQuantifiedFormulaFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
LiteralsSmallerThanFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
ClausesSmallerThanFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
ExistentiallyConnectedFormulasFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
HeuristicInstantiation.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
LiteralsSmallerThanFeature.lessThan(Term t1,
Term t2,
PosInOccurrence focus,
Goal goal)
this overwrites the method of
SmallerThanFeature |
protected boolean |
ClausesSmallerThanFeature.lessThan(Term t1,
Term t2,
PosInOccurrence focus,
Goal goal)
this overwrites the method of
SmallerThanFeature |
Constructor and Description |
---|
ConstraintAwareSyntacticalReplaceVisitor(TermLabelState termLabelState,
Services services,
Constraint metavariableInst,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Taclet.TacletLabelHint labelHint,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
protected boolean |
ContainsLabelNameFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
ContainsLabelFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
protected abstract java.util.Iterator<Term> |
SuperTermGenerator.createIterator(PosInOccurrence focus) |
java.util.Iterator<Term> |
HeapGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
TriggeredInstantiations.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
MultiplesModEquationsGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
TermGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
AllowedCutPositionsGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
SequentFormulasGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
RootsGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
SuperTermGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected Term |
SubtermGenerator.getTermInst(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
Term |
TermBuffer.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
AssumptionProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
ProjectionToTerm.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
TermConstructionProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
SVInstantiationProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
CoeffGcdProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
SubtermProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
TriggerVariableInstantiationProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
AbstractDividePolynomialsProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
ReduceMonomialsProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
FocusProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
FocusFormulaProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Modifier and Type | Field and Description |
---|---|
protected PosInOccurrence |
AbstractUpdateExtractor.modalityPio
The
PosInOccurrence of the modality or its updates. |
Modifier and Type | Method and Description |
---|---|
PosInOccurrence |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
PosInOccurrence |
ExecutionNodeReader.KeYlessMethodReturnValue.getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
PosInOccurrence |
ExecutionNodeReader.KeYlessConstraint.getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
PosInOccurrence |
ExecutionNodeReader.KeYlessVariable.getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
PosInOccurrence |
ExecutionNodeReader.KeYlessValue.getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
Modifier and Type | Method and Description |
---|---|
protected static void |
TruthValueTracingUtil.checkForNewMinorIds(Node childNode,
Term term,
Name termLabelName,
PosInOccurrence parentPio,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Checks if new minor IDs are available.
|
protected static void |
TruthValueTracingUtil.checkForNewMinorIdsOSS(SequentFormula onlyChangedChildSF,
Term term,
Name termLabelName,
PosInOccurrence parentPio,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Checks if new minor IDs are available in case of
OneStepSimplifier usage. |
protected ImmutableList<Term> |
AbstractUpdateExtractor.computeOriginalUpdates(PosInOccurrence pio,
boolean currentLayout)
Computes the original updates.
|
protected void |
SymbolicExecutionTreeBuilder.initNewMethodCallStack(Node currentNode,
PosInOccurrence childPIO)
Initializes a new method call stack.
|
protected static void |
TruthValueTracingUtil.updatePredicateResultBasedOnNewMinorIdsOSS(PosInOccurrence childPio,
PosInOccurrence parentPio,
Name termLabelName,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Updates the
PredicateResult s based on minor ID changes if
available in case of OneStepSimplifier usage. |
Constructor and Description |
---|
AbstractUpdateExtractor(Node node,
PosInOccurrence modalityPio)
Constructor.
|
ExecutionVariableExtractor(Node node,
PosInOccurrence modalityPio,
IExecutionNode<?> executionNode,
Term condition,
boolean simplifyConditions)
Constructor.
|
ExtractedExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
IProgramVariable programVariable,
Term arrayIndex,
Term arrayStartIndex,
Term arrayEndIndex,
Term additionalCondition,
ExecutionVariableExtractor.ExtractedExecutionValue parentValue)
Constructor.
|
SymbolicLayoutExtractor(Node node,
PosInOccurrence modalityPio,
boolean useUnicode,
boolean usePrettyPrinting,
boolean simplifyConditions)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
PosInOccurrence |
IExecutionElement.getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
Modifier and Type | Method and Description |
---|---|
PosInOccurrence |
AbstractExecutionVariable.getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
PosInOccurrence |
ExecutionConstraint.getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
PosInOccurrence |
ExecutionMethodReturnValue.getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
PosInOccurrence |
AbstractExecutionValue.getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
PosInOccurrence |
AbstractExecutionNode.getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
protected PosInOccurrence |
ExecutionStart.lazyComputeModalityPIO()
Computes the
PosInOccurrence lazily when AbstractExecutionNode.getModalityPIO() is
called the first time. |
protected PosInOccurrence |
ExecutionBranchCondition.lazyComputeModalityPIO()
Computes the
PosInOccurrence lazily when AbstractExecutionNode.getModalityPIO() is
called the first time. |
protected PosInOccurrence |
AbstractExecutionNode.lazyComputeModalityPIO()
Computes the
PosInOccurrence lazily when AbstractExecutionNode.getModalityPIO() is
called the first time. |
Constructor and Description |
---|
AbstractExecutionVariable(ITreeSettings settings,
Node proofNode,
IProgramVariable programVariable,
IExecutionValue parentValue,
Term arrayIndex,
Term additionalCondition,
PosInOccurrence modalityPIO)
Constructor.
|
ExecutionAllArrayIndicesVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
IProgramVariable arrayProgramVariable,
Term additionalCondition)
Constructor.
|
ExecutionConstraint(ITreeSettings settings,
Node proofNode,
PosInOccurrence modalityPIO,
Term term)
Constructor.
|
ExecutionMethodReturnValue(ITreeSettings settings,
Node proofNode,
PosInOccurrence modalityPIO,
Term returnValue,
Term condition)
Constructor.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
IProgramVariable programVariable,
Term additionalCondition)
Constructor for a "normal" child value.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
Term arrayIndex,
ExecutionValue lengthValue,
Term additionalCondition)
Constructor for an array cell value.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
IProgramVariable programVariable,
Term additionalCondition)
Constructor for a "normal" value.
|
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
ModalitySideProofRule.createApp(PosInOccurrence pos,
TermServices services) |
IBuiltInRuleApp |
QuerySideProofRule.createApp(PosInOccurrence pos,
TermServices services) |
boolean |
ModalitySideProofRule.isApplicable(Goal goal,
PosInOccurrence pio)
returns true iff a rule is applicable at the given
position.
|
boolean |
QuerySideProofRule.isApplicable(Goal goal,
PosInOccurrence pio)
returns true iff a rule is applicable at the given
position.
|
protected boolean |
QuerySideProofRule.isApplicableQuery(Goal goal,
Term pmTerm,
PosInOccurrence pio)
Checks if the query term is supported.
|
protected static SequentFormula |
AbstractSideProofRule.replace(PosInOccurrence pio,
Term newTerm,
Services services)
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
CutHeapObjectsFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal)
Compute whether the result of the feature is zero (
true )
or infinity (false ) |
java.util.Iterator<Term> |
CutHeapObjectsTermGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
static IExecutionVariable[] |
SymbolicExecutionUtil.createAllExecutionVariables(IExecutionNode<?> node,
Node proofNode,
PosInOccurrence modalityPIO,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static IExecutionVariable[] |
SymbolicExecutionUtil.createExecutionVariables(IExecutionNode<?> node,
Node proofNode,
PosInOccurrence modalityPIO,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.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 |
SymbolicExecutionUtil.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 Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term newSuccedent)
|
static Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term additionalAntecedent,
Term newSuccedent,
boolean addResultLabel)
|
static Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term additionalAntecedent,
Term newSuccedent,
ImmutableList<Term> updates,
boolean addResultLabel)
|
static Node |
SymbolicExecutionUtil.findMethodCallNode(Node node,
PosInOccurrence pio)
Searches for the given
Node the parent node
which also represents a symbolic execution tree node
(checked via SymbolicExecutionUtil.isSymbolicExecutionTreeNode(Node, RuleApp) ). |
static IProgramVariable |
SymbolicExecutionUtil.findSelfTerm(Node node,
PosInOccurrence pio)
|
static Term |
SymbolicExecutionUtil.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 boolean |
SymbolicExecutionUtil.isBlockContractValidityBranch(PosInOccurrence pio)
Checks if the modality at the given
PosInOccurrence represents the validity branch of an applied block contract. |
static Term |
SymbolicExecutionUtil.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 |
SymbolicExecutionUtil.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 |
SymbolicExecutionUtil.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 |
SymbolicExecutionUtil.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. |
Modifier and Type | Method and Description |
---|---|
void |
MediatorProofControl.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc)
|
boolean |
MediatorProofControl.selectedTaclet(Taclet taclet,
Goal goal,
PosInOccurrence pos) |
Modifier and Type | Method and Description |
---|---|
static void |
MergeRuleUtils.closeMergePartnerGoal(Node mergeNodeParent,
Goal mergePartner,
PosInOccurrence pio,
SymbolicExecutionState mergeState,
SymbolicExecutionState mergePartnerState,
Term pc,
java.util.Set<Name> newNames)
Closes the given partner goal, using the
CloseAfterMerge rule. |
static SymbolicExecutionState |
MergeRuleUtils.sequentToSEPair(Node node,
PosInOccurrence pio,
Services services)
Converts a sequent (given by goal & pos in occurrence) to an SE state
(U,C).
|
static SymbolicExecutionStateWithProgCnt |
MergeRuleUtils.sequentToSETriple(Node node,
PosInOccurrence pio,
Services services)
Converts a sequent (given by goal & pos in occurrence) to an SE state
(U,C,p).
|
Modifier and Type | Method and Description |
---|---|
Node |
ProofExplorationService.applyChangeFormula(Goal g,
PosInOccurrence pio,
Term term,
Term newTerm) |
void |
ProofExplorationService.soundHide(Goal g,
PosInOccurrence pio,
Term term) |
Modifier and Type | Method and Description |
---|---|
void |
InteractionRecorder.runBuiltInRule(Goal goal,
IBuiltInRuleApp app,
BuiltInRule rule,
PosInOccurrence pos,
boolean forced) |
void |
InteractionRecorder.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc,
ProofMacroFinishedInfo info) |
Modifier and Type | Method and Description |
---|---|
PosInOccurrence |
MacroInteraction.getPos() |
PosInOccurrence |
OccurenceIdentifier.rebuildOn(Goal goal) |
Modifier and Type | Method and Description |
---|---|
static OccurenceIdentifier |
OccurenceIdentifier.get(PosInOccurrence p) |
void |
MacroInteraction.setPos(PosInOccurrence pos) |
Constructor and Description |
---|
MacroInteraction(Node node,
ProofMacro macro,
PosInOccurrence posInOcc,
ProofMacroFinishedInfo info) |
Copyright © 2003-2019 The KeY-Project.