Z3
src/api/java/TupleSort.java
Go to the documentation of this file.
00001 
00018 package com.microsoft.z3;
00019 
00023 public class TupleSort extends Sort
00024 {
00029     public FuncDecl mkDecl() throws Z3Exception
00030     {
00031 
00032         return new FuncDecl(getContext(), Native.getTupleSortMkDecl(getContext()
00033                 .nCtx(), getNativeObject()));
00034     }
00035 
00039     public int getNumFields() throws Z3Exception
00040     {
00041         return Native.getTupleSortNumFields(getContext().nCtx(), getNativeObject());
00042     }
00043 
00048     public FuncDecl[] getFieldDecls() throws Z3Exception
00049     {
00050 
00051         int n = getNumFields();
00052         FuncDecl[] res = new FuncDecl[n];
00053         for (int i = 0; i < n; i++)
00054             res[i] = new FuncDecl(getContext(), Native.getTupleSortFieldDecl(
00055                     getContext().nCtx(), getNativeObject(), i));
00056         return res;
00057     }
00058 
00059     TupleSort(Context ctx, Symbol name, int numFields, Symbol[] fieldNames,
00060             Sort[] fieldSorts) throws Z3Exception
00061     {
00062         super(ctx);
00063 
00064         Native.LongPtr t = new Native.LongPtr();
00065         setNativeObject(Native.mkTupleSort(ctx.nCtx(), name.getNativeObject(),
00066                 numFields, Symbol.arrayToNative(fieldNames),
00067                 AST.arrayToNative(fieldSorts), t, new long[numFields]));
00068     }
00069 };
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines