See: Description
| Interface | Description |
|---|---|
| GoalListener |
interface to be implemented by a goal listener
|
| InstantiationProposer |
Provides proposals for schema variable instantiations.
|
| ITermTacletAppIndexCache |
The general interface for caches for accelerating
TermTacletAppIndex. |
| ModelChangeListener |
this interface is implemented by listener of change
events of a model
|
| NewRuleListener |
Interface for tracking new RuleApps
|
| ProofTreeListener | |
| ProofVisitor | |
| RuleAppListener | |
| StrategyInfoUndoMethod |
| Class | Description |
|---|---|
| BuiltInRuleAppIndex | |
| BuiltInRuleIndex |
Index for managing built-in-rules usch as integer decision or update
simplification rule.
|
| CompoundProof | |
| Counter |
Proof-specific counter object: taclet names, var names, node numbers, &c
|
| FormulaTag |
Class whose instances represent tags to identify the formulas of sequents
persistently, i.e. a tag does not become invalid when a formula is modified
by a rule application.
|
| FormulaTagManager |
Class to manage the tags of the formulas of a sequent (node).
|
| FormulaTagManager.FormulaInfo |
Class that holds information about a formula, namely the current position
(
PosInOccurrence) as well as a list of the modifications
that have been applied to the formula so far. |
| Goal |
A proof is represented as a tree of nodes containing sequents.
|
| InstantiationProposerCollection |
Composite of instantiation proposers.
|
| JavaModel | |
| ModelEvent |
this class represents a Model event
|
| MultiThreadedTacletIndex |
A multi-threaded taclet index implementation.
|
| MultiThreadedTacletIndex.TacletSetMatchTask |
The callable implementing the actual matching task.
|
| NameRecorder | |
| Node | |
| NodeInfo |
The node info object contains additional information about a node used to
give user feedback.
|
| NodeIterator | |
| NullNewRuleListener |
Implementation of the NewRuleListener interface
that does nothing
|
| ObserverWithType | |
| OpReplacer |
Replaces operators in a term by other operators with the same signature,
or subterms of the term by other terms with the same sort.
|
| PrefixTermTacletAppIndexCache |
The abstract superclass of caches for taclet app indexes that are separated
by different prefixes of bound variables.
|
| PrefixTermTacletAppIndexCacheImpl |
The abstract superclass of caches for taclet app indexes that are implemented
using a common backend
LRUCache (the backend is stored in
TermTacletAppIndexCacheSet). |
| PrefixTermTacletAppIndexCacheImpl.CacheKey | |
| ProgVarReplacer |
Replaces program variables.
|
| Proof |
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
| ProofAggregate | |
| ProofEvent |
an object indicating that a proof event has happpend
|
| ProofTreeAdapter |
An abstract adapter class for receiving proof tree events.
|
| ProofTreeEvent |
Encapsulates information describing changes to a proof tree, and
used to notify proof tree listeners of the change.
|
| RuleAppIndex |
manages the possible application of rules (RuleApps)
|
| SemisequentTacletAppIndex |
This class holds
TermTacletAppIndexs for all formulas of
a semisequent. |
| SingleProof | |
| SingleThreadedTacletIndex |
The default taclet index implementation.
|
| Statistics |
Instances of this class encapsulate statistical information about proofs,
such as the number of nodes, or the number of interactions.
|
| SubtreeIterator |
Iterator over subtree.
|
| TacletAppIndex |
the class manages the available TacletApps.
|
| TacletIndex |
manages all applicable Taclets (more precisely: Taclets with
instantiations but without position information, the NoPosTacletApps)
at one node.
|
| TacletIndex.PrefixOccurrences |
Inner class to track the occurrences of prefix elements in java blocks
|
| TacletIndexKit |
Abstract factory for creating
TacletIndex instances |
| TacletIndexKit.MultiThreadedTacletIndexKit |
Concrete factory creating the multi threaded version of the
TacletIndex
(performs matching using multiple threads) |
| TacletIndexKit.SingleThreadedTacletIndexKit |
Concrete factory creating the single threaded version of the
TacletIndex |
| TermProgramVariableCollector | |
| TermProgramVariableCollectorKeepUpdatesForBreakpointconditions | |
| TermTacletAppIndex |
Class whose objects represent an index of taclet apps for one particular
position within a formula, and that also contain references to the indices of
direct subformulas
|
| TermTacletAppIndexCacheSet |
Cache that is used for accelerating
TermTacletAppIndex. |
| VariableNameProposer |
Proposes names for variables (except program variables).
|
| Exception | Description |
|---|---|
| IfMismatchException |
this exception thrown if an if-sequent match failed
|
| MissingInstantiationException | |
| MissingSortException | |
| SortMismatchException | |
| SVInstantiationException | |
| SVInstantiationExceptionWithPosition |
Represents an exception with position information.
|
| SVInstantiationParserException | |
| SVRigidnessException |