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].