Z3 |

Public Member Functions | Static Public Member Functions
Lambda< R extends Sort > Class Template Reference
Inheritance diagram for Lambda< R extends Sort >:

## 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)

## Detailed Description

Lambda expressions.

Definition at line 26 of file Lambda.java.

## Member Function Documentation

## ◆ getBody()

Expr< R > getBody | ( |  | ) |
| inline

The body of the quantifier.

Exceptions

  Z3Exception |

Definition at line 73 of file Lambda.java.

74 {
75 return (Expr<R>) Expr.create(getContext(), Native.getQuantifierBody(getContext()
76 .nCtx(), getNativeObject()));
77 }

## ◆ getBoundVariableNames()

Symbol[] getBoundVariableNames | ( |  | ) |
| inline

The symbols for the bound variables.

Exceptions

  Z3Exception |

Definition at line 42 of file Lambda.java.

43 {
44 int n = getNumBound();
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));
49 return res;
50 }
com.microsoft.z3.Lambda.getNumBound
int getNumBound()
Definition: Lambda.java:32

## ◆ getBoundVariableSorts()

Sort[] getBoundVariableSorts | ( |  | ) |
| inline

The sorts of the bound variables.

Exceptions

  Z3Exception |

Definition at line 57 of file Lambda.java.

58 {
59 int n = getNumBound();
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));
64 return res;
65 }

## ◆ getNumBound()

int getNumBound | ( |  | ) |
| inline

The number of bound variables.

Definition at line 32 of file Lambda.java.

33 {
34 return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
35 }

Referenced by Lambda< R extends Sort >.getBoundVariableNames(), and Lambda< R extends Sort >.getBoundVariableSorts().

## ◆ of() [1/2]

static< R extends Sort > Lambda< R > of | ( | Context | ctx,
|  | Expr<?>[] | bound,
|  | Expr< R > | body
| ) |  |
| inline static

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.

118 {
119 ctx.checkContextMatch(body);
120
121
122 long nativeObject = Native.mkLambdaConst(ctx.nCtx(),
123 AST.arrayLength(bound), AST.arrayToNative(bound),
124 body.getNativeObject());
125 return new Lambda<>(ctx, nativeObject);
126 }

## ◆ of() [2/2]

static< R extends Sort > Lambda< R > of | ( | Context | ctx,
|  | Sort[] | sorts,
|  | Symbol[] | names,
|  | Expr< R > | body
| ) |  |
| inline static

Definition at line 94 of file Lambda.java.

95 {
96 ctx.checkContextMatch(sorts);
97 ctx.checkContextMatch(names);
98 ctx.checkContextMatch(body);
99
100 if (sorts.length != names.length)
101 throw new Z3Exception("Number of sorts does not match number of names");
102
103
104 long nativeObject = Native.mkLambda(ctx.nCtx(),
105 AST.arrayLength(sorts), AST.arrayToNative(sorts),
106 Symbol.arrayToNative(names),
107 body.getNativeObject());
108
109 return new Lambda<>(ctx, nativeObject);
110 }

## ◆ translate()

Lambda< R > translate | ( | Context | ctx | ) |
| inline

Translates (copies) the quantifier to the Context `ctx`.

Parameters

  ctx | A context

Returns
  A copy of the quantifier which is associated with `ctx`

Exceptions

  Z3Exception | on error

Definition at line 88 of file Lambda.java.

89 {
90 return (Lambda<R>) super.translate(ctx);
91 }

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__().