Z3
AST.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 AST.cs
7
8Abstract:
9
10 Z3 Managed API: ASTs
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-16
15
16Notes:
17
18--*/
19
20using System.Diagnostics;
21using System;
22using System.Collections;
23using System.Collections.Generic;
24
25namespace Microsoft.Z3
26{
30 public class AST : Z3Object, IComparable
31 {
39 public static bool operator ==(AST a, AST b)
40 {
41 return Object.ReferenceEquals(a, b) ||
42 (!Object.ReferenceEquals(a, null) &&
43 !Object.ReferenceEquals(b, null) &&
44 a.Context.nCtx == b.Context.nCtx &&
45 0 != Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject));
46 }
47
55 public static bool operator !=(AST a, AST b)
56 {
57 return !(a == b);
58 }
59
63 public override bool Equals(object o)
64 {
65 AST casted = o as AST;
66 if (casted == null) return false;
67 return this == casted;
68 }
69
75 public virtual int CompareTo(object other)
76 {
77 if (other == null) return 1;
78 AST oAST = other as AST;
79 if (oAST == null)
80 return 1;
81 else
82 {
83 if (Id < oAST.Id)
84 return -1;
85 else if (Id > oAST.Id)
86 return +1;
87 else
88 return 0;
89 }
90 }
91
96 public override int GetHashCode()
97 {
98 return (int)Native.Z3_get_ast_hash(Context.nCtx, NativeObject);
99 }
100
104 public uint Id
105 {
106 get { return Native.Z3_get_ast_id(Context.nCtx, NativeObject); }
107 }
108
115 {
116 Debug.Assert(ctx != null);
117
118 if (ReferenceEquals(Context, ctx))
119 return this;
120 else
121 return Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
122 }
123
128 {
129 get { return (Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, NativeObject); }
130 }
131
135 public bool IsExpr
136 {
137 get
138 {
139 switch (ASTKind)
140 {
141 case Z3_ast_kind.Z3_APP_AST:
142 case Z3_ast_kind.Z3_NUMERAL_AST:
143 case Z3_ast_kind.Z3_QUANTIFIER_AST:
144 case Z3_ast_kind.Z3_VAR_AST: return true;
145 default: return false;
146 }
147 }
148 }
149
153 public bool IsApp
154 {
155 get { return this.ASTKind == Z3_ast_kind.Z3_APP_AST; }
156 }
157
161 public bool IsVar
162 {
163 get { return this.ASTKind == Z3_ast_kind.Z3_VAR_AST; }
164 }
165
169 public bool IsQuantifier
170 {
171 get { return this.ASTKind == Z3_ast_kind.Z3_QUANTIFIER_AST; }
172 }
173
177 public bool IsSort
178 {
179 get { return this.ASTKind == Z3_ast_kind.Z3_SORT_AST; }
180 }
181
185 public bool IsFuncDecl
186 {
187 get { return this.ASTKind == Z3_ast_kind.Z3_FUNC_DECL_AST; }
188 }
189
193 public override string ToString()
194 {
195 return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
196 }
197
201 public string SExpr()
202 {
203
204 return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
205 }
206
207 #region Internal
208 internal AST(Context ctx) : base(ctx) { Debug.Assert(ctx != null); }
209 internal AST(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
210
211 internal class DecRefQueue : IDecRefQueue
212 {
213 public DecRefQueue() : base() { }
214 public DecRefQueue(uint move_limit) : base(move_limit) { }
215 internal override void IncRef(Context ctx, IntPtr obj)
216 {
217 Native.Z3_inc_ref(ctx.nCtx, obj);
218 }
219
220 internal override void DecRef(Context ctx, IntPtr obj)
221 {
222 Native.Z3_dec_ref(ctx.nCtx, obj);
223 }
224 };
225
226 internal override void IncRef(IntPtr o)
227 {
228 // Console.WriteLine("AST IncRef()");
229 if (Context == null || o == IntPtr.Zero)
230 return;
231 Context.AST_DRQ.IncAndClear(Context, o);
232 base.IncRef(o);
233 }
234
235 internal override void DecRef(IntPtr o)
236 {
237 // Console.WriteLine("AST DecRef()");
238 if (Context == null || o == IntPtr.Zero)
239 return;
240 Context.AST_DRQ.Add(o);
241 base.DecRef(o);
242 }
243
244 internal static AST Create(Context ctx, IntPtr obj)
245 {
246 Debug.Assert(ctx != null);
247
248 switch ((Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj))
249 {
250 case Z3_ast_kind.Z3_FUNC_DECL_AST: return new FuncDecl(ctx, obj);
251 case Z3_ast_kind.Z3_QUANTIFIER_AST: return new Quantifier(ctx, obj);
252 case Z3_ast_kind.Z3_SORT_AST: return Sort.Create(ctx, obj);
253 case Z3_ast_kind.Z3_APP_AST:
254 case Z3_ast_kind.Z3_NUMERAL_AST:
255 case Z3_ast_kind.Z3_VAR_AST: return Expr.Create(ctx, obj);
256 default:
257 throw new Z3Exception("Unknown AST kind");
258 }
259 }
260 #endregion
261 }
262}
The abstract syntax tree (AST) class.
Definition: AST.cs:31
override bool Equals(object o)
Object comparison.
Definition: AST.cs:63
static bool operator==(AST a, AST b)
Comparison operator.
Definition: AST.cs:39
virtual int CompareTo(object other)
Object Comparison.
Definition: AST.cs:75
bool IsFuncDecl
Indicates whether the AST is a FunctionDeclaration
Definition: AST.cs:186
static bool operator!=(AST a, AST b)
Comparison operator.
Definition: AST.cs:55
bool IsSort
Indicates whether the AST is a Sort
Definition: AST.cs:178
bool IsVar
Indicates whether the AST is a BoundVariable
Definition: AST.cs:162
Z3_ast_kind ASTKind
The kind of the AST.
Definition: AST.cs:128
override int GetHashCode()
The AST's hash code.
Definition: AST.cs:96
uint Id
A unique identifier for the AST (unique among all ASTs).
Definition: AST.cs:105
bool IsQuantifier
Indicates whether the AST is a Quantifier
Definition: AST.cs:170
override string ToString()
A string representation of the AST.
Definition: AST.cs:193
string SExpr()
A string representation of the AST in s-expression notation.
Definition: AST.cs:201
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:154
AST Translate(Context ctx)
Translates (copies) the AST to the Context ctx .
Definition: AST.cs:114
bool IsExpr
Indicates whether the AST is an Expr
Definition: AST.cs:136
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
IDecRefQueue AST_DRQ
AST DRQ
Definition: Context.cs:4725
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180