Z3
Public Member Functions | Protected Member Functions
Constructor Class Reference
+ Inheritance diagram for Constructor:

Public Member Functions

int getNumFields () throws Z3Exception
 
FuncDecl ConstructorDecl () throws Z3Exception
 
FuncDecl getTesterDecl () throws Z3Exception
 
FuncDecl[] getAccessorDecls () throws Z3Exception
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Protected Member Functions

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

Detailed Description

Constructors are used for datatype sorts.

Definition at line 23 of file Constructor.java.

Member Function Documentation

FuncDecl ConstructorDecl ( ) throws Z3Exception
inline

The function declaration of the constructor.

Exceptions
Z3Exception

Definition at line 38 of file Constructor.java.

39  {
40  Native.LongPtr constructor = new Native.LongPtr();
41  Native.LongPtr tester = new Native.LongPtr();
42  long[] accessors = new long[n];
43  Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
44  return new FuncDecl(getContext(), constructor.value);
45  }
void finalize ( ) throws Z3Exception
inlineprotected

Destructor.

Definition at line 79 of file Constructor.java.

80  {
81  Native.delConstructor(getContext().nCtx(), getNativeObject());
82  }
FuncDecl [] getAccessorDecls ( ) throws Z3Exception
inline

The function declarations of the accessors

Exceptions
Z3Exception

Definition at line 64 of file Constructor.java.

65  {
66  Native.LongPtr constructor = new Native.LongPtr();
67  Native.LongPtr tester = new Native.LongPtr();
68  long[] accessors = new long[n];
69  Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
70  FuncDecl[] t = new FuncDecl[n];
71  for (int i = 0; i < n; i++)
72  t[i] = new FuncDecl(getContext(), accessors[i]);
73  return t;
74  }
int getNumFields ( ) throws Z3Exception
inline

The number of fields of the constructor.

Exceptions
Z3Exception

Definition at line 29 of file Constructor.java.

30  {
31  return n;
32  }
FuncDecl getTesterDecl ( ) throws Z3Exception
inline

The function declaration of the tester.

Exceptions
Z3Exception

Definition at line 51 of file Constructor.java.

52  {
53  Native.LongPtr constructor = new Native.LongPtr();
54  Native.LongPtr tester = new Native.LongPtr();
55  long[] accessors = new long[n];
56  Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
57  return new FuncDecl(getContext(), tester.value);
58  }