Package com.microsoft.z3

Class ListSort<R extends Sort>

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.AST

com.microsoft.z3.Sort

com.microsoft.z3.ListSort<R>

All Implemented Interfaces:

Comparable<AST>

public class ListSort<R extends Sort>
extends Sort

List sorts.

Method Summary

Modifier and Type	Method	Description
FuncDecl<ListSort<R>>	getConsDecl()	The declaration of the cons function of this list sort.
FuncDecl<R>	getHeadDecl()	The declaration of the head function of this list sort.
FuncDecl<BoolSort>	getIsConsDecl()	The declaration of the isCons function of this list sort.
FuncDecl<BoolSort>	getIsNilDecl()	The declaration of the isNil function of this list sort.
Expr<ListSort<R>>	getNil()	The empty list.
FuncDecl<ListSort<R>>	getNilDecl()	The declaration of the nil function of this list sort.
FuncDecl<ListSort<R>>	getTailDecl()	The declaration of the tail function of this list sort.

Methods inherited from class com.microsoft.z3.Sort

equals, getId, getName, getSortKind, hashCode, toString, translate

Methods inherited from class com.microsoft.z3.AST

compareTo, getASTKind, getSExpr, isApp, isExpr, isFuncDecl, isQuantifier, isSort, isVar

Methods inherited from class com.microsoft.z3.Z3Object

arrayLength, arrayToNative

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Method Details

getNilDecl

public FuncDecl<ListSort<R>> getNilDecl()

The declaration of the nil function of this list sort.

Throws:

Z3Exception

getNil

public Expr<ListSort<R>> getNil()

The empty list.

Throws:

Z3Exception

getIsNilDecl

public FuncDecl<BoolSort> getIsNilDecl()

The declaration of the isNil function of this list sort.

Throws:

Z3Exception

getConsDecl

public FuncDecl<ListSort<R>> getConsDecl()

The declaration of the cons function of this list sort.

Throws:

Z3Exception

getIsConsDecl

public FuncDecl<BoolSort> getIsConsDecl()

The declaration of the isCons function of this list sort.

Throws:

Z3Exception

getHeadDecl

public FuncDecl<R> getHeadDecl()

The declaration of the head function of this list sort.

Throws:

Z3Exception

getTailDecl

public FuncDecl<ListSort<R>> getTailDecl()

The declaration of the tail function of this list sort.

Throws:

Z3Exception