Z3 |

ArraySort.java
Go to the documentation of this file.
1
18 package 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};
com.microsoft.z3.ArraySort
Definition: ArraySort.java:25
com.microsoft.z3.ArraySort.getDomain
D getDomain()
Definition: ArraySort.java:32
com.microsoft.z3.ArraySort.getRange
R getRange()
Definition: ArraySort.java:44
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Sort
Definition: Sort.java:27
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
z3py.ArraySort
def ArraySort(*sig)
Definition: z3py.py:4645