Z3
Lambda.java
Go to the documentation of this file.
1
20package com.microsoft.z3;
21
22import com.microsoft.z3.enumerations.Z3_ast_kind;
23
24public class Lambda extends ArrayExpr
28{
29
33 public int getNumBound()
34 {
35 return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
36 }
37
44 {
45 int n = getNumBound();
46 Symbol[] res = new Symbol[n];
47 for (int i = 0; i < n; i++)
48 res[i] = Symbol.create(getContext(), Native.getQuantifierBoundName(
49 getContext().nCtx(), getNativeObject(), i));
50 return res;
51 }
52
59 {
60 int n = getNumBound();
61 Sort[] res = new Sort[n];
62 for (int i = 0; i < n; i++)
63 res[i] = Sort.create(getContext(), Native.getQuantifierBoundSort(
64 getContext().nCtx(), getNativeObject(), i));
65 return res;
66 }
67
73 public Expr getBody()
74 {
75 return Expr.create(getContext(), Native.getQuantifierBody(getContext()
76 .nCtx(), getNativeObject()));
77 }
78
79
89 {
90 return (Lambda) super.translate(ctx);
91 }
92
93
94 public static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr 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 Lambda of(Context ctx, Expr[] bound, Expr 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}
static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body)
Definition: Lambda.java:94
Sort[] getBoundVariableSorts()
Definition: Lambda.java:58
Lambda translate(Context ctx)
Definition: Lambda.java:88
static Lambda of(Context ctx, Expr[] bound, Expr body)
Definition: Lambda.java:118
Symbol[] getBoundVariableNames()
Definition: Lambda.java:43
static long getQuantifierBody(long a0, long a1)
Definition: Native.java:3431
static long mkLambdaConst(long a0, int a1, long[] a2, long a3)
Definition: Native.java:2621
static long getQuantifierBoundName(long a0, long a1, int a2)
Definition: Native.java:3413
static long getQuantifierBoundSort(long a0, long a1, int a2)
Definition: Native.java:3422
static long mkLambda(long a0, int a1, long[] a2, long[] a3, long a4)
Definition: Native.java:2612
static int getQuantifierNumBound(long a0, long a1)
Definition: Native.java:3404
def Lambda(vs, body)
Definition: z3py.py:2081