Z3
Lambda.java
Go to the documentation of this file.
1
20package com.microsoft.z3;
21
22
26public class Lambda<R extends Sort> extends ArrayExpr<Sort, R>
27{
28
32 public int getNumBound()
33 {
34 return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
35 }
36
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 }
51
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 }
66
72 @SuppressWarnings("unchecked")
73 public Expr<R> getBody()
74 {
75 return (Expr<R>) Expr.create(getContext(), Native.getQuantifierBody(getContext()
76 .nCtx(), getNativeObject()));
77 }
78
79
89 {
90 return (Lambda<R>) super.translate(ctx);
91 }
92
93
94 public static <R extends Sort> Lambda<R> of(Context ctx, Sort[] sorts, Symbol[] names, Expr<R> body)
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 }
111
118 public static <R extends Sort> Lambda<R> of(Context ctx, Expr<?>[] bound, Expr<R> body) {
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 }
127
128
129 private Lambda(Context ctx, long obj)
130 {
131 super(ctx, obj);
132 }
133
134}
Expr< R > getBody()
Definition: Lambda.java:73
static< R extends Sort > Lambda< R > of(Context ctx, Sort[] sorts, Symbol[] names, Expr< R > body)
Definition: Lambda.java:94
Sort[] getBoundVariableSorts()
Definition: Lambda.java:57
Lambda< R > translate(Context ctx)
Definition: Lambda.java:88
Symbol[] getBoundVariableNames()
Definition: Lambda.java:42
static< R extends Sort > Lambda< R > of(Context ctx, Expr<?>[] bound, Expr< R > body)
Definition: Lambda.java:118
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
static int arrayLength(Z3Object[] a)
Definition: Z3Object.java:83