Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups 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 IsVar
156  {
157  get { return this.ASTKind == Z3_ast_kind.Z3_VAR_AST; }
158  }
159 
163  public bool IsQuantifier
164  {
165  get { return this.ASTKind == Z3_ast_kind.Z3_QUANTIFIER_AST; }
166  }
167 
171  public bool IsSort
172  {
173  get { return this.ASTKind == Z3_ast_kind.Z3_SORT_AST; }
174  }
175 
179  public bool IsFuncDecl
180  {
181  get { return this.ASTKind == Z3_ast_kind.Z3_FUNC_DECL_AST; }
182  }
183 
187  public override string ToString()
188  {
189  return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
190  }
191 
195  public string SExpr()
196  {
197  Contract.Ensures(Contract.Result<string>() != null);
198 
199  return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
200  }
201 
202  #region Internal
203  internal AST(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
204  internal AST(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
205 
206  internal class DecRefQueue : Z3.DecRefQueue
207  {
208  public override void IncRef(Context ctx, IntPtr obj)
209  {
210  Native.Z3_inc_ref(ctx.nCtx, obj);
211  }
212 
213  public override void DecRef(Context ctx, IntPtr obj)
214  {
215  Native.Z3_dec_ref(ctx.nCtx, obj);
216  }
217  };
218 
219  internal override void IncRef(IntPtr o)
220  {
221  // Console.WriteLine("AST IncRef()");
222  if (Context == null)
223  throw new Z3Exception("inc() called on null context");
224  if (o == IntPtr.Zero)
225  throw new Z3Exception("inc() called on null AST");
226  Context.AST_DRQ.IncAndClear(Context, o);
227  base.IncRef(o);
228  }
229 
230  internal override void DecRef(IntPtr o)
231  {
232  // Console.WriteLine("AST DecRef()");
233  if (Context == null)
234  throw new Z3Exception("dec() called on null context");
235  if (o == IntPtr.Zero)
236  throw new Z3Exception("dec() called on null AST");
237  Context.AST_DRQ.Add(o);
238  base.DecRef(o);
239  }
240 
241  internal static AST Create(Context ctx, IntPtr obj)
242  {
243  Contract.Requires(ctx != null);
244  Contract.Ensures(Contract.Result<AST>() != null);
245 
246  switch ((Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj))
247  {
248  case Z3_ast_kind.Z3_FUNC_DECL_AST: return new FuncDecl(ctx, obj);
249  case Z3_ast_kind.Z3_QUANTIFIER_AST: return new Quantifier(ctx, obj);
250  case Z3_ast_kind.Z3_SORT_AST: return Sort.Create(ctx, obj);
251  case Z3_ast_kind.Z3_APP_AST:
252  case Z3_ast_kind.Z3_NUMERAL_AST:
253  case Z3_ast_kind.Z3_VAR_AST: return Expr.Create(ctx, obj);
254  default:
255  throw new Z3Exception("Unknown AST kind");
256  }
257  }
258  #endregion
259  }
260 }