Z3 |

Public Member Functions
Sort Class Reference
Inheritance diagram for Sort:

## Public Member Functions
boolean | equals (Object o)
int | hashCode ()
int | getId ()
Z3_sort_kind | getSortKind ()
Symbol | getName ()
String | toString ()
Sort | translate (Context ctx)
Public Member Functions inherited from AST
boolean | equals (Object o)
int | compareTo (AST other)
int | hashCode ()
int | getId ()
AST | translate (Context ctx)
Z3_ast_kind | getASTKind ()
boolean | isExpr ()
boolean | isApp ()
boolean | isVar ()
boolean | isQuantifier ()
boolean | isSort ()
boolean | isFuncDecl ()
String | toString ()
String | getSExpr ()

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## Detailed Description

The Sort class implements type information for ASTs.

Definition at line 26 of file Sort.java.

## Member Function Documentation

## ◆ equals()

boolean equals | ( | Object | o | ) |
| inline

Equality operator for objects of type Sort.

Reimplemented from AST.

Definition at line 32 of file Sort.java.

33 {
34 if (o == this) return true;
35 if (!(o instanceof Sort)) return false;
36 Sort other = (Sort) o;
37
38 return (getContext().nCtx() == other.getContext().nCtx()) &&
39 (Native.isEqSort(getContext().nCtx(), getNativeObject(), other.getNativeObject()));
40 }
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:4008

## ◆ getId()

int getId | ( |  | ) |
| inline

Returns a unique identifier for the sort.

Reimplemented from AST.

Definition at line 55 of file Sort.java.

56 {
57 return Native.getSortId(getContext().nCtx(), getNativeObject());
58 }

## ◆ getName()

Symbol getName | ( |  | ) |
| inline

The name of the sort

Definition at line 72 of file Sort.java.

73 {
74 return Symbol.create(getContext(),
75 Native.getSortName(getContext().nCtx(), getNativeObject()));
76 }

## ◆ getSortKind()

Z3_sort_kind getSortKind | ( |  | ) |
| inline

The kind of the sort.

Definition at line 63 of file Sort.java.

64 {
65 return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(),
66 getNativeObject()));
67 }
Z3_sort_kind
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:150

## ◆ hashCode()

int hashCode | ( |  | ) |
| inline

Hash code generation for Sorts

Returns
  A hash code

Reimplemented from AST.

Definition at line 47 of file Sort.java.

48 {
49 return super.hashCode();
50 }

## ◆ toString()

String toString | ( |  | ) |
| inline

A string representation of the sort.

Reimplemented from AST.

Definition at line 82 of file Sort.java.

82 {
83 return Native.sortToString(getContext().nCtx(), getNativeObject());
84 }

## ◆ translate()

Sort translate | ( | Context | ctx | ) |
| inline

Translates (copies) the sort to the Context `ctx`.

Parameters

  ctx | A context

Returns
  A copy of the sort which is associated with `ctx`

Exceptions

  Z3Exception | on error

Reimplemented from AST.

Definition at line 94 of file Sort.java.

95 {
96 return (Sort) super.translate(ctx);
97 }

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Solver.__deepcopy__(), and Sort.translate().