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

Enumeration sorts.

Definition at line 23 of file EnumSort.java.

Member Function Documentation

§ getConst()

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:644
FuncDecl getConstDecl(int inx)
Definition: EnumSort.java:42

§ getConstDecl()

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  }

§ getConstDecls()

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  }

§ getConsts()

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:644

§ getTesterDecl()

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  }

§ getTesterDecls()

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  }