Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
AST.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  AST.cs
7 
8 Abstract:
9 
10  Z3 Managed API: ASTs
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-16
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Collections;
22 using System.Collections.Generic;
23 using System.Diagnostics.Contracts;
24 
25 namespace Microsoft.Z3
26 {
30  [ContractVerification(true)]
31  public class AST : Z3Object, IComparable
32  {
40  public static bool operator ==(AST a, AST b)
41  {
42  return Object.ReferenceEquals(a, b) ||
43  (!Object.ReferenceEquals(a, null) &&
44  !Object.ReferenceEquals(b, null) &&
45  a.Context.nCtx == b.Context.nCtx &&
46  Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
47  }
48 
56  public static bool operator !=(AST a, AST b)
57  {
58  return !(a == b);
59  }
60 
64  public override bool Equals(object o)
65  {
66  AST casted = o as AST;
67  if (casted == null) return false;
68  return this == casted;
69  }
70 
76  public virtual int CompareTo(object other)
77  {
78  if (other == null) return 1;
79  AST oAST = other as AST;
80  if (oAST == null)
81  return 1;
82  else
83  {
84  if (Id < oAST.Id)
85  return -1;
86  else if (Id > oAST.Id)
87  return +1;
88  else
89  return 0;
90  }
91  }
92 
97  public override int GetHashCode()
98  {
99  return (int)Native.Z3_get_ast_hash(Context.nCtx, NativeObject);
100  }
101 
105  public uint Id
106  {
107  get { return Native.Z3_get_ast_id(Context.nCtx, NativeObject); }
108  }
109 
115  public AST Translate(Context ctx)
116  {
117  Contract.Requires(ctx != null);
118  Contract.Ensures(Contract.Result<AST>() != null);
119 
120  if (ReferenceEquals(Context, ctx))
121  return this;
122  else
123  return new AST(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
124  }
125 
129  public Z3_ast_kind ASTKind
130  {
131  get { return (Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, NativeObject); }
132  }
133 
137  public bool IsExpr
138  {
139  get
140  {
141  switch (ASTKind)
142  {
143  case Z3_ast_kind.Z3_APP_AST:
144  case Z3_ast_kind.Z3_NUMERAL_AST:
145  case Z3_ast_kind.Z3_QUANTIFIER_AST:
146  case Z3_ast_kind.Z3_VAR_AST: return true;
147  default: return false;
148  }
149  }
150  }
151 
155  public bool IsApp
156  {
157  get { return this.ASTKind == Z3_ast_kind.Z3_APP_AST; }
158  }
159 
163  public bool IsVar
164  {
165  get { return this.ASTKind == Z3_ast_kind.Z3_VAR_AST; }
166  }
167 
171  public bool IsQuantifier
172  {
173  get { return this.ASTKind == Z3_ast_kind.Z3_QUANTIFIER_AST; }
174  }
175 
179  public bool IsSort
180  {
181  get { return this.ASTKind == Z3_ast_kind.Z3_SORT_AST; }
182  }
183 
187  public bool IsFuncDecl
188  {
189  get { return this.ASTKind == Z3_ast_kind.Z3_FUNC_DECL_AST; }
190  }
191 
195  public override string ToString()
196  {
197  return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
198  }
199 
203  public string SExpr()
204  {
205  Contract.Ensures(Contract.Result<string>() != null);
206 
207  return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
208  }
209 
210  #region Internal
211  internal AST(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
212  internal AST(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
213 
214  internal class DecRefQueue : IDecRefQueue
215  {
216  public override void IncRef(Context ctx, IntPtr obj)
217  {
218  Native.Z3_inc_ref(ctx.nCtx, obj);
219  }
220 
221  public override void DecRef(Context ctx, IntPtr obj)
222  {
223  Native.Z3_dec_ref(ctx.nCtx, obj);
224  }
225  };
226 
227  internal override void IncRef(IntPtr o)
228  {
229  // Console.WriteLine("AST IncRef()");
230  if (Context == null)
231  throw new Z3Exception("inc() called on null context");
232  if (o == IntPtr.Zero)
233  throw new Z3Exception("inc() called on null AST");
234  Context.AST_DRQ.IncAndClear(Context, o);
235  base.IncRef(o);
236  }
237 
238  internal override void DecRef(IntPtr o)
239  {
240  // Console.WriteLine("AST DecRef()");
241  if (Context == null)
242  throw new Z3Exception("dec() called on null context");
243  if (o == IntPtr.Zero)
244  throw new Z3Exception("dec() called on null AST");
245  Context.AST_DRQ.Add(o);
246  base.DecRef(o);
247  }
248 
249  internal static AST Create(Context ctx, IntPtr obj)
250  {
251  Contract.Requires(ctx != null);
252  Contract.Ensures(Contract.Result<AST>() != null);
253 
254  switch ((Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj))
255  {
256  case Z3_ast_kind.Z3_FUNC_DECL_AST: return new FuncDecl(ctx, obj);
257  case Z3_ast_kind.Z3_QUANTIFIER_AST: return new Quantifier(ctx, obj);
258  case Z3_ast_kind.Z3_SORT_AST: return Sort.Create(ctx, obj);
259  case Z3_ast_kind.Z3_APP_AST:
260  case Z3_ast_kind.Z3_NUMERAL_AST:
261  case Z3_ast_kind.Z3_VAR_AST: return Expr.Create(ctx, obj);
262  default:
263  throw new Z3Exception("Unknown AST kind");
264  }
265  }
266  #endregion
267  }
268 }
string SExpr()
A string representation of the AST in s-expression notation.
Definition: AST.cs:203
override string ToString()
A string representation of the AST.
Definition: AST.cs:195
AST Translate(Context ctx)
Translates (copies) the AST to the Context ctx .
Definition: AST.cs:115
uint Id
A unique identifier for the AST (unique among all ASTs).
Definition: AST.cs:106
static string Z3_ast_to_string(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3832
override int GetHashCode()
The AST's hash code.
Definition: AST.cs:97
static Z3_ast Z3_translate(Z3_context a0, Z3_ast a1, Z3_context a2)
Definition: Native.cs:3598
Z3_ast_kind
Z3_ast_kind
Definition: Enumerations.cs:48
static uint Z3_get_ast_id(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3246
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
static uint Z3_get_ast_hash(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3254
static int Z3_is_eq_ast(Z3_context a0, Z3_ast a1, Z3_ast a2)
Definition: Native.cs:3238
static uint Z3_get_ast_kind(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3286
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
override bool Equals(object o)
Object comparison.
Definition: AST.cs:64
The abstract syntax tree (AST) class.
Definition: AST.cs:31
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31
virtual int CompareTo(object other)
Object Comparison.
Definition: AST.cs:76