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