20using System.Diagnostics;
38 return Sort.Create(
Context, Native.Z3_get_array_sort_domain(
Context.nCtx, NativeObject));
50 return Sort.Create(
Context, Native.Z3_get_array_sort_range(
Context.nCtx, NativeObject));
55 internal ArraySort(
Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx !=
null); }
56 internal ArraySort(Context ctx, Sort domain, Sort
range)
59 Debug.Assert(ctx !=
null);
60 Debug.Assert(domain !=
null);
61 Debug.Assert(
range !=
null);
63 internal ArraySort(Context ctx, Sort[] domain, Sort
range)
66 Debug.Assert(ctx !=
null);
67 Debug.Assert(domain !=
null);
68 Debug.Assert(
range !=
null);
Sort Range
The range of the array sort.
Sort Domain
The domain of the array sort.
The main interaction with Z3 happens via the Context.
The Sort class implements type information for ASTs.
expr range(expr const &lo, expr const &hi)
Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)
Create an array type with N arguments.
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.