public class MasterHandler
extends java.lang.Object
SMTHandler
s and
collects the translations.
It keeps track of the actual translation of an expression but collects also
the declarations and axioms that occur during the translation.
It has measures to ensure that symbols are defined and axiomatized at most
once. This allows us to add these entries on the fly and on demand.Modifier and Type | Class and Description |
---|---|
static interface |
MasterHandler.SymbolIntroducer
This interface is used for routines that can be used to flexibly
introduce function symbols.
|
Constructor and Description |
---|
MasterHandler(Services services,
SMTSettings settings)
Create a new handler.
|
Modifier and Type | Method and Description |
---|---|
void |
addDeclarationsAndAxioms(java.util.Properties snippets)
Copy toplevel declarations and axioms from a collection of snippets
directly and make all named declarations (name.decl) and axioms
(name.axioms)
|
void |
addSort(Sort s) |
java.util.List<Writable> |
getAxioms() |
java.util.List<Writable> |
getDeclarations() |
java.util.List<java.lang.Throwable> |
getExceptions() |
java.util.Set<Sort> |
getSorts() |
java.util.Map<Term,SExpr> |
getUnknownValues() |
java.util.List<SExpr> |
translate(java.lang.Iterable<Term> terms)
Translate a list of terms into a list of SExprs without coercion.
|
java.util.List<SExpr> |
translate(java.lang.Iterable<Term> terms,
SExpr.Type type)
Translate a list of terms into a list of SExprs.
|
SExpr |
translate(Term problem)
Translate a single term to an SMTLib S-Expression.
|
SExpr |
translate(Term problem,
SExpr.Type type)
Translate a single term to an SMTLib S-Expression.
|
public MasterHandler(Services services, SMTSettings settings) throws java.io.IOException
services
- non-null servicessettings
- settings from the proof for the property settings.java.io.IOException
public void addDeclarationsAndAxioms(java.util.Properties snippets)
snippets
- public SExpr translate(Term problem)
SMTHandler
that can deal with the argument and
delegates to that.
A default translation is triggered if no handler can be found.problem
- the non-null term to translatepublic SExpr translate(Term problem, SExpr.Type type)
SMTHandler
that can deal with the argument and
delegates to that.
A default translation is triggered if no handler can be found.problem
- the non-null term to translatepublic java.util.List<java.lang.Throwable> getExceptions()
public java.util.List<SExpr> translate(java.lang.Iterable<Term> terms, SExpr.Type type) throws SMTTranslationException
terms
- non-null list of terms.type
- the non-null smt type to coerce toSMTTranslationException
public java.util.List<SExpr> translate(java.lang.Iterable<Term> terms)
terms
- non-null list of terms.public java.util.List<Writable> getDeclarations()
public java.util.List<Writable> getAxioms()
public void addSort(Sort s)
public java.util.Set<Sort> getSorts()
Copyright © 2003-2019 The KeY-Project.