Package | Description |
---|---|
de.uka.ilkd.key.smt.newsmt2 |
Modifier and Type | Field and Description |
---|---|
static SExpr |
SExprs.FALSE
The constant "false" of type Bool
|
static SExpr |
SExprs.TRUE
The constant "true" of type Bool
|
static SExpr |
SExprs.ZERO
The constant "0" of type Int
|
Modifier and Type | Method and Description |
---|---|
static SExpr |
SExprs.and(java.util.List<SExpr> clauses)
Produce a conjunction of SExprs.
|
static SExpr |
SExprs.assertion(SExpr assertion)
Produce an anssertion.
|
static SExpr |
SExprs.castExpr(SExpr sortExp,
SExpr exp)
Produce a cast expression
|
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 |
HandlerUtil.funDeclaration(SortedOperator op,
java.lang.String name)
Generate a smtlib expression for the smtlib declaration that
represents the operator op.
|
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 |
LogicalVariableHandler.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 |
UpdateHandler.handle(MasterHandler trans,
Term term) |
SExpr |
SumProdHandler.handle(MasterHandler trans,
Term term) |
SExpr |
NumberConstantsHandler.handle(MasterHandler trans,
Term term) |
SExpr |
CastHandler.handle(MasterHandler trans,
Term term) |
static SExpr |
SExprs.imp(SExpr ante,
SExpr cons)
Produce an implication from an assumption and a conclusion.
|
static SExpr |
SExprs.instanceOf(SExpr var,
SExpr sortExpr) |
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.let(java.lang.String var,
SExpr val,
SExpr in) |
static SExpr |
LogicalVariableHandler.makeVarDecl(java.lang.String name,
Sort sort) |
static SExpr |
LogicalVariableHandler.makeVarRef(java.lang.String name,
Sort sort) |
SExpr |
SExpr.map(java.util.function.Function<SExpr,SExpr> mapFunction)
Create a new
SExpr by applying a function to all children of this object. |
static SExpr |
SExprs.minus(SExpr a,
SExpr b) |
static SExpr |
SExprs.patternSExpr(SExpr e,
java.util.List<SExpr> patterns)
Produce a smt matching pattern.
|
static SExpr |
SExprs.patternSExpr(SExpr e,
SExpr... patterns)
Produce a smt matching pattern.
|
static SExpr |
SExprs.plus(SExpr a,
SExpr b) |
static SExpr |
SExprs.pullOutPatterns(SExpr matrix)
Collects the :pattern annations from any nesting depth in a term and
brings it to toplevel.
|
static SExpr |
SExprs.sortExpr(Sort sort)
Turn a KeY sort into an SMT sort (by prefixing
SExprs.SORT_PREFIX . |
SExpr |
MasterHandler.translate(Term problem)
Translate a single term to an SMTLib S-Expression.
|
SExpr |
MasterHandler.translate(Term problem,
SExpr.Type type)
Translate a single term to an SMTLib S-Expression.
|
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. |
java.util.List<SExpr> |
SExpr.getChildren() |
java.util.Map<Term,SExpr> |
MasterHandler.getUnknownValues() |
java.util.List<SExpr> |
MasterHandler.translate(java.lang.Iterable<Term> terms)
Translate a list of terms into a list of SExprs without coercion.
|
java.util.List<SExpr> |
MasterHandler.translate(java.lang.Iterable<Term> terms,
SExpr.Type type)
Translate a list of terms into a list of SExprs.
|
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 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) |
static SExpr |
SExprs.imp(SExpr ante,
SExpr cons)
Produce an implication from an assumption and a conclusion.
|
static SExpr |
SExprs.instanceOf(SExpr var,
SExpr sortExpr) |
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.let(java.lang.String var,
SExpr val,
SExpr in) |
static SExpr |
SExprs.minus(SExpr a,
SExpr b) |
static SExpr |
SExprs.patternSExpr(SExpr e,
java.util.List<SExpr> patterns)
Produce a smt matching pattern.
|
static SExpr |
SExprs.patternSExpr(SExpr e,
SExpr... patterns)
Produce a smt matching pattern.
|
static SExpr |
SExprs.patternSExpr(SExpr e,
SExpr... patterns)
Produce a smt matching pattern.
|
static SExpr |
SExprs.plus(SExpr a,
SExpr b) |
static SExpr |
SExprs.pullOutPatterns(SExpr matrix)
Collects the :pattern annations from any nesting depth in a term and
brings it to toplevel.
|
Modifier and Type | Method and Description |
---|---|
static SExpr |
SExprs.and(java.util.List<SExpr> clauses)
Produce a conjunction of SExprs.
|
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.forall(java.util.List<SExpr> vars,
SExpr matrix)
Produce a universal quantification.
|
SExpr |
SExpr.map(java.util.function.Function<SExpr,SExpr> mapFunction)
Create a new
SExpr by applying a function to all children of this object. |
SExpr |
SExpr.map(java.util.function.Function<SExpr,SExpr> mapFunction)
Create a new
SExpr by applying a function to all children of this object. |
static SExpr |
SExprs.patternSExpr(SExpr e,
java.util.List<SExpr> patterns)
Produce a smt matching pattern.
|
Constructor and Description |
---|
SExpr(SExpr... children)
Create a new s-expr without atomic name (set to "")
with children and type
SExpr.Type.NONE . |
SExpr(java.lang.String name,
SExpr... children)
Create a new s-expr with children and type
SExpr.Type.NONE . |
SExpr(java.lang.String name,
SExpr.Type type,
SExpr... children)
Create a new s-expr with children and a given type.
|
Constructor and Description |
---|
SExpr(java.util.List<SExpr> children)
Create a new s-expr without atomic name (set to "")
with children and type
SExpr.Type.NONE . |
SExpr(java.lang.String name,
java.util.List<SExpr> children)
Create a new s-expr with children and type
SExpr.Type.NONE . |
SExpr(java.lang.String name,
SExpr.Type type,
java.util.List<SExpr> children)
Create a new s-expr with children and a given type.
|
Copyright © 2003-2019 The KeY-Project.