Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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  if (getContext() == ctx) {
91  return this;
92  } else {
93  return create(ctx, Native.translate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
94  }
95  }
96 
102  {
103  return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(),
104  getNativeObject()));
105  }
106 
112  public boolean isExpr()
113  {
114  switch (getASTKind())
115  {
116  case Z3_APP_AST:
117  case Z3_NUMERAL_AST:
118  case Z3_QUANTIFIER_AST:
119  case Z3_VAR_AST:
120  return true;
121  default:
122  return false;
123  }
124  }
125 
131  public boolean isApp()
132  {
133  return this.getASTKind() == Z3_ast_kind.Z3_APP_AST;
134  }
135 
141  public boolean isVar()
142  {
143  return this.getASTKind() == Z3_ast_kind.Z3_VAR_AST;
144  }
145 
151  public boolean isQuantifier()
152  {
153  return this.getASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST;
154  }
155 
159  public boolean isSort()
160  {
161  return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST;
162  }
163 
167  public boolean isFuncDecl()
168  {
169  return this.getASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST;
170  }
171 
175  @Override
176  public String toString() {
177  return Native.astToString(getContext().nCtx(), getNativeObject());
178  }
179 
183  public String getSExpr()
184  {
185  return Native.astToString(getContext().nCtx(), getNativeObject());
186  }
187 
188  AST(Context ctx, long obj) {
189  super(ctx, obj);
190  }
191 
192  @Override
193  void incRef() {
194  Native.incRef(getContext().nCtx(), getNativeObject());
195  }
196 
197  @Override
198  void addToReferenceQueue() {
199  getContext().getASTDRQ().storeReference(getContext(), this);
200  }
201 
202  static AST create(Context ctx, long obj)
203  {
204  switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
205  {
206  case Z3_FUNC_DECL_AST:
207  return new FuncDecl(ctx, obj);
208  case Z3_QUANTIFIER_AST:
209  return new Quantifier(ctx, obj);
210  case Z3_SORT_AST:
211  return Sort.create(ctx, obj);
212  case Z3_APP_AST:
213  case Z3_NUMERAL_AST:
214  case Z3_VAR_AST:
215  return Expr.create(ctx, obj);
216  default:
217  throw new Z3Exception("Unknown AST kind");
218  }
219  }
220 }
String toString()
Definition: AST.java:176
String getSExpr()
Definition: AST.java:183
boolean isApp()
Definition: AST.java:131
boolean isSort()
Definition: AST.java:159
boolean isQuantifier()
Definition: AST.java:151
boolean equals(Object o)
Definition: AST.java:33
int compareTo(AST other)
Definition: AST.java:53
IDecRefQueue< AST > getASTDRQ()
Definition: Context.java:4026
static final Z3_ast_kind fromInt(int v)
boolean isFuncDecl()
Definition: AST.java:167
def String
Definition: z3py.py:10043
static int getAstId(long a0, long a1)
Definition: Native.java:3049
Z3_ast_kind getASTKind()
Definition: AST.java:101
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:176
boolean isVar()
Definition: AST.java:141
boolean isExpr()
Definition: AST.java:112
AST translate(Context ctx)
Definition: AST.java:88
static int getAstHash(long a0, long a1)
Definition: Native.java:3058
static int getAstKind(long a0, long a1)
Definition: Native.java:3094
static String astToString(long a0, long a1)
Definition: Native.java:3789
static boolean isEqAst(long a0, long a1, long a2)
Definition: Native.java:3040
static long translate(long a0, long a1, long a2)
Definition: Native.java:3472