Z3
Public Member Functions
ArraySort Class Reference
+ Inheritance diagram for ArraySort:

Public Member Functions

Sort getDomain ()
 
Sort getRange ()
 
- Public Member Functions inherited from Sort
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

Array sorts.

Definition at line 23 of file ArraySort.java.

Member Function Documentation

Sort getDomain ( )
inline

The domain of the array sort.

Exceptions
Z3Exception
Z3Exceptionon error
Returns
a sort

Definition at line 31 of file ArraySort.java.

32  {
33  return Sort.create(getContext(),
34  Native.getArraySortDomain(getContext().nCtx(), getNativeObject()));
35  }
Sort getRange ( )
inline

The range of the array sort.

Exceptions
Z3Exception
Z3Exceptionon error
Returns
a sort

Definition at line 43 of file ArraySort.java.

44  {
45  return Sort.create(getContext(),
46  Native.getArraySortRange(getContext().nCtx(), getNativeObject()));
47  }