ListSort< R extends Sort > Class Template Reference

Inheritance diagram for ListSort< R extends Sort >:

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

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)
static int	arrayLength (Z3Object[] a)

Detailed Description

List sorts.

Definition at line 25 of file ListSort.java.

Member Function Documentation

getConsDecl()

FuncDecl<ListSort<R> > getConsDecl ( )

inline

The declaration of the cons function of this list sort.

Exceptions

Z3Exception

Definition at line 58 of file ListSort.java.

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

getHeadDecl()

FuncDecl<R> getHeadDecl ( )

inline

The declaration of the head function of this list sort.

Exceptions

Z3Exception

Definition at line 77 of file ListSort.java.

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

getIsConsDecl()

FuncDecl<BoolSort> getIsConsDecl ( )

inline

The declaration of the isCons function of this list sort.

Exceptions

Z3Exception

Definition at line 68 of file ListSort.java.

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

getIsNilDecl()

FuncDecl<BoolSort> getIsNilDecl ( )

inline

The declaration of the isNil function of this list sort.

Exceptions

Z3Exception

Definition at line 49 of file ListSort.java.

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

getNil()

Expr<ListSort<R> > getNil ( )

inline

The empty list.

Exceptions

Z3Exception

Definition at line 40 of file ListSort.java.

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

getNilDecl()

FuncDecl<ListSort<R> > getNilDecl ( )

inline

The declaration of the nil function of this list sort.

Exceptions

Z3Exception

Definition at line 31 of file ListSort.java.

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

Referenced by ListSort< R extends Sort >.getNil().

getTailDecl()

FuncDecl<ListSort<R> > getTailDecl ( )

inline

The declaration of the tail function of this list sort.

Exceptions

Z3Exception

Definition at line 86 of file ListSort.java.

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