Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Sort.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Sort.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Sorts
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-15
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Diagnostics.Contracts;
22 
23 namespace Microsoft.Z3
24 {
28  [ContractVerification(true)]
29  public class Sort : AST
30  {
38  public static bool operator ==(Sort a, Sort b)
39  {
40  return Object.ReferenceEquals(a, b) ||
41  (!Object.ReferenceEquals(a, null) &&
42  !Object.ReferenceEquals(b, null) &&
43  a.Context == b.Context &&
44  Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
45  }
46 
54  public static bool operator !=(Sort a, Sort b)
55  {
56  return !(a == b);
57  }
58 
64  public override bool Equals(object o)
65  {
66  Sort casted = o as Sort;
67  if (casted == null) return false;
68  return this == casted;
69  }
70 
75  public override int GetHashCode()
76  {
77  return base.GetHashCode();
78  }
79 
83  new public uint Id
84  {
85  get { return Native.Z3_get_sort_id(Context.nCtx, NativeObject); }
86  }
87 
91  public Z3_sort_kind SortKind
92  {
93  get { return (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, NativeObject); }
94  }
95 
99  public Symbol Name
100  {
101  get
102  {
103  Contract.Ensures(Contract.Result<Symbol>() != null);
104  return Symbol.Create(Context, Native.Z3_get_sort_name(Context.nCtx, NativeObject));
105  }
106  }
107 
111  public override string ToString()
112  {
113  return Native.Z3_sort_to_string(Context.nCtx, NativeObject);
114  }
115 
116  #region Internal
117  internal protected Sort(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
121  internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
122 
123 #if DEBUG
124  internal override void CheckNativeObject(IntPtr obj)
125  {
126  if (Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_SORT_AST)
127  throw new Z3Exception("Underlying object is not a sort");
128  base.CheckNativeObject(obj);
129  }
130 #endif
131 
132  [ContractVerification(true)]
133  new internal static Sort Create(Context ctx, IntPtr obj)
134  {
135  Contract.Requires(ctx != null);
136  Contract.Ensures(Contract.Result<Sort>() != null);
137 
138  switch ((Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, obj))
139  {
140  case Z3_sort_kind.Z3_ARRAY_SORT: return new ArraySort(ctx, obj);
141  case Z3_sort_kind.Z3_BOOL_SORT: return new BoolSort(ctx, obj);
142  case Z3_sort_kind.Z3_BV_SORT: return new BitVecSort(ctx, obj);
143  case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeSort(ctx, obj);
144  case Z3_sort_kind.Z3_INT_SORT: return new IntSort(ctx, obj);
145  case Z3_sort_kind.Z3_REAL_SORT: return new RealSort(ctx, obj);
146  case Z3_sort_kind.Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj);
147  case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj);
148  case Z3_sort_kind.Z3_RELATION_SORT: return new RelationSort(ctx, obj);
149  default:
150  throw new Z3Exception("Unknown sort kind");
151  }
152  }
153  #endregion
154  }
155 }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
def RealSort
Definition: z3py.py:2630
static IntPtr Z3_get_sort_name(Z3_context a0, Z3_sort a1)
Definition: Native.cs:2918
def IntSort
Definition: z3py.py:2614
def BoolSort
Definition: z3py.py:1325
def BitVecSort
Definition: z3py.py:3435
static uint Z3_get_sort_kind(Z3_context a0, Z3_sort a1)
Definition: Native.cs:2950
static uint Z3_get_sort_id(Z3_context a0, Z3_sort a1)
Definition: Native.cs:2926
Z3_sort_kind
Z3_sort_kind
Definition: Enumerations.cs:34
def ArraySort
Definition: z3py.py:3955
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
static int Z3_is_eq_sort(Z3_context a0, Z3_sort a1, Z3_sort a2)
Definition: Native.cs:2942
override int GetHashCode()
Hash code generation for Sorts
Definition: Sort.cs:75
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
override bool Equals(object o)
Equality operator for objects of type Sort.
Definition: Sort.cs:64
The abstract syntax tree (AST) class.
Definition: AST.cs:31
static string Z3_sort_to_string(Z3_context a0, Z3_sort a1)
Definition: Native.cs:3848
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
override string ToString()
A string representation of the sort.
Definition: Sort.cs:111