Structures

A sort that describes an array with a domain and range, specified by two generic type arguments.

A unicode character sort.

An integer sort. Note that this is not the same as a machine integer.

A real number sort. Note that this type is not a floating point number.

A BitVector sort to type-erase Z3Ast<T> instances to. Note: You should not pass this bit vector sort to methods that create new AST based on sort, and doing so will result in a runtime error when trying to call getSort.

A bit width sort which fits as many bits as the bit width of its T parameter

A bit vector of length 1

A bit vector of length 128

A FP sort to type-erase Z3Ast<T> instances to. Note: You should not pass this float sort to methods that create new AST based on sort, and doing so will result in a runtime error when trying to call getSort.

A Quadruple-precision floating point sort

A half precision floating point sort

A RoundingMode sort for values that specify the rounding mode of floating point values

A meta-sort that is used to represent regular expression sorts. Is not a SortKind itself as it is not a concrete type that can specialize Z3Ast instances, but used solely to refer to regular expression sorts.

The element is the element of the underlying sequence sort of the regular expression.

A meta-sort that is used to represent sequence sorts. Is not a SortKind itself as it is not a concrete type that can specialize Z3Ast instances, but used solely to refer to sequence sorts.