Package com.microsoft.z3

Class DatatypeSort<R>

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.AST

com.microsoft.z3.Sort

com.microsoft.z3.DatatypeSort<R>

All Implemented Interfaces:

Comparable<AST>

public class DatatypeSort<R>
extends Sort

Datatype sorts.

Method Summary

Modifier and Type	Method	Description
FuncDecl<?>[][]	getAccessors()	The constructor accessors.
FuncDecl<DatatypeSort<R>>[]	getConstructors()	The constructors.
int	getNumConstructors()	The number of constructors of the datatype sort.
FuncDecl<BoolSort>[]	getRecognizers()	The recognizers.

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

getNumConstructors

public int getNumConstructors()

The number of constructors of the datatype sort.

Returns:

an int

Throws:

Z3Exception - on error

getConstructors

public FuncDecl<DatatypeSort<R>>[] getConstructors()

The constructors.

Throws:

Z3Exception

Z3Exception - on error

getRecognizers

public FuncDecl<BoolSort>[] getRecognizers()

The recognizers.

Throws:

Z3Exception

Z3Exception - on error

getAccessors

public FuncDecl<?>[][] getAccessors()

The constructor accessors.

Throws:

Z3Exception

Z3Exception - on error