public class DefinedSymbolsHandler extends java.lang.Object implements SMTHandler
XXX.DefinedSymbolsHandler.preamble.xml
for some
prefix XXX
. This file must be located in the resources for the package in which this
class resides.
Such an xml file is not an actual xml file but rather an xml fragment consisting of a set of entries to be used as axiomatisation when the SMT translation is triggered. Three kind of entries are possible for a function symbol f:
<<Trigger>>
term label to
specify the subterm which should be used as a trigger (:pattern) in SMTLib to
help Z3 (and other solvers) to instantiate the quantified variables suitably.
\forall Seq s; seqLen(s)<<Trigger>> >= 0is the axiom for seqLen (hence stored in seqLen.dl). The trigger pattern to be used for instantiation is seqLen(s) matching against any ground instance of seqLen.
SMTHandler.Capability
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
PREFIX |
static TermLabel |
TRIGGER_LABEL |
Constructor and Description |
---|
DefinedSymbolsHandler() |
Modifier and Type | Method and Description |
---|---|
boolean |
canHandle(Operator op)
Query if this handler can translate an operator.
|
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.
|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
canHandle
public static final java.lang.String PREFIX
public static final TermLabel TRIGGER_LABEL
public void init(MasterHandler masterHandler, Services services, java.util.Properties handlerSnippets) throws java.io.IOException
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 handlerjava.io.IOException
- if resources cannot be read.public 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.public java.util.List<SMTHandlerProperty<?>> getProperties()
SMTHandler
SMTHandlerServices
and will
not be modified.getProperties
in interface SMTHandler
Copyright © 2003-2019 The KeY-Project.