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
int compareTo (AST other)
 
Z3_ast_kind getASTKind ()
 
boolean isExpr ()
 
boolean isApp ()
 
boolean isVar ()
 
boolean isQuantifier ()
 
boolean isSort ()
 
boolean isFuncDecl ()
 
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  }

◆ 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 Sort.translate().

com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:3992
Z3_sort_kind
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:149