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 | Method and Description |
---|---|
AutomatedRuleApplicationManager |
Goal.getRuleAppManager() |
Modifier and Type | Method and Description |
---|---|
void |
Goal.setRuleAppManager(AutomatedRuleApplicationManager manager) |
Modifier and Type | Interface and Description |
---|---|
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. |
Modifier and Type | Method and Description |
---|---|
AutomatedRuleApplicationManager |
FocussedBreakpointRuleApplicationManager.copy() |
AutomatedRuleApplicationManager |
FocussedRuleApplicationManager.copy() |
AutomatedRuleApplicationManager |
AutomatedRuleApplicationManager.copy() |
AutomatedRuleApplicationManager |
QueueRuleApplicationManager.copy() |
AutomatedRuleApplicationManager |
FocussedBreakpointRuleApplicationManager.getDelegate() |
AutomatedRuleApplicationManager |
DelegationBasedAutomatedRuleApplicationManager.getDelegate() |
AutomatedRuleApplicationManager |
FocussedRuleApplicationManager.getDelegate() |
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) |
Copyright © 2003-2019 The KeY-Project.