Z3
ArraySort.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
23@SuppressWarnings("unchecked")
24public class ArraySort<D extends Sort, R extends Sort> extends Sort
25{
32 public D getDomain()
33 {
34 return (D) Sort.create(getContext(),
35 Native.getArraySortDomain(getContext().nCtx(), getNativeObject()));
36 }
37
44 public R getRange()
45 {
46 return (R) Sort.create(getContext(),
47 Native.getArraySortRange(getContext().nCtx(), getNativeObject()));
48 }
49
50 ArraySort(Context ctx, long obj)
51 {
52 super(ctx, obj);
53 }
54
55 ArraySort(Context ctx, D domain, R range)
56 {
57 super(ctx, Native.mkArraySort(ctx.nCtx(), domain.getNativeObject(),
58 range.getNativeObject()));
59 }
60
61 ArraySort(Context ctx, Sort[] domains, R range)
62 {
63 super(ctx, Native.mkArraySortN(ctx.nCtx(), domains.length, AST.arrayToNative(domains),
64 range.getNativeObject()));
65 }
66};
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
def ArraySort(*sig)
Definition: z3py.py:4645