Z3
 
Loading...
Searching...
No Matches
Public Member Functions
FiniteSetSort Class Reference
+ Inheritance diagram for FiniteSetSort:

Public Member Functions

Sort getBasis ()
 
- Public Member Functions inherited from Sort
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)
 
int getDepth ()
 
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

Finite set sorts.

Definition at line 23 of file FiniteSetSort.java.

Member Function Documentation

◆ getBasis()

Sort getBasis ( )
inline

Get the element sort (basis) of this finite set sort.

Definition at line 38 of file FiniteSetSort.java.

39 {
40 return Sort.create(getContext(), Native.getFiniteSetSortBasis(getContext().nCtx(), getNativeObject()));
41 }
final Sort getFiniteSetSortBasis(Sort s)