Constructors are used for datatype sorts.
Definition at line 23 of file Constructor.java.
The function declaration of the constructor.
- Exceptions
-
Z3Exception | |
Z3Exception | on error |
Definition at line 47 of file Constructor.java.
49 Native.LongPtr constructor =
new Native.LongPtr();
50 Native.LongPtr tester =
new Native.LongPtr();
51 long[] accessors =
new long[n];
52 Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
53 return new FuncDecl(getContext(), constructor.value);
The function declarations of the accessors
- Exceptions
-
Z3Exception | |
Z3Exception | on error |
Definition at line 75 of file Constructor.java.
77 Native.LongPtr constructor =
new Native.LongPtr();
78 Native.LongPtr tester =
new Native.LongPtr();
79 long[] accessors =
new long[n];
80 Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
81 FuncDecl[] t =
new FuncDecl[n];
82 for (
int i = 0; i < n; i++)
83 t[i] =
new FuncDecl(getContext(), accessors[i]);
The number of fields of the constructor.
- Exceptions
-
Z3Exception | |
Z3Exception | on error |
- Returns
- an int
Definition at line 37 of file Constructor.java.
The function declaration of the tester.
- Exceptions
-
Z3Exception | |
Z3Exception | on error |
Definition at line 61 of file Constructor.java.
63 Native.LongPtr constructor =
new Native.LongPtr();
64 Native.LongPtr tester =
new Native.LongPtr();
65 long[] accessors =
new long[n];
66 Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
67 return new FuncDecl(getContext(), tester.value);