Public Member Functions
FiniteDomainSort< R > Class Template Reference
+ Inheritance diagram for FiniteDomainSort< R >:

Public Member Functions

long getSize ()
- 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)
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 domain sorts.

Definition at line 23 of file FiniteDomainSort.java.

Member Function Documentation

◆ getSize()

long getSize ( )

The size of the finite domain sort.

Z3Exceptionon error

Definition at line 29 of file FiniteDomainSort.java.

30  {
31  Native.LongPtr res = new Native.LongPtr();
32  Native.getFiniteDomainSortSize(getContext().nCtx(), getNativeObject(), res);
33  return res.value;
34  }