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 }

◆ 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
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
ctxA context
Returns
A copy of the sort which is associated with ctx
Exceptions
Z3Exceptionon 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().