ListSort.java

Go to the documentation of this file.

package com.microsoft.z3;

import com.microsoft.z3.Native.LongPtr;

public class ListSort extends Sort
{
    public FuncDecl getNilDecl()
    {
        return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
    }

    public Expr getNil()
    {
        return getContext().mkApp(getNilDecl());
    }

    public FuncDecl getIsNilDecl()
    {
        return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
    }

    public FuncDecl getConsDecl()
    {
        return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
    }

    public FuncDecl getIsConsDecl()
    {
        return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
    }

    public FuncDecl getHeadDecl()
    {
        return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
    }

    public FuncDecl getTailDecl()
    {
        return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1));
    }

    ListSort(Context ctx, Symbol name, Sort elemSort)
    {
        super(ctx, Native.mkListSort(ctx.nCtx(), name.getNativeObject(),
                elemSort.getNativeObject(),
                new LongPtr(), new Native.LongPtr(), new LongPtr(),
                new LongPtr(), new LongPtr(), new LongPtr()));
    }
};