ListSort Class Reference

Inheritance diagram for ListSort:

Public Member Functions
FuncDecl	getNilDecl () throws Z3Exception
Expr	getNil () throws Z3Exception
FuncDecl	getIsNilDecl () throws Z3Exception
FuncDecl	getConsDecl () throws Z3Exception
FuncDecl	getIsConsDecl () throws Z3Exception
FuncDecl	getHeadDecl () throws Z3Exception
FuncDecl	getTailDecl () throws Z3Exception
Package Functions
	ListSort (Context ctx, Symbol name, Sort elemSort) throws Z3Exception

---

Detailed Description

List sorts.

Definition at line 23 of file ListSort.java.

---

Constructor & Destructor Documentation

ListSort	(	Context	ctx,
		Symbol	name,
		Sort	elemSort
	)		throws Z3Exception [inline, package]

Definition at line 89 of file ListSort.java.

    {
        super(ctx);

        Native.LongPtr inil = new Native.LongPtr(), iisnil = new Native.LongPtr();
        Native.LongPtr icons = new Native.LongPtr(), iiscons = new Native.LongPtr();
        Native.LongPtr ihead = new Native.LongPtr(), itail = new Native.LongPtr();

        setNativeObject(Native.mkListSort(ctx.nCtx(), name.getNativeObject(),
                elemSort.getNativeObject(), inil, iisnil, icons, iiscons, ihead,
                itail));
    }

---

Member Function Documentation

FuncDecl getConsDecl

(

)

throws Z3Exception [inline]

The declaration of the cons function of this list sort.

Exceptions:

Z3Exception

Definition at line 56 of file ListSort.java.

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

FuncDecl getHeadDecl

(

)

throws Z3Exception [inline]

The declaration of the head function of this list sort.

Exceptions:

Z3Exception

Definition at line 75 of file ListSort.java.

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

FuncDecl getIsConsDecl

(

)

throws Z3Exception [inline]

The declaration of the isCons function of this list sort.

Exceptions:

Z3Exception

Definition at line 66 of file ListSort.java.

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

FuncDecl getIsNilDecl

(

)

throws Z3Exception [inline]

The declaration of the isNil function of this list sort.

Exceptions:

Z3Exception

Definition at line 47 of file ListSort.java.

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

Expr getNil

(

)

throws Z3Exception [inline]

The empty list.

Exceptions:

Z3Exception

Definition at line 38 of file ListSort.java.

    {
        return getContext().mkApp(getNilDecl());
    }

FuncDecl getNilDecl

(

)

throws Z3Exception [inline]

The declaration of the nil function of this list sort.

Exceptions:

Z3Exception

Definition at line 29 of file ListSort.java.

Referenced by ListSort.getNil().

    {
        return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
    }

FuncDecl getTailDecl

(

)

throws Z3Exception [inline]

The declaration of the tail function of this list sort.

Exceptions:

Z3Exception

Definition at line 84 of file ListSort.java.

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