Package | Description |
---|---|
de.uka.ilkd.key.control | |
de.uka.ilkd.key.core | |
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof.rulefilter | |
de.uka.ilkd.key.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
Modifier and Type | Method and Description |
---|---|
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
|
Modifier and Type | Method and Description |
---|---|
TacletFilter |
KeYMediator.getFilterForInteractiveProving()
Returns a filter that is used for filtering taclets that should not be showed
while interactive proving.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<NoPosTacletApp> |
TacletAppIndex.getFindTaclet(PosInOccurrence pos,
TacletFilter filter,
TermServices services)
collects all FindTaclets with instantiations and position
|
ImmutableList<NoPosTacletApp> |
RuleAppIndex.getFindTaclet(TacletFilter filter,
PosInOccurrence pos,
TermServices services)
collects all FindTacletInstantiations for the given
heuristics and position
|
ImmutableList<NoPosTacletApp> |
RuleAppIndex.getNoFindTaclet(TacletFilter filter,
Services services)
collects all NoFindTacletInstantiations for the given
heuristics
|
ImmutableList<NoPosTacletApp> |
TacletAppIndex.getNoFindTaclet(TacletFilter filter,
Services services)
collects all NoFindTacletInstantiations
|
ImmutableList<NoPosTacletApp> |
TacletAppIndex.getRewriteTaclet(PosInOccurrence pos,
TacletFilter filter,
TermServices services)
collects all RewriteTacletInstantiations in a subterm of the
constrainedFormula described by a PosInOccurrence.
|
ImmutableList<NoPosTacletApp> |
RuleAppIndex.getRewriteTaclet(TacletFilter filter,
PosInOccurrence pos,
TermServices services)
collects all RewriteTacletInstantiations for the given
heuristics in a subterm of the constraintformula described by a
PosInOccurrence
|
ImmutableList<TacletApp> |
TacletAppIndex.getTacletAppAt(PosInOccurrence pos,
TacletFilter filter,
Services services)
returns the set of rule applications
at the given position of the given sequent.
|
ImmutableList<TacletApp> |
RuleAppIndex.getTacletAppAt(TacletFilter filter,
PosInOccurrence pos,
Services services)
returns the set of rule applications for
the given heuristics
at the given position of the given sequent.
|
ImmutableList<TacletApp> |
TacletAppIndex.getTacletAppAtAndBelow(PosInOccurrence pos,
TacletFilter filter,
Services services)
returns the rule applications at the given PosInOccurrence and at all
Positions below this.
|
ImmutableList<TacletApp> |
RuleAppIndex.getTacletAppAtAndBelow(TacletFilter filter,
PosInOccurrence pos,
Services services)
returns the rule applications at the given PosInOccurrence and at all
Positions below this.
|
Modifier and Type | Class and Description |
---|---|
class |
AnyRuleSetTacletFilter
Filter that selects taclets that belong to at least one
rule set, i.e.
|
class |
IHTacletFilter
Filter that selects taclets using the method
admissible of the
Taclet class, i.e. |
class |
TacletFilterCloseGoal |
class |
TacletFilterSplitGoal |
Modifier and Type | Field and Description |
---|---|
static TacletFilter |
AnyRuleSetTacletFilter.INSTANCE |
static TacletFilter |
TacletFilter.TRUE
Trival TacletFilter that always returns true;
|
Modifier and Type | Method and Description |
---|---|
protected TacletFilter |
AbstractFeatureStrategy.getFilterFor(java.lang.String[] p_names) |
Copyright © 2003-2019 The KeY-Project.