4.2.3. Option type support

These functions and predicates implement the standard library for working with option types. Note that option type support is still incomplete.

4.2.3.1. Option type support for Booleans

predicate 'not'(var opt bool: x)

Usage: not x

True iff x is absent or false

More…

predicate absent(var opt bool: x)

True iff x is absent

More…

predicate absent(var opt int: x)

True iff x is absent

More…

predicate bool_eq(var opt bool: b0, var opt bool: b1)

True iff both b0 and b1 are absent or both are present and have the same value.

More…

predicate bool_eq(var opt bool: b0, var bool: b1)

True iff b0 occurs and is equal to b1

More…

predicate bool_eq(var bool: b0, var opt bool: b1)

True iff b1 occurs and is equal to b0

More…

predicate deopt(var opt bool: x)

Return value of x (assumes that x is not absent)

More…

function var int: deopt(var opt int: x)

Return value of x (assumes that x is not absent)

More…

function var opt bool: element(var opt int: idx,
                               array [int] of var bool: x)

Return absent if idx is absent, otherwise return x [ idx ]

More…

function var opt bool: element(var opt int: idx1,
                               var opt int: idx2,
                               array [int,int] of var bool: x)

Return absent if idx1 or idx2 is absent, otherwise return x [ idx1 , idx2 ]

More…

function var opt bool: element(var int: idx,
                               array [int] of var opt bool: x)

Return x [ idx ]

More…

function var opt bool: element(var int: idx1,
                               var int: idx2,
                               array [int,int] of var opt bool: x)

Return x [ idx1 , idx2 ]

More…

function var opt bool: element(var opt int: idx,
                               array [int] of var opt bool: x)

Return absent if idx is absent, otherwise return x [ idx ]

More…

function var opt bool: element(var opt int: idx1,
                               var opt int: idx2,
                               array [int,int] of var opt bool: x)

Return absent if idx1 or idx2 is absent, otherwise return x [ idx1 , idx2 ]

More…

predicate exists(array [int] of var opt bool: x)

True iff for at least one i , x [i] occurs and is true

More…

predicate forall(array [int] of var opt bool: x)

True iff for any i , x [i] is absent or true

More…

predicate occurs(var opt bool: x)

True iff x is not absent

More…

4.2.3.2. Option type support for integers

predicate '<'(var opt int: x, var opt int: y)

Usage: x < y

Weak comparison: true iff either x or y is absent, or both occur and the value of x is less than the value of y .

More…

test '<'(opt int: x, opt int: y)

Usage: x < y

Weak comparison: true iff either x or y is absent, or both occur and the value of x is less than the value of y .

More…

predicate '<='(var opt int: x, var opt int: y)

Usage: x <= y

Weak comparison: true iff either x or y is absent, or both occur and the value of x is less than or equal to the value of y .

More…

test '<='(opt int: x, opt int: y)

Usage: x <= y

Weak comparison: true iff either x or y is absent, or both occur and the value of x is less than or equal to the value of y .

More…

predicate '>'(var opt int: x, var opt int: y)

Usage: x > y

Weak comparison: true iff either x or y is absent, or both occur and the value of x is greater than the value of y .

More…

test '>'(opt int: x, opt int: y)

Usage: x > y

Weak comparison: true iff either x or y is absent, or both occur and the value of x is greater than the value of y .

More…

predicate '>='(var opt int: x, var opt int: y)

Usage: x >= y

Weak comparison: true iff either x or y is absent, or both occur and the value of x is greater than or equal to the value of y .

More…

test '>='(opt int: x, opt int: y)

Usage: x >= y

Weak comparison: true iff either x or y is absent, or both occur and the value of x is greater than or equal to the value of y .

More…

function var opt int: bool2int(var opt bool: x)

Return optional 0/1 integer that is absent iff x is absent, and 1 iff x occurs and is true.

More…

function var opt int: element(var opt int: idx,
                              array [int] of var int: x)

Return absent if idx is absent, otherwise return x [ idx ]

More…

function var opt int: element(var opt int: idx1,
                              var opt int: idx2,
                              array [int,int] of var int: x)

Return absent if idx1 or idx2 is absent, otherwise return x [ idx1 , idx2 ]

More…

function var opt int: element(var int: idx,
                              array [int] of var opt int: x)

Return x [ idx ]

More…

function var opt int: element(var int: idx1,
                              var int: idx2,
                              array [int,int] of var opt int: x)

Return x [ idx1 , idx2 ]

More…

function var opt int: element(var opt int: idx,
                              array [int] of var opt int: x)

Return absent if idx is absent, otherwise return x [ idx ]

More…

function var opt int: element(var opt int: idx1,
                              var opt int: idx2,
                              array [int,int] of var opt int: x)

Return absent if idx1 or idx2 is absent, otherwise return x [ idx1 , idx2 ]

More…

predicate int_eq(var opt int: x, var opt int: y)

True iff both x and y are absent or both are present and have the same value.

More…

predicate int_ne(var opt int: x, var opt int: y)

True iff only one of x and y is absent or both are present and have different values.

More…

function var opt int: max(array [int] of var opt int: x)

Return maximum of elements in x that are not absent, or absent if all elements in x are absent.

More…

function var opt int: min(array [int] of var opt int: x)

Return minimum of elements in x that are not absent, or absent if all elements in x are absent.

More…

predicate occurs(var opt int: x)

True iff x is not absent

More…

function var int: product(array [int] of var opt int: x)

Return product of non-absent elements of x .

More…

function var int: sum(array [int] of var opt int: x)

Return sum of non-absent elements of x .

More…

function var opt int: ~*(var opt int: x, var opt int: y)

Weak multiplication. Return product of x and y if both are present, otherwise return absent.

More…

function var opt int: ~+(var opt int: x, var opt int: y)

Weak addition. Return sum of x and y if both are present, otherwise return absent.

More…

function var opt int: ~-(var opt int: x, var opt int: y)

Weak subtraction. Return difference of x and y if both are present, otherwise return absent.

More…

predicate ~=(var opt int: x, var opt int: y)

Weak equality. True if either x or y are absent, or present and equal.

More…

4.2.3.3. Other declarations

test absent(var $T: x)

Test if x is absent (always returns false)

More…

test absent(opt $T: x)

Test if x is absent

More…

function $T: deopt(opt $T: x)

Return value of x if x is not absent. Aborts when evaluated on absent value.

function var $T: deopt(var $T: x)

Return value x unchanged (since x is guaranteed to be non-optional).

More…

test occurs(var $T: x)

Test if x is not absent (always returns true)

More…

test occurs(opt $T: x)

Test if x is not absent