Go to the documentation of this file.00001
00018 package com.microsoft.z3;
00019
00023 public class EnumSort extends Sort
00024 {
00028 public FuncDecl[] getConstDecls() throws Z3Exception
00029 {
00030 int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
00031 FuncDecl[] t = new FuncDecl[n];
00032 for (int i = 0; i < n; i++)
00033 t[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
00034 return t;
00035 }
00036
00040 public Expr[] getConsts() throws Z3Exception
00041 {
00042 FuncDecl[] cds = getConstDecls();
00043 Expr[] t = new Expr[cds.length];
00044 for (int i = 0; i < t.length; i++)
00045 t[i] = getContext().mkApp(cds[i]);
00046 return t;
00047 }
00048
00052 public FuncDecl[] getTesterDecls() throws Z3Exception
00053 {
00054 int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
00055 FuncDecl[] t = new FuncDecl[n];
00056 for (int i = 0; i < n; i++)
00057 t[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
00058 return t;
00059 }
00060
00061 EnumSort(Context ctx, Symbol name, Symbol[] enumNames) throws Z3Exception
00062 {
00063 super(ctx);
00064
00065 int n = enumNames.length;
00066 long[] n_constdecls = new long[n];
00067 long[] n_testers = new long[n];
00068 setNativeObject(Native.mkEnumerationSort(ctx.nCtx(),
00069 name.getNativeObject(), (int) n, Symbol.arrayToNative(enumNames),
00070 n_constdecls, n_testers));
00071 }
00072 };