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<AST>
26 {
32  @Override
33  public boolean equals(Object o)
34  {
35  if (o == this) return true;
36  if (!(o instanceof AST)) return false;
37  AST casted = (AST) o;
38 
39  return
40  (getContext().nCtx() == casted.getContext().nCtx()) &&
41  (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
42  }
43 
52  @Override
53  public int compareTo(AST other)
54  {
55  if (other == null) {
56  return 1;
57  }
58  return Integer.compare(getId(), other.getId());
59  }
60 
66  @Override
67  public int hashCode()
68  {
69  return Native.getAstHash(getContext().nCtx(), getNativeObject());
70  }
71 
76  public int getId()
77  {
78  return Native.getAstId(getContext().nCtx(), getNativeObject());
79  }
80 
88  public AST translate(Context ctx)
89  {
90 
91  if (getContext() == ctx) {
92  return this;
93  } else {
94  return new AST(ctx, Native.translate(getContext().nCtx(),
95  getNativeObject(), ctx.nCtx()));
96  }
97  }
98 
104  {
105  return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(),
106  getNativeObject()));
107  }
108 
114  public boolean isExpr()
115  {
116  switch (getASTKind())
117  {
118  case Z3_APP_AST:
119  case Z3_NUMERAL_AST:
120  case Z3_QUANTIFIER_AST:
121  case Z3_VAR_AST:
122  return true;
123  default:
124  return false;
125  }
126  }
127 
133  public boolean isApp()
134  {
135  return this.getASTKind() == Z3_ast_kind.Z3_APP_AST;
136  }
137 
143  public boolean isVar()
144  {
145  return this.getASTKind() == Z3_ast_kind.Z3_VAR_AST;
146  }
147 
153  public boolean isQuantifier()
154  {
155  return this.getASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST;
156  }
157 
161  public boolean isSort()
162  {
163  return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST;
164  }
165 
169  public boolean isFuncDecl()
170  {
171  return this.getASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST;
172  }
173 
177  @Override
178  public String toString() {
179  return Native.astToString(getContext().nCtx(), getNativeObject());
180  }
181 
185  public String getSExpr()
186  {
187  return Native.astToString(getContext().nCtx(), getNativeObject());
188  }
189 
190  AST(Context ctx, long obj) {
191  super(ctx, obj);
192  }
193 
194  @Override
195  void incRef() {
196  Native.incRef(getContext().nCtx(), getNativeObject());
197  }
198 
199  @Override
200  void addToReferenceQueue() {
201  getContext().getASTDRQ().storeReference(getContext(), this);
202  }
203 
204  static AST create(Context ctx, long obj)
205  {
206  switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
207  {
208  case Z3_FUNC_DECL_AST:
209  return new FuncDecl(ctx, obj);
210  case Z3_QUANTIFIER_AST:
211  return new Quantifier(ctx, obj);
212  case Z3_SORT_AST:
213  return Sort.create(ctx, obj);
214  case Z3_APP_AST:
215  case Z3_NUMERAL_AST:
216  case Z3_VAR_AST:
217  return Expr.create(ctx, obj);
218  default:
219  throw new Z3Exception("Unknown AST kind");
220  }
221  }
222 }
String toString()
Definition: AST.java:178
String getSExpr()
Definition: AST.java:185
boolean isApp()
Definition: AST.java:133
boolean isSort()
Definition: AST.java:161
static void incRef(long a0, long a1)
Definition: Native.java:700
boolean isQuantifier()
Definition: AST.java:153
boolean equals(Object o)
Definition: AST.java:33
int compareTo(AST other)
Definition: AST.java:53
IDecRefQueue< AST > getASTDRQ()
Definition: Context.java:3934
static final Z3_ast_kind fromInt(int v)
boolean isFuncDecl()
Definition: AST.java:169
static int getAstId(long a0, long a1)
Definition: Native.java:2717
Z3_ast_kind getASTKind()
Definition: AST.java:103
void storeReference(Context ctx, T obj)
boolean isVar()
Definition: AST.java:143
boolean isExpr()
Definition: AST.java:114
AST translate(Context ctx)
Definition: AST.java:88
static int getAstHash(long a0, long a1)
Definition: Native.java:2726
static int getAstKind(long a0, long a1)
Definition: Native.java:2762
static String astToString(long a0, long a1)
Definition: Native.java:3379
static boolean isEqAst(long a0, long a1, long a2)
Definition: Native.java:2708
static long translate(long a0, long a1, long a2)
Definition: Native.java:3113
def String(name, ctx=None)
Definition: z3py.py:9443