Z3 |

Lambda.java
Go to the documentation of this file.
1
20 package com.microsoft.z3;
21
22
26 public 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
42 public Symbol[] getBoundVariableNames()
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
57 public Sort[] getBoundVariableSorts()
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
88 public Lambda<R> translate(Context ctx)
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}
com.microsoft.z3.AST
Definition: AST.java:26
com.microsoft.z3.ArrayExpr
Definition: ArrayExpr.java:25
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:4008
com.microsoft.z3.Expr
Definition: Expr.java:35
com.microsoft.z3.Lambda
Definition: Lambda.java:27
com.microsoft.z3.Lambda.getBody
Expr< R > getBody()
Definition: Lambda.java:73
com.microsoft.z3.Lambda.of
static< R extends Sort > Lambda< R > of(Context ctx, Sort[] sorts, Symbol[] names, Expr< R > body)
Definition: Lambda.java:94
com.microsoft.z3.Lambda.getNumBound
int getNumBound()
Definition: Lambda.java:32
com.microsoft.z3.Lambda.getBoundVariableSorts
Sort[] getBoundVariableSorts()
Definition: Lambda.java:57
com.microsoft.z3.Lambda.translate
Lambda< R > translate(Context ctx)
Definition: Lambda.java:88
com.microsoft.z3.Lambda.getBoundVariableNames
Symbol[] getBoundVariableNames()
Definition: Lambda.java:42
com.microsoft.z3.Lambda.of
static< R extends Sort > Lambda< R > of(Context ctx, Expr<?>[] bound, Expr< R > body)
Definition: Lambda.java:118
com.microsoft.z3.Sort
Definition: Sort.java:27
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:26
com.microsoft.z3.Z3Object.arrayToNative
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
com.microsoft.z3.Z3Object.arrayLength
static int arrayLength(Z3Object[] a)
Definition: Z3Object.java:83