Z3
ArraySort.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 public 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 };
com.microsoft.z3.ArraySort.getDomain
Sort getDomain()
Definition: ArraySort.java:31
com.microsoft.z3.Sort
Definition: Sort.java:26
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
com.microsoft.z3.ArraySort
Definition: ArraySort.java:23
com.microsoft.z3.ArraySort.getRange
Sort getRange()
Definition: ArraySort.java:43
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.Native.getArraySortRange
static long getArraySortRange(long a0, long a1)
Definition: Native.java:2729
com.microsoft.z3.Native.getArraySortDomain
static long getArraySortDomain(long a0, long a1)
Definition: Native.java:2720
com.microsoft.z3.Context
Definition: Context.java:35