ListSort.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import com.microsoft.z3.Native.LongPtr;
 
public class ListSort<R extends Sort> extends Sort
{
    public FuncDecl<ListSort<R>> getNilDecl()
    {
        return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
    }
 
    public Expr<ListSort<R>> getNil()
    {
        return getContext().mkApp(getNilDecl());
    }
 
    public FuncDecl<BoolSort> getIsNilDecl()
    {
        return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
    }
 
    public FuncDecl<ListSort<R>> getConsDecl()
    {
        return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
    }
 
    public FuncDecl<BoolSort> getIsConsDecl()
    {
        return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
    }
 
    public FuncDecl<R> getHeadDecl()
    {
        return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
    }
 
    public FuncDecl<ListSort<R>> 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()));
    }
};