Z3
src/api/dotnet/Sort.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Sort.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Sorts
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-15
00015 
00016 Notes:
00017     
00018 --*/
00019 
00020 using System;
00021 using System.Diagnostics.Contracts;
00022 
00023 namespace Microsoft.Z3
00024 {
00028     [ContractVerification(true)]
00029     public class Sort : AST
00030     {
00038         public static bool operator ==(Sort a, Sort b)
00039         {
00040             return Object.ReferenceEquals(a, b) ||
00041                    (!Object.ReferenceEquals(a, null) &&
00042                     !Object.ReferenceEquals(b, null) &&
00043                     a.Context == b.Context &&
00044                     Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
00045         }
00046 
00054         public static bool operator !=(Sort a, Sort b)
00055         {
00056             return !(a == b);
00057         }
00058 
00064         public override bool Equals(object o)
00065         {
00066             Sort casted = o as Sort;
00067             if (casted == null) return false;
00068             return this == casted;
00069         }
00070 
00075         public override int GetHashCode()
00076         {
00077             return base.GetHashCode();
00078         }
00079 
00083         new public uint Id
00084         {
00085             get { return Native.Z3_get_sort_id(Context.nCtx, NativeObject); }
00086         }
00087 
00091         public Z3_sort_kind SortKind
00092         {
00093             get { return (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, NativeObject); }
00094         }
00095 
00099         public Symbol Name
00100         {
00101             get
00102             {
00103                 Contract.Ensures(Contract.Result<Symbol>() != null);
00104                 return Symbol.Create(Context, Native.Z3_get_sort_name(Context.nCtx, NativeObject));
00105             }
00106         }
00107 
00111         public override string ToString()
00112         {
00113             return Native.Z3_sort_to_string(Context.nCtx, NativeObject);
00114         }
00115 
00116         #region Internal
00117 
00118 
00119 
00120         internal protected Sort(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
00121         internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
00122 
00123 #if DEBUG
00124         internal override void CheckNativeObject(IntPtr obj)
00125         {
00126             if (Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_SORT_AST)
00127                 throw new Z3Exception("Underlying object is not a sort");
00128             base.CheckNativeObject(obj);
00129         }
00130 #endif
00131 
00132         [ContractVerification(true)]
00133         new internal static Sort Create(Context ctx, IntPtr obj)
00134         {
00135             Contract.Requires(ctx != null);
00136             Contract.Ensures(Contract.Result<Sort>() != null);
00137 
00138             switch ((Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, obj))
00139             {
00140                 case Z3_sort_kind.Z3_ARRAY_SORT: return new ArraySort(ctx, obj);
00141                 case Z3_sort_kind.Z3_BOOL_SORT: return new BoolSort(ctx, obj);
00142                 case Z3_sort_kind.Z3_BV_SORT: return new BitVecSort(ctx, obj);
00143                 case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeSort(ctx, obj);
00144                 case Z3_sort_kind.Z3_INT_SORT: return new IntSort(ctx, obj);
00145                 case Z3_sort_kind.Z3_REAL_SORT: return new RealSort(ctx, obj);
00146                 case Z3_sort_kind.Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj);
00147                 case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj);
00148                 case Z3_sort_kind.Z3_RELATION_SORT: return new RelationSort(ctx, obj);
00149                 default:
00150                     throw new Z3Exception("Unknown sort kind");
00151             }
00152         }
00153         #endregion
00154     }    
00155 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines