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

Public Member Functions

int getNumConstructors () throws Z3Exception
 
FuncDecl[] getConstructors () throws Z3Exception
 
FuncDecl[] getRecognizers () throws Z3Exception
 
FuncDecl[][] getAccessors () throws Z3Exception
 
- Public Member Functions inherited from Sort
boolean equals (Object o)
 
int hashCode ()
 
int getId () throws Z3Exception
 
Z3_sort_kind getSortKind () throws Z3Exception
 
Symbol getName () throws Z3Exception
 
String toString ()
 
- Public Member Functions inherited from AST
boolean equals (Object o)
 
int compareTo (Object other) throws Z3Exception
 
int hashCode ()
 
int getId () throws Z3Exception
 
AST translate (Context ctx) throws Z3Exception
 
Z3_ast_kind getASTKind () throws Z3Exception
 
boolean isExpr () throws Z3Exception
 
boolean isApp () throws Z3Exception
 
boolean isVar () throws Z3Exception
 
boolean isQuantifier () throws Z3Exception
 
boolean isSort () throws Z3Exception
 
boolean isFuncDecl () throws Z3Exception
 
String toString ()
 
String getSExpr () throws Z3Exception
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Additional Inherited Members

- Protected Member Functions inherited from Sort
 Sort (Context ctx) throws Z3Exception
 
- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

Detailed Description

Datatype sorts.

Definition at line 23 of file DatatypeSort.java.

Member Function Documentation

FuncDecl [][] getAccessors ( ) throws Z3Exception
inline

The constructor accessors.

Exceptions
Z3Exception

Definition at line 69 of file DatatypeSort.java.

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

The constructors.

Exceptions
Z3Exception

Definition at line 39 of file DatatypeSort.java.

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

The number of constructors of the datatype sort.

Definition at line 28 of file DatatypeSort.java.

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

29  {
30  return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
31  getNativeObject());
32  }
FuncDecl [] getRecognizers ( ) throws Z3Exception
inline

The recognizers.

Exceptions
Z3Exception

Definition at line 54 of file DatatypeSort.java.

55  {
56  int n = getNumConstructors();
57  FuncDecl[] res = new FuncDecl[n];
58  for (int i = 0; i < n; i++)
59  res[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(
60  getContext().nCtx(), getNativeObject(), i));
61  return res;
62  }