Z3
Sort.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 Sort.cs
7
8Abstract:
9
10 Z3 Managed API: Sorts
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-15
15
16Notes:
17
18--*/
19
20using System.Diagnostics;
21using System;
22
23namespace Microsoft.Z3
24{
28 public class Sort : AST
29 {
37 public static bool operator ==(Sort a, Sort b)
38 {
39 return Object.ReferenceEquals(a, b) ||
40 (!Object.ReferenceEquals(a, null) &&
41 !Object.ReferenceEquals(b, null) &&
42 a.Context == b.Context &&
43 0 != Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject));
44 }
45
53 public static bool operator !=(Sort a, Sort b)
54 {
55 return !(a == b);
56 }
57
63 public override bool Equals(object o)
64 {
65 Sort casted = o as Sort;
66 if (casted == null) return false;
67 return this == casted;
68 }
69
74 public override int GetHashCode()
75 {
76 return base.GetHashCode();
77 }
78
82 new public uint Id
83 {
84 get { return Native.Z3_get_sort_id(Context.nCtx, NativeObject); }
85 }
86
91 {
92 get { return (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, NativeObject); }
93 }
94
98 public Symbol Name
99 {
100 get
101 {
102 return Symbol.Create(Context, Native.Z3_get_sort_name(Context.nCtx, NativeObject));
103 }
104 }
105
109 public override string ToString()
110 {
111 return Native.Z3_sort_to_string(Context.nCtx, NativeObject);
112 }
113
119 new public Sort Translate(Context ctx)
120 {
121 return (Sort)base.Translate(ctx);
122 }
123
124 #region Internal
128 internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
129
130#if DEBUG
131 internal override void CheckNativeObject(IntPtr obj)
132 {
133 if (Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_SORT_AST)
134 throw new Z3Exception("Underlying object is not a sort");
135 base.CheckNativeObject(obj);
136 }
137#endif
138
139 new internal static Sort Create(Context ctx, IntPtr obj)
140 {
141 Debug.Assert(ctx != null);
142
143 switch ((Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, obj))
144 {
145 case Z3_sort_kind.Z3_ARRAY_SORT: return new ArraySort(ctx, obj);
146 case Z3_sort_kind.Z3_BOOL_SORT: return new BoolSort(ctx, obj);
147 case Z3_sort_kind.Z3_BV_SORT: return new BitVecSort(ctx, obj);
148 case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeSort(ctx, obj);
149 case Z3_sort_kind.Z3_INT_SORT: return new IntSort(ctx, obj);
150 case Z3_sort_kind.Z3_REAL_SORT: return new RealSort(ctx, obj);
151 case Z3_sort_kind.Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj);
152 case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj);
153 case Z3_sort_kind.Z3_RELATION_SORT: return new RelationSort(ctx, obj);
154 case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPSort(ctx, obj);
155 case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMSort(ctx, obj);
156 case Z3_sort_kind.Z3_SEQ_SORT: return new SeqSort(ctx, obj);
157 case Z3_sort_kind.Z3_RE_SORT: return new ReSort(ctx, obj);
158 default:
159 throw new Z3Exception("Unknown sort kind");
160 }
161 }
162 #endregion
163 }
164}
The abstract syntax tree (AST) class.
Definition: AST.cs:31
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
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:63
new Sort Translate(Context ctx)
Translates (copies) the sort to the Context ctx .
Definition: Sort.cs:119
static bool operator!=(Sort a, Sort b)
Comparison operator.
Definition: Sort.cs:53
override int GetHashCode()
Hash code generation for Sorts
Definition: Sort.cs:74
Z3_sort_kind SortKind
The kind of the sort.
Definition: Sort.cs:91
override string ToString()
A string representation of the sort.
Definition: Sort.cs:109
static bool operator==(Sort a, Sort b)
Comparison operator.
Definition: Sort.cs:37
Symbol Name
The name of the sort
Definition: Sort.cs:99
new uint Id
Returns a unique identifier for the sort.
Definition: Sort.cs:83
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
def IntSort(ctx=None)
Definition: z3py.py:3100
def SeqSort(s)
Definition: z3py.py:10579
def RealSort(ctx=None)
Definition: z3py.py:3117
def ArraySort(*sig)
Definition: z3py.py:4645
def BoolSort(ctx=None)
Definition: z3py.py:1655
def ReSort(s)
Definition: z3py.py:10904
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:7590
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9727
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3967
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:150