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();
115 void checkNativeObject(
long obj)
throws Z3Exception
117 if (Native.getAstKind(getContext().nCtx(), obj) !=
Z3_ast_kind.Z3_SORT_AST
119 throw new Z3Exception(
"Underlying object is not a sort");
120 super.checkNativeObject(obj);
123 static Sort create(Context ctx,
long obj)
throws Z3Exception
135 return new DatatypeSort(ctx, obj);
141 return new UninterpretedSort(ctx, obj);
143 return new FiniteDomainSort(ctx, obj);
145 return new RelationSort(ctx, obj);
147 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)