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 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()) &&
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
70 {
71 return (FuncDecl) super.translate(ctx);
72 }
73
77 public int getArity()
78 {
79 return Native.getArity(getContext().nCtx(), getNativeObject());
80 }
81
86 public int getDomainSize()
87 {
88 return Native.getDomainSize(getContext().nCtx(), getNativeObject());
89 }
90
94 public Sort[] getDomain()
95 {
96
97 int n = getDomainSize();
98
99 Sort[] res = new Sort[n];
100 for (int i = 0; i < n; i++)
101 res[i] = Sort.create(getContext(),
102 Native.getDomain(getContext().nCtx(), getNativeObject(), i));
103 return res;
104 }
105
109 public Sort getRange()
110 {
111
112 return Sort.create(getContext(),
113 Native.getRange(getContext().nCtx(), getNativeObject()));
114 }
115
120 {
121 return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
122 getNativeObject()));
123 }
124
129 {
130
131 return Symbol.create(getContext(),
132 Native.getDeclName(getContext().nCtx(), getNativeObject()));
133 }
134
138 public int getNumParameters()
139 {
140 return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject());
141 }
142
147 {
148
149 int num = getNumParameters();
150 Parameter[] res = new Parameter[num];
151 for (int i = 0; i < num; i++)
152 {
154 .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
155 switch (k)
156 {
157 case Z3_PARAMETER_INT:
158 res[i] = new Parameter(k, Native.getDeclIntParameter(getContext()
159 .nCtx(), getNativeObject(), i));
160 break;
163 getContext().nCtx(), getNativeObject(), i));
164 break;
166 res[i] = new Parameter(k, Symbol.create(getContext(), Native
167 .getDeclSymbolParameter(getContext().nCtx(),
168 getNativeObject(), i)));
169 break;
171 res[i] = new Parameter(k, Sort.create(getContext(), Native
172 .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
173 i)));
174 break;
175 case Z3_PARAMETER_AST:
176 res[i] = new Parameter(k, new AST(getContext(),
177 Native.getDeclAstParameter(getContext().nCtx(),
178 getNativeObject(), i)));
179 break;
181 res[i] = new Parameter(k, new FuncDecl(getContext(),
182 Native.getDeclFuncDeclParameter(getContext().nCtx(),
183 getNativeObject(), i)));
184 break;
187 getContext().nCtx(), getNativeObject(), i));
188 break;
189 default:
190 throw new Z3Exception(
191 "Unknown function declaration parameter kind encountered");
192 }
193 }
194 return res;
195 }
196
200 public class Parameter
201 {
202 private Z3_parameter_kind kind;
203 private int i;
204 private double d;
205 private Symbol sym;
206 private Sort srt;
207 private AST ast;
208 private FuncDecl fd;
209 private String r;
210
214 public int getInt()
215 {
217 throw new Z3Exception("parameter is not an int");
218 return i;
219 }
220
224 public double getDouble()
225 {
227 throw new Z3Exception("parameter is not a double ");
228 return d;
229 }
230
235 {
237 throw new Z3Exception("parameter is not a Symbol");
238 return sym;
239 }
240
244 public Sort getSort()
245 {
247 throw new Z3Exception("parameter is not a Sort");
248 return srt;
249 }
250
254 public AST getAST()
255 {
257 throw new Z3Exception("parameter is not an AST");
258 return ast;
259 }
260
265 {
267 throw new Z3Exception("parameter is not a function declaration");
268 return fd;
269 }
270
275 {
277 throw new Z3Exception("parameter is not a rational String");
278 return r;
279 }
280
285 {
286 return kind;
287 }
288
290 {
291 this.kind = k;
292 this.i = i;
293 }
294
295 Parameter(Z3_parameter_kind k, double d)
296 {
297 this.kind = k;
298 this.d = d;
299 }
300
301 Parameter(Z3_parameter_kind k, Symbol s)
302 {
303 this.kind = k;
304 this.sym = s;
305 }
306
307 Parameter(Z3_parameter_kind k, Sort s)
308 {
309 this.kind = k;
310 this.srt = s;
311 }
312
313 Parameter(Z3_parameter_kind k, AST a)
314 {
315 this.kind = k;
316 this.ast = a;
317 }
318
319 Parameter(Z3_parameter_kind k, FuncDecl fd)
320 {
321 this.kind = k;
322 this.fd = fd;
323 }
324
325 Parameter(Z3_parameter_kind k, String r)
326 {
327 this.kind = k;
328 this.r = r;
329 }
330 }
331
332 FuncDecl(Context ctx, long obj)
333 {
334 super(ctx, obj);
335
336 }
337
338 FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
339
340 {
341 super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
342 AST.arrayLength(domain), AST.arrayToNative(domain),
343 range.getNativeObject()));
344
345 }
346
347 FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range)
348
349 {
350 super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix,
351 AST.arrayLength(domain), AST.arrayToNative(domain),
352 range.getNativeObject()));
353
354 }
355
356 void checkNativeObject(long obj)
357 {
358 if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_FUNC_DECL_AST
359 .toInt())
360 throw new Z3Exception(
361 "Underlying object is not a function declaration");
362 super.checkNativeObject(obj);
363 }
364
368 public Expr apply(Expr ... args)
369 {
370 getContext().checkContextMatch(args);
371 return Expr.create(getContext(), this, args);
372 }
373}
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:284
boolean equals(Object o)
Definition: FuncDecl.java:33
FuncDecl translate(Context ctx)
Definition: FuncDecl.java:69
Parameter[] getParameters()
Definition: FuncDecl.java:146
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:119
Expr apply(Expr ... args)
Definition: FuncDecl.java:368
static int getDomainSize(long a0, long a1)
Definition: Native.java:2918
static int getDeclIntParameter(long a0, long a1, int a2)
Definition: Native.java:2972
static double getDeclDoubleParameter(long a0, long a1, int a2)
Definition: Native.java:2981
static long getDeclFuncDeclParameter(long a0, long a1, int a2)
Definition: Native.java:3017
static int getFuncDeclId(long a0, long a1)
Definition: Native.java:2891
static boolean isEqFuncDecl(long a0, long a1, long a2)
Definition: Native.java:2882
static long getRange(long a0, long a1)
Definition: Native.java:2945
static int getArity(long a0, long a1)
Definition: Native.java:2927
static long getDeclAstParameter(long a0, long a1, int a2)
Definition: Native.java:3008
static long getDomain(long a0, long a1, int a2)
Definition: Native.java:2936
static String funcDeclToString(long a0, long a1)
Definition: Native.java:3847
static int getDeclKind(long a0, long a1)
Definition: Native.java:2909
static int getDeclNumParameters(long a0, long a1)
Definition: Native.java:2954
static long getDeclName(long a0, long a1)
Definition: Native.java:2900
static String getDeclRationalParameter(long a0, long a1, int a2)
Definition: Native.java:3026
static final Z3_decl_kind fromInt(int v)
static final Z3_parameter_kind fromInt(int v)
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
def String(name, ctx=None)
Definition: z3py.py:10085
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:178
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:134
@ Z3_PARAMETER_INT
Definition: z3_api.h:135
@ Z3_PARAMETER_FUNC_DECL
Definition: z3_api.h:141
@ Z3_PARAMETER_SORT
Definition: z3_api.h:139
@ Z3_PARAMETER_RATIONAL
Definition: z3_api.h:137
@ Z3_PARAMETER_AST
Definition: z3_api.h:140
@ Z3_PARAMETER_DOUBLE
Definition: z3_api.h:136
@ Z3_PARAMETER_SYMBOL
Definition: z3_api.h:138