Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Collections;
00022 using System.Collections.Generic;
00023 using System.Diagnostics.Contracts;
00024
00025 namespace Microsoft.Z3
00026 {
00030 [ContractVerification(true)]
00031 public class AST : Z3Object, IComparable
00032 {
00040 public static bool operator ==(AST a, AST b)
00041 {
00042 return Object.ReferenceEquals(a, b) ||
00043 (!Object.ReferenceEquals(a, null) &&
00044 !Object.ReferenceEquals(b, null) &&
00045 a.Context.nCtx == b.Context.nCtx &&
00046 Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
00047 }
00048
00056 public static bool operator !=(AST a, AST b)
00057 {
00058 return !(a == b);
00059 }
00060
00064 public override bool Equals(object o)
00065 {
00066 AST casted = o as AST;
00067 if (casted == null) return false;
00068 return this == casted;
00069 }
00070
00076 public virtual int CompareTo(object other)
00077 {
00078 if (other == null) return 1;
00079 AST oAST = other as AST;
00080 if (oAST == null)
00081 return 1;
00082 else
00083 {
00084 if (Id < oAST.Id)
00085 return -1;
00086 else if (Id > oAST.Id)
00087 return +1;
00088 else
00089 return 0;
00090 }
00091 }
00092
00097 public override int GetHashCode()
00098 {
00099 return (int)Native.Z3_get_ast_hash(Context.nCtx, NativeObject);
00100 }
00101
00105 public uint Id
00106 {
00107 get { return Native.Z3_get_ast_id(Context.nCtx, NativeObject); }
00108 }
00109
00115 public AST Translate(Context ctx)
00116 {
00117 Contract.Requires(ctx != null);
00118 Contract.Ensures(Contract.Result<AST>() != null);
00119
00120 if (ReferenceEquals(Context, ctx))
00121 return this;
00122 else
00123 return new AST(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
00124 }
00125
00129 public Z3_ast_kind ASTKind
00130 {
00131 get { return (Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, NativeObject); }
00132 }
00133
00137 public bool IsExpr
00138 {
00139 get
00140 {
00141 switch (ASTKind)
00142 {
00143 case Z3_ast_kind.Z3_APP_AST:
00144 case Z3_ast_kind.Z3_NUMERAL_AST:
00145 case Z3_ast_kind.Z3_QUANTIFIER_AST:
00146 case Z3_ast_kind.Z3_VAR_AST: return true;
00147 default: return false;
00148 }
00149 }
00150 }
00151
00155 public bool IsApp
00156 {
00157 get { return this.ASTKind == Z3_ast_kind.Z3_APP_AST; }
00158 }
00159
00163 public bool IsVar
00164 {
00165 get { return this.ASTKind == Z3_ast_kind.Z3_VAR_AST; }
00166 }
00167
00171 public bool IsQuantifier
00172 {
00173 get { return this.ASTKind == Z3_ast_kind.Z3_QUANTIFIER_AST; }
00174 }
00175
00179 public bool IsSort
00180 {
00181 get { return this.ASTKind == Z3_ast_kind.Z3_SORT_AST; }
00182 }
00183
00187 public bool IsFuncDecl
00188 {
00189 get { return this.ASTKind == Z3_ast_kind.Z3_FUNC_DECL_AST; }
00190 }
00191
00195 public override string ToString()
00196 {
00197 return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
00198 }
00199
00203 public string SExpr()
00204 {
00205 Contract.Ensures(Contract.Result<string>() != null);
00206
00207 return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
00208 }
00209
00210 #region Internal
00211 internal AST(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
00212 internal AST(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
00213
00214 internal class DecRefQueue : IDecRefQueue
00215 {
00216 public override void IncRef(Context ctx, IntPtr obj)
00217 {
00218 Native.Z3_inc_ref(ctx.nCtx, obj);
00219 }
00220
00221 public override void DecRef(Context ctx, IntPtr obj)
00222 {
00223 Native.Z3_dec_ref(ctx.nCtx, obj);
00224 }
00225 };
00226
00227 internal override void IncRef(IntPtr o)
00228 {
00229
00230 if (Context == null)
00231 throw new Z3Exception("inc() called on null context");
00232 if (o == IntPtr.Zero)
00233 throw new Z3Exception("inc() called on null AST");
00234 Context.AST_DRQ.IncAndClear(Context, o);
00235 base.IncRef(o);
00236 }
00237
00238 internal override void DecRef(IntPtr o)
00239 {
00240
00241 if (Context == null)
00242 throw new Z3Exception("dec() called on null context");
00243 if (o == IntPtr.Zero)
00244 throw new Z3Exception("dec() called on null AST");
00245 Context.AST_DRQ.Add(o);
00246 base.DecRef(o);
00247 }
00248
00249 internal static AST Create(Context ctx, IntPtr obj)
00250 {
00251 Contract.Requires(ctx != null);
00252 Contract.Ensures(Contract.Result<AST>() != null);
00253
00254 switch ((Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj))
00255 {
00256 case Z3_ast_kind.Z3_FUNC_DECL_AST: return new FuncDecl(ctx, obj);
00257 case Z3_ast_kind.Z3_QUANTIFIER_AST: return new Quantifier(ctx, obj);
00258 case Z3_ast_kind.Z3_SORT_AST: return Sort.Create(ctx, obj);
00259 case Z3_ast_kind.Z3_APP_AST:
00260 case Z3_ast_kind.Z3_NUMERAL_AST:
00261 case Z3_ast_kind.Z3_VAR_AST: return Expr.Create(ctx, obj);
00262 default:
00263 throw new Z3Exception("Unknown AST kind");
00264 }
00265 }
00266 #endregion
00267 }
00268 }