Package | Description |
---|---|
de.uka.ilkd.key.macros | |
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.
|
de.uka.ilkd.key.strategy.feature |
Modifier and Type | Method and Description |
---|---|
protected abstract RuleFilter |
AbstractBlastingMacro.getEqualityRuleFilter() |
protected RuleFilter |
SemanticsBlastingMacro.getEqualityRuleFilter() |
protected abstract RuleFilter |
AbstractBlastingMacro.getSemanticsRuleFilter() |
protected RuleFilter |
SemanticsBlastingMacro.getSemanticsRuleFilter() |
Modifier and Type | Method and Description |
---|---|
TermTacletAppIndex |
TermTacletAppIndex.addTaclets(RuleFilter filter,
PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Create a new tree of indices that additionally contain the taclets that
are selected by
filter |
SemisequentTacletAppIndex |
SemisequentTacletAppIndex.addTaclets(RuleFilter filter,
Sequent s,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Create an index that additionally contains the taclets that are selected
by
filter |
static TermTacletAppIndex |
TermTacletAppIndex.create(PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
RuleFilter filter,
TermTacletAppIndexCacheSet indexCaches)
Create an index for the given term
|
static ImmutableList<NoPosTacletApp> |
TermTacletAppIndex.filter(RuleFilter p_filter,
ImmutableList<NoPosTacletApp> taclets) |
ImmutableList<NoPosTacletApp> |
TacletIndex.getAntecedentTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Taclets for the antecedent.
|
ImmutableList<NoPosTacletApp> |
TacletIndex.getNoFindTaclet(RuleFilter filter,
Services services)
get all Taclets having no find expression.
|
ImmutableList<NoPosTacletApp> |
TacletIndex.getRewriteTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Rewrite-Taclets.
|
ImmutableList<NoPosTacletApp> |
TacletIndex.getSuccedentTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Taclets for the succedent.
|
ImmutableList<NoPosTacletApp> |
TermTacletAppIndex.getTacletAppAt(PosInOccurrence pos,
RuleFilter p_filter) |
ImmutableList<NoPosTacletApp> |
SemisequentTacletAppIndex.getTacletAppAt(PosInOccurrence pos,
RuleFilter filter) |
ImmutableList<TacletApp> |
TermTacletAppIndex.getTacletAppAtAndBelow(PosInOccurrence pos,
RuleFilter filter,
Services services) |
ImmutableList<TacletApp> |
SemisequentTacletAppIndex.getTacletAppAtAndBelow(PosInOccurrence pos,
RuleFilter filter,
Services services) |
protected abstract ImmutableList<NoPosTacletApp> |
TacletIndex.matchTaclets(ImmutableList<NoPosTacletApp> tacletApps,
RuleFilter p_filter,
PosInOccurrence pos,
Services services)
Filter the given list of taclet apps, and match their find
parts at the given position of the sequent
|
void |
TacletAppIndex.setRuleFilter(RuleFilter p_ruleFilter) |
Modifier and Type | Class and Description |
---|---|
class |
AndRuleFilter
Intersection (conjunction) of two rule filters
|
class |
AnyRuleSetTacletFilter
Filter that selects taclets that belong to at least one
rule set, i.e.
|
class |
ClassRuleFilter
Rule filter that selects taclets which are of a specific class
|
class |
IHTacletFilter
Filter that selects taclets using the method
admissible of the
Taclet class, i.e. |
class |
NotRuleFilter
Inversion of a rule filter
|
class |
SetRuleFilter
Rule filter that selects taclets which are members of a given explicit set
|
class |
TacletFilter
Interface for filtering a list of TacletApps, for example to
choose only taclets for interactive application or taclets
belonging to some given heuristics.
|
class |
TacletFilterCloseGoal |
class |
TacletFilterSplitGoal |
Constructor and Description |
---|
AndRuleFilter(RuleFilter p_a,
RuleFilter p_b) |
NotRuleFilter(RuleFilter p_a) |
Constructor and Description |
---|
SimpleFilteredStrategy(RuleFilter p_ruleFilter) |
Modifier and Type | Method and Description |
---|---|
static Feature |
FormulaAddedByRuleFeature.create(RuleFilter p_filter) |
static Feature |
ConditionalFeature.createConditional(RuleFilter cond,
Feature thenFeature) |
static Feature |
ConditionalFeature.createConditional(RuleFilter cond,
Feature thenFeature,
Feature elseFeature) |
static Feature |
ConditionalFeature.createConditional(RuleFilter cond,
Feature thenFeature,
RuleAppCost elseValue) |
static Feature |
ConditionalFeature.createConditional(RuleFilter cond,
RuleAppCost thenValue) |
static Feature |
ConditionalFeature.createConditional(RuleFilter cond,
RuleAppCost thenValue,
RuleAppCost elseValue) |
Copyright © 2003-2019 The KeY-Project.