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.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 }