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);
64 public override bool Equals(
object o)
67 if (casted == null)
return false;
68 return this == casted;
77 return base.GetHashCode();
85 get {
return Native.Z3_get_sort_id(
Context.nCtx, NativeObject); }
103 Contract.Ensures(Contract.Result<
Symbol>() != null);
113 return Native.Z3_sort_to_string(
Context.nCtx, NativeObject);
117 internal Sort(
Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
123 internal override void CheckNativeObject(IntPtr obj)
126 throw new Z3Exception(
"Underlying object is not a sort");
127 base.CheckNativeObject(obj);
132 new internal static Sort Create(
Context ctx, IntPtr obj)
134 Contract.Requires(ctx != null);
135 Contract.Ensures(Contract.Result<
Sort>() != null);
137 switch ((
Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, obj))
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
expr operator!=(expr const &a, expr const &b)
def FiniteDomainSort(name, sz, ctx=None)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
The FloatingPoint RoundingMode sort
def FPSort(ebits, sbits, ctx=None)
expr operator==(expr const &a, expr const &b)
override int GetHashCode()
Hash code generation for Sorts
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.
The exception base class for error reporting from Z3
The abstract syntax tree (AST) class.
def BitVecSort(sz, ctx=None)
Symbols are used to name several term and type constructors.
override string ToString()
A string representation of the sort.