public class IntegerOpHandler extends java.lang.Object implements SMTHandler
SMTHandler.Capability
Modifier and Type | Field and Description |
---|---|
static SExpr.Type |
INT
to indicate that an expression holds a value of type Int.
|
static SMTHandlerProperty.BooleanProperty |
PROPERTY_PRESBURGER |
Constructor and Description |
---|
IntegerOpHandler() |
Modifier and Type | Method and Description |
---|---|
boolean |
canHandle(Operator op)
Query if this handler can translate an operator.
|
SMTHandler.Capability |
canHandle(Term term)
Query if this handler can translate a term.
|
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.
|
public static final SExpr.Type INT
public static final SMTHandlerProperty.BooleanProperty PROPERTY_PRESBURGER
public void init(MasterHandler masterHandler, Services services, java.util.Properties handlerSnippets)
SMTHandler
init
in interface SMTHandler
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 handlerpublic boolean canHandle(Operator op)
SMTHandler
canHandle
in interface SMTHandler
op
- a non-null operator to translatepublic SMTHandler.Capability canHandle(Term term)
SMTHandler
canHandle
in interface SMTHandler
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.public SExpr handle(MasterHandler trans, Term term) throws SMTTranslationException
SMTHandler
SMTHandler.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.handle
in interface SMTHandler
trans
- the non-null master handler to which it belongsterm
- the non-null term to translateSMTTranslationException
- if the translation fails unexpectedly.public java.util.List<SMTHandlerProperty<?>> getProperties()
SMTHandler
SMTHandlerServices
and will
not be modified.getProperties
in interface SMTHandler
Copyright © 2003-2019 The KeY-Project.