Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
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 }