Package com.microsoft.z3

Class TupleSort

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.AST

com.microsoft.z3.Sort

com.microsoft.z3.TupleSort

All Implemented Interfaces:

Comparable<AST>

public class TupleSort
extends Sort

Tuple sorts.

Method Summary

Modifier and Type	Method	Description
FuncDecl<?>[]	getFieldDecls()	The field declarations.
int	getNumFields()	The number of fields in the tuple.
FuncDecl<TupleSort>	mkDecl()	The constructor function of the tuple.

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

mkDecl

public FuncDecl<TupleSort> mkDecl()

The constructor function of the tuple.

Throws:

Z3Exception

getNumFields

public int getNumFields()

The number of fields in the tuple.

getFieldDecls

public FuncDecl<?>[] getFieldDecls()

The field declarations.

Throws:

Z3Exception