18 package com.microsoft.z3;
40 casted =
Sort.class.cast(o);
41 }
catch (ClassCastException e) {
45 return this.getNativeObject() == casted.getNativeObject();
55 return super.hashCode();
80 return Symbol.create(getContext(),
94 return "Z3Exception: " + e.getMessage();
106 void checkNativeObject(
long obj)
108 if (Native.getAstKind(getContext().nCtx(), obj) !=
Z3_ast_kind.Z3_SORT_AST
110 throw new Z3Exception(
"Underlying object is not a sort");
111 super.checkNativeObject(obj);
114 static Sort create(Context ctx,
long obj)
126 return new DatatypeSort(ctx, obj);
132 return new UninterpretedSort(ctx, obj);
134 return new FiniteDomainSort(ctx, obj);
136 return new RelationSort(ctx, obj);
138 return new FPSort(ctx, obj);
140 return new FPRMSort(ctx, obj);
142 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)
Z3_sort_kind getSortKind()
static int getSortId(long a0, long a1)
static String sortToString(long a0, long a1)