Z3
ArraySort.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
23public class ArraySort extends Sort
24{
31 public Sort getDomain()
32 {
33 return Sort.create(getContext(),
34 Native.getArraySortDomain(getContext().nCtx(), getNativeObject()));
35 }
36
43 public Sort getRange()
44 {
45 return Sort.create(getContext(),
46 Native.getArraySortRange(getContext().nCtx(), getNativeObject()));
47 }
48
49 ArraySort(Context ctx, long obj)
50 {
51 super(ctx, obj);
52 }
53
54 ArraySort(Context ctx, Sort domain, Sort range)
55 {
56 super(ctx, Native.mkArraySort(ctx.nCtx(), domain.getNativeObject(),
57 range.getNativeObject()));
58 }
59
60 ArraySort(Context ctx, Sort[] domains, Sort range)
61 {
62 super(ctx, Native.mkArraySortN(ctx.nCtx(), domains.length, AST.arrayToNative(domains),
63 range.getNativeObject()));
64 }
65};
static long getArraySortDomain(long a0, long a1)
Definition: Native.java:2720
static long getArraySortRange(long a0, long a1)
Definition: Native.java:2729
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431