Z3
src/api/dotnet/Pattern.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Pattern.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Patterns
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-16
00015 
00016 Notes:
00017     
00018 --*/
00019 
00020 using System;
00021 using System.Runtime.InteropServices;
00022 using System.Diagnostics.Contracts;
00023 
00024 namespace Microsoft.Z3
00025 {
00031     [ContractVerification(true)]
00032     public class Pattern : AST
00033     {
00037         public uint NumTerms
00038         {
00039             get { return Native.Z3_get_pattern_num_terms(Context.nCtx, NativeObject); }
00040         }
00041 
00045         public Expr[] Terms
00046         {
00047             get
00048             {
00049                 Contract.Ensures(Contract.Result<Expr[]>() != null);
00050 
00051                 uint n = NumTerms;
00052                 Expr[] res = new Expr[n];
00053                 for (uint i = 0; i < n; i++)
00054                     res[i] = Expr.Create(Context, Native.Z3_get_pattern(Context.nCtx, NativeObject, i));
00055                 return res;
00056             }
00057         }
00058 
00062         public override string ToString()
00063         {
00064             return Native.Z3_pattern_to_string(Context.nCtx, NativeObject);
00065         }
00066 
00067         #region Internal
00068         internal Pattern(Context ctx, IntPtr obj)
00069             : base(ctx, obj)
00070         {
00071             Contract.Requires(ctx != null);
00072         }
00073         #endregion
00074     }
00075 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines