18 package com.microsoft.z3;
34 if (o ==
this)
return true;
35 if (!(o instanceof
Sort))
return false;
36 Sort other = (Sort) o;
38 return (getContext().nCtx() == other.getContext().nCtx()) &&
42 other.getNativeObject()
53 return super.hashCode();
78 return Symbol.create(getContext(),
99 void checkNativeObject(
long obj)
103 throw new Z3Exception(
"Underlying object is not a sort");
104 super.checkNativeObject(obj);
131 return new FPSort(ctx, obj);
137 return new ReSort(ctx, obj);
static int getSortKind(long a0, long a1)
static final Z3_sort_kind fromInt(int v)
def FiniteDomainSort(name, sz, ctx=None)
static long getSortName(long a0, long a1)
def FPSort(ebits, sbits, ctx=None)
Z3_sort_kind getSortKind()
static boolean isEqSort(long a0, long a1, long a2)
def BitVecSort(sz, ctx=None)
static int getAstKind(long a0, long a1)
static int getSortId(long a0, long a1)
static String sortToString(long a0, long a1)
def String(name, ctx=None)