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

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

Finite domain sorts.

Definition at line 23 of file FiniteDomainSort.java.

Member Function Documentation

§ getSize()

long getSize ( )
inline

The size of the finite domain sort.

Exceptions
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  }