public class SMTObjTranslator extends java.lang.Object implements SMTTranslator
Modifier and Type | Class and Description |
---|---|
class |
SMTObjTranslator.ConstantCounter
Class for counting constants of different types appearing in the proof
obligation.
|
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
ANY_SORT |
static java.lang.String |
BINT_SORT |
static java.lang.String |
CLASS_INVARIANT |
static java.lang.String |
ELEMENTOF |
static java.lang.String |
FIELD_SORT |
static java.lang.String |
HEAP_SORT |
static java.lang.String |
LENGTH |
static java.lang.String |
LOCSET_SORT |
static java.lang.String |
OBJECT_SORT |
static java.lang.String |
SEQ_GET |
static java.lang.String |
SEQ_LEN |
static java.lang.String |
SEQ_SORT |
Constructor and Description |
---|
SMTObjTranslator(SMTSettings settings,
Services services,
KeYJavaType typeOfClassUnderTest) |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
getExactInstanceName(java.lang.String sortName) |
ModelExtractor |
getQuery() |
static java.lang.String |
getTypePredicateName(java.lang.String id) |
ProblemTypeInformation |
getTypes() |
java.lang.StringBuffer |
translateProblem(Sequent sequent,
Services services,
SMTSettings settings)
Translates a problem into the given syntax.
|
SMTFile |
translateProblem(Term problem)
Translates a KeY problem into a SMTFile.
|
SMTTerm |
translateTerm(Term term)
Translates a KeY term to an SMT term.
|
public static final java.lang.String CLASS_INVARIANT
public static final java.lang.String LENGTH
public static final java.lang.String BINT_SORT
public static final java.lang.String HEAP_SORT
public static final java.lang.String FIELD_SORT
public static final java.lang.String LOCSET_SORT
public static final java.lang.String OBJECT_SORT
public static final java.lang.String ANY_SORT
public static final java.lang.String SEQ_SORT
public static final java.lang.String ELEMENTOF
public static final java.lang.String SEQ_GET
public static final java.lang.String SEQ_LEN
public SMTObjTranslator(SMTSettings settings, Services services, KeYJavaType typeOfClassUnderTest)
public ProblemTypeInformation getTypes()
public java.lang.StringBuffer translateProblem(Sequent sequent, Services services, SMTSettings settings) throws IllegalFormulaException
SMTTranslator
translate(Term t, Services services)
is that assumptions
will be added.translateProblem
in interface SMTTranslator
sequent
- the sequent to be translated.IllegalFormulaException
public ModelExtractor getQuery()
public SMTFile translateProblem(Term problem) throws IllegalFormulaException
problem
- The KeY proof obligation.IllegalFormulaException
public SMTTerm translateTerm(Term term) throws IllegalFormulaException
term
- the KeY term.IllegalFormulaException
public static java.lang.String getTypePredicateName(java.lang.String id)
public static java.lang.String getExactInstanceName(java.lang.String sortName)
Copyright © 2003-2019 The KeY-Project.