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 };
static long getArraySortRange(long a0, long a1)
Definition: Native.java:2535
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
static long getArraySortDomain(long a0, long a1)
Definition: Native.java:2526