Constructor.cs

Go to the documentation of this file.

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    Constructor.cs

Abstract:

    Z3 Managed API: Constructors

Author:

    Christoph Wintersteiger (cwinter) 2012-03-22

Notes:
    
--*/

using System;
using System.Diagnostics.Contracts;

namespace Microsoft.Z3
{
    [ContractVerification(true)]
    public class Constructor : Z3Object
    {
        public uint NumFields
        {
            get
            {                
                return n;
            }
        }

        public FuncDecl ConstructorDecl
        {
            get
            {
                Contract.Ensures(Contract.Result<FuncDecl>() != null);
                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);                
            }
        }

        public FuncDecl TesterDecl
        {
            get
            {
                Contract.Ensures(Contract.Result<FuncDecl>() != null);
                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);                
            }
        }

        public FuncDecl[] AccessorDecls
        {
            get
            {
                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
                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;
            }
        }

        ~Constructor()
        {
            Native.Z3_del_constructor(Context.nCtx, NativeObject);
        }        

        #region Internal
        private uint n = 0;
        
        internal Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
                             Sort[] sorts, uint[] sortRefs)
            : base(ctx)
        {
            Contract.Requires(ctx != null);
            Contract.Requires(name != null);
            Contract.Requires(recognizer != null);

            n = AST.ArrayLength(fieldNames);

            if (n != AST.ArrayLength(sorts))
                throw new Z3Exception("Number of field names does not match number of sorts");
            if (sortRefs != null && sortRefs.Length != n)
                throw new Z3Exception("Number of field names does not match number of sort refs");

            if (sortRefs == null) sortRefs = new uint[n];

            NativeObject = Native.Z3_mk_constructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
                                                    n,
                                                    Symbol.ArrayToNative(fieldNames),
                                                    Sort.ArrayToNative(sorts),
                                                    sortRefs);

        }

        #endregion
    }
}