00001 00018 package com.microsoft.z3; 00019 00023 public class FiniteDomainSort extends Sort 00024 { 00028 public long getSize() throws Z3Exception 00029 { 00030 Native.LongPtr res = new Native.LongPtr(); 00031 Native.getFiniteDomainSortSize(getContext().nCtx(), getNativeObject(), res); 00032 return res.value; 00033 } 00034 00035 FiniteDomainSort(Context ctx, long obj) throws Z3Exception 00036 { 00037 super(ctx, obj); 00038 } 00039 00040 FiniteDomainSort(Context ctx, Symbol name, long size) throws Z3Exception 00041 { 00042 super(ctx, Native.mkFiniteDomainSort(ctx.nCtx(), name.getNativeObject(), 00043 size)); 00044 } 00045 }