Z3
src/api/java/FiniteDomainSort.java
Go to the documentation of this file.
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines