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 |
---|---|
SMTTerm |
OverflowChecker.addGuardIfNecessary(SMTTerm t)
Adds a guard for the given term if that term may overflow.
|
SMTTerm |
SMTObjTranslator.translateTerm(Term term)
Translates a KeY term to an SMT term.
|
Modifier and Type | Method and Description |
---|---|
java.util.List<SMTTerm> |
OverflowChecker.createGuards(java.util.Set<SMTTerm> terms)
Creates guards for the given terms
|
Modifier and Type | Method and Description |
---|---|
SMTTerm |
OverflowChecker.addGuardIfNecessary(SMTTerm t)
Adds a guard for the given term if that term may overflow.
|
void |
OverflowChecker.processTerm(SMTTerm t)
Recursively adds overflow guards for non ground terms if necessary.
|
void |
OverflowChecker.searchArithGroundTerms(java.util.Set<SMTTerm> terms,
SMTTerm sub)
Searches for arithmetical 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 |
---|---|
java.util.List<SMTTerm> |
OverflowChecker.createGuards(java.util.Set<SMTTerm> terms)
Creates guards for the given terms
|
void |
OverflowChecker.searchArithGroundTerms(java.util.Set<SMTTerm> terms,
SMTTerm sub)
Searches for arithmetical 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 | Class and Description |
---|---|
static class |
SMTTerm.False |
static class |
SMTTerm.True |
class |
SMTTermBinOp |
class |
SMTTermCall
SMTLib supports functions as well as predicates.
|
class |
SMTTermITE |
class |
SMTTermMultOp |
class |
SMTTermNumber |
class |
SMTTermQuant |
class |
SMTTerms |
class |
SMTTermUnaryOp |
class |
SMTTermVariable |
Modifier and Type | Field and Description |
---|---|
static SMTTerm |
SMTTerm.FALSE |
static SMTTerm |
SMTTerm.TRUE |
SMTTerm |
SMTTerm.upp |
Modifier and Type | Field and Description |
---|---|
protected java.util.List<SMTTerm> |
SMTTermMultOp.subs |
protected java.util.List<SMTTerm> |
SMTTerms.terms |
Modifier and Type | Method and Description |
---|---|
static SMTTerm |
SMTTerm.and(java.util.List<SMTTerm> args) |
SMTTerm |
SMTTerm.and(SMTTerm right) |
SMTTerm |
SMTTerm.True.and(SMTTerm right) |
SMTTerm |
SMTTerm.False.and(SMTTerm right) |
SMTTerm |
SMTTerm.binOp(SMTTermBinOp.Op op,
SMTTerm f) |
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) |
SMTTerm |
SMTTerm.concat(SMTTerm f) |
abstract SMTTerm |
SMTTerm.copy() |
SMTTerm |
SMTTerm.True.copy() |
SMTTerm |
SMTTerm.False.copy() |
SMTTerm |
SMTTermITE.copy() |
SMTTerm |
SMTTerm.div(SMTTerm right) |
static SMTTerm |
SMTTerm.equal(java.util.List<SMTTerm> args) |
SMTTerm |
SMTTerm.equal(SMTTerm right) |
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) |
static SMTTerm |
SMTTerm.exists(java.util.List<SMTTermVariable> bindVars,
SMTTerm subForm,
java.util.List<SMTTerm> pats) |
SMTTerm |
SMTTerm.exists(SMTTermVariable var) |
SMTTerm |
SMTTerm.exists(SMTTermVariable var,
SMTTerm pat) |
static SMTTerm |
SMTTerm.exists(SMTTermVariable bindVar,
SMTTerm subForm,
java.util.List<SMTTerm> pats) |
static SMTTerm |
SMTTerm.exists(SMTTermVariable bindVar,
SMTTerm subForm,
SMTTerm pat) |
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,
SMTTerm pat) |
static SMTTerm |
SMTTerm.forall(java.util.List<SMTTermVariable> bindVars,
SMTTerm subForm,
java.util.List<SMTTerm> pats) |
SMTTerm |
SMTTerm.forall(SMTTerms terms) |
SMTTerm |
SMTTerm.forall(SMTTerms terms,
SMTTerm pat) |
SMTTerm |
SMTTerm.forall(SMTTermVariable var) |
SMTTerm |
SMTTerm.forall(SMTTermVariable var,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerm |
SMTTerm.forall(SMTTermVariable var,
SMTTerm pat) |
static SMTTerm |
SMTTerm.forall(SMTTermVariable bindVar,
SMTTerm subForm,
java.util.List<SMTTerm> pats) |
SMTTerm |
SMTTermITE.getCondition() |
SMTTerm |
SMTTermITE.getFalseCase() |
SMTTerm |
SMTTermMultOp.Op.getIdem() |
SMTTerm |
SMTTermBinOp.getLeft() |
SMTTerm |
SMTTermVariable.getQuant() |
SMTTerm |
SMTTermBinOp.getRight() |
SMTTerm |
SMTTermUnaryOp.getSub() |
SMTTerm |
SMTTermQuant.getSub() |
SMTTerm |
SMTFunctionDef.getSub() |
SMTTerm |
SMTTermITE.getTrueCase() |
SMTTerm |
SMTTermNumber.getUpp() |
SMTTerm |
SMTTerm.gt(SMTTerm right) |
SMTTerm |
SMTTerm.gte(SMTTerm right) |
SMTTerm |
SMTTerm.iff(SMTTerm right) |
SMTTerm |
SMTTerm.True.iff(SMTTerm right) |
SMTTerm |
SMTTerm.False.iff(SMTTerm right) |
static SMTTerm |
SMTTerm.implies(java.util.List<SMTTerm> args) |
SMTTerm |
SMTTerm.implies(SMTTerm right) |
SMTTerm |
SMTTerm.True.implies(SMTTerm right) |
SMTTerm |
SMTTerm.False.implies(SMTTerm right) |
abstract SMTTerm |
SMTTerm.instantiate(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTerm.True.instantiate(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTerm.False.instantiate(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermVariable.instantiate(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermBinOp.instantiate(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermITE.instantiate(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermMultOp.instantiate(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermUnaryOp.instantiate(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermQuant.instantiate(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermNumber.instantiate(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermCall.instantiate(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTerms.instantiate(SMTTermVariable a,
SMTTerm b) |
static SMTTerm |
SMTTerm.ite(SMTTerm condition,
SMTTerm trueCase,
SMTTerm falseCase) |
SMTTerm |
SMTTerm.lt(SMTTerm right) |
SMTTerm |
SMTTerm.lte(SMTTerm right) |
SMTTerm |
SMTTerm.minus(SMTTerm right) |
SMTTerm |
SMTTermMultOp.mkChain() |
SMTTerm |
SMTTerm.mul(SMTTerm right) |
SMTTerm |
SMTTerm.multOp(SMTTermMultOp.Op op,
SMTTerm t) |
SMTTerm |
SMTTerm.not() |
static SMTTerm |
SMTTerm.not(SMTTerm subForm) |
static SMTTerm |
SMTTerm.number(int n) |
static SMTTerm |
SMTTerm.number(int n,
int bitSize) |
static SMTTerm |
SMTTerm.or(java.util.List<SMTTerm> args) |
SMTTerm |
SMTTerm.or(SMTTerm right) |
SMTTerm |
SMTTerm.True.or(SMTTerm right) |
SMTTerm |
SMTTerm.False.or(SMTTerm right) |
SMTTerm |
SMTTerm.plus(SMTTerm right) |
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) |
SMTTerm |
SMTTerm.rem(SMTTerm right) |
abstract SMTTerm |
SMTTerm.replace(SMTTermCall a,
SMTTerm b) |
SMTTerm |
SMTTerm.True.replace(SMTTermCall a,
SMTTerm b) |
SMTTerm |
SMTTerm.False.replace(SMTTermCall a,
SMTTerm b) |
SMTTerm |
SMTTermVariable.replace(SMTTermCall a,
SMTTerm b) |
SMTTerm |
SMTTermBinOp.replace(SMTTermCall a,
SMTTerm b) |
SMTTerm |
SMTTermITE.replace(SMTTermCall a,
SMTTerm b) |
SMTTerm |
SMTTermMultOp.replace(SMTTermCall a,
SMTTerm b) |
SMTTerm |
SMTTermUnaryOp.replace(SMTTermCall a,
SMTTerm b) |
SMTTerm |
SMTTermQuant.replace(SMTTermCall a,
SMTTerm b) |
SMTTerm |
SMTTermNumber.replace(SMTTermCall a,
SMTTerm b) |
SMTTerm |
SMTTermCall.replace(SMTTermCall a,
SMTTerm b) |
SMTTerm |
SMTTerms.replace(SMTTermCall a,
SMTTerm b) |
SMTTerm |
SMTTerm.sign(boolean pol) |
SMTTerm |
SMTTerm.True.sign(boolean pol) |
SMTTerm |
SMTTerm.False.sign(boolean pol) |
abstract SMTTerm |
SMTTerm.substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
SMTTerm.True.substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
SMTTerm.False.substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
SMTTermVariable.substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
SMTTermBinOp.substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
SMTTermITE.substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
SMTTermMultOp.substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
SMTTermUnaryOp.substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
SMTTermQuant.substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
SMTTermNumber.substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
SMTTermCall.substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
SMTTerms.substitute(SMTTerm a,
SMTTerm b) |
abstract SMTTerm |
SMTTerm.substitute(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTerm.True.substitute(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTerm.False.substitute(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermVariable.substitute(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermBinOp.substitute(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermITE.substitute(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermMultOp.substitute(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermUnaryOp.substitute(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermQuant.substitute(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermNumber.substitute(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTermCall.substitute(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTerms.substitute(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
SMTTerm.unaryOp(SMTTermUnaryOp.Op op) |
Modifier and Type | Method and Description |
---|---|
java.util.List<SMTTerm> |
SMTTerms.flatten() |
java.util.List<SMTTerm> |
SMTTermCall.getArgs() |
java.util.List<SMTTerm> |
SMTFile.getFormulas() |
java.util.List<java.util.List<SMTTerm>> |
SMTTermQuant.getPats() |
java.util.List<SMTTerm> |
SMTTerm.getSubs() |
java.util.List<SMTTerm> |
SMTTermMultOp.getSubs() |
java.util.List<SMTTerm> |
SMTTerms.getTerms() |
java.util.List<SMTTerm> |
SMTTerm.toList() |
Modifier and Type | Method and Description |
---|---|
void |
SMTFile.addFormulas(java.util.List<SMTTerm> terms) |
static SMTTerm |
SMTTerm.and(java.util.List<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.equal(java.util.List<SMTTerm> args) |
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) |
static SMTTerm |
SMTTerm.exists(java.util.List<SMTTermVariable> bindVars,
SMTTerm subForm,
java.util.List<SMTTerm> pats) |
static SMTTerm |
SMTTerm.exists(SMTTermVariable bindVar,
SMTTerm subForm,
java.util.List<SMTTerm> pats) |
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) |
static SMTTerm |
SMTTerm.forall(java.util.List<SMTTermVariable> bindVars,
SMTTerm subForm,
java.util.List<SMTTerm> pats) |
SMTTerm |
SMTTerm.forall(SMTTermVariable var,
java.util.List<java.util.List<SMTTerm>> pats) |
static SMTTerm |
SMTTerm.forall(SMTTermVariable bindVar,
SMTTerm subForm,
java.util.List<SMTTerm> pats) |
static SMTTerm |
SMTTerm.implies(java.util.List<SMTTerm> args) |
static SMTTerm |
SMTTerm.or(java.util.List<SMTTerm> args) |
SMTTerm |
SMTTerm.quant(SMTTermQuant.Quant quant,
java.util.List<SMTTermVariable> bindVars,
java.util.List<java.util.List<SMTTerm>> pats) |
void |
SMTTermCall.setArgs(java.util.List<SMTTerm> args) |
void |
SMTFile.setFormulas(java.util.List<SMTTerm> formulas) |
void |
SMTTermQuant.setPats(java.util.List<java.util.List<SMTTerm>> pats) |
void |
SMTTermMultOp.setSubs(java.util.List<SMTTerm> subs) |
void |
SMTTerms.setTerms(java.util.List<SMTTerm> terms) |
static SMTTerms |
SMTTerm.terms(java.util.List<SMTTerm> terms) |
Constructor and Description |
---|
SMTFunctionDef(SMTFunction f,
java.util.List<SMTTermVariable> vars,
SMTTerm sub) |
SMTFunctionDef(SMTFunction f,
SMTTermVariable var,
SMTTerm sub) |
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) |
SMTTermBinOp(SMTTermBinOp.Op operator,
SMTTerm left,
SMTTerm right) |
SMTTermCall(SMTFunction func,
SMTTerm arg) |
SMTTermITE(SMTTerm condition,
SMTTerm trueCase,
SMTTerm falseCase) |
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) |
SMTTermUnaryOp(SMTTermUnaryOp.Op operator,
SMTTerm sub) |
Constructor and Description |
---|
SMTTermCall(SMTFunction func,
java.util.List<SMTTerm> args) |
SMTTermMultOp(SMTTermMultOp.Op operator,
java.util.List<SMTTerm> subs) |
SMTTermQuant(SMTTermQuant.Quant quant,
java.util.List<SMTTermVariable> bindVars,
SMTTerm sub,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerms(java.util.List<SMTTerm> terms) |
Copyright © 2003-2019 The KeY-Project.