Z3
src/api/dotnet/Constructor.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Constructor.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Constructors
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-22
00015 
00016 Notes:
00017     
00018 --*/
00019 
00020 using System;
00021 using System.Diagnostics.Contracts;
00022 
00023 namespace Microsoft.Z3
00024 {
00028     [ContractVerification(true)]
00029     public class Constructor : Z3Object
00030     {
00034         public uint NumFields
00035         {
00036             get
00037             {                
00038                 return n;
00039             }
00040         }
00041 
00045         public FuncDecl ConstructorDecl
00046         {
00047             get
00048             {
00049                 Contract.Ensures(Contract.Result<FuncDecl>() != null);
00050                 IntPtr constructor = IntPtr.Zero;
00051                 IntPtr tester = IntPtr.Zero;
00052                 IntPtr[] accessors = new IntPtr[n];
00053                 Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
00054                 return new FuncDecl(Context, constructor);                
00055             }
00056         }
00057 
00061         public FuncDecl TesterDecl
00062         {
00063             get
00064             {
00065                 Contract.Ensures(Contract.Result<FuncDecl>() != null);
00066                 IntPtr constructor = IntPtr.Zero;
00067                 IntPtr tester = IntPtr.Zero;
00068                 IntPtr[] accessors = new IntPtr[n];
00069                 Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
00070                 return new FuncDecl(Context, tester);                
00071             }
00072         }
00073 
00077         public FuncDecl[] AccessorDecls
00078         {
00079             get
00080             {
00081                 Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
00082                 IntPtr constructor = IntPtr.Zero;
00083                 IntPtr tester = IntPtr.Zero;
00084                 IntPtr[] accessors = new IntPtr[n];
00085                 Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);                
00086                 FuncDecl[] t = new FuncDecl[n];
00087                 for (uint i = 0; i < n; i++)
00088                     t[i] = new FuncDecl(Context, accessors[i]); 
00089                 return t;
00090             }
00091         }
00092 
00096         ~Constructor()
00097         {
00098             Native.Z3_del_constructor(Context.nCtx, NativeObject);
00099         }        
00100 
00101         #region Internal
00102         private uint n = 0;
00103         
00104         internal Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
00105                              Sort[] sorts, uint[] sortRefs)
00106             : base(ctx)
00107         {
00108             Contract.Requires(ctx != null);
00109             Contract.Requires(name != null);
00110             Contract.Requires(recognizer != null);
00111 
00112             n = AST.ArrayLength(fieldNames);
00113 
00114             if (n != AST.ArrayLength(sorts))
00115                 throw new Z3Exception("Number of field names does not match number of sorts");
00116             if (sortRefs != null && sortRefs.Length != n)
00117                 throw new Z3Exception("Number of field names does not match number of sort refs");
00118 
00119             if (sortRefs == null) sortRefs = new uint[n];
00120 
00121             NativeObject = Native.Z3_mk_constructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
00122                                                     n,
00123                                                     Symbol.ArrayToNative(fieldNames),
00124                                                     Sort.ArrayToNative(sorts),
00125                                                     sortRefs);
00126 
00127         }
00128 
00129         #endregion
00130     }
00131 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines