Z3 |

AST.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
20 import com.microsoft.z3.enumerations.Z3_ast_kind;
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
101 public Z3_ast_kind getASTKind()
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}
Comparable
com.microsoft.z3.AST
Definition: AST.java:26
com.microsoft.z3.AST.hashCode
int hashCode()
Definition: AST.java:67
com.microsoft.z3.AST.getSExpr
String getSExpr()
Definition: AST.java:183
com.microsoft.z3.AST.isFuncDecl
boolean isFuncDecl()
Definition: AST.java:167
com.microsoft.z3.AST.isQuantifier
boolean isQuantifier()
Definition: AST.java:151
com.microsoft.z3.AST.equals
boolean equals(Object o)
Definition: AST.java:33
com.microsoft.z3.AST.compareTo
int compareTo(AST other)
Definition: AST.java:53
com.microsoft.z3.AST.getId
int getId()
Definition: AST.java:76
com.microsoft.z3.AST.isApp
boolean isApp()
Definition: AST.java:131
com.microsoft.z3.AST.isSort
boolean isSort()
Definition: AST.java:159
com.microsoft.z3.AST.translate
AST translate(Context ctx)
Definition: AST.java:88
com.microsoft.z3.AST.isExpr
boolean isExpr()
Definition: AST.java:112
com.microsoft.z3.AST.isVar
boolean isVar()
Definition: AST.java:141
com.microsoft.z3.AST.toString
String toString()
Definition: AST.java:176
com.microsoft.z3.AST.getASTKind
Z3_ast_kind getASTKind()
Definition: AST.java:101
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Context.getASTDRQ
IDecRefQueue< AST > getASTDRQ()
Definition: Context.java:4070
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:4008
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693
Z3_ast_kind
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180
Z3_APP_AST
@ Z3_APP_AST
Definition: z3_api.h:182
Z3_VAR_AST
@ Z3_VAR_AST
Definition: z3_api.h:183
Z3_SORT_AST
@ Z3_SORT_AST
Definition: z3_api.h:185
Z3_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition: z3_api.h:181
Z3_FUNC_DECL_AST
@ Z3_FUNC_DECL_AST
Definition: z3_api.h:186
Z3_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:184