Package | Description |
---|---|
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.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
Modifier and Type | Class and Description |
---|---|
class |
NullNewRuleListener
Implementation of the NewRuleListener interface
that does nothing
|
Modifier and Type | Field and Description |
---|---|
static NewRuleListener |
NullNewRuleListener.INSTANCE |
Modifier and Type | Method and Description |
---|---|
void |
RuleAppIndex.addNewRuleListener(NewRuleListener l)
adds a change listener to the index
|
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
|
void |
RuleAppIndex.removeNewRuleListener(NewRuleListener l)
removes a change listener to the index
|
void |
RuleAppIndex.reportAutomatedRuleApps(NewRuleListener l,
Services services)
Report all rule applications that are supposed to be applied
automatically, and that are currently stored by the index
|
void |
BuiltInRuleAppIndex.reportRuleApps(NewRuleListener l,
Goal goal) |
void |
TacletAppIndex.reportRuleApps(NewRuleListener l,
Services services)
Reports all cached rule apps.
|
SemisequentTacletAppIndex |
SemisequentTacletAppIndex.sequentChanged(SequentChangeInfo sci,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
called if a formula has been replaced
|
void |
BuiltInRuleAppIndex.setNewRuleListener(NewRuleListener p_newRuleListener) |
void |
TacletAppIndex.setNewRuleListener(NewRuleListener p_newRuleListener) |
Constructor and Description |
---|
BuiltInRuleAppIndex(BuiltInRuleIndex index,
NewRuleListener p_newRuleListener) |
Modifier and Type | Interface and Description |
---|---|
interface |
AutomatedRuleApplicationManager |
interface |
DelegationBasedAutomatedRuleApplicationManager
An
AutomatedRuleApplicationManager based on delegation. |
Modifier and Type | Class and Description |
---|---|
class |
FocussedBreakpointRuleApplicationManager
A rule app manager that ensures that rules are only applied to a certain
subterm within the proof (within a goal).
|
class |
FocussedRuleApplicationManager
A rule app manager that ensures that rules are only applied to a certain
subterm within the proof (within a goal).
|
class |
QueueRuleApplicationManager
Implementation of
AutomatedRuleApplicationManager that stores
possible RuleApp s in a priority queue. |
Copyright © 2003-2019 The KeY-Project.