18package com.microsoft.z3;
20import com.microsoft.z3.enumerations.Z3_ast_kind;
21import com.microsoft.z3.enumerations.Z3_sort_kind;
34 if (o ==
this)
return true;
35 if (!(o instanceof
Sort))
return false;
38 return (getContext().nCtx() == other.getContext().nCtx()) &&
39 (
Native.
isEqSort(getContext().nCtx(), getNativeObject(), other.getNativeObject()));
49 return super.hashCode();
74 return Symbol.create(getContext(),
108 void checkNativeObject(
long obj)
110 if (Native.getAstKind(getContext().nCtx(), obj) !=
Z3_ast_kind.Z3_SORT_AST
112 throw new Z3Exception(
"Underlying object is not a sort");
113 super.checkNativeObject(obj);
116 static Sort create(Context ctx,
long obj)
128 return new DatatypeSort(ctx, obj);
134 return new UninterpretedSort(ctx, obj);
138 return new RelationSort(ctx, obj);
140 return new FPSort(ctx, obj);
142 return new FPRMSort(ctx, obj);
146 return new ReSort(ctx, obj);
148 throw new Z3Exception(
"Unknown sort kind");
static int getSortKind(long a0, long a1)
static String sortToString(long a0, long a1)
static long getSortName(long a0, long a1)
static boolean isEqSort(long a0, long a1, long a2)
static int getSortId(long a0, long a1)
Z3_sort_kind getSortKind()
Sort translate(Context ctx)
static final Z3_sort_kind fromInt(int v)
def String(name, ctx=None)
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).