Z3
Pattern.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 Pattern.cs
7
8Abstract:
9
10 Z3 Managed API: Patterns
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-16
15
16Notes:
17
18--*/
19
20using System.Diagnostics;
21using System;
22using System.Runtime.InteropServices;
23
24namespace Microsoft.Z3
25{
31 public class Pattern : AST
32 {
36 public uint NumTerms
37 {
38 get { return Native.Z3_get_pattern_num_terms(Context.nCtx, NativeObject); }
39 }
40
44 public Expr[] Terms
45 {
46 get
47 {
48
49 uint n = NumTerms;
50 Expr[] res = new Expr[n];
51 for (uint i = 0; i < n; i++)
52 res[i] = Expr.Create(Context, Native.Z3_get_pattern(Context.nCtx, NativeObject, i));
53 return res;
54 }
55 }
56
60 public override string ToString()
61 {
62 return Native.Z3_pattern_to_string(Context.nCtx, NativeObject);
63 }
64
65 #region Internal
66 internal Pattern(Context ctx, IntPtr obj)
67 : base(ctx, obj)
68 {
69 Debug.Assert(ctx != null);
70 }
71 #endregion
72 }
73}
The abstract syntax tree (AST) class.
Definition: AST.cs:31
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Expressions are terms.
Definition: Expr.cs:31
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than o...
Definition: Pattern.cs:32
uint NumTerms
The number of terms in the pattern.
Definition: Pattern.cs:37
override string ToString()
A string representation of the pattern.
Definition: Pattern.cs:60
Expr[] Terms
The terms in the pattern.
Definition: Pattern.cs:45