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

Public Member Functions

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

Protected Member Functions

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

Detailed Description

Constructors are used for datatype sorts.

Definition at line 23 of file Constructor.java.

Member Function Documentation

FuncDecl ConstructorDecl ( )
inline

The function declaration of the constructor.

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 41 of file Constructor.java.

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

Destructor.

Exceptions
Z3Exceptionon error

Definition at line 85 of file Constructor.java.

86  {
87  Native.delConstructor(getContext().nCtx(), getNativeObject());
88  }
FuncDecl [] getAccessorDecls ( )
inline

The function declarations of the accessors

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 69 of file Constructor.java.

70  {
71  Native.LongPtr constructor = new Native.LongPtr();
72  Native.LongPtr tester = new Native.LongPtr();
73  long[] accessors = new long[n];
74  Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
75  FuncDecl[] t = new FuncDecl[n];
76  for (int i = 0; i < n; i++)
77  t[i] = new FuncDecl(getContext(), accessors[i]);
78  return t;
79  }
int getNumFields ( )
inline

The number of fields of the constructor.

Exceptions
Z3Exception
Z3Exceptionon error
Returns
an int

Definition at line 31 of file Constructor.java.

32  {
33  return n;
34  }
FuncDecl getTesterDecl ( )
inline

The function declaration of the tester.

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 55 of file Constructor.java.

56  {
57  Native.LongPtr constructor = new Native.LongPtr();
58  Native.LongPtr tester = new Native.LongPtr();
59  long[] accessors = new long[n];
60  Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
61  return new FuncDecl(getContext(), tester.value);
62  }