Z3
Public Member Functions | Protected Member Functions
Sort Class Reference
+ Inheritance diagram for Sort:

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 ()
 
- Public Member Functions inherited from AST
boolean equals (Object o)
 
int compareTo (Object other) throws Z3Exception
 
int hashCode ()
 
int getId () throws Z3Exception
 
AST translate (Context ctx) throws Z3Exception
 
Z3_ast_kind getASTKind () throws Z3Exception
 
boolean isExpr () throws Z3Exception
 
boolean isApp () throws Z3Exception
 
boolean isVar () throws Z3Exception
 
boolean isQuantifier () throws Z3Exception
 
boolean isSort () throws Z3Exception
 
boolean isFuncDecl () throws Z3Exception
 
String toString ()
 
String getSExpr () throws Z3Exception
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Protected Member Functions

 Sort (Context ctx) throws Z3Exception
 
- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

Detailed Description

The Sort class implements type information for ASTs.

Definition at line 26 of file Sort.java.

Constructor & Destructor Documentation

Sort ( Context  ctx) throws Z3Exception
inlineprotected

Sort constructor

Definition at line 101 of file Sort.java.

102  {
103  super(ctx);
104  {
105  }
106  }

Member Function Documentation

boolean equals ( Object  o)
inline

Equality operator for objects of type Sort.

Parameters
o
Returns

Definition at line 35 of file Sort.java.

36  {
37  Sort casted = null;
38 
39  try {
40  casted = Sort.class.cast(o);
41  } catch (ClassCastException e) {
42  return false;
43  }
44 
45  return this.getNativeObject() == casted.getNativeObject();
46  }
Sort(Context ctx)
Definition: Sort.java:101
int getId ( ) throws Z3Exception
inline

Returns a unique identifier for the sort.

Definition at line 61 of file Sort.java.

62  {
63  return Native.getSortId(getContext().nCtx(), getNativeObject());
64  }
Symbol getName ( ) throws Z3Exception
inline

The name of the sort

Definition at line 78 of file Sort.java.

79  {
80  return Symbol.create(getContext(),
81  Native.getSortName(getContext().nCtx(), getNativeObject()));
82  }
Z3_sort_kind getSortKind ( ) throws Z3Exception
inline

The kind of the sort.

Definition at line 69 of file Sort.java.

70  {
71  return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(),
72  getNativeObject()));
73  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
int hashCode ( )
inline

Hash code generation for Sorts

Returns
A hash code

Definition at line 53 of file Sort.java.

54  {
55  return super.hashCode();
56  }
String toString ( )
inline

A string representation of the sort.

Definition at line 87 of file Sort.java.

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