Public Member Functions | |
int | getNumBound () |
Symbol[] | getBoundVariableNames () |
Sort[] | getBoundVariableSorts () |
Expr< R > | getBody () |
Lambda< R > | translate (Context ctx) |
Static Public Member Functions | |
static< R extends Sort > Lambda< R > | of (Context ctx, Sort[] sorts, Symbol[] names, Expr< R > body) |
static< R extends Sort > Lambda< R > | of (Context ctx, Expr<?>[] bound, Expr< R > body) |
Lambda expressions.
Definition at line 26 of file Lambda.java.
|
inline |
The body of the quantifier.
Z3Exception |
Definition at line 73 of file Lambda.java.
|
inline |
The symbols for the bound variables.
Z3Exception |
Definition at line 42 of file Lambda.java.
|
inline |
The sorts of the bound variables.
Z3Exception |
Definition at line 57 of file Lambda.java.
|
inline |
The number of bound variables.
Definition at line 32 of file Lambda.java.
Referenced by Lambda< R extends Sort >.getBoundVariableNames(), and Lambda< R extends Sort >.getBoundVariableSorts().
|
inlinestatic |
ctx | Context to create the lambda on. |
bound | Bound variables. |
body | Body of the lambda expression. |
Definition at line 118 of file Lambda.java.
|
inlinestatic |
Definition at line 94 of file Lambda.java.
Translates (copies) the quantifier to the Context ctx
.
ctx | A context |
ctx
Z3Exception | on error |
Definition at line 88 of file Lambda.java.
Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().