| Interface | Description |
|---|---|
| AST |
Interface to abstract syntax trees.
|
| ASTVisitor |
Interface to visitor of abstract syntax trees.
|
| Declaration |
Interface for declarations.
|
| Expression |
Interface to expressions (terms and formulas).
|
| Selector |
Interface to selectors.
|
| Type |
Interface to types.
|
| Class | Description |
|---|---|
| AndFormula |
Handling of conjunctions.
|
| ApplicationExpression |
Handling of function and predicate applications.
|
| ArrayTerm |
Handling of array terms.
|
| ArrayType |
Handling of array types.
|
| ASTBase |
Base class of abstract syntax trees.
|
| ASTUtil |
Collect state related to handling of abstract syntax trees.
|
| ASTVisitorBase |
Base class of visitors of abstract syntax trees.
|
| AtomicType |
Handling of atomic types.
|
| AxiomDeclaration |
Handling of type declarations.
|
| BinaryExpression |
Abstract base class of binary expressions
|
| BitAndTerm |
Handling of bit conjunctions.
|
| BitLogical |
Bit logical constants.
|
| BitNotTerm |
Handling of bit negations
|
| BitOrTerm |
Handling of bit disjunctions.
|
| Construct |
Construct abstract syntax trees.
|
| DeclarationBase |
Base class of type expressions.
|
| DividesTerm |
Handling of quotients.
|
| EqualsFormula |
Handling of equalities.
|
| EquivalentFormula |
Handling of equivalences.
|
| ExistsFormula |
Handling of universally quantified formulas.
|
| ExpressionBase |
Base class of all expressions (terms and formulas)
|
| ForallFormula |
Handling of universally quantified formulas.
|
| FormulaDeclaration |
Handling of type declarations.
|
| FormulaDeclIdentifier |
Handling of identifiers used in type declarations
|
| FunctionType |
Handling of function type expressions
|
| GreaterEqualFormula |
Handling of greater-than-or-equal formulas.
|
| GreaterFormula |
Handling of greater-than formulas.
|
| Identifier |
Handling of identifiers.
|
| IfThenElseExpression |
Handling of if-then-else expressions.
|
| ImpliesFormula |
Handling of implications
|
| LambdaTerm |
Handling of lambda terms.
|
| LessEqualFormula |
Handling of less-than-or-equal formulas.
|
| LessFormula |
Handling of less-than formulas.
|
| LetExpression |
Handling of terms with local bindings.
|
| LetType |
Handling of terms with local bindings.
|
| Logical |
Logical constants.
|
| MinusTerm |
Handling of differences.
|
| NegationTerm |
Handling of negated (minus) terms
|
| NotEqualsFormula |
Handling of conjunctions
|
| NotEquivalentFormula |
Handling of conjunctions
|
| NotFormula |
Handling of negations
|
| Number |
Handling of numbers.
|
| OrFormula |
Handling of disjunctions.
|
| PlusTerm |
Handling of binary sums.
|
| PowerTerm |
Handling of power terms.
|
| QuantifiedExpression |
Abstract base class of quantified expressions.
|
| RecordTerm |
Handling of record terms.
|
| RecordType |
Handling of record types.
|
| Reference |
Handling of identifiers used in declarations
|
| SelectionTerm |
Handling of component access by index selections.
|
| SelectorBase |
Base class of selector expressions.
|
| SelectorIdentifier |
Identifier as selector.
|
| SelectorIndex |
General index expression as selector.
|
| SelectorNumber |
Number as selector.
|
| SubrangeType |
Subranges of integers.
|
| SubType |
Predicated subtypes.
|
| TimesTerm |
Handling of conjunctions
|
| TupleTerm |
Handling of tuple terms.
|
| TupleType |
Handling of tuple types.
|
| TypeBase |
Base class of type expressions.
|
| TypeDeclaration |
Handling of type declarations.
|
| TypeDeclIdentifier |
Handling of identifiers used in type declarations
|
| TypedIdentifier |
Handling of typed identifiers.
|
| UnaryExpression |
Abstract base class of unary expressions
|
| UniqueNameTable |
Table used to create unique names from given names.
|
| UpdateTerm |
Handling of component updates by index selection.
|
| ValueDeclaration |
Handling of value declarations.
|
| ValueDeclIdentifier |
Handling of identifiers used in value declarations
|
| ValuedIdentifier |
Handling of identifier with value
|