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  @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
48  public String toString()
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 
128  public Symbol getName()
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;
161  case Z3_PARAMETER_DOUBLE:
162  res[i] = new Parameter(k, Native.getDeclDoubleParameter(
163  getContext().nCtx(), getNativeObject(), i));
164  break;
165  case Z3_PARAMETER_SYMBOL:
166  res[i] = new Parameter(k, Symbol.create(getContext(), Native
167  .getDeclSymbolParameter(getContext().nCtx(),
168  getNativeObject(), i)));
169  break;
170  case Z3_PARAMETER_SORT:
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;
186  res[i] = new Parameter(k, Native.getDeclRationalParameter(
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 
234  public Symbol getSymbol()
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 
289  Parameter(Z3_parameter_kind k, int i)
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 }
static final Z3_decl_kind fromInt(int v)
static long getDeclFuncDeclParameter(long a0, long a1, int a2)
Definition: Native.java:2823
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:284
static String getDeclRationalParameter(long a0, long a1, int a2)
Definition: Native.java:2832
Expr apply(Expr ... args)
Definition: FuncDecl.java:368
static long getDomain(long a0, long a1, int a2)
Definition: Native.java:2742
static int getDeclNumParameters(long a0, long a1)
Definition: Native.java:2760
static int getDomainSize(long a0, long a1)
Definition: Native.java:2724
boolean equals(Object o)
Definition: FuncDecl.java:33
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:184
static String funcDeclToString(long a0, long a1)
Definition: Native.java:3617
static final Z3_parameter_kind fromInt(int v)
static int getDeclKind(long a0, long a1)
Definition: Native.java:2715
static int getArity(long a0, long a1)
Definition: Native.java:2733
static long getDeclAstParameter(long a0, long a1, int a2)
Definition: Native.java:2814
static int getDeclIntParameter(long a0, long a1, int a2)
Definition: Native.java:2778
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:119
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:140
static int getFuncDeclId(long a0, long a1)
Definition: Native.java:2697
static boolean isEqFuncDecl(long a0, long a1, long a2)
Definition: Native.java:2688
static double getDeclDoubleParameter(long a0, long a1, int a2)
Definition: Native.java:2787
FuncDecl translate(Context ctx)
Definition: FuncDecl.java:69
Parameter [] getParameters()
Definition: FuncDecl.java:146
static long getRange(long a0, long a1)
Definition: Native.java:2751
def String(name, ctx=None)
Definition: z3py.py:9738
static long getDeclName(long a0, long a1)
Definition: Native.java:2706