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

Public Member Functions

FuncDecl[] getConstDecls ()
 
FuncDecl getConstDecl (int inx)
 
Expr[] getConsts ()
 
Expr getConst (int inx)
 
FuncDecl[] getTesterDecls ()
 
FuncDecl getTesterDecl (int inx)
 
- 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

Enumeration sorts.

Definition at line 23 of file EnumSort.java.

Member Function Documentation

Expr getConst ( int  inx)
inline

Retrieves the inx'th constant in the enumeration.

Exceptions
Z3Exceptionon error
Returns
an Expr

Definition at line 66 of file EnumSort.java.

67  {
68  return getContext().mkApp(getConstDecl(inx));
69  }
Expr mkApp(FuncDecl f, Expr...args)
Definition: Context.java:610
FuncDecl getConstDecl(int inx)
Definition: EnumSort.java:42
FuncDecl getConstDecl ( int  inx)
inline

Retrieves the inx'th constant declaration in the enumeration.

Exceptions
Z3Exceptionon error

Definition at line 42 of file EnumSort.java.

Referenced by EnumSort.getConst().

43  {
44  return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
45  }
FuncDecl [] getConstDecls ( )
inline

The function declarations of the constants in the enumeration.

Exceptions
Z3Exceptionon error

Definition at line 29 of file EnumSort.java.

Referenced by EnumSort.getConsts().

30  {
31  int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
32  FuncDecl[] t = new FuncDecl[n];
33  for (int i = 0; i < n; i++)
34  t[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
35  return t;
36  }
Expr [] getConsts ( )
inline

The constants in the enumeration.

Exceptions
Z3Exceptionon error
Returns
an Expr[]

Definition at line 52 of file EnumSort.java.

53  {
54  FuncDecl[] cds = getConstDecls();
55  Expr[] t = new Expr[cds.length];
56  for (int i = 0; i < t.length; i++)
57  t[i] = getContext().mkApp(cds[i]);
58  return t;
59  }
FuncDecl[] getConstDecls()
Definition: EnumSort.java:29
Expr mkApp(FuncDecl f, Expr...args)
Definition: Context.java:610
FuncDecl getTesterDecl ( int  inx)
inline

Retrieves the inx'th tester/recognizer declaration in the enumeration.

Exceptions
Z3Exceptionon error

Definition at line 88 of file EnumSort.java.

89  {
90  return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
91  }
FuncDecl [] getTesterDecls ( )
inline

The test predicates for the constants in the enumeration.

Exceptions
Z3Exceptionon error

Definition at line 75 of file EnumSort.java.

76  {
77  int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
78  FuncDecl[] t = new FuncDecl[n];
79  for (int i = 0; i < n; i++)
80  t[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
81  return t;
82  }