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 75 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 45 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 34 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 60 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  }