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 {
35  /* Overloaded operators are not translated. */
36 
43  /* Overloaded operators are not translated. */
44 
48  public boolean equals(Object o)
49  {
50  FuncDecl casted = (FuncDecl) o;
51  if (casted == null)
52  return false;
53  return this == casted;
54  }
55 
59  public int hashCode()
60  {
61  return super.hashCode();
62  }
63 
67  public String toString()
68  {
69  try
70  {
71  return Native.funcDeclToString(getContext().nCtx(), getNativeObject());
72  } catch (Z3Exception e)
73  {
74  return "Z3Exception: " + e.getMessage();
75  }
76  }
77 
81  public int getId() throws Z3Exception
82  {
83  return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
84  }
85 
89  public int getArity() throws Z3Exception
90  {
91  return Native.getArity(getContext().nCtx(), getNativeObject());
92  }
93 
98  public int getDomainSize() throws Z3Exception
99  {
100  return Native.getDomainSize(getContext().nCtx(), getNativeObject());
101  }
102 
106  public Sort[] getDomain() throws Z3Exception
107  {
108 
109  int n = getDomainSize();
110 
111  Sort[] res = new Sort[n];
112  for (int i = 0; i < n; i++)
113  res[i] = Sort.create(getContext(),
114  Native.getDomain(getContext().nCtx(), getNativeObject(), i));
115  return res;
116  }
117 
121  public Sort getRange() throws Z3Exception
122  {
123 
124  return Sort.create(getContext(),
125  Native.getRange(getContext().nCtx(), getNativeObject()));
126  }
127 
132  {
133  return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
134  getNativeObject()));
135  }
136 
140  public Symbol getName() throws Z3Exception
141  {
142 
143  return Symbol.create(getContext(),
144  Native.getDeclName(getContext().nCtx(), getNativeObject()));
145  }
146 
150  public int getNumParameters() throws Z3Exception
151  {
152  return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject());
153  }
154 
159  {
160 
161  int num = getNumParameters();
162  Parameter[] res = new Parameter[num];
163  for (int i = 0; i < num; i++)
164  {
166  .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
167  switch (k)
168  {
169  case Z3_PARAMETER_INT:
170  res[i] = new Parameter(k, Native.getDeclIntParameter(getContext()
171  .nCtx(), getNativeObject(), i));
172  break;
173  case Z3_PARAMETER_DOUBLE:
174  res[i] = new Parameter(k, Native.getDeclDoubleParameter(
175  getContext().nCtx(), getNativeObject(), i));
176  break;
177  case Z3_PARAMETER_SYMBOL:
178  res[i] = new Parameter(k, Symbol.create(getContext(), Native
179  .getDeclSymbolParameter(getContext().nCtx(),
180  getNativeObject(), i)));
181  break;
182  case Z3_PARAMETER_SORT:
183  res[i] = new Parameter(k, Sort.create(getContext(), Native
184  .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
185  i)));
186  break;
187  case Z3_PARAMETER_AST:
188  res[i] = new Parameter(k, new AST(getContext(),
189  Native.getDeclAstParameter(getContext().nCtx(),
190  getNativeObject(), i)));
191  break;
193  res[i] = new Parameter(k, new FuncDecl(getContext(),
194  Native.getDeclFuncDeclParameter(getContext().nCtx(),
195  getNativeObject(), i)));
196  break;
198  res[i] = new Parameter(k, Native.getDeclRationalParameter(
199  getContext().nCtx(), getNativeObject(), i));
200  break;
201  default:
202  throw new Z3Exception(
203  "Unknown function declaration parameter kind encountered");
204  }
205  }
206  return res;
207  }
208 
212  public class Parameter
213  {
214  private Z3_parameter_kind kind;
215  private int i;
216  private double d;
217  private Symbol sym;
218  private Sort srt;
219  private AST ast;
220  private FuncDecl fd;
221  private String r;
222 
226  public int getInt() throws Z3Exception
227  {
229  throw new Z3Exception("parameter is not an int");
230  return i;
231  }
232 
236  public double getDouble() throws Z3Exception
237  {
239  throw new Z3Exception("parameter is not a double ");
240  return d;
241  }
242 
246  public Symbol getSymbol() throws Z3Exception
247  {
249  throw new Z3Exception("parameter is not a Symbol");
250  return sym;
251  }
252 
256  public Sort getSort() throws Z3Exception
257  {
259  throw new Z3Exception("parameter is not a Sort");
260  return srt;
261  }
262 
266  public AST getAST() throws Z3Exception
267  {
269  throw new Z3Exception("parameter is not an AST");
270  return ast;
271  }
272 
277  {
279  throw new Z3Exception("parameter is not a function declaration");
280  return fd;
281  }
282 
286  public String getRational() throws Z3Exception
287  {
289  throw new Z3Exception("parameter is not a rational String");
290  return r;
291  }
292 
297  {
298  return kind;
299  }
300 
301  Parameter(Z3_parameter_kind k, int i)
302  {
303  this.kind = k;
304  this.i = i;
305  }
306 
307  Parameter(Z3_parameter_kind k, double d)
308  {
309  this.kind = k;
310  this.d = d;
311  }
312 
313  Parameter(Z3_parameter_kind k, Symbol s)
314  {
315  this.kind = k;
316  this.sym = s;
317  }
318 
319  Parameter(Z3_parameter_kind k, Sort s)
320  {
321  this.kind = k;
322  this.srt = s;
323  }
324 
325  Parameter(Z3_parameter_kind k, AST a)
326  {
327  this.kind = k;
328  this.ast = a;
329  }
330 
331  Parameter(Z3_parameter_kind k, FuncDecl fd)
332  {
333  this.kind = k;
334  this.fd = fd;
335  }
336 
337  Parameter(Z3_parameter_kind k, String r)
338  {
339  this.kind = k;
340  this.r = r;
341  }
342  }
343 
344  FuncDecl(Context ctx, long obj) throws Z3Exception
345  {
346  super(ctx, obj);
347 
348  }
349 
350  FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
351  throws Z3Exception
352  {
353  super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
354  AST.arrayLength(domain), AST.arrayToNative(domain),
355  range.getNativeObject()));
356 
357  }
358 
359  FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range)
360  throws Z3Exception
361  {
362  super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix,
363  AST.arrayLength(domain), AST.arrayToNative(domain),
364  range.getNativeObject()));
365 
366  }
367 
368  void checkNativeObject(long obj) throws Z3Exception
369  {
370  if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_FUNC_DECL_AST
371  .toInt())
372  throw new Z3Exception(
373  "Underlying object is not a function declaration");
374  super.checkNativeObject(obj);
375  }
376 
383  public Expr apply(Expr ... args) throws Z3Exception
384  {
385  getContext().checkContextMatch(args);
386  return Expr.create(getContext(), this, args);
387  }
388 }
static final Z3_decl_kind fromInt(int v)
static long getDeclFuncDeclParameter(long a0, long a1, int a2)
Definition: Native.java:2264
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:296
Expr apply(Expr...args)
Definition: FuncDecl.java:383
static String getDeclRationalParameter(long a0, long a1, int a2)
Definition: Native.java:2273
static long getDomain(long a0, long a1, int a2)
Definition: Native.java:2183
static int getDeclNumParameters(long a0, long a1)
Definition: Native.java:2201
static int getDomainSize(long a0, long a1)
Definition: Native.java:2165
boolean equals(Object o)
Definition: FuncDecl.java:48
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
static String funcDeclToString(long a0, long a1)
Definition: Native.java:3016
static final Z3_parameter_kind fromInt(int v)
static int getDeclKind(long a0, long a1)
Definition: Native.java:2156
static int getArity(long a0, long a1)
Definition: Native.java:2174
static long getDeclAstParameter(long a0, long a1, int a2)
Definition: Native.java:2255
static int getDeclIntParameter(long a0, long a1, int a2)
Definition: Native.java:2219
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:171
static int getFuncDeclId(long a0, long a1)
Definition: Native.java:2138
static double getDeclDoubleParameter(long a0, long a1, int a2)
Definition: Native.java:2228
Parameter[] getParameters()
Definition: FuncDecl.java:158
static long getRange(long a0, long a1)
Definition: Native.java:2192
static long getDeclName(long a0, long a1)
Definition: Native.java:2147