Package | Description |
---|---|
de.uka.ilkd.key.smt.newsmt2 |
Modifier and Type | Method and Description |
---|---|
static SExpr |
SExprs.assertion(SExpr assertion)
Produce an anssertion.
|
static SExpr |
SExprs.castExpr(SExpr sortExp,
SExpr exp)
Produce a cast expression
|
static java.util.List<SExpr> |
SExprs.coerce(java.util.List<SExpr> exprs,
SExpr.Type type)
Takes a list of
SExpr s and converts it to a list of the given
type, if possible. |
static SExpr |
SExprs.coerce(SExpr exp,
SExpr.Type type)
Takes an SExpression and converts it to the given type, if possible.
|
static SExpr |
SExprs.eq(SExpr a,
SExpr b) |
static SExpr |
SExprs.forall(java.util.List<SExpr> vars,
SExpr matrix)
Produce a universal quantification.
|
static SExpr |
SExprs.greaterEqual(SExpr a,
SExpr b) |
SExpr |
DefinedSymbolsHandler.handle(MasterHandler trans,
Term term) |
SExpr |
SeqDefHandler.handle(MasterHandler trans,
Term term) |
SExpr |
CastingFunctionsHandler.handle(MasterHandler trans,
Term term) |
SExpr |
QuantifierHandler.handle(MasterHandler trans,
Term term) |
SExpr |
SMTHandler.handle(MasterHandler trans,
Term term)
Translate the given term into an SMT SExpression.
|
SExpr |
BooleanConnectiveHandler.handle(MasterHandler trans,
Term term) |
SExpr |
UninterpretedSymbolsHandler.handle(MasterHandler trans,
Term term) |
SExpr |
PolymorphicHandler.handle(MasterHandler trans,
Term term) |
SExpr |
InstanceOfHandler.handle(MasterHandler trans,
Term term) |
SExpr |
IntegerOpHandler.handle(MasterHandler trans,
Term term) |
SExpr |
FieldConstantHandler.handle(MasterHandler trans,
Term term) |
SExpr |
SumProdHandler.handle(MasterHandler trans,
Term term) |
SExpr |
CastHandler.handle(MasterHandler trans,
Term term) |
void |
MasterHandler.SymbolIntroducer.introduce(MasterHandler masterHandler,
java.lang.String name) |
static SExpr |
SExprs.ite(SExpr cond,
SExpr _then,
SExpr _else) |
static SExpr |
SExprs.lessEqual(SExpr a,
SExpr b) |
static SExpr |
SExprs.lessThan(SExpr a,
SExpr b) |
static SExpr |
SExprs.minus(SExpr a,
SExpr b) |
static SExpr |
SExprs.plus(SExpr a,
SExpr b) |
java.util.List<SExpr> |
MasterHandler.translate(java.lang.Iterable<Term> terms,
SExpr.Type type)
Translate a list of terms into a list of SExprs.
|
Term |
SMTTacletTranslator.translate(Taclet taclet) |
Copyright © 2003-2019 The KeY-Project.