public class SExprs
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
static SExpr |
FALSE
The constant "false" of type Bool
|
static java.lang.String |
SORT_PREFIX
The string prefix used for sort names in SMT,
|
static SExpr |
TRUE
The constant "true" of type Bool
|
static SExpr |
ZERO
The constant "0" of type Int
|
Modifier and Type | Method and Description |
---|---|
static SExpr |
and(java.util.List<SExpr> clauses)
Produce a conjunction of SExprs.
|
static SExpr |
assertion(SExpr assertion)
Produce an anssertion.
|
static SExpr |
castExpr(SExpr sortExp,
SExpr exp)
Produce a cast expression
|
static java.util.List<SExpr> |
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 |
coerce(SExpr exp,
SExpr.Type type)
Takes an SExpression and converts it to the given type, if possible.
|
static SExpr |
eq(SExpr a,
SExpr b) |
static SExpr |
forall(java.util.List<SExpr> vars,
SExpr matrix)
Produce a universal quantification.
|
static SExpr |
greaterEqual(SExpr a,
SExpr b) |
static SExpr |
imp(SExpr ante,
SExpr cons)
Produce an implication from an assumption and a conclusion.
|
static SExpr |
instanceOf(SExpr var,
SExpr sortExpr) |
static SExpr |
ite(SExpr cond,
SExpr _then,
SExpr _else) |
static SExpr |
lessEqual(SExpr a,
SExpr b) |
static SExpr |
lessThan(SExpr a,
SExpr b) |
static SExpr |
let(java.lang.String var,
SExpr val,
SExpr in) |
static SExpr |
minus(SExpr a,
SExpr b) |
static SExpr |
patternSExpr(SExpr e,
java.util.List<SExpr> patterns)
Produce a smt matching pattern.
|
static SExpr |
patternSExpr(SExpr e,
SExpr... patterns)
Produce a smt matching pattern.
|
static SExpr |
plus(SExpr a,
SExpr b) |
static SExpr |
pullOutPatterns(SExpr matrix)
Collects the :pattern annations from any nesting depth in a term and
brings it to toplevel.
|
static SExpr |
sortExpr(Sort sort)
Turn a KeY sort into an SMT sort (by prefixing
SORT_PREFIX . |
public static final java.lang.String SORT_PREFIX
public static final SExpr TRUE
public static final SExpr FALSE
public static final SExpr ZERO
public static SExpr and(java.util.List<SExpr> clauses)
clauses
- non-null list of boolean expressionpublic static SExpr imp(SExpr ante, SExpr cons)
There is some optimisation if there are constants involved.
If the assumption is false, the result is true. If the assumption is true, the result is the conclusion. If the conclusion is true, the result is true. If the conclusion is false, the result is the negation of the assumption.
ante
- a boolean expressioncons
- a boolean expression(=> ante concl)
public static SExpr forall(java.util.List<SExpr> vars, SExpr matrix) throws SMTTranslationException
vars
- a list of variable declarations (var Type)
matrix
- a boolean expressionSMTTranslationException
public static SExpr coerce(SExpr exp, SExpr.Type type) throws SMTTranslationException
exp
- the SExpression to converttype
- the desired typeSMTTranslationException
- if an impossible conversion is attemptedpublic static java.util.List<SExpr> coerce(java.util.List<SExpr> exprs, SExpr.Type type) throws SMTTranslationException
SExpr
s and converts it to a list of the given
type, if possible.exprs
- the list to converttype
- the desired target typeSMTTranslationException
- if an impossible conversion is attemptedpublic static SExpr patternSExpr(SExpr e, SExpr... patterns)
(! e :patterns ((patterns))
.
If the list is empty, then e
is returned.e
- the expression to wrappatterns
- a possibly empty list of expressionspublic static SExpr patternSExpr(SExpr e, java.util.List<SExpr> patterns)
(! e :patterns ((patterns))
.
If the list is empty, then e
is returned.e
- the expression to wrappatterns
- a possibly empty collection of expressionspublic static SExpr sortExpr(Sort sort)
SORT_PREFIX
.sort
- the sort to translate to SMTpublic static SExpr castExpr(SExpr sortExp, SExpr exp) throws SMTTranslationException
sortExp
- the sort as an SExprexp
- the expression to castSMTTranslationException
- if coercion failspublic static SExpr assertion(SExpr assertion) throws SMTTranslationException
assertion
- the SExpr to wrap.SMTTranslationException
- if coercion failspublic static SExpr pullOutPatterns(SExpr matrix)
(and (! (.A.) :pattern ((p1))) (! (.B.) :pattern ((p2))) )yields
(! (and (.A.) (.B:)) :pattern ((p1)(p2)))
matrix
- the SExpr to pull the patterns frompublic static SExpr greaterEqual(SExpr a, SExpr b) throws SMTTranslationException
SMTTranslationException
public static SExpr lessEqual(SExpr a, SExpr b) throws SMTTranslationException
SMTTranslationException
public static SExpr lessThan(SExpr a, SExpr b) throws SMTTranslationException
SMTTranslationException
public static SExpr eq(SExpr a, SExpr b) throws SMTTranslationException
SMTTranslationException
public static SExpr minus(SExpr a, SExpr b) throws SMTTranslationException
SMTTranslationException
public static SExpr plus(SExpr a, SExpr b) throws SMTTranslationException
SMTTranslationException
public static SExpr ite(SExpr cond, SExpr _then, SExpr _else) throws SMTTranslationException
SMTTranslationException
Copyright © 2003-2019 The KeY-Project.