Z3
AST.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import com.microsoft.z3.enumerations.Z3_ast_kind;
21
25public 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:
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 {
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
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);
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 getSExpr()
Definition: AST.java:183
boolean isFuncDecl()
Definition: AST.java:167
boolean isQuantifier()
Definition: AST.java:151
boolean equals(Object o)
Definition: AST.java:33
int compareTo(AST other)
Definition: AST.java:53
boolean isApp()
Definition: AST.java:131
boolean isSort()
Definition: AST.java:159
AST translate(Context ctx)
Definition: AST.java:88
boolean isExpr()
Definition: AST.java:112
boolean isVar()
Definition: AST.java:141
String toString()
Definition: AST.java:176
Z3_ast_kind getASTKind()
Definition: AST.java:101
IDecRefQueue< AST > getASTDRQ()
Definition: Context.java:4028
void storeReference(Context ctx, T obj)
static int getAstHash(long a0, long a1)
Definition: Native.java:3089
static int getAstId(long a0, long a1)
Definition: Native.java:3080
static int getAstKind(long a0, long a1)
Definition: Native.java:3125
static long translate(long a0, long a1, long a2)
Definition: Native.java:3503
static boolean isEqAst(long a0, long a1, long a2)
Definition: Native.java:3071
static String astToString(long a0, long a1)
Definition: Native.java:3820
static final Z3_ast_kind fromInt(int v)
def String(name, ctx=None)
Definition: z3py.py:10085
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:178
@ Z3_APP_AST
Definition: z3_api.h:180
@ Z3_VAR_AST
Definition: z3_api.h:181
@ Z3_SORT_AST
Definition: z3_api.h:183
@ Z3_NUMERAL_AST
Definition: z3_api.h:179
@ Z3_FUNC_DECL_AST
Definition: z3_api.h:184
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:182