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 };