QType Type

QType represents the data types that are available in the Quartz language. Qbool and Qreal implement booleans and real numbers (NOT floats), respectively. Qbtv, Qnat, and Qint represent bitvectors, natural numbers, and integer numbers that can be bounded or unbounded. The unbounded case is indicated with argument "None", while Qbtv(Some len) denotes bitvectors with "len" bits, and Qnat(Some bl) and Qint(Some bl) represent the numbers {0,...,N-1} {-N,...,N-1}, respectively, where bl is the radix-2 representation of N. Qarr(dim,qty) represents arrays with dimension dim whose elements have type qty, and Qtup tyL represents tuples consisting of elements (e1,...,en) having types tyL=[ty1;...;tyn].

Union cases

Union case Description

Qarr int * QType

Full Usage: Qarr int * QType


real numbers

Item : int * QType


Full Usage: Qbool

Qbtv int option

Full Usage: Qbtv int option

    Item : int option

Item : int option

Qint bool list option

Full Usage: Qint bool list option

    Item : bool list option

bounded/unbounded unsigned integers

Item : bool list option

Qnat bool list option

Full Usage: Qnat bool list option

    Item : bool list option

bitvectors of finite/infinite length

Item : bool list option


Full Usage: Qreal

bounded/unbounded signed integers

Qtup QType list

Full Usage: Qtup QType list


array with index space and base type

Item : QType list