Z3
FiniteDomainSort.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 public class FiniteDomainSort extends Sort
24 {
28  public long getSize() throws Z3Exception
29  {
30  Native.LongPtr res = new Native.LongPtr();
31  Native.getFiniteDomainSortSize(getContext().nCtx(), getNativeObject(), res);
32  return res.value;
33  }
34 
35  FiniteDomainSort(Context ctx, long obj) throws Z3Exception
36  {
37  super(ctx, obj);
38  }
39 
40  FiniteDomainSort(Context ctx, Symbol name, long size) throws Z3Exception
41  {
42  super(ctx, Native.mkFiniteDomainSort(ctx.nCtx(), name.getNativeObject(),
43  size));
44  }
45 }
static boolean getFiniteDomainSortSize(long a0, long a1, LongPtr a2)
Definition: Native.java:2012