Z3
FiniteDomainSort.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  FiniteDomainSort.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Finite Domain Sorts
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-11-23
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Diagnostics.Contracts;
22 
23 namespace Microsoft.Z3
24 {
28  [ContractVerification(true)]
29  public class FiniteDomainSort : Sort
30  {
34  public ulong Size
35  {
36  get
37  {
38  ulong res = 0;
39  Native.Z3_get_finite_domain_sort_size(Context.nCtx, NativeObject, ref res);
40  return res;
41  }
42  }
43 
44  #region Internal
45  internal FiniteDomainSort(Context ctx, IntPtr obj)
46  : base(ctx, obj)
47  {
48  Contract.Requires(ctx != null);
49  }
50  internal FiniteDomainSort(Context ctx, Symbol name, ulong size)
51  : base(ctx, Native.Z3_mk_finite_domain_sort(ctx.nCtx, name.NativeObject, size))
52  {
53  Contract.Requires(ctx != null);
54  Contract.Requires(name != null);
55 
56  }
57  #endregion
58  }
59 }
using System
static Z3_sort Z3_mk_finite_domain_sort(Z3_context a0, IntPtr a1, UInt64 a2)
Definition: Native.cs:2194
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6389
static int Z3_get_finite_domain_sort_size(Z3_context a0, Z3_sort a1, [In, Out] ref UInt64 a2)
Definition: Native.cs:3246
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30