TupleSort.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
public class TupleSort extends Sort
{
    public FuncDecl<TupleSort> mkDecl()
    {
 
        return new FuncDecl<>(getContext(), Native.getTupleSortMkDecl(getContext()
                .nCtx(), getNativeObject()));
    }
 
    public int getNumFields()
    {
        return Native.getTupleSortNumFields(getContext().nCtx(), getNativeObject());
    }
 
    public FuncDecl<?>[] getFieldDecls()
    {
 
        int n = getNumFields();
        FuncDecl<?>[] res = new FuncDecl[n];
        for (int i = 0; i < n; i++)
            res[i] = new FuncDecl<>(getContext(), Native.getTupleSortFieldDecl(
                    getContext().nCtx(), getNativeObject(), i));
        return res;
    }
 
    TupleSort(Context ctx, Symbol name, int numFields, Symbol[] fieldNames,
            Sort[] fieldSorts)
    {
        super(ctx, Native.mkTupleSort(ctx.nCtx(), name.getNativeObject(),
                numFields, Symbol.arrayToNative(fieldNames),
                AST.arrayToNative(fieldSorts), new Native.LongPtr(),
                new long[numFields]));
    }
};