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 ()
 
- Public Member Functions inherited from AST
boolean equals (Object o)
 
int compareTo (Object 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 ()
 
- Public Member Functions inherited from Z3Object
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize ()
 

Detailed Description

The Sort class implements type information for ASTs.

Definition at line 26 of file Sort.java.

Member Function Documentation

boolean equals ( Object  o)
inline

Equality operator for objects of type Sort.

Parameters
o
Returns

Definition at line 33 of file Sort.java.

34  {
35  Sort casted = null;
36 
37  try {
38  casted = Sort.class.cast(o);
39  } catch (ClassCastException e) {
40  return false;
41  }
42 
43  return
44  (this == casted) ||
45  (this != null) &&
46  (casted != null) &&
47  (getContext().nCtx() == casted.getContext().nCtx()) &&
48  (Native.isEqSort(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
49  }
int getId ( )
inline

Returns a unique identifier for the sort.

Definition at line 64 of file Sort.java.

65  {
66  return Native.getSortId(getContext().nCtx(), getNativeObject());
67  }
Symbol getName ( )
inline

The name of the sort

Definition at line 81 of file Sort.java.

82  {
83  return Symbol.create(getContext(),
84  Native.getSortName(getContext().nCtx(), getNativeObject()));
85  }
Z3_sort_kind getSortKind ( )
inline

The kind of the sort.

Definition at line 72 of file Sort.java.

73  {
74  return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(),
75  getNativeObject()));
76  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:194
int hashCode ( )
inline

Hash code generation for Sorts

Returns
A hash code

Definition at line 56 of file Sort.java.

57  {
58  return super.hashCode();
59  }
String toString ( )
inline

A string representation of the sort.

Definition at line 90 of file Sort.java.

91  {
92  try
93  {
94  return Native.sortToString(getContext().nCtx(), getNativeObject());
95  } catch (Z3Exception e)
96  {
97  return "Z3Exception: " + e.getMessage();
98  }
99  }