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 
65  public int getArity()
66  {
67  return Native.getArity(getContext().nCtx(), getNativeObject());
68  }
69 
74  public int getDomainSize()
75  {
76  return Native.getDomainSize(getContext().nCtx(), getNativeObject());
77  }
78 
82  public Sort[] getDomain()
83  {
84 
85  int n = getDomainSize();
86 
87  Sort[] res = new Sort[n];
88  for (int i = 0; i < n; i++)
89  res[i] = Sort.create(getContext(),
90  Native.getDomain(getContext().nCtx(), getNativeObject(), i));
91  return res;
92  }
93 
97  public Sort getRange()
98  {
99 
100  return Sort.create(getContext(),
101  Native.getRange(getContext().nCtx(), getNativeObject()));
102  }
103 
108  {
109  return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
110  getNativeObject()));
111  }
112 
116  public Symbol getName()
117  {
118 
119  return Symbol.create(getContext(),
120  Native.getDeclName(getContext().nCtx(), getNativeObject()));
121  }
122 
126  public int getNumParameters()
127  {
128  return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject());
129  }
130 
135  {
136 
137  int num = getNumParameters();
138  Parameter[] res = new Parameter[num];
139  for (int i = 0; i < num; i++)
140  {
142  .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
143  switch (k)
144  {
145  case Z3_PARAMETER_INT:
146  res[i] = new Parameter(k, Native.getDeclIntParameter(getContext()
147  .nCtx(), getNativeObject(), i));
148  break;
149  case Z3_PARAMETER_DOUBLE:
150  res[i] = new Parameter(k, Native.getDeclDoubleParameter(
151  getContext().nCtx(), getNativeObject(), i));
152  break;
153  case Z3_PARAMETER_SYMBOL:
154  res[i] = new Parameter(k, Symbol.create(getContext(), Native
155  .getDeclSymbolParameter(getContext().nCtx(),
156  getNativeObject(), i)));
157  break;
158  case Z3_PARAMETER_SORT:
159  res[i] = new Parameter(k, Sort.create(getContext(), Native
160  .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
161  i)));
162  break;
163  case Z3_PARAMETER_AST:
164  res[i] = new Parameter(k, new AST(getContext(),
165  Native.getDeclAstParameter(getContext().nCtx(),
166  getNativeObject(), i)));
167  break;
169  res[i] = new Parameter(k, new FuncDecl(getContext(),
170  Native.getDeclFuncDeclParameter(getContext().nCtx(),
171  getNativeObject(), i)));
172  break;
174  res[i] = new Parameter(k, Native.getDeclRationalParameter(
175  getContext().nCtx(), getNativeObject(), i));
176  break;
177  default:
178  throw new Z3Exception(
179  "Unknown function declaration parameter kind encountered");
180  }
181  }
182  return res;
183  }
184 
188  public class Parameter
189  {
190  private Z3_parameter_kind kind;
191  private int i;
192  private double d;
193  private Symbol sym;
194  private Sort srt;
195  private AST ast;
196  private FuncDecl fd;
197  private String r;
198 
202  public int getInt()
203  {
205  throw new Z3Exception("parameter is not an int");
206  return i;
207  }
208 
212  public double getDouble()
213  {
215  throw new Z3Exception("parameter is not a double ");
216  return d;
217  }
218 
222  public Symbol getSymbol()
223  {
225  throw new Z3Exception("parameter is not a Symbol");
226  return sym;
227  }
228 
232  public Sort getSort()
233  {
235  throw new Z3Exception("parameter is not a Sort");
236  return srt;
237  }
238 
242  public AST getAST()
243  {
245  throw new Z3Exception("parameter is not an AST");
246  return ast;
247  }
248 
253  {
255  throw new Z3Exception("parameter is not a function declaration");
256  return fd;
257  }
258 
263  {
265  throw new Z3Exception("parameter is not a rational String");
266  return r;
267  }
268 
273  {
274  return kind;
275  }
276 
277  Parameter(Z3_parameter_kind k, int i)
278  {
279  this.kind = k;
280  this.i = i;
281  }
282 
283  Parameter(Z3_parameter_kind k, double d)
284  {
285  this.kind = k;
286  this.d = d;
287  }
288 
290  {
291  this.kind = k;
292  this.sym = s;
293  }
294 
296  {
297  this.kind = k;
298  this.srt = s;
299  }
300 
302  {
303  this.kind = k;
304  this.ast = a;
305  }
306 
308  {
309  this.kind = k;
310  this.fd = fd;
311  }
312 
314  {
315  this.kind = k;
316  this.r = r;
317  }
318  }
319 
320  FuncDecl(Context ctx, long obj)
321  {
322  super(ctx, obj);
323 
324  }
325 
326  FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
327 
328  {
329  super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
330  AST.arrayLength(domain), AST.arrayToNative(domain),
331  range.getNativeObject()));
332 
333  }
334 
335  FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range)
336 
337  {
338  super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix,
339  AST.arrayLength(domain), AST.arrayToNative(domain),
340  range.getNativeObject()));
341 
342  }
343 
344  void checkNativeObject(long obj)
345  {
346  if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_FUNC_DECL_AST
347  .toInt())
348  throw new Z3Exception(
349  "Underlying object is not a function declaration");
350  super.checkNativeObject(obj);
351  }
352 
356  public Expr apply(Expr ... args)
357  {
358  getContext().checkContextMatch(args);
359  return Expr.create(getContext(), this, args);
360  }
361 }
static final Z3_decl_kind fromInt(int v)
static long getDeclFuncDeclParameter(long a0, long a1, int a2)
Definition: Native.java:2654
static long mkFuncDecl(long a0, long a1, int a2, long[] a3, long a4)
Definition: Native.java:1034
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:272
static String getDeclRationalParameter(long a0, long a1, int a2)
Definition: Native.java:2663
Expr apply(Expr ... args)
Definition: FuncDecl.java:356
static long getDomain(long a0, long a1, int a2)
Definition: Native.java:2573
static int getDeclNumParameters(long a0, long a1)
Definition: Native.java:2591
static int getDomainSize(long a0, long a1)
Definition: Native.java:2555
boolean equals(Object o)
Definition: FuncDecl.java:33
static String funcDeclToString(long a0, long a1)
Definition: Native.java:3406
static long mkFreshFuncDecl(long a0, String a1, int a2, long[] a3, long a4)
Definition: Native.java:1061
static final Z3_parameter_kind fromInt(int v)
static int getDeclKind(long a0, long a1)
Definition: Native.java:2546
static int getArity(long a0, long a1)
Definition: Native.java:2564
static long getDeclAstParameter(long a0, long a1, int a2)
Definition: Native.java:2645
static int getDeclIntParameter(long a0, long a1, int a2)
Definition: Native.java:2609
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:107
static int getFuncDeclId(long a0, long a1)
Definition: Native.java:2528
static int getAstKind(long a0, long a1)
Definition: Native.java:2762
static boolean isEqFuncDecl(long a0, long a1, long a2)
Definition: Native.java:2519
static double getDeclDoubleParameter(long a0, long a1, int a2)
Definition: Native.java:2618
Parameter [] getParameters()
Definition: FuncDecl.java:134
static long getRange(long a0, long a1)
Definition: Native.java:2582
def String(name, ctx=None)
Definition: z3py.py:9443
static long getDeclName(long a0, long a1)
Definition: Native.java:2537