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 }
com.microsoft.z3.Lambda.getBody
Expr getBody()
Definition: Lambda.java:73
com.microsoft.z3.enumerations
Definition: Z3_ast_kind.java:5
com.microsoft.z3.Sort
Definition: Sort.java:26
com.microsoft.z3.Native.getQuantifierBoundSort
static long getQuantifierBoundSort(long a0, long a1, int a2)
Definition: Native.java:3422
com.microsoft
com.microsoft.z3.Lambda.translate
Lambda translate(Context ctx)
Definition: Lambda.java:88
com.microsoft.z3.Native.getQuantifierBody
static long getQuantifierBody(long a0, long a1)
Definition: Native.java:3431
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.Native.getQuantifierNumBound
static int getQuantifierNumBound(long a0, long a1)
Definition: Native.java:3404
com.microsoft.z3.Lambda.of
static Lambda of(Context ctx, Expr[] bound, Expr body)
Definition: Lambda.java:118
com.microsoft.z3.Native
Definition: Native.java:4
z3py.Lambda
def Lambda(vs, body)
Definition: z3py.py:2081
com.microsoft.z3.Lambda.of
static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body)
Definition: Lambda.java:94
com.microsoft.z3
Definition: AlgebraicNum.java:18
com.microsoft.z3.Native.mkLambdaConst
static long mkLambdaConst(long a0, int a1, long[] a2, long a3)
Definition: Native.java:2621
com.microsoft.z3.enumerations.Z3_ast_kind
Definition: Z3_ast_kind.java:13
com.microsoft.z3.Lambda
Definition: Lambda.java:27
com.microsoft.z3.Native.mkLambda
static long mkLambda(long a0, int a1, long[] a2, long[] a3, long a4)
Definition: Native.java:2612
com.microsoft.z3.Expr
Definition: Expr.java:30
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:25
com.microsoft.z3.AST
Definition: AST.java:25
com.microsoft.z3.Lambda.getNumBound
int getNumBound()
Definition: Lambda.java:33
com.microsoft.z3.Lambda.getBoundVariableSorts
Sort[] getBoundVariableSorts()
Definition: Lambda.java:58
com.microsoft.z3.Lambda.getBoundVariableNames
Symbol[] getBoundVariableNames()
Definition: Lambda.java:43
com
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.Native.getQuantifierBoundName
static long getQuantifierBoundName(long a0, long a1, int a2)
Definition: Native.java:3413