Interface | Description |
---|---|
MasterHandler.SymbolIntroducer |
This interface is used for routines that can be used to flexibly
introduce function symbols.
|
SMTHandler |
General interface for routines that translate particular KeY data structures
to SMT.
|
SMTHandlerPropertyVisitor<A,R> |
Visitor pattern for
SMTHandlerProperty objects. |
Writable |
Writeable objects have the possibility to be written to a
StringBuilder . |
Class | Description |
---|---|
BooleanConnectiveHandler |
This SMT translation handler takes care of
the builtin Boolean connectives.
|
CastHandler |
This SMT translation handler takes care of cast expressions
T::cast(term) . |
CastingFunctionsHandler |
This SMT translation handler takes care of those sort-depending functions f whose return type is
coerced, i.e.
|
DefinedSymbolsHandler |
This handler is meant to translate all function symbols for which key axioms, SMT axioms or
defining taclets have been registered.
|
FieldConstantHandler |
This SMT translation handler takes care of field constants.
|
HandlerUtil |
A collection of static methods that
SMTHandler s are likely to use. |
InstanceOfHandler |
This SMT translation handler takes care of
instanceof and exactinstanceof functions.
|
IntegerOpHandler |
This SMT translation handler takes care of integer expressions.
|
LogicalVariableHandler |
This simple SMT translation handler takes care of logical variables.
|
MasterHandler |
Instances of this class are the controlling units of the translation.
|
ModularSMTLib2Translator |
This class provides a translation from a KeY sequent to the SMT-LIB 2 language, a common input
language for modern SMT solvers.
|
NumberConstantsHandler |
This handler is responsible to render number constants
Z(3(2(1(#)))) as "123".
|
PolymorphicHandler |
This handler treats polymorphic symbols, in particular if-then-else and
equals.
|
QuantifierHandler |
This SMT translation handler takes care of quantifier formulas using existential
or universal quantifiers.
|
SeqDefHandler |
This handler handles the seqDef binder function specially.
|
SExpr |
This class models s-expressions to be used for the SMT translation.
|
SExpr.Type |
An enumeration of the types that an
SExpr can assume. |
SExprs |
This class is a collection of static functions to construct SExpr objects.
|
SMTHandlerProperty<T> |
SMT handler properties are properties for the new modular smt handler.
|
SMTHandlerProperty.BooleanProperty |
A property of type boolean.
|
SMTHandlerProperty.EnumProperty<E extends java.lang.Enum<E>> |
A property for an enum type.
|
SMTHandlerProperty.IntegerProperty |
A property of type int.
|
SMTHandlerProperty.StringProperty |
A property of type String.
|
SMTHandlerServices |
This class provides some infrastructure to the smt translation proceess.
|
SMTTacletTranslator |
This class uses the existing taclet translation technology to translate
taclets to smt axioms.
|
SumProdHandler | |
UninterpretedSymbolsHandler |
This handler is a fallback handler that introduces a new uninterpreted
function symbol with prefix "u_".
|
UpdateHandler |
This handler treats KeY updated terms ({x:=5}x>4).
|
Enum | Description |
---|---|
SMTHandler.Capability |
An enumeration of the possible answers of an handler to the
SMTHandler.canHandle(Term) method. |
Copyright © 2003-2019 The KeY-Project.