ListSort Class Reference

Inheritance diagram for ListSort:

Public Member Functions
FuncDecl	getNilDecl ()
Expr	getNil ()
FuncDecl	getIsNilDecl ()
FuncDecl	getConsDecl ()
FuncDecl	getIsConsDecl ()
FuncDecl	getHeadDecl ()
FuncDecl	getTailDecl ()
Public Member Functions inherited from Sort
boolean	equals (Object o)
int	hashCode ()
int	getId ()
Z3_sort_kind	getSortKind ()
Symbol	getName ()
String	toString ()
Public Member Functions inherited from AST
boolean	equals (Object o)
int	compareTo (Object other)
int	hashCode ()
int	getId ()
AST	translate (Context ctx)
Z3_ast_kind	getASTKind ()
boolean	isExpr ()
boolean	isApp ()
boolean	isVar ()
boolean	isQuantifier ()
boolean	isSort ()
boolean	isFuncDecl ()
String	toString ()
String	getSExpr ()
Public Member Functions inherited from Z3Object
void	dispose ()
Public Member Functions inherited from IDisposable
void	dispose ()

Additional Inherited Members
Protected Member Functions inherited from Z3Object
void	finalize ()

Detailed Description

List sorts.

Definition at line 23 of file ListSort.java.

Member Function Documentation

FuncDecl getConsDecl ( )

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 ( )

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 ( )

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 ( )

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 ( )

inline

The empty list.

Exceptions

Z3Exception

Definition at line 38 of file ListSort.java.

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

FuncDecl getNilDecl ( )

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 ( )

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));
    }