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

Public Member Functions

int getNumConstructors ()
 
FuncDecl[] getConstructors ()
 
FuncDecl[] getRecognizers ()
 
FuncDecl[][] getAccessors ()
 
- 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

Datatype sorts.

Definition at line 23 of file DatatypeSort.java.

Member Function Documentation

FuncDecl [][] getAccessors ( )
inline

The constructor accessors.

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 74 of file DatatypeSort.java.

75  {
76 
77  int n = getNumConstructors();
78  FuncDecl[][] res = new FuncDecl[n][];
79  for (int i = 0; i < n; i++)
80  {
81  FuncDecl fd = new FuncDecl(getContext(),
82  Native.getDatatypeSortConstructor(getContext().nCtx(),
83  getNativeObject(), i));
84  int ds = fd.getDomainSize();
85  FuncDecl[] tmp = new FuncDecl[ds];
86  for (int j = 0; j < ds; j++)
87  tmp[j] = new FuncDecl(getContext(),
88  Native.getDatatypeSortConstructorAccessor(getContext()
89  .nCtx(), getNativeObject(), i, j));
90  res[i] = tmp;
91  }
92  return res;
93  }
FuncDecl [] getConstructors ( )
inline

The constructors.

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 42 of file DatatypeSort.java.

43  {
44  int n = getNumConstructors();
45  FuncDecl[] res = new FuncDecl[n];
46  for (int i = 0; i < n; i++)
47  res[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(
48  getContext().nCtx(), getNativeObject(), i));
49  return res;
50  }
int getNumConstructors ( )
inline

The number of constructors of the datatype sort.

Exceptions
Z3Exceptionon error
Returns
an int

Definition at line 30 of file DatatypeSort.java.

Referenced by DatatypeSort.getAccessors(), DatatypeSort.getConstructors(), and DatatypeSort.getRecognizers().

31  {
32  return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
33  getNativeObject());
34  }
FuncDecl [] getRecognizers ( )
inline

The recognizers.

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 58 of file DatatypeSort.java.

59  {
60  int n = getNumConstructors();
61  FuncDecl[] res = new FuncDecl[n];
62  for (int i = 0; i < n; i++)
63  res[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(
64  getContext().nCtx(), getNativeObject(), i));
65  return res;
66  }