Package | Description |
---|---|
de.uka.ilkd.key.smt.newsmt2 |
Modifier and Type | Class and Description |
---|---|
class |
BooleanConnectiveHandler
This SMT translation handler takes care of
the builtin Boolean connectives.
|
class |
CastHandler
This SMT translation handler takes care of cast expressions
T::cast(term) . |
class |
CastingFunctionsHandler
This SMT translation handler takes care of those sort-depending functions f whose return type is
coerced, i.e.
|
class |
DefinedSymbolsHandler
This handler is meant to translate all function symbols for which key axioms, SMT axioms or
defining taclets have been registered.
|
class |
FieldConstantHandler
This SMT translation handler takes care of field constants.
|
class |
InstanceOfHandler
This SMT translation handler takes care of
instanceof and exactinstanceof functions.
|
class |
IntegerOpHandler
This SMT translation handler takes care of integer expressions.
|
class |
LogicalVariableHandler
This simple SMT translation handler takes care of logical variables.
|
class |
NumberConstantsHandler
This handler is responsible to render number constants
Z(3(2(1(#)))) as "123".
|
class |
PolymorphicHandler
This handler treats polymorphic symbols, in particular if-then-else and
equals.
|
class |
QuantifierHandler
This SMT translation handler takes care of quantifier formulas using existential
or universal quantifiers.
|
class |
SeqDefHandler
This handler handles the seqDef binder function specially.
|
class |
SumProdHandler |
class |
UninterpretedSymbolsHandler
This handler is a fallback handler that introduces a new uninterpreted
function symbol with prefix "u_".
|
class |
UpdateHandler
This handler treats KeY updated terms ({x:=5}x>4).
|
Modifier and Type | Method and Description |
---|---|
java.util.List<SMTHandler> |
SMTHandlerServices.getFreshHandlers(Services services,
MasterHandler mh)
Get a copy of freshly created
SMTHandler s by cloning the reference
handlers. |
java.util.List<SMTHandler> |
SMTHandlerServices.getOriginalHandlers()
Get a list of all handlers available in the system.
|
Copyright © 2003-2019 The KeY-Project.