Z3 |

Public Member Functions
Constructor< R > Class Template Reference
Inheritance diagram for Constructor< R >:

## Public Member Functions
int | getNumFields ()
FuncDecl< DatatypeSort< R > > | ConstructorDecl ()
FuncDecl< BoolSort > | getTesterDecl ()
FuncDecl<?>[] | getAccessorDecls ()

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## Detailed Description

Constructors are used for datatype sorts.

Definition at line 23 of file Constructor.java.

## Member Function Documentation

## ◆ ConstructorDecl()

FuncDecl< DatatypeSort< R > > ConstructorDecl | ( |  | ) |
| inline

The function declaration of the constructor.

Exceptions

  Z3Exception |
  Z3Exception | on error

Definition at line 47 of file Constructor.java.

48 {
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);
54 }

## ◆ getAccessorDecls()

FuncDecl<?>[] getAccessorDecls | ( |  | ) |
| inline

The function declarations of the accessors

Exceptions

  Z3Exception |
  Z3Exception | on error

Definition at line 75 of file Constructor.java.

76 {
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]);
84 return t;
85 }
com.microsoft.z3.FuncDecl<?>

## ◆ getNumFields()

int getNumFields | ( |  | ) |
| inline

The number of fields of the constructor.

Exceptions

  Z3Exception |
  Z3Exception | on error

Returns
  an int

Definition at line 37 of file Constructor.java.

38 {
39 return n;
40 }

## ◆ getTesterDecl()

FuncDecl< BoolSort > getTesterDecl | ( |  | ) |
| inline

The function declaration of the tester.

Exceptions

  Z3Exception |
  Z3Exception | on error

Definition at line 61 of file Constructor.java.

62 {
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);
68 }