Numeric Data Types
Rel includes several numeric types, where the number of bits is specified to achieve a desired range and precision.
Int
and Float
are special names for 64-bit signed integers, SignedInt[64]
, and 64-bit floating-point numbers, Floating[64]
, respectively .
Number
As a convenience, Number
is a supertype that includes all the numeric types.
It doesn’t come with its own constructor, meaning you can’t create this data type directly.
You can only directly create primitive numeric data types.
Type Relation: Number(x)
Example:
// read query
def output = {1; 1.5; pi_float64; decimal[64, 2, 3.14159]; rational[64, 2, 3]}
ic number_ic { subset(output, Number) }
Noteworthy Operations
Numerical operations are usually only compatible between values of the same type.
When incompatible types are used, the result is the empty relation, false
.
Operations include: +
, -
, *
, ^
, and /
,
also known as add, subtract, multiply, power, and divide.
Rel also offers bit-level operations between integers or unsigned integers of the same width:
bitwise_or
.bitwise_and
.bitwise_not
.bitwise_left_shift
.bitwise_right_shift
.bitwise_unsigned_right_shift
.
Signed Integer
Integers are 64-bit signed integers, by default.
Construction
Integer constants and int[nbits, x]
with bit size nbits
, which can be 8, 16, 32, 64, or 128.
Shortcut constructors: int64
and int128
.
// read query
def output = {1; -10; int[8, 5]; int[128, -10^10]}
Type Relation: Int(x)
and SignedInt(nbits, x)
For 64-bit integers (the default): Int(x)
.
For other bit-lengths: SignedInt(nbits, x)
.
// read query
def R = 1234; int[8, 5]
def output:a(x) = R(x) and (Int(x))
def output:b(x) = R(x) and (SignedInt(8, x))
Noteworthy Operations
parse_int[string]
.int_float_convert[x]
- convertsInt
toFloat
.trunc_divide[x,y]
- x/y rounded towards zero.floor_divide[x,y]
.divide[x,y]
.
Examples
// read query
def a = 432123432123432123
def output:overflow = a^2
def output:wide = int128[a]^2
Unsigned Integer
Construction
Unsigned integers can be constructed with:
uint[nbits, x]
with bit sizenbits
, which can be 8, 16, 32, 64, or 128.0xNNNN
for hexadecimal (base 16) constants.0oNNNN
for octal (base 8) constants.
Hexadecimal and octal constants are assigned the unsigned integer with the lowest number of bits needed to represent it:
// read query
def output = {0xF; 0o77777777; 0xFFFF123FFFFF; uint[128, 1234]}
Shortcut constructors: uint64
and uint128
.
Type Relation: UInt(x)
(64-bit)
UInt(x)
holds if and only if x
is an unsigned 64-bit integer.
Generalized type relation: UnsignedInt(nbits, x)
with bit size nbits
, which can be 8, 16, 32, 64, or 128:
// read query
def R = {0xF; 0o77777777; uint128[1234]}
def output(x) = R(x) and (UInt(x) or UnsignedInt(32, x))
Noteworthy Operations
Mathematical operations between unsigned integers of different widths give an empty result.
Examples
// read query
def a = uint[64, 1000]
def b = uint[32, 100]
def uint_type[x] = UnsignedInt(16, x), "UInt16"
@inline
def uint_type[x] = UnsignedInt(32, x), "UInt32"
@inline
def uint_type[x] = UnsignedInt(64, x), "UInt64"
@inline
def uint_type[x] = UnsignedInt(128, x), "UInt128"
def output:sum = a + b // Empty
def output:atype = uint_type[a]
def output:btype = uint_type[b]
Float
Floats are 64-bit by default.
Construction
Floating-point constants can be specified using a decimal point, or with
scientific notation, as in 1e6
or 1.321E2
.
To specify the bit width, use the constructor
float[nbits, x]
, for a float constant x
with bit size nbits
, which can be 16, 32, or 64.
Shortcut constructor: float64[x]
.
// read query
def output = {2.0; float[32, 1.321]; 7.297e-3}
Floating-point numbers also support various special values, such as and . There exists no literal that can directly create infinity. It’s possible to generate the infinity value with some short arithmetic.
// read query
def infinity_positive = 1/0
def infinity_negative = -1/0
def zero_negative = -0.0
def output = {infinity_positive; infinity_negative; zero_negative}
Type Relation: Float(x)
and Floating(nbits, x)
(Shortcut) Type relation (64-bit): Float(x)
, true if and only if x
is a 64-bit floating-point number.
Generalized type relation: Floating(nbits, x)
. This works for 16, 32, and 64 bits:
// read query
def R = (2.0, float[32, 1.321])
ic float_ic {
subset(R, (Float, Floating[32]))
}
def output = R
Noteworthy Operations
float_int_convert[x]
- expects the floatx
to be equivalent to anInt
.floor_to_int[x]
- takes the floor of floatx
, then converts toInt
.parse_float
.
Rational
Construction
Rational numbers are constructed with rational[nbits, numerator, denominator]
for integer numerator and denominator.
The supported bit sizes for nbits
are: 8, 16, 32, 64, and 128.
// read query
def output = {rational[64, 2, 3]; rational[8, -1, 7]}
Type Relation : Rational(nbits, x)
The binary relation Rational(nbits, x)
checks that x
is of type Rational
with a bit size of nbits
.
// read query
def R = rational[16, -5, -7]
def output(x) = R(x) and Rational(16, x)
Noteworthy Operations
Accessors:
See also:
Examples
// read query
def x = rational[64, 200, 25]
def y = rational[64, 10, 3]
def output:fields = x, numerator[x], denominator[x]
def output:ops = x + y, x * y, x / y
You can add and multiply rationals by integers, but not by floats:
// read query
def x = rational[64, 1, 3]
def output = x * 3, x + 5
FixedDecimal
FixedDecimal
numbers have two parameters:
decimals
: the number of decimal digits (to the right of.
).bits
: the total number of bits used.
The following parameter combinations are supported:
bit size | decimals | range |
---|---|---|
8 | 0—2 | to |
16 | 0—4 | to |
32 | 0—9 | to |
64 | 0—18 | to |
128 | 0—38 | to |
Construction
The constructor decimal[nbits, ndecimals, v]
creates a fixed-size decimal
for v
:
// read query
def output = {decimal[32, 4, 2/3]; decimal[128, 20, sqrt[2]]}
Type Relation: FixedDecimal(nbits, ndecimals, x)
The ternary relation FixedDecimal(nbits, ndecimals, x)
checks that x
is of type FixedDecimal
with a bit size of nbits
and ndecimals
decimal precision:
// read query
def R = {decimal[64, 4, pi_float64]; decimal[64, 10, pi_float64]}
def output(x) = R(x) and FixedDecimal(64, 4, x)
Noteworthy Operations
Operations between fixed-size decimals with different digits of precision yield an empty result.
Examples
// read query
def output:pi_3 = decimal[64, 3, 3.14159265359]
def output:sum_one = decimal[64, 1, 4.5] * 2
def output:sum_two = decimal[64, 0, 4.5] * 2
// read query
def d = parse_decimal[64, 2, "10.6"]
ic fixed_decimal_ic {FixedDecimal(64, 2, d)}
def output = d
FixedDecimal
numbers are particularly useful when you want to avoid floating-point errors,
such as when dealing with financial data. For example:
// read query
@inline
def mydec[x] = decimal[64,2,x]
def output:float = 140.28 + 57.14 + 17.80
def output:fixed = mydec[140.28] + mydec[57.14] + mydec[17.80]
Next: Text Data Types