Z3
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 Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
121 
122 #if DEBUG
123  internal override void CheckNativeObject(IntPtr obj)
124  {
125  if (Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_SORT_AST)
126  throw new Z3Exception("Underlying object is not a sort");
127  base.CheckNativeObject(obj);
128  }
129 #endif
130 
131  [ContractVerification(true)]
132  new internal static Sort Create(Context ctx, IntPtr obj)
133  {
134  Contract.Requires(ctx != null);
135  Contract.Ensures(Contract.Result<Sort>() != null);
136 
137  switch ((Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, obj))
138  {
139  case Z3_sort_kind.Z3_ARRAY_SORT: return new ArraySort(ctx, obj);
140  case Z3_sort_kind.Z3_BOOL_SORT: return new BoolSort(ctx, obj);
141  case Z3_sort_kind.Z3_BV_SORT: return new BitVecSort(ctx, obj);
142  case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeSort(ctx, obj);
143  case Z3_sort_kind.Z3_INT_SORT: return new IntSort(ctx, obj);
144  case Z3_sort_kind.Z3_REAL_SORT: return new RealSort(ctx, obj);
145  case Z3_sort_kind.Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj);
146  case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj);
147  case Z3_sort_kind.Z3_RELATION_SORT: return new RelationSort(ctx, obj);
148  case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPSort(ctx, obj);
149  case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMSort(ctx, obj);
150  default:
151  throw new Z3Exception("Unknown sort kind");
152  }
153  }
154  #endregion
155  }
156 }
static IntPtr Z3_get_sort_name(Z3_context a0, Z3_sort a1)
Definition: Native.cs:3198
using System
def RealSort(ctx=None)
Definition: z3py.py:2655
static uint Z3_get_sort_kind(Z3_context a0, Z3_sort a1)
Definition: Native.cs:3230
static uint Z3_get_sort_id(Z3_context a0, Z3_sort a1)
Definition: Native.cs:3206
Z3_sort_kind
Z3_sort_kind
Definition: Enumerations.cs:34
Z3_ast_kind
Z3_ast_kind
Definition: Enumerations.cs:50
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6389
The FloatingPoint RoundingMode sort
Definition: FPRMSort.cs:28
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
static int Z3_is_eq_sort(Z3_context a0, Z3_sort a1, Z3_sort a2)
Definition: Native.cs:3222
def ArraySort(d, r)
Definition: z3py.py:4004
def IntSort(ctx=None)
Definition: z3py.py:2639
static uint Z3_get_ast_kind(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3590
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 exception base class for error reporting from Z3
Definition: Z3Exception.cs:27
The abstract syntax tree (AST) class.
Definition: AST.cs:31
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3460
static string Z3_sort_to_string(Z3_context a0, Z3_sort a1)
Definition: Native.cs:4152
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
def BoolSort(ctx=None)
Definition: z3py.py:1346
override string ToString()
A string representation of the sort.
Definition: Sort.cs:111