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  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 }
com.microsoft.z3.enumerations.Z3_ast_kind.Z3_FUNC_DECL_AST
Z3_FUNC_DECL_AST
Definition: Z3_ast_kind.java:19
com.microsoft.z3.AST.isSort
boolean isSort()
Definition: AST.java:159
com.microsoft.z3.enumerations
Definition: Z3_ast_kind.java:5
com.microsoft.z3.enumerations.Z3_ast_kind.Z3_VAR_AST
Z3_VAR_AST
Definition: Z3_ast_kind.java:16
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.enumerations.Z3_ast_kind.Z3_QUANTIFIER_AST
Z3_QUANTIFIER_AST
Definition: Z3_ast_kind.java:17
Z3_APP_AST
@ Z3_APP_AST
Definition: z3_api.h:180
com.microsoft.z3.AST.getASTKind
Z3_ast_kind getASTKind()
Definition: AST.java:101
com.microsoft.z3.AST.getId
int getId()
Definition: AST.java:76
com.microsoft
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.Native.getAstHash
static int getAstHash(long a0, long a1)
Definition: Native.java:3091
com.microsoft.z3.AST.hashCode
int hashCode()
Definition: AST.java:67
com.microsoft.z3.AST.toString
String toString()
Definition: AST.java:176
com.microsoft.z3.enumerations.Z3_ast_kind.fromInt
static final Z3_ast_kind fromInt(int v)
Definition: Z3_ast_kind.java:38
com.microsoft.z3.AST.translate
AST translate(Context ctx)
Definition: AST.java:88
Z3_FUNC_DECL_AST
@ Z3_FUNC_DECL_AST
Definition: z3_api.h:184
com.microsoft.z3.enumerations.Z3_ast_kind.Z3_APP_AST
Z3_APP_AST
Definition: Z3_ast_kind.java:15
com.microsoft.z3.Native.getAstId
static int getAstId(long a0, long a1)
Definition: Native.java:3082
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:3966
com.microsoft.z3.enumerations.Z3_ast_kind.Z3_SORT_AST
Z3_SORT_AST
Definition: Z3_ast_kind.java:18
com.microsoft.z3.AST.compareTo
int compareTo(AST other)
Definition: AST.java:53
Z3_VAR_AST
@ Z3_VAR_AST
Definition: z3_api.h:181
com.microsoft.z3.Native.translate
static long translate(long a0, long a1, long a2)
Definition: Native.java:3505
com.microsoft.z3.Native
Definition: Native.java:4
Z3_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition: z3_api.h:179
Comparable
com.microsoft.z3
Definition: AlgebraicNum.java:18
com.microsoft.z3.AST.getSExpr
String getSExpr()
Definition: AST.java:183
com.microsoft.z3.enumerations.Z3_ast_kind
Definition: Z3_ast_kind.java:13
com.microsoft.z3.Native.getAstKind
static int getAstKind(long a0, long a1)
Definition: Native.java:3127
com.microsoft.z3.AST
Definition: AST.java:26
com.microsoft.z3.Context.getASTDRQ
IDecRefQueue< AST > getASTDRQ()
Definition: Context.java:4028
com.microsoft.z3.AST.isFuncDecl
boolean isFuncDecl()
Definition: AST.java:167
Z3_SORT_AST
@ Z3_SORT_AST
Definition: z3_api.h:183
com
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.AST.isExpr
boolean isExpr()
Definition: AST.java:112
com.microsoft.z3.Native.astToString
static String astToString(long a0, long a1)
Definition: Native.java:3822
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:178
com.microsoft.z3.AST.isApp
boolean isApp()
Definition: AST.java:131
com.microsoft.z3.Native.isEqAst
static boolean isEqAst(long a0, long a1, long a2)
Definition: Native.java:3073
com.microsoft.z3.AST.isVar
boolean isVar()
Definition: AST.java:141
Z3_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:182
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10111