public interface SMTHandler
ServiceLoader
.
To implement a new handler, implement this interface and add the classname to
a file that ServiceLoader reads for SMTHandler.
init(MasterHandler, Services, Properties)
method is called that injects the
Services
object belonging to the proof.
During translation, an SMT handler can be asked via canHandle(Term)
if it can translate a term into smt.
If it returns true, the method handle(MasterHandler, Term)
will be
called which returns the SMT result in form of an SExpr
.Modifier and Type | Interface and Description |
---|---|
static class |
SMTHandler.Capability
An enumeration of the possible answers of an handler to the
canHandle(Term) method. |
Modifier and Type | Method and Description |
---|---|
boolean |
canHandle(Operator op)
Query if this handler can translate an operator.
|
default SMTHandler.Capability |
canHandle(Term term)
Query if this handler can translate a term.
|
default java.util.List<SMTHandlerProperty<?>> |
getProperties()
Any handler can offer a collection of properties that can be set
in the GUI/script to control the translation.
|
SExpr |
handle(MasterHandler trans,
Term term)
Translate the given term into an SMT SExpression.
|
void |
init(MasterHandler masterHandler,
Services services,
java.util.Properties handlerSnippets)
Initialise this handler.
|
void init(MasterHandler masterHandler, Services services, java.util.Properties handlerSnippets) throws java.io.IOException
masterHandler
- services
- the non-null services object which is relevant for
this handlerhandlerSnippets
- the snippets loaded for this handler, null if no
snippet property file is available for this handlerjava.io.IOException
- if resources cannot be read.default SMTHandler.Capability canHandle(Term term)
term
- a non-null term to translateSMTHandler.Capability.YES_THIS_OPERATOR
if this handler can successfully translate any
term with the same toplevel operator, SMTHandler.Capability.YES_THIS_INSTANCE
if this
handler can successfully translate this particular term, SMTHandler.Capability.UNABLE
if this handler cannot deal with the term.boolean canHandle(Operator op)
op
- a non-null operator to translateSExpr handle(MasterHandler trans, Term term) throws SMTTranslationException
canHandle(Term)
returned
true for the same term argument.
The translation may add to the set of assumptions and declarations using
corresponding calls to the MasterHandler
that it receives.trans
- the non-null master handler to which it belongsterm
- the non-null term to translateSMTTranslationException
- if the translation fails unexpectedly.default java.util.List<SMTHandlerProperty<?>> getProperties()
SMTHandlerServices
and will
not be modified.Copyright © 2003-2019 The KeY-Project.