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 
33  public boolean equals(Object o)
34  {
35  AST casted = null;
36 
37  try
38  {
39  casted = AST.class.cast(o);
40  } catch (ClassCastException e)
41  {
42  return false;
43  }
44 
45  return this.getNativeObject() == casted.getNativeObject();
46  }
47 
54  public int compareTo(Object other) throws Z3Exception
55  {
56  if (other == null)
57  return 1;
58 
59  AST oAST = null;
60  try
61  {
62  oAST = AST.class.cast(other);
63  } catch (ClassCastException e)
64  {
65  return 1;
66  }
67 
68  if (getId() < oAST.getId())
69  return -1;
70  else if (getId() > oAST.getId())
71  return +1;
72  else
73  return 0;
74  }
75 
81  public int hashCode()
82  {
83  int r = 0;
84  try {
85  Native.getAstHash(getContext().nCtx(), getNativeObject());
86  }
87  catch (Z3Exception ex) {}
88  return r;
89  }
90 
94  public int getId() throws Z3Exception
95  {
96  return Native.getAstId(getContext().nCtx(), getNativeObject());
97  }
98 
105  public AST translate(Context ctx) throws Z3Exception
106  {
107 
108  if (getContext() == ctx)
109  return this;
110  else
111  return new AST(ctx, Native.translate(getContext().nCtx(),
112  getNativeObject(), ctx.nCtx()));
113  }
114 
119  {
120  return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(),
121  getNativeObject()));
122  }
123 
127  public boolean isExpr() throws Z3Exception
128  {
129  switch (getASTKind())
130  {
131  case Z3_APP_AST:
132  case Z3_NUMERAL_AST:
133  case Z3_QUANTIFIER_AST:
134  case Z3_VAR_AST:
135  return true;
136  default:
137  return false;
138  }
139  }
140 
144  public boolean isApp() throws Z3Exception
145  {
146  return this.getASTKind() == Z3_ast_kind.Z3_APP_AST;
147  }
148 
152  public boolean isVar() throws Z3Exception
153  {
154  return this.getASTKind() == Z3_ast_kind.Z3_VAR_AST;
155  }
156 
160  public boolean isQuantifier() throws Z3Exception
161  {
162  return this.getASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST;
163  }
164 
168  public boolean isSort() throws Z3Exception
169  {
170  return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST;
171  }
172 
176  public boolean isFuncDecl() throws Z3Exception
177  {
178  return this.getASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST;
179  }
180 
184  public String toString()
185  {
186  try
187  {
188  return Native.astToString(getContext().nCtx(), getNativeObject());
189  } catch (Z3Exception e)
190  {
191  return "Z3Exception: " + e.getMessage();
192  }
193  }
194 
198  public String getSExpr() throws Z3Exception
199  {
200  return Native.astToString(getContext().nCtx(), getNativeObject());
201  }
202 
203  AST(Context ctx)
204  {
205  super(ctx);
206  }
207 
208  AST(Context ctx, long obj) throws Z3Exception
209  {
210  super(ctx, obj);
211  }
212 
213  void incRef(long o) throws Z3Exception
214  {
215  // Console.WriteLine("AST IncRef()");
216  if (getContext() == null)
217  throw new Z3Exception("inc() called on null context");
218  if (o == 0)
219  throw new Z3Exception("inc() called on null AST");
220  getContext().ast_DRQ().incAndClear(getContext(), o);
221  super.incRef(o);
222  }
223 
224  void decRef(long o) throws Z3Exception
225  {
226  // Console.WriteLine("AST DecRef()");
227  if (getContext() == null)
228  throw new Z3Exception("dec() called on null context");
229  if (o == 0)
230  throw new Z3Exception("dec() called on null AST");
231  getContext().ast_DRQ().add(o);
232  super.decRef(o);
233  }
234 
235  static AST create(Context ctx, long obj) throws Z3Exception
236  {
237  switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
238  {
239  case Z3_FUNC_DECL_AST:
240  return new FuncDecl(ctx, obj);
241  case Z3_QUANTIFIER_AST:
242  return new Quantifier(ctx, obj);
243  case Z3_SORT_AST:
244  return Sort.create(ctx, obj);
245  case Z3_APP_AST:
246  case Z3_NUMERAL_AST:
247  case Z3_VAR_AST:
248  return Expr.create(ctx, obj);
249  default:
250  throw new Z3Exception("Unknown AST kind");
251  }
252  }
253 }
String toString()
Definition: AST.java:184
String getSExpr()
Definition: AST.java:198
boolean isApp()
Definition: AST.java:144
boolean isSort()
Definition: AST.java:168
boolean isQuantifier()
Definition: AST.java:160
boolean equals(Object o)
Definition: AST.java:33
static final Z3_ast_kind fromInt(int v)
boolean isFuncDecl()
Definition: AST.java:176
static int getAstId(long a0, long a1)
Definition: Native.java:2327
Z3_ast_kind getASTKind()
Definition: AST.java:118
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
boolean isVar()
Definition: AST.java:152
boolean isExpr()
Definition: AST.java:127
AST translate(Context ctx)
Definition: AST.java:105
static int getAstHash(long a0, long a1)
Definition: Native.java:2336
static int getAstKind(long a0, long a1)
Definition: Native.java:2372
static String astToString(long a0, long a1)
Definition: Native.java:2989
static long translate(long a0, long a1, long a2)
Definition: Native.java:2723
int compareTo(Object other)
Definition: AST.java:54