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 (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 ()
 

Detailed Description

Array sorts.

Definition at line 23 of file ArraySort.java.

Member Function Documentation

§ getDomain()

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  }

§ getRange()

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  }