public class FieldConstantHandler extends java.lang.Object implements SMTHandler
ClassName::$fieldName
.
This handler treats any unique function symbol of sort Field
that follows this
scheme as a function constant.
It is made sure that different symbols do not map to the field entity.
To this end a function fieldIdentifier is used and an assertion like the following
is added which states for C::$f
(assert (= (fieldIdentifier |field_C::$f|) -42)
Each function symbol gets a new unique negative integer.
Positive integers are kept for the arr() function to make sure that is an injection.
The integer constants are obtained via a counter stored in the state.
The key is CONSTANT_COUNTER_PROPERTY
.
TODO It seems that this could be extended to a general "UniqueHandler" if required.SMTHandler.Capability
Constructor and Description |
---|
FieldConstantHandler() |
Modifier and Type | Method and Description |
---|---|
boolean |
canHandle(Operator op)
Query if this handler can translate an operator.
|
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.
|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
canHandle, getProperties
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 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.Copyright © 2003-2019 The KeY-Project.