Package | Description |
---|---|
de.uka.ilkd.key.smt |
This package contains the SMT backend of KeY, allowing to translate KeY formulas
to formulas in formats such as SMT-LIB, and allowing to send such formulas to
SMT solvers such as Simplify or Z3.
|
de.uka.ilkd.key.smt.lang | |
de.uka.ilkd.key.smt.model |
Modifier and Type | Method and Description |
---|---|
SMTSort |
ProblemTypeInformation.getSort(java.lang.String sortName) |
SMTSort |
ProblemTypeInformation.getTypeForConstant(java.lang.Object key) |
SMTSort |
ProblemTypeInformation.getTypeForField(java.lang.Object key) |
SMTSort |
ProblemTypeInformation.putConstantType(java.lang.String key,
SMTSort value) |
SMTSort |
ProblemTypeInformation.putFieldType(java.lang.String key,
SMTSort value) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
ProblemTypeInformation.getPrefixForSort(SMTSort sort) |
SMTSort |
ProblemTypeInformation.putConstantType(java.lang.String key,
SMTSort value) |
SMTSort |
ProblemTypeInformation.putFieldType(java.lang.String key,
SMTSort value) |
Modifier and Type | Method and Description |
---|---|
void |
ProblemTypeInformation.setSortNumbers(java.util.Map<SMTSort,SMTTermNumber> sortNumbers) |
void |
ProblemTypeInformation.setSorts(java.util.Map<java.lang.String,SMTSort> sorts) |
Constructor and Description |
---|
OverflowChecker(SMTSort intsort) |
Modifier and Type | Field and Description |
---|---|
static SMTSort |
SMTSort.BOOL |
protected SMTSort |
SMTFunction.imageSort |
static SMTSort |
SMTSort.INT |
Modifier and Type | Field and Description |
---|---|
protected java.util.List<SMTSort> |
SMTFunction.domainSorts |
Modifier and Type | Method and Description |
---|---|
SMTSort |
SMTFunction.getImageSort() |
SMTSort |
SMTTermVariable.getSort() |
SMTSort |
SMTSort.getTopLevel() |
static SMTSort |
SMTSort.mkBV(long bitSize) |
abstract SMTSort |
SMTTerm.sort() |
SMTSort |
SMTTerm.True.sort() |
SMTSort |
SMTTerm.False.sort() |
SMTSort |
SMTTermVariable.sort() |
SMTSort |
SMTTermBinOp.sort() |
SMTSort |
SMTTermITE.sort() |
SMTSort |
SMTTermMultOp.sort() |
SMTSort |
SMTTermUnaryOp.sort() |
SMTSort |
SMTTermQuant.sort() |
SMTSort |
SMTTermNumber.sort() |
SMTSort |
SMTTermCall.sort() |
SMTSort |
SMTTerms.sort() |
Modifier and Type | Method and Description |
---|---|
java.util.List<SMTSort> |
SMTFunction.getDomainSorts() |
java.util.List<SMTSort> |
SMTFile.getSorts() |
Modifier and Type | Method and Description |
---|---|
void |
SMTFile.addSort(SMTSort sort) |
void |
SMTFunction.setImageSort(SMTSort imageSort) |
void |
SMTTermVariable.setSort(SMTSort sort) |
void |
SMTSort.setTopLevel(SMTSort topLevel) |
Modifier and Type | Method and Description |
---|---|
void |
SMTFunction.setDomainSorts(java.util.List<SMTSort> domainSorts) |
void |
SMTFile.setSorts(java.util.List<SMTSort> sorts) |
Constructor and Description |
---|
SMTFunction(java.lang.String id,
java.util.List<SMTSort> domainSorts,
SMTSort imageSort) |
SMTFunction(java.lang.String id,
SMTSort argSort1,
SMTSort argSort2,
SMTSort imageSort) |
SMTFunctionDef(java.lang.String id,
java.util.List<SMTTermVariable> vars,
SMTSort image,
SMTTerm sub) |
SMTFunctionDef(java.lang.String id,
SMTTermVariable var,
SMTSort image,
SMTTerm sub) |
SMTSort(java.lang.String name,
SMTSort topLevel,
SMTFunction is) |
SMTSort(java.lang.String name,
SMTSort topLevel,
SMTFunction is,
int bitSize) |
SMTSort(java.lang.String name,
SMTSort topLevel,
SMTFunction is,
int bound,
SMTFunction allocatedAtoms) |
SMTTermNumber(long intValue,
long bitSize,
SMTSort sort) |
SMTTermVariable(java.lang.String id,
SMTSort sort) |
Constructor and Description |
---|
SMTFunction(java.lang.String id,
java.util.List<SMTSort> domainSorts,
SMTSort imageSort) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
Model.processConstantValue(java.lang.String val,
SMTSort s)
Transforms a constant value from binary/hexadecimal form to a human
redable form.
|
Copyright © 2003-2019 The KeY-Project.