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...
Properties inherited from Z3Object
Context	Context [get]
	Access Context object 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.

        {
            get
            {
                IntPtr constructor = IntPtr.Zero;
                IntPtr tester = IntPtr.Zero;
                IntPtr[] accessors = new IntPtr[n];
                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);                
                FuncDecl[] t = new FuncDecl[n];
                for (uint i = 0; i < n; i++)
                    t[i] = new FuncDecl(Context, accessors[i]); 
                return t;
            }
        }

ConstructorDecl

FuncDecl ConstructorDecl

get

The function declaration of the constructor.

Definition at line 44 of file Constructor.cs.

        {
            get
            {
                IntPtr constructor = IntPtr.Zero;
                IntPtr tester = IntPtr.Zero;
                IntPtr[] accessors = new IntPtr[n];
                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
                return new FuncDecl(Context, constructor);                
            }
        }

NumFields

uint NumFields

get

The number of fields of the constructor.

Definition at line 33 of file Constructor.cs.

        {
            get
            {                
                return n;
            }
        }

TesterDecl

FuncDecl TesterDecl

get

The function declaration of the tester.

Definition at line 59 of file Constructor.cs.

        {
            get
            {
                IntPtr constructor = IntPtr.Zero;
                IntPtr tester = IntPtr.Zero;
                IntPtr[] accessors = new IntPtr[n];
                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
                return new FuncDecl(Context, tester);                
            }
        }