Class and Description |
---|
Strategy
Generic interface for evaluating the cost of
a RuleApp with regard to a specific strategy
|
StrategyFactory
Interface for creating Strategy instances.
|
StrategyProperties |
Class and Description |
---|
RuleAppCost |
RuleAppCostCollector
Interface for collecting
RuleApp s, together with their
assigned cost. |
Strategy
Generic interface for evaluating the cost of
a RuleApp with regard to a specific strategy
|
Class and Description |
---|
IfInstantiationCachePool
Direct-mapped cache of lists of formulas (potential instantiations of
if-formulas of taclets) that were modified after a certain point of time
Hashmaps of the particular lists of formulas; the keys of the maps is the
point of time that separates old from new (modified) formulas
Keys: Long Values: IList
|
RuleAppCost |
Class and Description |
---|
AbstractFeatureStrategy |
RuleAppCost |
RuleAppCostCollector
Interface for collecting
RuleApp s, together with their
assigned cost. |
StaticFeatureCollection
Collection of strategy features that can be accessed statically.
|
Strategy
Generic interface for evaluating the cost of
a RuleApp with regard to a specific strategy
|
Class and Description |
---|
AutomatedRuleApplicationManager |
IBreakpointStopCondition
Defines the basic functionality of an
StopCondition which
stops applying rules when at least one IBreakpoint is hit. |
Strategy
Generic interface for evaluating the cost of
a RuleApp with regard to a specific strategy
|
StrategyFactory
Interface for creating Strategy instances.
|
Class and Description |
---|
StrategyFactory
Interface for creating Strategy instances.
|
Class and Description |
---|
StrategyProperties |
Class and Description |
---|
AbstractFeatureStrategy |
AutomatedRuleApplicationManager |
DelegationBasedAutomatedRuleApplicationManager
An
AutomatedRuleApplicationManager based on delegation. |
IfInstantiationCachePool.IfInstantiationCache |
IsInRangeProvable
Feature used to check if the value of a given term with
moduloXXX
(with XXX being Long, Int, etc.) is in the range of Long, Integer etc. |
NumberRuleAppCost |
QueueRuleApplicationManager
Implementation of
AutomatedRuleApplicationManager that stores
possible RuleApp s in a priority queue. |
RuleAppContainer
Container for RuleApp instances with cost as determined by
a given Strategy.
|
RuleAppCost |
RuleAppCostCollector
Interface for collecting
RuleApp s, together with their
assigned cost. |
StaticFeatureCollection
Collection of strategy features that can be accessed statically.
|
Strategy
Generic interface for evaluating the cost of
a RuleApp with regard to a specific strategy
|
StrategyFactory
Interface for creating Strategy instances.
|
StrategyProperties |
TacletAppContainer
Instances of this class are immutable
|
TopRuleAppCost
Singleton implementation of the
RuleAppCost interface, which
denotes a maximum cost (rule applications with this cost can't be afforded
at all) |
Class and Description |
---|
StrategyProperties |
Class and Description |
---|
RuleAppCost |
Class and Description |
---|
RuleAppCost |
Class and Description |
---|
RuleAppCost |
Class and Description |
---|
RuleAppCost |
Class and Description |
---|
StrategyFactory
Interface for creating Strategy instances.
|
Class and Description |
---|
AbstractFeatureStrategy |
IBreakpointStopCondition
Defines the basic functionality of an
StopCondition which
stops applying rules when at least one IBreakpoint is hit. |
JavaCardDLStrategy
Strategy tailored to be used as long as a java program can be found in the
sequent.
|
StaticFeatureCollection
Collection of strategy features that can be accessed statically.
|
Strategy
Generic interface for evaluating the cost of
a RuleApp with regard to a specific strategy
|
StrategyFactory
Interface for creating Strategy instances.
|
StrategyProperties |
Class and Description |
---|
StrategyProperties |
Class and Description |
---|
Strategy
Generic interface for evaluating the cost of
a RuleApp with regard to a specific strategy
|
StrategyProperties |
Copyright © 2003-2019 The KeY-Project.