Z3
src/api/dotnet/AST.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     AST.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: ASTs
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-16
00015 
00016 Notes:
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             // Console.WriteLine("AST IncRef()");
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             // Console.WriteLine("AST DecRef()");
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines