Lambda expressions.
Definition at line 26 of file Lambda.java.
◆ getBody()
The body of the quantifier.
- Exceptions
-
Definition at line 73 of file Lambda.java.
75 return (Expr<R>) Expr.create(getContext(), Native.getQuantifierBody(getContext()
76 .nCtx(), getNativeObject()));
◆ getBoundVariableNames()
Symbol [] getBoundVariableNames |
( |
| ) |
|
|
inline |
The symbols for the bound variables.
- Exceptions
-
Definition at line 42 of file Lambda.java.
45 Symbol[] res =
new Symbol[n];
46 for (
int i = 0; i < n; i++)
47 res[i] = Symbol.create(getContext(), Native.getQuantifierBoundName(
48 getContext().nCtx(), getNativeObject(), i));
◆ getBoundVariableSorts()
Sort [] getBoundVariableSorts |
( |
| ) |
|
|
inline |
The sorts of the bound variables.
- Exceptions
-
Definition at line 57 of file Lambda.java.
60 Sort[] res =
new Sort[n];
61 for (
int i = 0; i < n; i++)
62 res[i] = Sort.create(getContext(), Native.getQuantifierBoundSort(
63 getContext().nCtx(), getNativeObject(), i));
◆ getNumBound()
◆ of() [1/2]
- Parameters
-
ctx | Context to create the lambda on. |
bound | Bound variables. |
body | Body of the lambda expression. |
Definition at line 118 of file Lambda.java.
119 ctx.checkContextMatch(body);
122 long nativeObject = Native.mkLambdaConst(ctx.nCtx(),
123 AST.arrayLength(bound), AST.arrayToNative(bound),
124 body.getNativeObject());
125 return new Lambda<>(ctx, nativeObject);
◆ of() [2/2]
Definition at line 94 of file Lambda.java.
96 ctx.checkContextMatch(sorts);
97 ctx.checkContextMatch(names);
98 ctx.checkContextMatch(body);
100 if (sorts.length != names.length)
101 throw new Z3Exception(
"Number of sorts does not match number of names");
104 long nativeObject = Native.mkLambda(ctx.nCtx(),
105 AST.arrayLength(sorts), AST.arrayToNative(sorts),
106 Symbol.arrayToNative(names),
107 body.getNativeObject());
109 return new Lambda<>(ctx, nativeObject);
◆ translate()
Translates (copies) the quantifier to the Context
.
- Parameters
-
- Returns
- A copy of the quantifier which is associated with
- Exceptions
-
Definition at line 88 of file Lambda.java.
90 return (Lambda<R>) super.translate(ctx);
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__().