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

Public Member Functions

int getNumFields ()
 
FuncDecl< DatatypeSort< R > > ConstructorDecl ()
 
FuncDecl< BoolSortgetTesterDecl ()
 
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
Z3Exceptionon 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
Z3Exceptionon 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  }

◆ getNumFields()

int getNumFields ( )
inline

The number of fields of the constructor.

Exceptions
Z3Exception
Z3Exceptionon 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
Z3Exceptionon 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  }
com.microsoft.z3.FuncDecl<?>