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()) &&
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");
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
static int getSortKind(long a0, long a1)
static final Z3_sort_kind fromInt(int v)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
static long getSortName(long a0, long a1)
Sort translate(Context ctx)
Z3_sort_kind getSortKind()
static boolean isEqSort(long a0, long a1, long a2)
static int getSortId(long a0, long a1)
static String sortToString(long a0, long a1)