20package com.microsoft.z3;
22import com.microsoft.z3.enumerations.Z3_ast_kind;
24public class Lambda extends ArrayExpr
47 for (
int i = 0; i < n; i++)
49 getContext().nCtx(), getNativeObject(), i));
62 for (
int i = 0; i < n; i++)
64 getContext().nCtx(), getNativeObject(), i));
76 .nCtx(), getNativeObject()));
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");
105 AST.arrayLength(sorts),
AST.arrayToNative(sorts),
106 Symbol.arrayToNative(names),
107 body.getNativeObject());
109 return new Lambda(ctx, nativeObject);
119 ctx.checkContextMatch(body);
123 AST.arrayLength(bound),
AST.arrayToNative(bound),
124 body.getNativeObject());
125 return new Lambda(ctx, nativeObject);
static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body)
Sort[] getBoundVariableSorts()
Lambda translate(Context ctx)
static Lambda of(Context ctx, Expr[] bound, Expr body)
Symbol[] getBoundVariableNames()
static long getQuantifierBody(long a0, long a1)
static long mkLambdaConst(long a0, int a1, long[] a2, long a3)
static long getQuantifierBoundName(long a0, long a1, int a2)
static long getQuantifierBoundSort(long a0, long a1, int a2)
static long mkLambda(long a0, int a1, long[] a2, long[] a3, long a4)
static int getQuantifierNumBound(long a0, long a1)