Skip to content
REL
REFERENCE
Data Types
Numeric

Data Types: 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:

// 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:

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.

// 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).

// 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

Examples

// 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 size nbits, 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:

// 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:

// 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

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

// query
 
def output = {2.0; float[32, 1.321]; 7.297e-3}

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:

// query
 
def R = (2.0, float[32, 1.321])
 
ic float_ic {
   subset(R, (Float, Floating[32]))
}
 
def output = R

Noteworthy Operations

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.

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

// query
 
def R = rational[16, -5, -7]
 
def output(x) = R(x) and Rational(16, x)

Noteworthy Operations

Accessors:

See also:

Examples

// 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:

// 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 sizedecimals (d)(d)range
80—2215/10d-2^{15}/10^d to (2151)/10d(2^{15}-1)/10^d
160—4215/10d-2^{15}/10^d to (2151)/10d(2^{15}-1)/10^d
320—9231/10d-2^{31}/10^d to (2311)/10d(2^{31}-1)/10^d
640—18(263)/10d-(2^{63})/10^d to (2631)/10d(2^{63}-1)/10^d
1280—38(2127)/10d-(2^{127})/10^d to (21271)/10d(2^{127}-1)/10^d

You can use Rel to compute the range of a FixedDecimal type:

// query
 
@inline
def decimal_range[bits, decimals] =
    -2^(bits-1)/10^(decimals), (2^(bits-1)-1)/10^(decimals)
def output = decimal_range[32, 4]

Construction

The constructor decimal[nbits, ndecimals, v] creates a fixed-size decimal for v:

// 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:

// 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

// 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
// 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:

// 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

Was this doc helpful?