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

Public Member Functions

FuncDecl mkDecl ()
 
int getNumFields ()
 
FuncDecl [] getFieldDecls ()
 
- 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

Tuple sorts.

Definition at line 23 of file TupleSort.java.

Member Function Documentation

§ getFieldDecls()

FuncDecl [] getFieldDecls ( )
inline

The field declarations.

Exceptions
Z3Exception

Definition at line 48 of file TupleSort.java.

49  {
50 
51  int n = getNumFields();
52  FuncDecl[] res = new FuncDecl[n];
53  for (int i = 0; i < n; i++)
54  res[i] = new FuncDecl(getContext(), Native.getTupleSortFieldDecl(
55  getContext().nCtx(), getNativeObject(), i));
56  return res;
57  }

§ getNumFields()

int getNumFields ( )
inline

The number of fields in the tuple.

Definition at line 39 of file TupleSort.java.

Referenced by TupleSort.getFieldDecls().

40  {
41  return Native.getTupleSortNumFields(getContext().nCtx(), getNativeObject());
42  }

§ mkDecl()

FuncDecl mkDecl ( )
inline

The constructor function of the tuple.

Exceptions
Z3Exception

Definition at line 29 of file TupleSort.java.

30  {
31 
32  return new FuncDecl(getContext(), Native.getTupleSortMkDecl(getContext()
33  .nCtx(), getNativeObject()));
34  }