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 |
Modifier and Type | Method and Description |
---|---|
void |
ModelExtractor.addFunction(SMTFunction f) |
Modifier and Type | Class and Description |
---|---|
class |
SMTFunctionDef |
Modifier and Type | Method and Description |
---|---|
SMTFunction |
SMTSort.getAllocatedAtoms() |
SMTFunction |
SMTSort.getBoundConst() |
SMTFunction |
SMTTermCall.getFunc() |
SMTFunction |
SMTSort.getIs() |
Modifier and Type | Method and Description |
---|---|
java.util.List<SMTFunction> |
SMTFile.getFunctions() |
Modifier and Type | Method and Description |
---|---|
void |
SMTFile.addFunction(SMTFunction function) |
static SMTTerm |
SMTTerm.call(SMTFunction func) |
static SMTTerm |
SMTTerm.call(SMTFunction func,
java.util.List<? extends SMTTerm>... args) |
static SMTTerm |
SMTTerm.call(SMTFunction func,
java.util.List<? extends SMTTerm> args,
SMTTerm... moreArgs) |
static SMTTerm |
SMTTerm.call(SMTFunction func,
java.util.List<SMTTerm> args) |
static SMTTerm |
SMTTerm.call(SMTFunction func,
SMTTerm... args) |
static SMTTerm |
SMTTerm.call(SMTFunction func,
SMTTerm arg) |
static SMTTerm |
SMTTerm.call(SMTFunction func,
SMTTerm[]... args) |
static SMTTerm |
SMTTerm.call(SMTFunction func,
SMTTerms t) |
void |
SMTFile.removeFunction(SMTFunction function) |
void |
SMTSort.setAllocatedAtoms(SMTFunction allocatedAtoms) |
void |
SMTSort.setBoundConst(SMTFunction boundConst) |
void |
SMTTermCall.setFunc(SMTFunction func) |
void |
SMTSort.setIs(SMTFunction is) |
Modifier and Type | Method and Description |
---|---|
void |
SMTFile.removeAllFunction(java.util.Set<SMTFunction> functions) |
void |
SMTFile.setFunctions(java.util.List<SMTFunction> functions) |
Constructor and Description |
---|
SMTFunctionDef(SMTFunction f,
java.util.List<SMTTermVariable> vars,
SMTTerm sub) |
SMTFunctionDef(SMTFunction f,
SMTTermVariable var,
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) |
SMTTermCall(SMTFunction func,
java.util.List<SMTTerm> args) |
SMTTermCall(SMTFunction func,
SMTTerm arg) |
Copyright © 2003-2019 The KeY-Project.