Package | Description |
---|---|
de.uka.ilkd.key.smt.newsmt2 |
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. |
SExpr |
DefinedSymbolsHandler.handle(MasterHandler trans,
Term term) |
SExpr |
SeqDefHandler.handle(MasterHandler trans,
Term term) |
SExpr |
CastingFunctionsHandler.handle(MasterHandler trans,
Term term) |
SExpr |
QuantifierHandler.handle(MasterHandler trans,
Term term) |
SExpr |
LogicalVariableHandler.handle(MasterHandler trans,
Term term) |
SExpr |
SMTHandler.handle(MasterHandler trans,
Term term)
Translate the given term into an SMT SExpression.
|
SExpr |
BooleanConnectiveHandler.handle(MasterHandler trans,
Term term) |
SExpr |
UninterpretedSymbolsHandler.handle(MasterHandler trans,
Term term) |
SExpr |
PolymorphicHandler.handle(MasterHandler trans,
Term term) |
SExpr |
InstanceOfHandler.handle(MasterHandler trans,
Term term) |
SExpr |
IntegerOpHandler.handle(MasterHandler trans,
Term term) |
SExpr |
FieldConstantHandler.handle(MasterHandler trans,
Term term) |
SExpr |
UpdateHandler.handle(MasterHandler trans,
Term term) |
SExpr |
SumProdHandler.handle(MasterHandler trans,
Term term) |
SExpr |
NumberConstantsHandler.handle(MasterHandler trans,
Term term) |
SExpr |
CastHandler.handle(MasterHandler trans,
Term term) |
void |
DefinedSymbolsHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
SeqDefHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
CastingFunctionsHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
QuantifierHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
LogicalVariableHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
SMTHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets)
Initialise this handler.
|
void |
BooleanConnectiveHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
UninterpretedSymbolsHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
PolymorphicHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
InstanceOfHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
IntegerOpHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
FieldConstantHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
UpdateHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
SumProdHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
NumberConstantsHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
CastHandler.init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets) |
void |
MasterHandler.SymbolIntroducer.introduce(MasterHandler masterHandler,
java.lang.String name) |
Copyright © 2003-2019 The KeY-Project.