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

Datatype sorts.

Definition at line 23 of file DatatypeSort.java.

Member Function Documentation

§ getAccessors()

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  }

§ getConstructors()

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  }

§ getNumConstructors()

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  }

§ getRecognizers()

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  }