Z3
src/api/java/EnumSort.java
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 };
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines