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 |
OverflowChecker.searchArithTerms(java.util.Set<SMTTerm> terms,
SMTTerm sub,
java.util.Set<SMTTermVariable> universalVars,
java.util.Set<SMTTermVariable> existentialVars,
java.util.List<SMTTermVariable> bind)
Searches for non ground terms in sub, and stores them in terms.
|
void |
OverflowChecker.searchArithTerms(java.util.Set<SMTTerm> terms,
SMTTerm sub,
java.util.Set<SMTTermVariable> universalVars,
java.util.Set<SMTTermVariable> existentialVars,
java.util.List<SMTTermVariable> bind)
Searches for non ground terms in sub, and stores them in terms.
|
void |
OverflowChecker.searchArithTerms(java.util.Set<SMTTerm> terms,
SMTTerm sub,
java.util.Set<SMTTermVariable> universalVars,
java.util.Set<SMTTermVariable> existentialVars,
java.util.List<SMTTermVariable> bind)
Searches for non ground terms in sub, and stores them in terms.
|
Modifier and Type | Method and Description |
---|---|
SMTTermVariable |
SMTTermVariable.copy() |
Modifier and Type | Method and Description |
---|---|
java.util.List<SMTTermVariable> |
SMTTermQuant.getBindVars() |
java.util.List<SMTTermVariable> |
SMTTerm.getEQVars() |
java.util.List<SMTTermVariable> |
SMTTermBinOp.getEQVars() |
java.util.List<SMTTermVariable> |
SMTTermMultOp.getEQVars() |
java.util.List<SMTTermVariable> |
SMTTermUnaryOp.getEQVars() |
java.util.List<SMTTermVariable> |
SMTTermQuant.getEQVars() |
java.util.List<SMTTermVariable> |
SMTTermCall.getEQVars() |
java.util.List<SMTTermVariable> |
SMTTerm.getQuantVars() |
java.util.List<SMTTermVariable> |
SMTTermBinOp.getQuantVars() |
java.util.List<SMTTermVariable> |
SMTTermITE.getQuantVars() |
java.util.List<SMTTermVariable> |
SMTTermMultOp.getQuantVars() |
java.util.List<SMTTermVariable> |
SMTTermUnaryOp.getQuantVars() |
java.util.List<SMTTermVariable> |
SMTTermQuant.getQuantVars() |
java.util.List<SMTTermVariable> |
SMTTermCall.getQuantVars() |
java.util.List<SMTTermVariable> |
SMTTerm.getUQVars() |
java.util.List<SMTTermVariable> |
SMTTermBinOp.getUQVars() |
java.util.List<SMTTermVariable> |
SMTTermMultOp.getUQVars() |
java.util.List<SMTTermVariable> |
SMTTermUnaryOp.getUQVars() |
java.util.List<SMTTermVariable> |
SMTTermQuant.getUQVars() |
java.util.List<SMTTermVariable> |
SMTTermCall.getUQVars() |
java.util.List<SMTTermVariable> |
SMTTerm.getVars() |
java.util.List<SMTTermVariable> |
SMTTermVariable.getVars() |
java.util.List<SMTTermVariable> |
SMTTermBinOp.getVars() |
java.util.List<SMTTermVariable> |
SMTTermMultOp.getVars() |
java.util.List<SMTTermVariable> |
SMTTermUnaryOp.getVars() |
java.util.List<SMTTermVariable> |
SMTTermQuant.getVars() |
java.util.List<SMTTermVariable> |
SMTFunctionDef.getVars() |
java.util.List<SMTTermVariable> |
SMTTermCall.getVars() |
Modifier and Type | Method and Description |
---|---|
SMTTerm |
SMTTerm.exists(java.util.List<SMTTermVariable> bindVars) |
SMTTerm |
SMTTerm.exists(java.util.List<SMTTermVariable> bindVars,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerm |
SMTTerm.exists(java.util.List<SMTTermVariable> bindVars1,
java.util.List<SMTTermVariable> bindVars2,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerm |
SMTTerm.exists(java.util.List<SMTTermVariable> bindVars1,
java.util.List<SMTTermVariable> bindVars2,
java.util.List<java.util.List<SMTTerm>> pats) |
static SMTTerm |
SMTTerm.exists(java.util.List<SMTTermVariable> bindVars,
SMTTerm subForm,
java.util.List<SMTTerm> pats) |
SMTTerm |
SMTTerm.forall(java.util.List<SMTTermVariable> bindVars) |
SMTTerm |
SMTTerm.forall(java.util.List<SMTTermVariable> bindVars,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerm |
SMTTerm.True.forall(java.util.List<SMTTermVariable> bindVars,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerm |
SMTTerm.False.forall(java.util.List<SMTTermVariable> bindVars,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerm |
SMTTerm.forall(java.util.List<SMTTermVariable> bindVars1,
java.util.List<SMTTermVariable> bindVars2,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerm |
SMTTerm.forall(java.util.List<SMTTermVariable> bindVars1,
java.util.List<SMTTermVariable> bindVars2,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerm |
SMTTerm.forall(java.util.List<SMTTermVariable> bindVars1,
java.util.List<SMTTermVariable> bindVars2,
SMTTerm pat) |
SMTTerm |
SMTTerm.forall(java.util.List<SMTTermVariable> bindVars1,
java.util.List<SMTTermVariable> bindVars2,
SMTTerm pat) |
static SMTTerm |
SMTTerm.forall(java.util.List<SMTTermVariable> bindVars,
SMTTerm subForm,
java.util.List<SMTTerm> pats) |
SMTTerm |
SMTTerm.quant(SMTTermQuant.Quant quant,
java.util.List<SMTTermVariable> bindVars) |
SMTTerm |
SMTTerm.quant(SMTTermQuant.Quant quant,
java.util.List<SMTTermVariable> bindVars,
java.util.List<java.util.List<SMTTerm>> pats) |
void |
SMTTermQuant.setBindVars(java.util.List<SMTTermVariable> bindVars) |
Constructor and Description |
---|
SMTFunctionDef(SMTFunction f,
SMTTermVariable var,
SMTTerm sub) |
SMTFunctionDef(java.lang.String id,
SMTTermVariable var,
SMTSort image,
SMTTerm sub) |
Constructor and Description |
---|
SMTFunctionDef(SMTFunction f,
java.util.List<SMTTermVariable> vars,
SMTTerm sub) |
SMTFunctionDef(java.lang.String id,
java.util.List<SMTTermVariable> vars,
SMTSort image,
SMTTerm sub) |
SMTTermQuant(SMTTermQuant.Quant quant,
java.util.List<SMTTermVariable> bindVars,
SMTTerm sub,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTermQuant(SMTTermQuant.Quant quant,
java.util.List<SMTTermVariable> bindVars,
SMTTerm sub,
SMTTerm pat) |
Copyright © 2003-2019 The KeY-Project.