Z3 |

Pattern.cs
Go to the documentation of this file.
1/*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 Pattern.cs
7
8 Abstract:
9
10 Z3 Managed API: Patterns
11
12 Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-16
15
16 Notes:
17
18--*/
19
20 using System.Diagnostics;
21 using System;
22 using System.Runtime.InteropServices;
23
24 namespace 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}
Microsoft.Z3.AST
The abstract syntax tree (AST) class.
Definition: AST.cs:31
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.Expr
Expressions are terms.
Definition: Expr.cs:31
Microsoft.Z3.Pattern
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than o...
Definition: Pattern.cs:32
Microsoft.Z3.Pattern.NumTerms
uint NumTerms
The number of terms in the pattern.
Definition: Pattern.cs:37
Microsoft.Z3.Pattern.ToString
override string ToString()
A string representation of the pattern.
Definition: Pattern.cs:60
Microsoft.Z3.Pattern.Terms
Expr[] Terms
The terms in the pattern.
Definition: Pattern.cs:45
Microsoft.Z3
Definition: AlgebraicNum.cs:27