Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
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));
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines