Z3
FuncDecl.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 
27 public class FuncDecl extends AST
28 {
32  public boolean equals(Object o)
33  {
34  FuncDecl casted = null;
35 
36  try {
37  casted = FuncDecl.class.cast(o);
38  } catch (ClassCastException e) {
39  return false;
40  }
41 
42  return
43  (this == casted) ||
44  (this != null) &&
45  (casted != null) &&
46  (getContext().nCtx() == casted.getContext().nCtx()) &&
47  (Native.isEqFuncDecl(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
48  }
49 
53  public int hashCode()
54  {
55  return super.hashCode();
56  }
57 
61  public String toString()
62  {
63  try
64  {
65  return Native.funcDeclToString(getContext().nCtx(), getNativeObject());
66  } catch (Z3Exception e)
67  {
68  return "Z3Exception: " + e.getMessage();
69  }
70  }
71 
75  public int getId()
76  {
77  return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
78  }
79 
83  public int getArity()
84  {
85  return Native.getArity(getContext().nCtx(), getNativeObject());
86  }
87 
92  public int getDomainSize()
93  {
94  return Native.getDomainSize(getContext().nCtx(), getNativeObject());
95  }
96 
100  public Sort[] getDomain()
101  {
102 
103  int n = getDomainSize();
104 
105  Sort[] res = new Sort[n];
106  for (int i = 0; i < n; i++)
107  res[i] = Sort.create(getContext(),
108  Native.getDomain(getContext().nCtx(), getNativeObject(), i));
109  return res;
110  }
111 
115  public Sort getRange()
116  {
117 
118  return Sort.create(getContext(),
119  Native.getRange(getContext().nCtx(), getNativeObject()));
120  }
121 
126  {
127  return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
128  getNativeObject()));
129  }
130 
134  public Symbol getName()
135  {
136 
137  return Symbol.create(getContext(),
138  Native.getDeclName(getContext().nCtx(), getNativeObject()));
139  }
140 
144  public int getNumParameters()
145  {
146  return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject());
147  }
148 
153  {
154 
155  int num = getNumParameters();
156  Parameter[] res = new Parameter[num];
157  for (int i = 0; i < num; i++)
158  {
160  .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
161  switch (k)
162  {
163  case Z3_PARAMETER_INT:
164  res[i] = new Parameter(k, Native.getDeclIntParameter(getContext()
165  .nCtx(), getNativeObject(), i));
166  break;
167  case Z3_PARAMETER_DOUBLE:
168  res[i] = new Parameter(k, Native.getDeclDoubleParameter(
169  getContext().nCtx(), getNativeObject(), i));
170  break;
171  case Z3_PARAMETER_SYMBOL:
172  res[i] = new Parameter(k, Symbol.create(getContext(), Native
173  .getDeclSymbolParameter(getContext().nCtx(),
174  getNativeObject(), i)));
175  break;
176  case Z3_PARAMETER_SORT:
177  res[i] = new Parameter(k, Sort.create(getContext(), Native
178  .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
179  i)));
180  break;
181  case Z3_PARAMETER_AST:
182  res[i] = new Parameter(k, new AST(getContext(),
183  Native.getDeclAstParameter(getContext().nCtx(),
184  getNativeObject(), i)));
185  break;
187  res[i] = new Parameter(k, new FuncDecl(getContext(),
188  Native.getDeclFuncDeclParameter(getContext().nCtx(),
189  getNativeObject(), i)));
190  break;
192  res[i] = new Parameter(k, Native.getDeclRationalParameter(
193  getContext().nCtx(), getNativeObject(), i));
194  break;
195  default:
196  throw new Z3Exception(
197  "Unknown function declaration parameter kind encountered");
198  }
199  }
200  return res;
201  }
202 
206  public class Parameter
207  {
208  private Z3_parameter_kind kind;
209  private int i;
210  private double d;
211  private Symbol sym;
212  private Sort srt;
213  private AST ast;
214  private FuncDecl fd;
215  private String r;
216 
220  public int getInt()
221  {
223  throw new Z3Exception("parameter is not an int");
224  return i;
225  }
226 
230  public double getDouble()
231  {
233  throw new Z3Exception("parameter is not a double ");
234  return d;
235  }
236 
240  public Symbol getSymbol()
241  {
243  throw new Z3Exception("parameter is not a Symbol");
244  return sym;
245  }
246 
250  public Sort getSort()
251  {
253  throw new Z3Exception("parameter is not a Sort");
254  return srt;
255  }
256 
260  public AST getAST()
261  {
263  throw new Z3Exception("parameter is not an AST");
264  return ast;
265  }
266 
271  {
273  throw new Z3Exception("parameter is not a function declaration");
274  return fd;
275  }
276 
280  public String getRational()
281  {
283  throw new Z3Exception("parameter is not a rational String");
284  return r;
285  }
286 
291  {
292  return kind;
293  }
294 
295  Parameter(Z3_parameter_kind k, int i)
296  {
297  this.kind = k;
298  this.i = i;
299  }
300 
301  Parameter(Z3_parameter_kind k, double d)
302  {
303  this.kind = k;
304  this.d = d;
305  }
306 
308  {
309  this.kind = k;
310  this.sym = s;
311  }
312 
314  {
315  this.kind = k;
316  this.srt = s;
317  }
318 
320  {
321  this.kind = k;
322  this.ast = a;
323  }
324 
326  {
327  this.kind = k;
328  this.fd = fd;
329  }
330 
331  Parameter(Z3_parameter_kind k, String r)
332  {
333  this.kind = k;
334  this.r = r;
335  }
336  }
337 
338  FuncDecl(Context ctx, long obj)
339  {
340  super(ctx, obj);
341 
342  }
343 
344  FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
345 
346  {
347  super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
348  AST.arrayLength(domain), AST.arrayToNative(domain),
349  range.getNativeObject()));
350 
351  }
352 
353  FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range)
354 
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 
377  public Expr apply(Expr ... args)
378  {
379  getContext().checkContextMatch(args);
380  return Expr.create(getContext(), this, args);
381  }
382 }
static final Z3_decl_kind fromInt(int v)
static long getDeclFuncDeclParameter(long a0, long a1, int a2)
Definition: Native.java:2387
static long mkFuncDecl(long a0, long a1, int a2, long[] a3, long a4)
Definition: Native.java:1028
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:290
Expr apply(Expr...args)
Definition: FuncDecl.java:377
static String getDeclRationalParameter(long a0, long a1, int a2)
Definition: Native.java:2396
static long getDomain(long a0, long a1, int a2)
Definition: Native.java:2306
static int getDeclNumParameters(long a0, long a1)
Definition: Native.java:2324
static int getDomainSize(long a0, long a1)
Definition: Native.java:2288
boolean equals(Object o)
Definition: FuncDecl.java:32
static String funcDeclToString(long a0, long a1)
Definition: Native.java:3139
static long mkFreshFuncDecl(long a0, String a1, int a2, long[] a3, long a4)
Definition: Native.java:1055
static final Z3_parameter_kind fromInt(int v)
static int getDeclKind(long a0, long a1)
Definition: Native.java:2279
static int getArity(long a0, long a1)
Definition: Native.java:2297
static long getDeclAstParameter(long a0, long a1, int a2)
Definition: Native.java:2378
static int getDeclIntParameter(long a0, long a1, int a2)
Definition: Native.java:2342
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:125
static int getFuncDeclId(long a0, long a1)
Definition: Native.java:2261
static int getAstKind(long a0, long a1)
Definition: Native.java:2495
static boolean isEqFuncDecl(long a0, long a1, long a2)
Definition: Native.java:2252
static double getDeclDoubleParameter(long a0, long a1, int a2)
Definition: Native.java:2351
Parameter[] getParameters()
Definition: FuncDecl.java:152
static long getRange(long a0, long a1)
Definition: Native.java:2315
static long getDeclName(long a0, long a1)
Definition: Native.java:2270