Z3
ArraySort.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  ArraySort.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Array 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 ArraySort : Sort
30  {
34  public Sort Domain
35  {
36  get
37  {
38  Contract.Ensures(Contract.Result<Sort>() != null);
39 
40  return Sort.Create(Context, Native.Z3_get_array_sort_domain(Context.nCtx, NativeObject));
41  }
42  }
43 
47  public Sort Range
48  {
49  get
50  {
51  Contract.Ensures(Contract.Result<Sort>() != null);
52 
53  return Sort.Create(Context, Native.Z3_get_array_sort_range(Context.nCtx, NativeObject));
54  }
55  }
56 
57  #region Internal
58  internal ArraySort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
59  internal ArraySort(Context ctx, Sort domain, Sort range)
60  : base(ctx, Native.Z3_mk_array_sort(ctx.nCtx, domain.NativeObject, range.NativeObject))
61  {
62  Contract.Requires(ctx != null);
63  Contract.Requires(domain != null);
64  Contract.Requires(range != null);
65  }
66  #endregion
67  };
68 
69 }
static Z3_sort Z3_get_array_sort_range(Z3_context a0, Z3_sort a1)
Definition: Native.cs:3262
using System
Array sorts.
Definition: ArraySort.cs:29
static Z3_sort Z3_get_array_sort_domain(Z3_context a0, Z3_sort a1)
Definition: Native.cs:3254
static Z3_sort Z3_mk_array_sort(Z3_context a0, Z3_sort a1, Z3_sort a2)
Definition: Native.cs:2202
def ArraySort(d, r)
Definition: z3py.py:4004
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