See: Description
| Interface | Description |
|---|---|
| AutomatedRuleApplicationManager | |
| DelegationBasedAutomatedRuleApplicationManager |
An
AutomatedRuleApplicationManager based on delegation. |
| IBreakpointStopCondition |
Defines the basic functionality of an
StopCondition which
stops applying rules when at least one IBreakpoint is hit. |
| RuleAppCost | |
| RuleAppCostCollector |
Interface for collecting
RuleApps, together with their
assigned cost. |
| RuleAppFeature |
Generic interface for evaluating the cost of
a RuleApp with regard to a specific feature
(like term size, ...)
|
| Strategy |
Generic interface for evaluating the cost of
a RuleApp with regard to a specific strategy
|
| StrategyFactory |
Interface for creating Strategy instances.
|
| Class | Description |
|---|---|
| AbstractFeatureStrategy | |
| ArithTermFeatures | |
| BuiltInRuleAppContainer |
Instances of this class are immutable
|
| FIFOStrategy |
Trivial implementation of the Strategy interface
that uses only the goal time to determine the cost
of a RuleApp.
|
| FIFOStrategy.Factory | |
| FindTacletAppContainer |
Instances of this class are immutable
|
| FocussedBreakpointRuleApplicationManager |
A rule app manager that ensures that rules are only applied to a certain
subterm within the proof (within a goal).
|
| FocussedRuleApplicationManager |
A rule app manager that ensures that rules are only applied to a certain
subterm within the proof (within a goal).
|
| FormulaTermFeatures | |
| 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
|
| IfInstantiationCachePool.IfInstantiationCache | |
| IfInstantiator |
This class implements custom instantiation of if-formulas.
|
| IntroducedSymbolBy | |
| 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. |
| JavaCardDLStrategy |
Strategy tailored to be used as long as a java program can be found in the
sequent.
|
| JavaCardDLStrategyFactory | |
| NoFindTacletAppContainer |
Instances of this class are immutable
|
| NumberRuleAppCost | |
| NumberRuleAppCost.IntRuleAppCost | |
| NumberRuleAppCost.LongRuleAppCost |
Implementation of the
RuleAppCost interface that uses
a long value for the representation of costs, ordered by the
usual ordering of natural numbers. |
| QueueRuleApplicationManager |
Implementation of
AutomatedRuleApplicationManager that stores
possible RuleApps in a priority queue. |
| RuleAppContainer |
Container for RuleApp instances with cost as determined by
a given Strategy.
|
| SimpleFilteredStrategy |
Trivial implementation of the Strategy interface
that uses only the goal time to determine the cost
of a RuleApp.
|
| StaticFeatureCollection |
Collection of strategy features that can be accessed statically.
|
| 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) |
| ValueTermFeature |