21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
40 return Object.ReferenceEquals(a, b) ||
41 (!Object.ReferenceEquals(a, null) &&
42 !Object.ReferenceEquals(b, null) &&
43 a.Context == b.Context &&
64 public override bool Equals(
object o)
67 if (casted == null)
return false;
68 return this == casted;
77 return base.GetHashCode();
103 Contract.Ensures(Contract.Result<
Symbol>() != null);
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);
131 [ContractVerification(
true)]
132 new internal static Sort Create(
Context ctx, IntPtr obj)
134 Contract.Requires(ctx != null);
135 Contract.Ensures(Contract.Result<
Sort>() != null);
static IntPtr Z3_get_sort_name(Z3_context a0, Z3_sort a1)
static uint Z3_get_sort_kind(Z3_context a0, Z3_sort a1)
static uint Z3_get_sort_id(Z3_context a0, Z3_sort a1)
def FiniteDomainSort(name, sz, ctx=None)
The FloatingPoint RoundingMode sort
def FPSort(ebits, sbits, ctx=None)
static int Z3_is_eq_sort(Z3_context a0, Z3_sort a1, Z3_sort a2)
static uint Z3_get_ast_kind(Z3_context a0, Z3_ast a1)
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)
static string Z3_sort_to_string(Z3_context a0, Z3_sort a1)
Symbols are used to name several term and type constructors.
override string ToString()
A string representation of the sort.