Z3 |

Properties
Constructor Class Reference

Constructors are used for datatype sorts. More...

Inheritance diagram for Constructor:

## Properties
uint | NumFields`[get]`
| The number of fields of the constructor. More...
FuncDecl | ConstructorDecl`[get]`
| The function declaration of the constructor. More...
FuncDecl | TesterDecl`[get]`
| The function declaration of the tester. More...
FuncDecl[] | AccessorDecls`[get]`
| The function declarations of the accessors More...

## Additional Inherited Members
Public Member Functions inherited from Z3Object
void | Dispose ()
| Disposes of the underlying native Z3 object. More...

## Detailed Description

Constructors are used for datatype sorts.

Definition at line 28 of file Constructor.cs.

## Property Documentation

## ◆ AccessorDecls

FuncDecl [] AccessorDecls
| get

The function declarations of the accessors

Definition at line 74 of file Constructor.cs.

75 {
76 get
77 {
78 IntPtr constructor = IntPtr.Zero;
79 IntPtr tester = IntPtr.Zero;
80 IntPtr[] accessors = new IntPtr[n];
81 Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
82 FuncDecl[] t = new FuncDecl[n];
83 for (uint i = 0; i < n; i++)
84 t[i] = new FuncDecl(Context, accessors[i]);
85 return t;
86 }
87 }

## ◆ ConstructorDecl

FuncDecl ConstructorDecl
| get

The function declaration of the constructor.

Definition at line 44 of file Constructor.cs.

45 {
46 get
47 {
48 IntPtr constructor = IntPtr.Zero;
49 IntPtr tester = IntPtr.Zero;
50 IntPtr[] accessors = new IntPtr[n];
51 Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
52 return new FuncDecl(Context, constructor);
53 }
54 }

## ◆ NumFields

uint NumFields
| get

The number of fields of the constructor.

Definition at line 33 of file Constructor.cs.

34 {
35 get
36 {
37 return n;
38 }
39 }

## ◆ TesterDecl

FuncDecl TesterDecl
| get

The function declaration of the tester.

Definition at line 59 of file Constructor.cs.

60 {
61 get
62 {
63 IntPtr constructor = IntPtr.Zero;
64 IntPtr tester = IntPtr.Zero;
65 IntPtr[] accessors = new IntPtr[n];
66 Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
67 return new FuncDecl(Context, tester);
68 }
69 }