Z3
FuncDecl.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import com.microsoft.z3.enumerations.Z3_ast_kind;
21import com.microsoft.z3.enumerations.Z3_decl_kind;
22import com.microsoft.z3.enumerations.Z3_parameter_kind;
23
27public class FuncDecl<R extends Sort> extends AST
28{
32 @Override
33 public boolean equals(Object o)
34 {
35 if (o == this) return true;
36 if (!(o instanceof FuncDecl)) return false;
37 FuncDecl<?> other = (FuncDecl<?>) o;
38
39 return
40 (getContext().nCtx() == other.getContext().nCtx()) &&
41 (Native.isEqFuncDecl(
42 getContext().nCtx(),
43 getNativeObject(),
44 other.getNativeObject()));
45 }
46
47 @Override
49 {
50 return Native.funcDeclToString(getContext().nCtx(), getNativeObject());
51 }
52
56 @Override
57 public int getId()
58 {
59 return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
60 }
61
69 @SuppressWarnings("unchecked")
70 public FuncDecl<R> translate(Context ctx)
71 {
72 return (FuncDecl<R>) super.translate(ctx);
73 }
74
78 public int getArity()
79 {
80 return Native.getArity(getContext().nCtx(), getNativeObject());
81 }
82
87 public int getDomainSize()
88 {
89 return Native.getDomainSize(getContext().nCtx(), getNativeObject());
90 }
91
95 public Sort[] getDomain()
96 {
97
98 int n = getDomainSize();
99
100 Sort[] res = new Sort[n];
101 for (int i = 0; i < n; i++)
102 res[i] = Sort.create(getContext(),
103 Native.getDomain(getContext().nCtx(), getNativeObject(), i));
104 return res;
105 }
106
110 @SuppressWarnings("unchecked")
111 public R getRange()
112 {
113 return (R) Sort.create(getContext(),
114 Native.getRange(getContext().nCtx(), getNativeObject()));
115 }
116
121 {
122 return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
123 getNativeObject()));
124 }
125
130 {
131
132 return Symbol.create(getContext(),
133 Native.getDeclName(getContext().nCtx(), getNativeObject()));
134 }
135
139 public int getNumParameters()
140 {
141 return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject());
142 }
143
147 public Parameter[] getParameters()
148 {
149
150 int num = getNumParameters();
151 Parameter[] res = new Parameter[num];
152 for (int i = 0; i < num; i++)
153 {
154 Z3_parameter_kind k = Z3_parameter_kind.fromInt(Native
155 .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
156 switch (k)
157 {
158 case Z3_PARAMETER_INT:
159 res[i] = new Parameter(k, Native.getDeclIntParameter(getContext()
160 .nCtx(), getNativeObject(), i));
161 break;
163 res[i] = new Parameter(k, Native.getDeclDoubleParameter(
164 getContext().nCtx(), getNativeObject(), i));
165 break;
167 res[i] = new Parameter(k, Symbol.create(getContext(), Native
168 .getDeclSymbolParameter(getContext().nCtx(),
169 getNativeObject(), i)));
170 break;
172 res[i] = new Parameter(k, Sort.create(getContext(), Native
173 .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
174 i)));
175 break;
176 case Z3_PARAMETER_AST:
177 res[i] = new Parameter(k, new AST(getContext(),
178 Native.getDeclAstParameter(getContext().nCtx(),
179 getNativeObject(), i)));
180 break;
182 res[i] = new Parameter(k, new FuncDecl<>(getContext(),
183 Native.getDeclFuncDeclParameter(getContext().nCtx(),
184 getNativeObject(), i)));
185 break;
187 res[i] = new Parameter(k, Native.getDeclRationalParameter(
188 getContext().nCtx(), getNativeObject(), i));
189 break;
190 default:
191 throw new Z3Exception(
192 "Unknown function declaration parameter kind encountered");
193 }
194 }
195 return res;
196 }
197
201 public static class Parameter
202 {
203 private Z3_parameter_kind kind;
204 private int i;
205 private double d;
206 private Symbol sym;
207 private Sort srt;
208 private AST ast;
209 private FuncDecl<?> fd;
210 private String r;
211
215 public int getInt()
216 {
217 if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_INT)
218 throw new Z3Exception("parameter is not an int");
219 return i;
220 }
221
225 public double getDouble()
226 {
227 if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_DOUBLE)
228 throw new Z3Exception("parameter is not a double ");
229 return d;
230 }
231
235 public Symbol getSymbol()
236 {
237 if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SYMBOL)
238 throw new Z3Exception("parameter is not a Symbol");
239 return sym;
240 }
241
245 public Sort getSort()
246 {
247 if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SORT)
248 throw new Z3Exception("parameter is not a Sort");
249 return srt;
250 }
251
255 public AST getAST()
256 {
257 if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_AST)
258 throw new Z3Exception("parameter is not an AST");
259 return ast;
260 }
261
265 public FuncDecl<?> getFuncDecl()
266 {
267 if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL)
268 throw new Z3Exception("parameter is not a function declaration");
269 return fd;
270 }
271
275 public String getRational()
276 {
277 if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_RATIONAL)
278 throw new Z3Exception("parameter is not a rational String");
279 return r;
280 }
281
285 public Z3_parameter_kind getParameterKind()
286 {
287 return kind;
288 }
289
290 Parameter(Z3_parameter_kind k, int i)
291 {
292 this.kind = k;
293 this.i = i;
294 }
295
296 Parameter(Z3_parameter_kind k, double d)
297 {
298 this.kind = k;
299 this.d = d;
300 }
301
302 Parameter(Z3_parameter_kind k, Symbol s)
303 {
304 this.kind = k;
305 this.sym = s;
306 }
307
308 Parameter(Z3_parameter_kind k, Sort s)
309 {
310 this.kind = k;
311 this.srt = s;
312 }
313
314 Parameter(Z3_parameter_kind k, AST a)
315 {
316 this.kind = k;
317 this.ast = a;
318 }
319
320 Parameter(Z3_parameter_kind k, FuncDecl<?> fd)
321 {
322 this.kind = k;
323 this.fd = fd;
324 }
325
326 Parameter(Z3_parameter_kind k, String r)
327 {
328 this.kind = k;
329 this.r = r;
330 }
331 }
332
333 FuncDecl(Context ctx, long obj)
334 {
335 super(ctx, obj);
336
337 }
338
339 FuncDecl(Context ctx, Symbol name, Sort[] domain, R range)
340 {
341 super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
342 AST.arrayLength(domain), AST.arrayToNative(domain),
343 range.getNativeObject()));
344 }
345
346 FuncDecl(Context ctx, Symbol name, Sort[] domain, R range, boolean is_rec)
347 {
348 super(ctx, Native.mkRecFuncDecl(ctx.nCtx(), name.getNativeObject(),
349 AST.arrayLength(domain), AST.arrayToNative(domain),
350 range.getNativeObject()));
351
352 }
353
354 FuncDecl(Context ctx, String prefix, Sort[] domain, R range)
355 {
356 super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix,
357 AST.arrayLength(domain), AST.arrayToNative(domain),
358 range.getNativeObject()));
359
360 }
361
362 void checkNativeObject(long obj)
363 {
364 if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_FUNC_DECL_AST
365 .toInt())
366 throw new Z3Exception(
367 "Underlying object is not a function declaration");
368 super.checkNativeObject(obj);
369 }
370
374 public Expr<R> apply(Expr<?> ... args)
375 {
376 getContext().checkContextMatch(args);
377 return Expr.create(getContext(), this, args);
378 }
379}
Expr< R > apply(Expr<?> ... args)
Definition: FuncDecl.java:374
boolean equals(Object o)
Definition: FuncDecl.java:33
Parameter[] getParameters()
Definition: FuncDecl.java:147
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:120
FuncDecl< R > translate(Context ctx)
Definition: FuncDecl.java:70
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
def String(name, ctx=None)
Definition: z3py.py:10693
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1000
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:136
@ Z3_PARAMETER_INT
Definition: z3_api.h:137
@ Z3_PARAMETER_FUNC_DECL
Definition: z3_api.h:143
@ Z3_PARAMETER_SORT
Definition: z3_api.h:141
@ Z3_PARAMETER_RATIONAL
Definition: z3_api.h:139
@ Z3_PARAMETER_AST
Definition: z3_api.h:142
@ Z3_PARAMETER_DOUBLE
Definition: z3_api.h:138
@ Z3_PARAMETER_SYMBOL
Definition: z3_api.h:140