20using System.Diagnostics;
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));
63 public override bool Equals(
object o)
66 if (casted ==
null)
return false;
67 return this == casted;
76 return base.GetHashCode();
84 get {
return Native.Z3_get_sort_id(
Context.nCtx, NativeObject); }
111 return Native.Z3_sort_to_string(
Context.nCtx, NativeObject);
128 internal Sort(
Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx !=
null); }
131 internal override void CheckNativeObject(IntPtr obj)
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);
139 new internal static Sort Create(Context ctx, IntPtr obj)
141 Debug.Assert(ctx !=
null);
143 switch ((
Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, obj))
148 case Z3_sort_kind.Z3_DATATYPE_SORT:
return new DatatypeSort(ctx, obj);
151 case Z3_sort_kind.Z3_UNINTERPRETED_SORT:
return new UninterpretedSort(ctx, obj);
153 case Z3_sort_kind.Z3_RELATION_SORT:
return new RelationSort(ctx, obj);
155 case Z3_sort_kind.Z3_ROUNDING_MODE_SORT:
return new FPRMSort(ctx, obj);
159 throw new Z3Exception(
"Unknown sort kind");
The abstract syntax tree (AST) class.
The main interaction with Z3 happens via the Context.
The Sort class implements type information for ASTs.
override bool Equals(object o)
Equality operator for objects of type Sort.
new Sort Translate(Context ctx)
Translates (copies) the sort to the Context ctx .
static bool operator!=(Sort a, Sort b)
Comparison operator.
override int GetHashCode()
Hash code generation for Sorts
Z3_sort_kind SortKind
The kind of the sort.
override string ToString()
A string representation of the sort.
static bool operator==(Sort a, Sort b)
Comparison operator.
Symbol Name
The name of the sort
new uint Id
Returns a unique identifier for the sort.
Symbols are used to name several term and type constructors.
def FiniteDomainSort(name, sz, ctx=None)
def FPSort(ebits, sbits, ctx=None)
def BitVecSort(sz, ctx=None)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).