Modifier and Type | Method and Description |
---|---|
void |
AbstractProofControl.applyInteractive(RuleApp app,
Goal goal) |
void |
ProofControl.applyInteractive(RuleApp app,
Goal goal)
Apply a RuleApp and continue with update simplification or strategy
application according to current settings.
|
TacletInstantiationModel[] |
AbstractProofControl.completeAndApplyApp(java.util.List<TacletApp> apps,
Goal goal) |
void |
RuleCompletionHandler.completeAndApplyTacletMatch(TacletInstantiationModel[] models,
Goal goal)
called to complete and apply a taclet instantiations
|
protected void |
AbstractProofControl.completeAndApplyTacletMatch(TacletInstantiationModel[] models,
Goal goal) |
IBuiltInRuleApp |
RuleCompletionHandler.completeBuiltInRuleApp(IBuiltInRuleApp app,
Goal goal,
boolean forced)
completes rule applications of built in rules
|
protected IBuiltInRuleApp |
AbstractProofControl.completeBuiltInRuleApp(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
static IBuiltInRuleApp |
AbstractProofControl.completeBuiltInRuleAppByDefault(IBuiltInRuleApp app,
Goal goal,
boolean forced)
Default implementation of
RuleCompletionHandler.completeBuiltInRuleApp(IBuiltInRuleApp, Goal, boolean) . |
TacletInstantiationModel |
AbstractProofControl.createModel(TacletApp app,
Goal goal) |
protected void |
AbstractProofControl.emitInteractiveRuleApplication(Goal goal,
RuleApp app) |
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.getNoFindTaclet(Goal focusedGoal) |
ImmutableList<TacletApp> |
ProofControl.getNoFindTaclet(Goal focusedGoal)
collects all applicable NoFindTaclets 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 |
AbstractProofControl.pruneTo(Goal goal)
Undo the last rule application on the given goal.
|
void |
InteractionListener.runBuiltInRule(Goal goal,
IBuiltInRuleApp app,
BuiltInRule rule,
PosInOccurrence pos,
boolean forced) |
void |
InteractionListener.runRule(Goal goal,
RuleApp app) |
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(ImmutableSet<TacletApp> applics,
Goal goal) |
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 |
---|---|
void |
AbstractProofControl.startAndWaitForAutoMode(Proof proof,
ImmutableList<Goal> goals)
Starts the auto mode for the given proof which must be contained
in this user interface and blocks the current thread until it
has finished.
|
void |
ProofControl.startAndWaitForAutoMode(Proof proof,
ImmutableList<Goal> goals)
Starts the auto mode for the given proof which must be contained
in this user interface and blocks the current thread until it
has finished.
|
void |
AbstractProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals)
|
void |
ProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals)
|
void |
DefaultProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals,
ProverTaskListener ptl) |
protected abstract void |
AbstractProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals,
ProverTaskListener ptl) |
Constructor and Description |
---|
TacletAssumesModel(Term ifFma,
ImmutableList<IfFormulaInstantiation> candidates,
TacletApp app,
Goal goal,
Services services,
NamespaceSet nss,
AbbrevMap scm) |
TacletFindModel(TacletApp app,
Services services,
NamespaceSet nss,
AbbrevMap scm,
Goal goal)
Create new data model for tree.
|
TacletInstantiationModel(TacletApp app,
Sequent seq,
NamespaceSet nss,
AbbrevMap scm,
Goal goal)
Create new data model for the apply Taclet dialog wrapping a combo box model
and a table model.
|
Modifier and Type | Method and Description |
---|---|
Goal |
KeYMediator.getSelectedGoal()
returns the current selected goal
|
Goal |
KeYSelectionModel.getSelectedGoal()
returns the goal the selected node belongs to, null if it is an inner node
|
Goal |
KeYSelectionModel.DefaultSelectionIterator.next() |
Modifier and Type | Method and Description |
---|---|
void |
KeYMediator.goalChosen(Goal goal)
sets the current goal
|
void |
KeYMediator.setBack(Goal goal) |
void |
KeYSelectionModel.setSelectedGoal(Goal g)
sets the node that is focused by the user
|
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
LoopContractExternalCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
LoopApplyHeadCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
BlockContractInternalCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
InteractiveRuleApplicationCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced)
method called to complete the given builtin rule application
|
IBuiltInRuleApp |
BlockContractExternalCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
LoopInvariantRuleCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
IBuiltInRuleApp |
FunctionalOperationContractCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
IBuiltInRuleApp |
LoopContractInternalCompletion.complete(IBuiltInRuleApp application,
Goal goal,
boolean force) |
IBuiltInRuleApp |
DependencyContractCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
void |
WindowUserInterfaceControl.completeAndApplyTacletMatch(TacletInstantiationModel[] models,
Goal goal) |
IBuiltInRuleApp |
WindowUserInterfaceControl.completeBuiltInRuleApp(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
Constructor and Description |
---|
InfoTreeModel(Goal goal,
XMLResources xmlResources,
MainWindow mainWindow) |
ProofScriptWorker(KeYMediator mediator,
java.lang.String script,
Location location,
Goal initiallySelectedGoal)
Instantiates a new proof script worker.
|
TacletMatchCompletionDialog(MainWindow parent,
TacletInstantiationModel[] model,
Goal goal,
KeYMediator mediator) |
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
MergeRuleCompletion.complete(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
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 |
---|
AbstractionPredicatesChoiceDialog(Goal goal,
java.util.List<LocationVariable> differingLocVars)
Constructs a new
AbstractionPredicatesChoiceDialog . |
Modifier and Type | Method and Description |
---|---|
void |
CurrentGoalView.setPrinter(Goal goal)
sets the LogicPrinter to use
|
Modifier and Type | Method and Description |
---|---|
abstract java.lang.Iterable<Goal> |
DisableGoal.getGoalList()
an implementation should return an iterable collection over those
goals that are to be disabled or enabled according to the setting of
DisableGoal.enableGoals . |
Modifier and Type | Method and Description |
---|---|
protected static void |
AbstractFinishAuxiliaryComputationMacro.addContractApplicationTaclets(Goal initiatingGoal,
Proof symbExecProof) |
RuleAppCost |
UseInformationFlowContractMacro.PropExpansionStrategy.computeCost(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal) |
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 |
---|---|
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) |
Modifier and Type | Method and Description |
---|---|
Goal |
LoopInvExecutionPO.getInitiatingGoal() |
Goal |
BlockExecutionPO.getInitiatingGoal() |
Goal |
SymbolicExecutionPO.getInitiatingGoal() |
Constructor and Description |
---|
BlockExecutionPO(InitConfig initConfig,
BlockContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context) |
BlockExecutionPO(InitConfig initConfig,
BlockContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Services services)
To be used only for auxiliary proofs where the services object of
the actual proof has to be used instead of the initial services form
the InitConfig.
|
LoopInvExecutionPO(InitConfig initConfig,
LoopSpecification loopInv,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Term guardTerm) |
LoopInvExecutionPO(InitConfig initConfig,
LoopSpecification loopInv,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Term guardTerm,
Services services)
To be used only for auxiliary proofs where the services object of
the actual proof has to be used instead of the initial services form
the InitConfig.
|
SymbolicExecutionPO(InitConfig initConfig,
InformationFlowContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal) |
SymbolicExecutionPO(InitConfig initConfig,
InformationFlowContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
Services services)
To be used only for auxiliary proofs where the services object of
the actual proof has to be used instead of the initial services form
the InitConfig.
|
Modifier and Type | Method and Description |
---|---|
static boolean |
InfFlowCheckInfo.get(Goal goal) |
static boolean |
InfFlowCheckInfo.isInfFlow(Goal goal) |
static void |
InfFlowCheckInfo.set(Goal goal,
boolean checkForInfFlow) |
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 |
---|---|
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) |
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 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 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 |
---|---|
ImmutableList<Goal> |
ProofMacroFinishedInfo.getGoals() |
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractBlastingMacro.addInvariantFormula(Goal goal) |
RuleAppCost |
FilterStrategy.computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal) |
RuleAppCost |
PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy.computeCost(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal) |
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 |
---|---|
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 |
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) |
Constructor and Description |
---|
ProofMacroFinishedInfo(ProofMacro macro,
Goal goal) |
Constructor and Description |
---|
ProofMacroFinishedInfo(ProofMacro macro,
ImmutableList<Goal> goals) |
Modifier and Type | Method and Description |
---|---|
Goal |
EngineState.getFirstOpenAutomaticGoal() |
Goal |
EngineState.getFirstOpenGoal(boolean checkAutomatic)
Returns the first open goal, which has to be automatic iff checkAutomatic
is true.
|
protected static Goal |
EngineState.getGoal(ImmutableList<Goal> openGoals,
Node node) |
Modifier and Type | Method and Description |
---|---|
void |
EngineState.setGoal(Goal g) |
Modifier and Type | Method and Description |
---|---|
protected static Goal |
EngineState.getGoal(ImmutableList<Goal> openGoals,
Node node) |
Constructor and Description |
---|
ProofScriptEngine(java.lang.String script,
Location initLocation,
Goal initiallySelectedGoal)
Instantiates a new proof script engine.
|
Modifier and Type | Method and Description |
---|---|
Goal |
Goal.clone(Node node)
clones the goal (with copy of tacletindex and ruleAppIndex).
|
Goal |
Goal.copy()
like the clone method but returns right type
|
Goal |
Proof.getClosedGoal(Node node)
Get the closed goal belonging to the given node if it exists.
|
Goal |
ProofTreeEvent.getGoal() |
Goal |
Proof.getGoal(Node node)
returns the goal that belongs to the given node or null if the
node is an inner one
|
Goal |
Goal.getLinkedGoal()
Returns the goal that this goal is linked to.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
Proof.allGoals()
Returns the list of all, open and closed, goals.
|
ImmutableList<Goal> |
Goal.apply(RuleApp ruleApp) |
ImmutableList<Goal> |
Proof.closedGoals()
Returns the list of closed goals, needed to make pruning in closed branches
possible.
|
ImmutableList<Goal> |
Proof.getClosedSubtreeGoals(Node node)
Returns a list of all (closed) goals of the closed subtree pending from this node.
|
ImmutableList<Goal> |
ProofTreeEvent.getGoals() |
ImmutableList<Goal> |
ProofEvent.getNewGoals()
returns the list of new goals (empty if a goal was closed) in case of a rule
application otherwise null
|
ImmutableList<Goal> |
Proof.getSubtreeEnabledGoals(Node node)
get the list of goals of the subtree starting with node which are enabled.
|
ImmutableList<Goal> |
Proof.getSubtreeGoals(Node node)
returns the list of goals of the subtree starting with node.
|
ImmutableList<Goal> |
Proof.openEnabledGoals()
return the list of open and enabled goals
|
ImmutableList<Goal> |
Proof.openGoals()
Returns the list of open goals.
|
ImmutableList<Goal> |
Goal.split(int n)
creates n new nodes as children of the
referenced node and new
n goals that have references to these new nodes.
|
Modifier and Type | Method and Description |
---|---|
void |
Proof.add(Goal goal)
adds a new goal to the list of goals
|
void |
GoalListener.automaticStateChanged(Goal source,
boolean oldAutomatic,
boolean newAutomatic)
Informs the listener that the automatic state
isAutomatic() has changed. |
void |
Proof.closeGoal(Goal goalToClose)
Add the given constraint to the closure constraint of the given
goal, i.e.
|
protected void |
Goal.fireGoalReplaced(Goal goal,
Node parent,
ImmutableList<Goal> newGoals) |
protected void |
Proof.fireProofGoalRemoved(Goal goal)
fires the event that a goal has been removed from the list of goals
|
protected void |
Proof.fireProofGoalsAdded(Goal goal)
fires the event that new goals have been added to the list of
goals
|
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
|
void |
GoalListener.goalReplaced(Goal source,
Node parent,
ImmutableList<Goal> newGoals)
Informs the listener that the given goal
source
has been replaced by the goals newGoals (note that
source may be an element of
newGoals ). |
static boolean |
Goal.hasApplicableRules(Goal goal)
Checks if the
Goal has applicable rules. |
void |
Proof.pruneProof(Goal goal)
Performs an undo operation on the given goal.
|
void |
Proof.reOpenGoal(Goal goal)
Opens a previously closed node (the one corresponding to p_goal)
and all its closed parents.
|
void |
Proof.replace(Goal oldGoal,
ImmutableList<Goal> newGoals)
removes the given goal and adds the new goals in list
|
void |
BuiltInRuleAppIndex.reportRuleApps(NewRuleListener l,
Goal goal) |
void |
BuiltInRuleAppIndex.scanApplicableRules(Goal goal) |
void |
RuleAppIndex.scanBuiltInRules(Goal p_goal)
Report builtin rules to all registered NewRuleListener instances.
|
void |
FormulaTagManager.sequentChanged(Goal source,
SequentChangeInfo sci) |
void |
RuleAppIndex.sequentChanged(Goal g,
SequentChangeInfo sci)
called if a formula has been replaced
|
void |
BuiltInRuleAppIndex.sequentChanged(Goal goal,
SequentChangeInfo sci)
called if a formula has been replaced
|
void |
TacletAppIndex.sequentChanged(Goal goal,
SequentChangeInfo sci)
called if a formula has been replaced
|
void |
GoalListener.sequentChanged(Goal source,
SequentChangeInfo sci)
informs the listener about a change that occured to the sequent of goal
|
void |
Goal.setLinkedGoal(Goal linkedGoal)
Sets the node that this goal is linked to; also sets this for
all parents.
|
void |
RuleAppIndex.setup(Goal p_goal) |
void |
TacletAppIndex.setup(Goal p_goal)
Set the goal association of this index to the given object
p_goal . |
Modifier and Type | Method and Description |
---|---|
void |
Proof.add(ImmutableList<Goal> goals)
adds a list with new goals to the list of open goals
|
protected void |
Goal.fireGoalReplaced(Goal goal,
Node parent,
ImmutableList<Goal> newGoals) |
protected void |
Proof.fireProofGoalsAdded(ImmutableList<Goal> goals)
fires the event that new goals have been added to the list of
goals
|
void |
GoalListener.goalReplaced(Goal source,
Node parent,
ImmutableList<Goal> newGoals)
Informs the listener that the given goal
source
has been replaced by the goals newGoals (note that
source may be an element of
newGoals ). |
void |
Proof.replace(Goal oldGoal,
ImmutableList<Goal> newGoals)
removes the given goal and adds the new goals in list
|
Constructor and Description |
---|
ProofTreeEvent(Proof source,
Goal goal)
Create ProofTreeEvent for the event that happened to the
given goal
|
Constructor and Description |
---|
ProofEvent(Proof source,
RuleAppInfo rai,
ImmutableList<Goal> newGoals)
creates a proof event for a change triggered by a rule applications
|
ProofTreeEvent(Proof source,
ImmutableList<Goal> goals)
Create ProofTreeEvent for the event that affects the goals
given in the list.
|
Modifier and Type | Field and Description |
---|---|
Goal |
NodeGoalPair.goal |
Modifier and Type | Method and Description |
---|---|
Goal |
DelayedCut.getRemainingGoal() |
Constructor and Description |
---|
NodeGoalPair(Node node,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
Goal |
IntermediateProofReplayer.getLastSelectedGoal() |
Modifier and Type | Method and Description |
---|---|
static TacletApp |
IntermediateProofReplayer.parseSV2(TacletApp app,
SchemaVariable sv,
java.lang.String value,
Goal targetGoal)
Instantiates a schema variable in the given taclet application.
|
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 |
---|---|
void |
JoinProcessor.Listener.endOfJoining(ImmutableList<Goal> goals) |
Modifier and Type | Method and Description |
---|---|
void |
NodeChangeJournal.automaticStateChanged(Goal source,
boolean oldAutomatic,
boolean newAutomatic) |
void |
NodeChangeJournal.goalReplaced(Goal source,
Node parent,
ImmutableList<Goal> newGoals)
Informs the listener that the given goal
source
has been replaced by the goals newGoals (note that
source may be an element of
newGoals ). |
void |
NodeChangeJournal.sequentChanged(Goal source,
SequentChangeInfo sci)
informs the listener about a change that occured to the sequent
of goal
|
Modifier and Type | Method and Description |
---|---|
void |
NodeChangeJournal.goalReplaced(Goal source,
Node parent,
ImmutableList<Goal> newGoals)
Informs the listener that the given goal
source
has been replaced by the goals newGoals (note that
source may be an element of
newGoals ). |
Constructor and Description |
---|
NodeChangeJournal(Proof p_proof,
Goal p_goal) |
Modifier and Type | Method and Description |
---|---|
Goal |
GoalChooser.getNextGoal() |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
StopCondition.getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
boolean |
StopCondition.isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
void |
GoalChooser.removeGoal(Goal p_goal)
Remove p_goal from selectedList (e.g.
|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
Goal goal)
starts a proof search for a given goals using the given strategy settings
instead the ones configures in the proof
|
Modifier and Type | Method and Description |
---|---|
void |
GoalChooser.init(Proof p_proof,
ImmutableList<Goal> p_goals)
Initialise this DefaultGoalChooser for use with a given Proof and a list of goals.
|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
ImmutableList<Goal> goals)
starts a proof search for a set of goals using the given strategy settings
instead the ones configures in the proof
|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
ImmutableList<Goal> goals,
int maxSteps,
long timeout,
boolean stopAtFirstNonCloseableGoal)
This entry point to the proof may provide inconsistent data.
|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
ImmutableList<Goal> goals,
StrategySettings stratSet)
starts a proof search for a set of goals using the given strategy settings
instead the ones configures in the proof
|
void |
GoalChooser.updateGoalList(Node node,
ImmutableList<Goal> newGoals)
The given node has become an internal node of the proof tree, and the
children of the node are the given goals
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableList<Goal> |
DefaultGoalChooser.goalList
list of goals on which the strategy should be applied
|
protected ImmutableList<Goal> |
DefaultGoalChooser.nextGoals
part of goalList that should be worked on next
|
protected ImmutableList<Goal> |
DefaultGoalChooser.selectedList
Subset of the goals to which currently taclets are applied.
|
Modifier and Type | Method and Description |
---|---|
Goal |
SingleRuleApplicationInfo.getGoal() |
Goal |
DefaultGoalChooser.getNextGoal() |
Goal |
DepthFirstGoalChooser.getNextGoal() |
Goal |
ApplyStrategyInfo.nonCloseableGoal() |
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<Goal> |
DefaultGoalChooser.insertNewGoals(ImmutableList<Goal> newGoals,
ImmutableList<Goal> prevGoalList) |
protected ImmutableList<Goal> |
DepthFirstGoalChooser.insertNewGoals(ImmutableList<Goal> newGoals,
ImmutableList<Goal> prevGoalList) |
protected static ImmutableList<Goal> |
DefaultGoalChooser.rotateList(ImmutableList<Goal> p_list) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
AppliedRuleStopCondition.getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
boolean |
AppliedRuleStopCondition.isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
void |
DefaultGoalChooser.removeGoal(Goal p_goal) |
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
void |
DefaultGoalChooser.init(Proof p_proof,
ImmutableList<Goal> p_goals) |
protected ImmutableList<Goal> |
DefaultGoalChooser.insertNewGoals(ImmutableList<Goal> newGoals,
ImmutableList<Goal> prevGoalList) |
protected ImmutableList<Goal> |
DefaultGoalChooser.insertNewGoals(ImmutableList<Goal> newGoals,
ImmutableList<Goal> prevGoalList) |
protected ImmutableList<Goal> |
DepthFirstGoalChooser.insertNewGoals(ImmutableList<Goal> newGoals,
ImmutableList<Goal> prevGoalList) |
protected ImmutableList<Goal> |
DepthFirstGoalChooser.insertNewGoals(ImmutableList<Goal> newGoals,
ImmutableList<Goal> prevGoalList) |
protected static ImmutableList<Goal> |
DefaultGoalChooser.rotateList(ImmutableList<Goal> p_list) |
protected void |
DefaultGoalChooser.setupGoals(ImmutableList<Goal> p_goals) |
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
ImmutableList<Goal> goals) |
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
ImmutableList<Goal> goals,
int maxSteps,
long timeout,
boolean stopAtFirstNonCloseableGoal) |
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
ImmutableList<Goal> goals,
StrategySettings stratSet) |
void |
DefaultGoalChooser.updateGoalList(Node node,
ImmutableList<Goal> newGoals) |
protected void |
DefaultGoalChooser.updateGoalListHelp(Node node,
ImmutableList<Goal> newGoals) |
protected void |
DepthFirstGoalChooser.updateGoalListHelp(Node node,
ImmutableList<Goal> newGoals) |
Constructor and Description |
---|
ApplyStrategyInfo(java.lang.String message,
Proof proof,
java.lang.Throwable error,
Goal nonCloseableGoal,
long timeInMillis,
int appliedRuleAppsCount,
int nrClosedGoals) |
Modifier and Type | Field and Description |
---|---|
protected Goal |
SyntacticalReplaceVisitor.goal |
Goal |
AbstractLoopInvariantRule.LoopInvariantInformation.goal
The original goal.
|
Modifier and Type | Field and Description |
---|---|
ImmutableList<Goal> |
AbstractLoopInvariantRule.LoopInvariantInformation.goals
The goals created by the invariant rules application; those are
filled with content by the concrete loop invariant rules.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
BlockContractExternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
Taclet.apply(Goal goal,
Services services,
RuleApp tacletApp)
applies the given rule application to the specified goal
|
ImmutableList<Goal> |
QueryExpand.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
Rule.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
ImmutableList<Goal> |
OneStepSimplifier.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
WhileInvariantRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
BlockContractInternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopContractExternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopContractInternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
UseDependencyContractRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopApplyHeadRule.apply(Goal goal,
Services services,
RuleApp application) |
ImmutableList<Goal> |
UseOperationContractRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopScopeInvariantRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
AbstractBuiltInRuleApp.execute(Goal goal,
Services services)
applies the specified rule at the specified position
if all schema variables have been instantiated
|
ImmutableList<Goal> |
TacletApp.execute(Goal goal,
Services services)
applies the specified rule at the specified position if all schema
variables have been instantiated
|
ImmutableList<Goal> |
RuleApp.execute(Goal goal,
Services services)
applies the specified rule at the specified position
if all schema variables have been instantiated
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
BlockContractExternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
Taclet.apply(Goal goal,
Services services,
RuleApp tacletApp)
applies the given rule application to the specified goal
|
ImmutableList<Goal> |
QueryExpand.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
Rule.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
ImmutableList<Goal> |
OneStepSimplifier.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
WhileInvariantRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
BlockContractInternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopContractExternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopContractInternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
UseDependencyContractRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopApplyHeadRule.apply(Goal goal,
Services services,
RuleApp application) |
ImmutableList<Goal> |
UseOperationContractRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopScopeInvariantRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
boolean |
LoopApplyHeadBuiltInRuleApp.cannotComplete(Goal goal) |
boolean |
AbstractAuxiliaryContractBuiltInRuleApp.cannotComplete(Goal goal) |
protected static boolean |
AbstractBlockContractRule.contractApplied(BlockContract contract,
Goal goal) |
protected static boolean |
AbstractLoopContractRule.contractApplied(LoopContract contract,
Goal goal) |
AbstractLoopInvariantRule.LoopInvariantInformation |
AbstractLoopInvariantRule.doPreparations(Goal goal,
Services services,
RuleApp ruleApp)
Constructs the data needed for the currently implemented loop invariants;
also prepares the new set of goals, that is splitting the current goal is
no longer required after calling this method.
|
ImmutableList<Goal> |
AbstractBuiltInRuleApp.execute(Goal goal,
Services services)
applies the specified rule at the specified position
if all schema variables have been instantiated
|
ImmutableList<Goal> |
TacletApp.execute(Goal goal,
Services services)
applies the specified rule at the specified position if all schema
variables have been instantiated
|
ImmutableList<Goal> |
RuleApp.execute(Goal goal,
Services services)
applies the specified rule at the specified position
if all schema variables have been instantiated
|
protected static ImmutableSet<BlockContract> |
AbstractBlockContractRule.filterAppliedContracts(ImmutableSet<BlockContract> collectedContracts,
Goal goal) |
protected static ImmutableSet<LoopContract> |
AbstractLoopContractRule.filterAppliedContracts(ImmutableSet<LoopContract> collectedContracts,
Goal goal) |
IBuiltInRuleApp |
IBuiltInRuleApp.forceInstantiate(Goal goal) |
AbstractBuiltInRuleApp |
AbstractBuiltInRuleApp.forceInstantiate(Goal goal) |
ContractRuleApp |
ContractRuleApp.forceInstantiate(Goal goal) |
static ImmutableSet<BlockContract> |
AbstractBlockContractRule.getApplicableContracts(AbstractAuxiliaryContractRule.Instantiation instantiation,
Goal goal,
Services services) |
static ImmutableSet<LoopContract> |
AbstractLoopContractRule.getApplicableContracts(AbstractAuxiliaryContractRule.Instantiation instantiation,
Goal goal,
Services services) |
static ImmutableSet<BlockContract> |
AbstractBlockContractRule.getApplicableContracts(SpecificationRepository specifications,
JavaStatement statement,
Modality modality,
Goal goal) |
static ImmutableSet<LoopContract> |
AbstractLoopContractRule.getApplicableContracts(SpecificationRepository specifications,
JavaStatement statement,
Modality modality,
Goal goal) |
SequentFormula |
RewriteTaclet.getRewriteResult(Goal goal,
TermLabelState termLabelState,
Services services,
TacletApp app) |
protected boolean |
AbstractBlockContractRule.Instantiator.hasApplicableContracts(Services services,
JavaStatement statement,
Modality modality,
Goal goal) |
protected abstract boolean |
AbstractAuxiliaryContractRule.Instantiator.hasApplicableContracts(Services services,
JavaStatement element,
Modality modality,
Goal goal) |
protected boolean |
AbstractLoopContractRule.Instantiator.hasApplicableContracts(Services services,
JavaStatement statement,
Modality modality,
Goal goal) |
AbstractAuxiliaryContractRule.Instantiation |
AbstractBlockContractRule.instantiate(Term formula,
Goal goal,
Services services) |
AbstractAuxiliaryContractRule.Instantiation |
AbstractLoopContractRule.instantiate(Term formula,
Goal goal,
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. |
protected void |
AbstractBlockContractRule.setUpInfFlowPartOfUsageGoal(Goal usageGoal,
AbstractBlockContractRule.InfFlowValidityData infFlowValitidyData,
Term contextUpdate,
Term remembranceUpdate,
Term anonymisationUpdate,
TermBuilder tb) |
protected AbstractBlockContractRule.InfFlowValidityData |
AbstractBlockContractRule.setUpInfFlowValidityGoal(Goal infFlowGoal,
BlockContract contract,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
Services services,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
java.util.List<LocationVariable> heaps,
ImmutableSet<ProgramVariable> localInVariables,
ImmutableSet<ProgramVariable> localOutVariables,
BlockContractInternalBuiltInRuleApp application,
AbstractAuxiliaryContractRule.Instantiation instantiation) |
Term |
AuxiliaryContractBuilders.GoalsConfigurator.setUpLoopValidityGoal(Goal goal,
LoopContract contract,
Term context,
Term remember,
Term rememberNext,
java.util.Map<LocationVariable,Function> anonOutHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
Term[] assumptions,
Term decreasesCheck,
Term[] postconditions,
Term[] postconditionsNext,
ProgramVariable exceptionParameter,
AuxiliaryContract.Terms terms,
AuxiliaryContract.Variables nextVars) |
void |
AuxiliaryContractBuilders.GoalsConfigurator.setUpPreconditionGoal(Goal goal,
Term update,
Term[] preconditions)
Sets up the precondition goal.
|
void |
AuxiliaryContractBuilders.GoalsConfigurator.setUpUsageGoal(Goal goal,
Term[] updates,
Term[] assumptions)
Sets up the usage goal.
|
Term |
AuxiliaryContractBuilders.GoalsConfigurator.setUpValidityGoal(Goal goal,
Term[] updates,
Term[] assumptions,
Term[] postconditions,
ProgramVariable exceptionParameter,
AuxiliaryContract.Terms terms) |
Term |
AuxiliaryContractBuilders.GoalsConfigurator.setUpWdGoal(Goal goal,
BlockContract contract,
Term update,
Term anonUpdate,
LocationVariable heap,
Function anonHeap,
ImmutableSet<ProgramVariable> localIns) |
LoopInvariantBuiltInRuleApp |
LoopInvariantBuiltInRuleApp.tryToInstantiate(Goal goal) |
IBuiltInRuleApp |
IBuiltInRuleApp.tryToInstantiate(Goal goal)
Tries to complete the rule application from the available information.
|
abstract AbstractBuiltInRuleApp |
AbstractBuiltInRuleApp.tryToInstantiate(Goal goal) |
DefaultBuiltInRuleApp |
DefaultBuiltInRuleApp.tryToInstantiate(Goal goal) |
AbstractBuiltInRuleApp |
LoopApplyHeadBuiltInRuleApp.tryToInstantiate(Goal goal) |
LoopContractExternalBuiltInRuleApp |
LoopContractExternalBuiltInRuleApp.tryToInstantiate(Goal goal) |
UseDependencyContractApp |
UseDependencyContractApp.tryToInstantiate(Goal goal) |
BlockContractInternalBuiltInRuleApp |
BlockContractInternalBuiltInRuleApp.tryToInstantiate(Goal goal) |
abstract AbstractContractRuleApp |
AbstractContractRuleApp.tryToInstantiate(Goal goal) |
ContractRuleApp |
ContractRuleApp.tryToInstantiate(Goal goal) |
BlockContractExternalBuiltInRuleApp |
BlockContractExternalBuiltInRuleApp.tryToInstantiate(Goal goal) |
LoopContractInternalBuiltInRuleApp |
LoopContractInternalBuiltInRuleApp.tryToInstantiate(Goal goal) |
AbstractBlockContractBuiltInRuleApp |
AbstractBlockContractBuiltInRuleApp.tryToInstantiate(Goal goal,
AbstractBlockContractRule rule) |
AbstractLoopContractBuiltInRuleApp |
AbstractLoopContractBuiltInRuleApp.tryToInstantiate(Goal goal,
AbstractLoopContractRule rule) |
Constructor and Description |
---|
Instantiator(Term formula,
Goal goal,
Services services) |
Instantiator(Term formula,
Goal goal,
Services services) |
Instantiator(Term formula,
Goal goal,
Services services) |
LoopInvariantInformation(Goal goal,
Services services,
AbstractLoopInvariantRule.Instantiation inst,
LoopInvariantBuiltInRuleApp ruleApp,
ImmutableList<Goal> goals,
TermLabelState termLabelState,
Term invTerm,
Term variantPO,
Term reachableState,
Term anonUpdate,
Term wellFormedAnon,
Term uAnonInv,
Term frameCondition,
Term[] uBeforeLoopDefAnonVariant,
ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> anonUpdateData)
Creates a new
AbstractLoopInvariantRule.LoopInvariantInformation object. |
SyntacticalReplaceVisitor(TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
Goal goal,
Rule rule,
RuleApp ruleApp,
Services services,
TermBuilder termBuilder) |
SyntacticalReplaceVisitor(TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
SVInstantiations svInst,
Goal goal,
Rule rule,
RuleApp ruleApp,
Services services)
constructs a term visitor replacing any occurrence of a schemavariable found
in
svInst by its instantiation |
VariablesCreatorAndRegistrar(Goal goal,
AuxiliaryContract.Variables placeholderVariables,
Services services) |
Constructor and Description |
---|
LoopInvariantInformation(Goal goal,
Services services,
AbstractLoopInvariantRule.Instantiation inst,
LoopInvariantBuiltInRuleApp ruleApp,
ImmutableList<Goal> goals,
TermLabelState termLabelState,
Term invTerm,
Term variantPO,
Term reachableState,
Term anonUpdate,
Term wellFormedAnon,
Term uAnonInv,
Term frameCondition,
Term[] uBeforeLoopDefAnonVariant,
ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> anonUpdateData)
Creates a new
AbstractLoopInvariantRule.LoopInvariantInformation object. |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
RuleExecutor.apply(Goal goal,
Services services,
RuleApp ruleApp)
applies the given rule application to the specified goal
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
RuleExecutor.apply(Goal goal,
Services services,
RuleApp ruleApp)
applies the given rule application to the specified goal
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
NoFindTacletExecutor.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
abstract ImmutableList<Goal> |
TacletExecutor.apply(Goal goal,
Services services,
RuleApp tacletApp)
applies the given rule application to the specified goal
|
ImmutableList<Goal> |
FindTacletExecutor.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
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).
|
ImmutableList<Goal> |
NoFindTacletExecutor.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
abstract ImmutableList<Goal> |
TacletExecutor.apply(Goal goal,
Services services,
RuleApp tacletApp)
applies the given rule application to the specified goal
|
ImmutableList<Goal> |
FindTacletExecutor.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
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 |
NoFindTacletExecutor.applyAdd(TermLabelState termLabelState,
Sequent add,
SequentChangeInfo currentSequent,
Services services,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp)
adds the sequent of the add part of the Taclet to the goal sequent
|
protected void |
TacletExecutor.applyAddProgVars(ImmutableSet<SchemaVariable> pvs,
SequentChangeInfo currentSequent,
Goal goal,
PosInOccurrence posOfFind,
Services services,
MatchConditions matchCond) |
protected void |
TacletExecutor.applyAddrule(ImmutableList<Taclet> rules,
Goal goal,
Services services,
MatchConditions matchCond)
adds the given rules (i.e.
|
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<SequentChangeInfo> |
TacletExecutor.checkIfGoals(Goal p_goal,
ImmutableList<IfFormulaInstantiation> p_list,
MatchConditions p_matchCond,
int p_numberOfNewGoals)
Search for formulas within p_list that have to be proved by an
explicit assumes-goal, i.e.
|
SequentFormula |
RewriteTacletExecutor.getRewriteResult(Goal goal,
TermLabelState termLabelState,
Services services,
TacletApp app) |
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 . |
static boolean |
FormulaTermLabelRefactoring.isInnerMostParentRefactored(TermLabelState state,
Goal goal)
Checks if the inner most parent was already refactored on the given
Goal . |
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.refactorInCaseOfNewIdRequired(TermLabelState state,
Goal goal,
Term term,
Services services,
java.util.List<TermLabel> labels)
Refactors in case that the inner most label needs a new ID.
|
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 . |
protected void |
FormulaTermLabelRefactoring.refactorSpecificationApplication(Term term,
Goal goal,
Services services,
java.util.List<TermLabel> labels,
java.lang.Object hint)
Refactors a specification application.
|
static void |
FormulaTermLabelRefactoring.setInnerMostParentRefactored(TermLabelState state,
Goal goal,
boolean refactored)
Defines if the inner most parent was already refactored on the given
Goal . |
static boolean |
TermLabelRefactoring.shouldRefactorOnBuiltInRule(Rule rule,
Goal goal,
java.lang.Object hint)
Determines whether any refatorings should be applied on an application of the given
BuiltInRule . |
protected boolean |
FormulaTermLabelRefactoring.shouldRefactorSpecificationApplication(Rule rule,
Goal goal,
java.lang.Object hint)
Checks if the given hint requires a refactoring.
|
Modifier and Type | Method and Description |
---|---|
Goal |
MergePartner.getGoal() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
MergeRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
CloseAfterMerge.apply(Goal goal,
Services services,
RuleApp ruleApp) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
MergeRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
CloseAfterMerge.apply(Goal goal,
Services services,
RuleApp ruleApp) |
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 \<{ ...
|
void |
MergePartner.setGoal(Goal goal) |
AbstractBuiltInRuleApp |
CloseAfterMergeRuleBuiltInRuleApp.tryToInstantiate(Goal goal) |
AbstractBuiltInRuleApp |
MergeRuleBuiltInRuleApp.tryToInstantiate(Goal goal) |
Constructor and Description |
---|
MergePartner(Goal goal,
PosInOccurrence pio) |
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 |
---|---|
Goal |
SMTProblem.getGoal() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
RuleAppSMT.SMTRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
RuleAppSMT.SMTRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
boolean |
RuleAppSMT.SMTRule.isApplicable(Goal goal,
PosInOccurrence pio) |
RuleAppSMT |
RuleAppSMT.tryToInstantiate(Goal goal) |
Constructor and Description |
---|
SMTProblem(Goal goal) |
Modifier and Type | Method and Description |
---|---|
TacletApp |
TacletAppContainer.completeRuleApp(Goal p_goal)
Create a
RuleApp that is suitable to be applied
or null . |
abstract RuleApp |
RuleAppContainer.completeRuleApp(Goal p_goal)
Create a
RuleApp that is suitable to be applied
or null . |
RuleApp |
BuiltInRuleAppContainer.completeRuleApp(Goal goal) |
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 . |
long |
RuleAppFeature.cost(RuleApp app,
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 static TacletAppContainer |
TacletAppContainer.createContainer(NoPosTacletApp p_app,
PosInOccurrence p_pio,
Goal p_goal,
boolean p_initial) |
ImmutableList<RuleAppContainer> |
TacletAppContainer.createFurtherApps(Goal p_goal)
Create a list of new RuleAppContainers that are to be
considered for application.
|
abstract ImmutableList<RuleAppContainer> |
RuleAppContainer.createFurtherApps(Goal p_goal)
Create a list of new RuleAppContainers that are to be
considered for application.
|
ImmutableList<RuleAppContainer> |
BuiltInRuleAppContainer.createFurtherApps(Goal goal) |
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 PosInOccurrence |
FindTacletAppContainer.getPosInOccurrence(Goal p_goal) |
protected PosInOccurrence |
TacletAppContainer.getPosInOccurrence(Goal p_goal) |
protected boolean |
TacletAppContainer.ifFormulasStillValid(Goal p_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 |
FindTacletAppContainer.isStillApplicable(Goal p_goal) |
protected abstract boolean |
TacletAppContainer.isStillApplicable(Goal p_goal) |
protected boolean |
NoFindTacletAppContainer.isStillApplicable(Goal p_goal) |
void |
FocussedBreakpointRuleApplicationManager.setGoal(Goal p_goal) |
void |
FocussedRuleApplicationManager.setGoal(Goal p_goal) |
void |
AutomatedRuleApplicationManager.setGoal(Goal p_goal)
Set the goal
this is the rule app manager for |
void |
QueueRuleApplicationManager.setGoal(Goal p_goal) |
Constructor and Description |
---|
FocussedBreakpointRuleApplicationManager(AutomatedRuleApplicationManager delegate,
Goal goal,
java.util.Optional<PosInOccurrence> focussedSubterm,
java.util.Optional<java.lang.String> breakpoint) |
FocussedRuleApplicationManager(AutomatedRuleApplicationManager delegate,
Goal goal,
PosInOccurrence focussedSubterm) |
Modifier and Type | Method and Description |
---|---|
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 |
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 int |
AbstractMonomialSmallerThanFeature.introductionTime(Operator op,
Goal goal) |
protected static boolean |
QueryExpandCost.isStepCaseBranch(Goal goal)
This method determines whether the given goal belongs to a subtree of a
step case or body preserves case.
|
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 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.
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
FindPrefixRestrictionFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
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.
|
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 |
---|---|
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 abstract java.util.Iterator<SequentFormula> |
SequentFormulasGenerator.generateForIt(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 | Method and Description |
---|---|
protected java.util.Map<Goal,Term> |
AbstractUpdateExtractor.computeValueConditions(java.util.Set<Goal> valueGoals,
java.util.Map<Node,Term> branchConditionCache,
boolean simplifyConditions)
This method computes for all given
Goal s representing the same
value their path conditions. |
ImmutableList<Goal> |
AbstractUpdateExtractor.NodeGoal.getStartingGoals()
Returns the
Goal s at which backward iteration has started. |
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<Goal,Term> |
AbstractUpdateExtractor.computeValueConditions(java.util.Set<Goal> valueGoals,
java.util.Map<Node,Term> branchConditionCache,
boolean simplifyConditions)
This method computes for all given
Goal s representing the same
value their path conditions. |
Constructor and Description |
---|
NodeGoal(Goal goal)
Constructor.
|
Constructor and Description |
---|
NodeGoal(Node currentNode,
ImmutableList<Goal> startingGoals)
A reached child node during backward iteration.
|
Modifier and Type | Method and Description |
---|---|
protected Term |
ExecutionVariable.computeValueCondition(TermBuilder tb,
java.util.List<Goal> valueGoals,
InitConfig initConfig)
|
protected void |
ExecutionVariable.groupGoalsByValue(ImmutableList<Goal> goals,
Operator operator,
Term siteProofSelectTerm,
Term siteProofCondition,
java.util.Map<Term,java.util.List<Goal>> valueMap,
java.util.List<Goal> unknownValues,
Services services)
Groups all
Goal s which provides the same value. |
protected void |
ExecutionVariable.groupGoalsByValue(ImmutableList<Goal> goals,
Operator operator,
Term siteProofSelectTerm,
Term siteProofCondition,
java.util.Map<Term,java.util.List<Goal>> valueMap,
java.util.List<Goal> unknownValues,
Services services)
Groups all
Goal s which provides the same value. |
protected void |
ExecutionVariable.groupGoalsByValue(ImmutableList<Goal> goals,
Operator operator,
Term siteProofSelectTerm,
Term siteProofCondition,
java.util.Map<Term,java.util.List<Goal>> valueMap,
java.util.List<Goal> unknownValues,
Services services)
Groups all
Goal s which provides the same value. |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
ModalitySideProofRule.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
ImmutableList<Goal> |
QuerySideProofRule.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
ModalitySideProofRule.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
ImmutableList<Goal> |
QuerySideProofRule.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
protected java.util.List<Triple<Term,java.util.Set<Term>,Node>> |
AbstractSideProofRule.computeResultsAndConditions(Services services,
Goal goal,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
Function newPredicate)
Starts the side proof and extracts the result
Term and conditions. |
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.
|
Modifier and Type | Method and Description |
---|---|
Goal |
SymbolicExecutionGoalChooser.getNextGoal() |
Modifier and Type | Method and Description |
---|---|
java.util.Map<Goal,java.lang.Integer> |
ExecutedSymbolicExecutionTreeNodesStopCondition.getExectuedSetNodesPerGoal()
Returns the number of executed symbolic execution tree nodes per
Goal . |
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) |
java.lang.String |
StepReturnSymbolicExecutionTreeNodesStopCondition.getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
java.lang.String |
StepOverSymbolicExecutionTreeNodesStopCondition.getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
java.lang.String |
CompoundStopCondition.getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
java.lang.String |
ExecutedSymbolicExecutionTreeNodesStopCondition.getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
java.lang.String |
BreakpointStopCondition.getGoalNotAllowedMessage(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Returns the reason why the previous check via
#isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)
has stopped the apply strategy. |
protected void |
ExecutedSymbolicExecutionTreeNodesStopCondition.handleNodeLimitExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is exceeded.
|
protected void |
ExecutedSymbolicExecutionTreeNodesStopCondition.handleNodeLimitNotExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is not exceeded.
|
protected void |
SymbolicExecutionBreakpointStopCondition.handleNodeLimitNotExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is not exceeded.
|
boolean |
CompoundStopCondition.isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
boolean |
ExecutedSymbolicExecutionTreeNodesStopCondition.isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
boolean |
SymbolicExecutionBreakpointStopCondition.isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
boolean |
AbstractCallStackBasedStopCondition.isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
boolean |
BreakpointStopCondition.isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
void |
SymbolicExecutionGoalChooser.removeGoal(Goal p_goal)
Remove p_goal from selectedList (e.g.
|
Modifier and Type | Method and Description |
---|---|
void |
SymbolicExecutionGoalChooser.init(Proof p_proof,
ImmutableList<Goal> p_goals)
Initialise this DefaultGoalChooser for use with a given Proof and a list of goals.
|
void |
SymbolicExecutionGoalChooser.updateGoalList(Node node,
ImmutableList<Goal> newGoals)
The given node has become an internal node of the proof tree, and the
children of the node are the given goals
|
Modifier and Type | Method and Description |
---|---|
void |
AbstractConditionalBreakpoint.updateState(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
This method is called from
StopCondition.isGoalAllowed(int, long, Proof, long, int, Goal)
and can be used to update the state of the IBreakpoint . |
void |
SymbolicExecutionExceptionBreakpoint.updateState(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
This method is called from
StopCondition.isGoalAllowed(int, long, Proof, long, int, Goal)
and can be used to update the state of the IBreakpoint . |
void |
IBreakpoint.updateState(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
This method is called from
StopCondition.isGoalAllowed(int, long, Proof, long, int, Goal)
and can be used to update the state of the IBreakpoint . |
void |
AbstractBreakpoint.updateState(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
This method is called from
StopCondition.isGoalAllowed(int, long, Proof, long, int, Goal)
and can be used to update the state of the IBreakpoint . |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<Goal> |
SymbolicExecutionUtil.collectGoalsInSubtree(IExecutionElement executionElement)
Collects all
Goal s in the subtree of the given IExecutionElement . |
static ImmutableList<Goal> |
SymbolicExecutionUtil.collectGoalsInSubtree(Node node)
|
Modifier and Type | Method and Description |
---|---|
static Term |
SymbolicExecutionSideProofUtil.extractOperatorTerm(Goal goal,
Operator operator)
|
static Term |
SymbolicExecutionSideProofUtil.extractOperatorValue(Goal goal,
Operator operator)
|
static boolean |
SymbolicExecutionUtil.hasApplicableRules(Goal goal)
Checks if the
Goal has applicable rules. |
Constructor and Description |
---|
ModelGenerator(Goal s,
int target,
Services services) |
Modifier and Type | Method and Description |
---|---|
void |
ConsoleUserInterfaceControl.completeAndApplyTacletMatch(TacletInstantiationModel[] models,
Goal goal) |
IBuiltInRuleApp |
ConsoleUserInterfaceControl.completeBuiltInRuleApp(IBuiltInRuleApp app,
Goal goal,
boolean forced) |
boolean |
MediatorProofControl.selectedTaclet(Taclet taclet,
Goal goal,
PosInOccurrence pos) |
Modifier and Type | Method and Description |
---|---|
void |
MediatorProofControl.startAutoMode(Proof proof,
ImmutableList<Goal> goals,
ProverTaskListener ptl) |
Modifier and Type | Method and Description |
---|---|
ApplyStrategyInfo |
ProofStarter.start(ImmutableList<Goal> goals)
starts proof attempt
|
Constructor and Description |
---|
InfFlowProgVarRenamer(Term[] terms,
java.util.Map<Term,Term> preInitialisedReplaceMap,
java.lang.String postfix,
Goal goalForVariableRegistration,
Services services) |
InfFlowProgVarRenamer(Term[] terms,
java.lang.String postfix,
Goal goalForVariableRegistration,
Services services) |
Modifier and Type | Method and Description |
---|---|
static void |
MergeRuleUtils.clearSemisequent(Goal goal,
boolean antec)
Deletes all formulae of the succedent / antecedent.
|
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. |
Modifier and Type | Method and Description |
---|---|
Node |
ProofExplorationService.applyChangeFormula(Goal g,
PosInOccurrence pio,
Term term,
Term newTerm) |
Node |
ProofExplorationService.soundAddition(Goal g,
Term t,
boolean antecedent)
Create a new Tacletapp that add a formula to the sequent using the cut rule and disabeling one of the branches
|
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.runRule(Goal goal,
RuleApp app) |
Modifier and Type | Method and Description |
---|---|
default void |
Reapplicable.reapply(WindowUserInterfaceControl uic,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
static NodeIdentifier |
NodeIdentifier.get(Goal g) |
void |
AutoModeInteraction.reapply(WindowUserInterfaceControl uic,
Goal goal) |
void |
RuleInteraction.reapply(WindowUserInterfaceControl uic,
Goal goal) |
void |
SettingChangeInteraction.reapply(WindowUserInterfaceControl uic,
Goal goal) |
void |
PruneInteraction.reapply(WindowUserInterfaceControl uic,
Goal goal) |
void |
MacroInteraction.reapply(WindowUserInterfaceControl uic,
Goal goal) |
PosInOccurrence |
OccurenceIdentifier.rebuildOn(Goal goal) |
Modifier and Type | Method and Description |
---|---|
void |
OSSBuiltInRuleInteraction.reapply(WindowUserInterfaceControl uic,
Goal goal) |
Copyright © 2003-2019 The KeY-Project.