Z3
 
Loading...
Searching...
No Matches
FiniteSetSort.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2024 Microsoft Corporation
3
4Module Name:
5
6 FiniteSetSort.cs
7
8Abstract:
9
10 Z3 Managed API: Finite Set Sorts
11
12Author:
13
14 GitHub Copilot
15
16Notes:
17
18--*/
19
20using System.Diagnostics;
21using System;
22
23namespace Microsoft.Z3
24{
28 public class FiniteSetSort : Sort
29 {
30 #region Internal
31 internal FiniteSetSort(Context ctx, IntPtr obj)
32 : base(ctx, obj)
33 {
34 Debug.Assert(ctx != null);
35 }
36
37 internal FiniteSetSort(Context ctx, Sort elemSort)
38 : base(ctx, Native.Z3_mk_finite_set_sort(ctx.nCtx, elemSort.NativeObject))
39 {
40 Debug.Assert(ctx != null);
41 Debug.Assert(elemSort != null);
42 }
43 #endregion
44
48 public Sort Basis
49 {
50 get { return Sort.Create(Context, Native.Z3_get_finite_set_sort_basis(Context.nCtx, NativeObject)); }
51 }
52 }
53}
The main interaction with Z3 happens via the Context.
Definition Context.cs:34
Sort Basis
Get the element sort (basis) of this finite set sort.
The Sort class implements type information for ASTs.
Definition Sort.cs:29