Public Member Functions | |
boolean | equals (Object o) |
int | hashCode () |
int | getId () throws Z3Exception |
Z3_sort_kind | getSortKind () throws Z3Exception |
Symbol | getName () throws Z3Exception |
String | toString () |
Protected Member Functions | |
Sort (Context ctx) throws Z3Exception | |
Package Functions | |
Sort (Context ctx, long obj) throws Z3Exception | |
void | checkNativeObject (long obj) throws Z3Exception |
Static Package Functions | |
static Sort | create (Context ctx, long obj) throws Z3Exception |
Sort | ( | Context | ctx | ) | throws Z3Exception [inline, protected] |
Sort | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
void checkNativeObject | ( | long | obj | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 115 of file Sort.java.
{ if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_SORT_AST .toInt()) throw new Z3Exception("Underlying object is not a sort"); super.checkNativeObject(obj); }
static Sort create | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, static, package] |
Reimplemented from AST.
Definition at line 123 of file Sort.java.
Referenced by AST.create(), Quantifier.getBoundVariableSorts(), RelationSort.getColumnSorts(), ArraySort.getDomain(), FuncDecl.getDomain(), FuncDecl.getParameters(), ArraySort.getRange(), FuncDecl.getRange(), Context.getSMTLIBSorts(), Expr.getSort(), and Model.getSorts().
{ Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj)); switch (sk) { case Z3_ARRAY_SORT: return new ArraySort(ctx, obj); case Z3_BOOL_SORT: return new BoolSort(ctx, obj); case Z3_BV_SORT: return new BitVecSort(ctx, obj); case Z3_DATATYPE_SORT: return new DatatypeSort(ctx, obj); case Z3_INT_SORT: return new IntSort(ctx, obj); case Z3_REAL_SORT: return new RealSort(ctx, obj); case Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj); case Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj); case Z3_RELATION_SORT: return new RelationSort(ctx, obj); default: throw new Z3Exception("Unknown sort kind"); } }
boolean equals | ( | Object | o | ) | [inline] |
int getId | ( | ) | throws Z3Exception [inline] |
Returns a unique identifier for the sort.
Reimplemented from AST.
Definition at line 61 of file Sort.java.
{ return Native.getSortId(getContext().nCtx(), getNativeObject()); }
Symbol getName | ( | ) | throws Z3Exception [inline] |
The name of the sort
Definition at line 78 of file Sort.java.
{ return Symbol.create(getContext(), Native.getSortName(getContext().nCtx(), getNativeObject())); }
Z3_sort_kind getSortKind | ( | ) | throws Z3Exception [inline] |
The kind of the sort.
Definition at line 69 of file Sort.java.
{ return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(), getNativeObject())); }
int hashCode | ( | ) | [inline] |
String toString | ( | ) | [inline] |
A string representation of the sort.
Reimplemented from AST.
Definition at line 87 of file Sort.java.
{ try { return Native.sortToString(getContext().nCtx(), getNativeObject()); } catch (Z3Exception e) { return "Z3Exception: " + e.getMessage(); } }