20package com.microsoft.z3;
34 return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
46 for (
int i = 0; i < n; i++)
47 res[i] =
Symbol.create(getContext(), Native.getQuantifierBoundName(
48 getContext().nCtx(), getNativeObject(), i));
61 for (
int i = 0; i < n; i++)
62 res[i] =
Sort.create(getContext(), Native.getQuantifierBoundSort(
63 getContext().nCtx(), getNativeObject(), i));
72 @SuppressWarnings(
"unchecked")
75 return (
Expr<R>)
Expr.create(getContext(), Native.getQuantifierBody(getContext()
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");
104 long nativeObject = Native.mkLambda(ctx.
nCtx(),
107 body.getNativeObject());
109 return new Lambda<>(ctx, nativeObject);
119 ctx.checkContextMatch(body);
122 long nativeObject = Native.mkLambdaConst(ctx.
nCtx(),
124 body.getNativeObject());
125 return new Lambda<>(ctx, nativeObject);
static< R extends Sort > Lambda< R > of(Context ctx, Sort[] sorts, Symbol[] names, Expr< R > body)
Sort[] getBoundVariableSorts()
Lambda< R > translate(Context ctx)
Symbol[] getBoundVariableNames()
static< R extends Sort > Lambda< R > of(Context ctx, Expr<?>[] bound, Expr< R > body)
static long[] arrayToNative(Z3Object[] a)
static int arrayLength(Z3Object[] a)