20 package com.microsoft.z3;
24 public 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);