Z3
Lambda.java
Go to the documentation of this file.
1 
20 package com.microsoft.z3;
21 
23 
24 public 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 
88  public Lambda translate(Context ctx)
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
static long getQuantifierBoundName(long a0, long a1, int a2)
Definition: Native.java:3382
Symbol [] getBoundVariableNames()
Definition: Lambda.java:43
static long mkLambda(long a0, int a1, long[] a2, long[] a3, long a4)
Definition: Native.java:2581
static long getQuantifierBoundSort(long a0, long a1, int a2)
Definition: Native.java:3391
static long getQuantifierBody(long a0, long a1)
Definition: Native.java:3400
def Lambda(vs, body)
Definition: z3py.py:2064
static int getQuantifierNumBound(long a0, long a1)
Definition: Native.java:3373
static Lambda of(Context ctx, Expr[] bound, Expr body)
Definition: Lambda.java:118
Sort [] getBoundVariableSorts()
Definition: Lambda.java:58
Lambda translate(Context ctx)
Definition: Lambda.java:88
static long mkLambdaConst(long a0, int a1, long[] a2, long a3)
Definition: Native.java:2590