Z3
AST.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
25 public class AST extends Z3Object implements Comparable
26 {
32  public boolean equals(Object o)
33  {
34  AST casted = null;
35 
36  try
37  {
38  casted = AST.class.cast(o);
39  } catch (ClassCastException e)
40  {
41  return false;
42  }
43 
44  return
45  (this == casted) ||
46  (this != null) &&
47  (casted != null) &&
48  (getContext().nCtx() == casted.getContext().nCtx()) &&
49  (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
50 }
51 
60  public int compareTo(Object other)
61  {
62  if (other == null)
63  return 1;
64 
65  AST oAST = null;
66  try
67  {
68  oAST = AST.class.cast(other);
69  } catch (ClassCastException e)
70  {
71  return 1;
72  }
73 
74  if (getId() < oAST.getId())
75  return -1;
76  else if (getId() > oAST.getId())
77  return +1;
78  else
79  return 0;
80  }
81 
87  public int hashCode()
88  {
89  int r = 0;
90  try {
91  Native.getAstHash(getContext().nCtx(), getNativeObject());
92  }
93  catch (Z3Exception ex) {}
94  return r;
95  }
96 
101  public int getId()
102  {
103  return Native.getAstId(getContext().nCtx(), getNativeObject());
104  }
105 
113  public AST translate(Context ctx)
114  {
115 
116  if (getContext() == ctx)
117  return this;
118  else
119  return new AST(ctx, Native.translate(getContext().nCtx(),
120  getNativeObject(), ctx.nCtx()));
121  }
122 
128  {
129  return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(),
130  getNativeObject()));
131  }
132 
138  public boolean isExpr()
139  {
140  switch (getASTKind())
141  {
142  case Z3_APP_AST:
143  case Z3_NUMERAL_AST:
144  case Z3_QUANTIFIER_AST:
145  case Z3_VAR_AST:
146  return true;
147  default:
148  return false;
149  }
150  }
151 
157  public boolean isApp()
158  {
159  return this.getASTKind() == Z3_ast_kind.Z3_APP_AST;
160  }
161 
167  public boolean isVar()
168  {
169  return this.getASTKind() == Z3_ast_kind.Z3_VAR_AST;
170  }
171 
177  public boolean isQuantifier()
178  {
179  return this.getASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST;
180  }
181 
185  public boolean isSort()
186  {
187  return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST;
188  }
189 
193  public boolean isFuncDecl()
194  {
195  return this.getASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST;
196  }
197 
201  public String toString()
202  {
203  try
204  {
205  return Native.astToString(getContext().nCtx(), getNativeObject());
206  } catch (Z3Exception e)
207  {
208  return "Z3Exception: " + e.getMessage();
209  }
210  }
211 
215  public String getSExpr()
216  {
217  return Native.astToString(getContext().nCtx(), getNativeObject());
218  }
219 
220  AST(Context ctx)
221  {
222  super(ctx);
223  }
224 
225  AST(Context ctx, long obj)
226  {
227  super(ctx, obj);
228  }
229 
230  void incRef(long o)
231  {
232  // Console.WriteLine("AST IncRef()");
233  if (getContext() == null || o == 0)
234  return;
235  getContext().getASTDRQ().incAndClear(getContext(), o);
236  super.incRef(o);
237  }
238 
239  void decRef(long o)
240  {
241  // Console.WriteLine("AST DecRef()");
242  if (getContext() == null || o == 0)
243  return;
244  getContext().getASTDRQ().add(o);
245  super.decRef(o);
246  }
247 
248  static AST create(Context ctx, long obj)
249  {
250  switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
251  {
252  case Z3_FUNC_DECL_AST:
253  return new FuncDecl(ctx, obj);
254  case Z3_QUANTIFIER_AST:
255  return new Quantifier(ctx, obj);
256  case Z3_SORT_AST:
257  return Sort.create(ctx, obj);
258  case Z3_APP_AST:
259  case Z3_NUMERAL_AST:
260  case Z3_VAR_AST:
261  return Expr.create(ctx, obj);
262  default:
263  throw new Z3Exception("Unknown AST kind");
264  }
265  }
266 }
String toString()
Definition: AST.java:201
String getSExpr()
Definition: AST.java:215
boolean isApp()
Definition: AST.java:157
boolean isSort()
Definition: AST.java:185
boolean isQuantifier()
Definition: AST.java:177
boolean equals(Object o)
Definition: AST.java:32
static final Z3_ast_kind fromInt(int v)
boolean isFuncDecl()
Definition: AST.java:193
static int getAstId(long a0, long a1)
Definition: Native.java:2450
Z3_ast_kind getASTKind()
Definition: AST.java:127
boolean isVar()
Definition: AST.java:167
boolean isExpr()
Definition: AST.java:138
void incAndClear(Context ctx, long o)
AST translate(Context ctx)
Definition: AST.java:113
static int getAstHash(long a0, long a1)
Definition: Native.java:2459
static int getAstKind(long a0, long a1)
Definition: Native.java:2495
IDecRefQueue getASTDRQ()
Definition: Context.java:3684
static String astToString(long a0, long a1)
Definition: Native.java:3112
static boolean isEqAst(long a0, long a1, long a2)
Definition: Native.java:2441
static long translate(long a0, long a1, long a2)
Definition: Native.java:2846
int compareTo(Object other)
Definition: AST.java:60