Z3 |

RelationSort.cs
Go to the documentation of this file.
1/*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 RelationSort.cs
7
8 Abstract:
9
10 Z3 Managed API: Relation Sorts
11
12 Author:
13
14 Christoph Wintersteiger (cwinter) 2012-11-23
15
16 Notes:
17
18--*/
19
20 using System.Diagnostics;
21 using System;
22
23 namespace Microsoft.Z3
24{
28 public class RelationSort : Sort
29 {
33 public uint Arity
34 {
35 get { return Native.Z3_get_relation_arity(Context.nCtx, NativeObject); }
36 }
37
41 public Sort[] ColumnSorts
42 {
43 get
44 {
45
46 if (m_columnSorts != null)
47 return m_columnSorts;
48
49 uint n = Arity;
50 Sort[] res = new Sort[n];
51 for (uint i = 0; i < n; i++)
52 res[i] = Sort.Create(Context, Native.Z3_get_relation_column(Context.nCtx, NativeObject, i));
53 return res;
54 }
55 }
56
57 #region Internal
58 private Sort[] m_columnSorts = null;
59
60 internal RelationSort(Context ctx, IntPtr obj)
61 : base(ctx, obj)
62 {
63 Debug.Assert(ctx != null);
64 }
65 #endregion
66 }
67}
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.RelationSort
Relation sorts.
Definition: RelationSort.cs:29
Microsoft.Z3.RelationSort.Arity
uint Arity
The arity of the relation sort.
Definition: RelationSort.cs:34
Microsoft.Z3.RelationSort.ColumnSorts
Sort[] ColumnSorts
The sorts of the columns of the relation sort.
Definition: RelationSort.cs:42
Microsoft.Z3.Sort
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
Microsoft.Z3
Definition: AlgebraicNum.cs:27