Package | Description |
---|---|
de.uka.ilkd.key.smt.newsmt2 |
Modifier and Type | Field and Description |
---|---|
static SExpr.Type |
SExpr.Type.BOOL
to indicate that an expression holds a value of type Bool
|
static SExpr.Type |
IntegerOpHandler.INT
to indicate that an expression holds a value of type Int.
|
static SExpr.Type |
SExpr.Type.NONE
to indicate that this expression has other or unknown type
|
static SExpr.Type |
SExpr.Type.UNIVERSE
to indicate that this expression holds a value of type U
|
static SExpr.Type |
SExpr.Type.VERBATIM
to indicate that this element needs no escaping despite its name
|
Modifier and Type | Method and Description |
---|---|
SExpr.Type |
SExpr.getType() |
Modifier and Type | Method and Description |
---|---|
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.
|
java.util.List<SExpr> |
MasterHandler.translate(java.lang.Iterable<Term> terms,
SExpr.Type type)
Translate a list of terms into a list of SExprs.
|
SExpr |
MasterHandler.translate(Term problem,
SExpr.Type type)
Translate a single term to an SMTLib S-Expression.
|
Constructor and Description |
---|
SExpr(java.lang.String name,
SExpr.Type type)
Create a new s-expr without children, but with a given type.
|
SExpr(java.lang.String name,
SExpr.Type type,
java.util.List<SExpr> children)
Create a new s-expr with children and a given type.
|
SExpr(java.lang.String name,
SExpr.Type type,
SExpr... children)
Create a new s-expr with children and a given type.
|
SExpr(java.lang.String name,
SExpr.Type type,
java.lang.String... children)
Create a new s-expr with children and a given type.
|
Copyright © 2003-2019 The KeY-Project.