Z3
AST.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
25 public class AST extends Z3Object
26 {
27  /* Overloaded operators are not translated. */
28 
34  public boolean equals(Object o)
35  {
36  AST casted = null;
37 
38  try
39  {
40  casted = AST.class.cast(o);
41  } catch (ClassCastException e)
42  {
43  return false;
44  }
45 
46  return this.getNativeObject() == casted.getNativeObject();
47  }
48 
57  public int compareTo(Object other)
58  {
59  if (other == null)
60  return 1;
61 
62  AST oAST = null;
63  try
64  {
65  oAST = AST.class.cast(other);
66  } catch (ClassCastException e)
67  {
68  return 1;
69  }
70 
71  if (getId() < oAST.getId())
72  return -1;
73  else if (getId() > oAST.getId())
74  return +1;
75  else
76  return 0;
77  }
78 
84  public int hashCode()
85  {
86  int r = 0;
87  try {
88  Native.getAstHash(getContext().nCtx(), getNativeObject());
89  }
90  catch (Z3Exception ex) {}
91  return r;
92  }
93 
98  public int getId()
99  {
100  return Native.getAstId(getContext().nCtx(), getNativeObject());
101  }
102 
110  public AST translate(Context ctx)
111  {
112 
113  if (getContext() == ctx)
114  return this;
115  else
116  return new AST(ctx, Native.translate(getContext().nCtx(),
117  getNativeObject(), ctx.nCtx()));
118  }
119 
125  {
126  return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(),
127  getNativeObject()));
128  }
129 
135  public boolean isExpr()
136  {
137  switch (getASTKind())
138  {
139  case Z3_APP_AST:
140  case Z3_NUMERAL_AST:
141  case Z3_QUANTIFIER_AST:
142  case Z3_VAR_AST:
143  return true;
144  default:
145  return false;
146  }
147  }
148 
154  public boolean isApp()
155  {
156  return this.getASTKind() == Z3_ast_kind.Z3_APP_AST;
157  }
158 
164  public boolean isVar()
165  {
166  return this.getASTKind() == Z3_ast_kind.Z3_VAR_AST;
167  }
168 
174  public boolean isQuantifier()
175  {
176  return this.getASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST;
177  }
178 
182  public boolean isSort()
183  {
184  return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST;
185  }
186 
190  public boolean isFuncDecl()
191  {
192  return this.getASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST;
193  }
194 
198  public String toString()
199  {
200  try
201  {
202  return Native.astToString(getContext().nCtx(), getNativeObject());
203  } catch (Z3Exception e)
204  {
205  return "Z3Exception: " + e.getMessage();
206  }
207  }
208 
212  public String getSExpr()
213  {
214  return Native.astToString(getContext().nCtx(), getNativeObject());
215  }
216 
217  AST(Context ctx)
218  {
219  super(ctx);
220  }
221 
222  AST(Context ctx, long obj)
223  {
224  super(ctx, obj);
225  }
226 
227  void incRef(long o)
228  {
229  // Console.WriteLine("AST IncRef()");
230  if (getContext() == null || o == 0)
231  return;
232  getContext().getASTDRQ().incAndClear(getContext(), o);
233  super.incRef(o);
234  }
235 
236  void decRef(long o)
237  {
238  // Console.WriteLine("AST DecRef()");
239  if (getContext() == null || o == 0)
240  return;
241  getContext().getASTDRQ().add(o);
242  super.decRef(o);
243  }
244 
245  static AST create(Context ctx, long obj)
246  {
247  switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
248  {
249  case Z3_FUNC_DECL_AST:
250  return new FuncDecl(ctx, obj);
251  case Z3_QUANTIFIER_AST:
252  return new Quantifier(ctx, obj);
253  case Z3_SORT_AST:
254  return Sort.create(ctx, obj);
255  case Z3_APP_AST:
256  case Z3_NUMERAL_AST:
257  case Z3_VAR_AST:
258  return Expr.create(ctx, obj);
259  default:
260  throw new Z3Exception("Unknown AST kind");
261  }
262  }
263 }
String toString()
Definition: AST.java:198
String getSExpr()
Definition: AST.java:212
boolean isApp()
Definition: AST.java:154
boolean isSort()
Definition: AST.java:182
boolean isQuantifier()
Definition: AST.java:174
boolean equals(Object o)
Definition: AST.java:34
static final Z3_ast_kind fromInt(int v)
boolean isFuncDecl()
Definition: AST.java:190
static int getAstId(long a0, long a1)
Definition: Native.java:2396
Z3_ast_kind getASTKind()
Definition: AST.java:124
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:214
boolean isVar()
Definition: AST.java:164
boolean isExpr()
Definition: AST.java:135
void incAndClear(Context ctx, long o)
AST translate(Context ctx)
Definition: AST.java:110
static int getAstHash(long a0, long a1)
Definition: Native.java:2405
static int getAstKind(long a0, long a1)
Definition: Native.java:2441
IDecRefQueue getASTDRQ()
Definition: Context.java:3665
static String astToString(long a0, long a1)
Definition: Native.java:3058
static long translate(long a0, long a1, long a2)
Definition: Native.java:2792
int compareTo(Object other)
Definition: AST.java:57