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();
57 return Native.getSortId(getContext().nCtx(), getNativeObject());
65 return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(),
74 return Symbol.create(getContext(),
75 Native.getSortName(getContext().nCtx(), getNativeObject()));
83 return Native.sortToString(getContext().nCtx(), getNativeObject());
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)
122 return new ArraySort<>(ctx, 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);
144 return new SeqSort<>(ctx, obj);
146 return new ReSort<>(ctx, obj);
148 throw new Z3Exception(
"Unknown sort kind");
Z3_sort_kind getSortKind()
Sort translate(Context ctx)
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).