4.2.2. 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.2.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 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…

annotation bool_search(array [int] of var opt bool: x,
                       ann: a1,
                       ann: a2,
                       ann: a3)

Search annotation for optional Boolean variables

More…

annotation bool_search(array [int] of var opt bool: x,
                       ann: a1,
                       ann: a2)

Search annotation for optional Boolean variables

More…

predicate deopt(var opt bool: 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.2.2. Option type support for integers

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

Usage: x * y

Optional multiplication. Return product of x and y , with absent replaced by 1.

More…

function int: '*'(opt int: x, opt int: y)

Usage: x * y

Optional multiplication. Return product of x and y , with absent replaced by 1.

More…

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

Usage: x + y

Optional addition. Return sum of x and y , with absent replaced by 0.

More…

function int: '+'(opt int: x, opt int: y)

Usage: x + y

Optional addition. Return sum of x and y , with absent replaced by 0.

More…

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

Usage: x - y

Optional subtraction. Return difference of x and y , with absent replaced by 0.

More…

function int: '-'(opt int: x, opt int: y)

Usage: x - y

Optional subtraction. Return difference of x and y , with absent replaced by 0.

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 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 int: 'div'(var opt int: x, var opt int: y)

Usage: x div y

Optional division. Return x div y , with absent replaced by 1.

More…

function int: 'div'(opt int: x, opt int: y)

Usage: x div y

Optional division. Return x div y , with absent replaced by 1.

More…

function var int: 'mod'(var opt int: x, var opt int: y)

Usage: x mod y

Optional modulo. Return x mod y , with absent replaced by 1.

More…

function int: 'mod'(opt int: x, opt int: y)

Usage: x mod y

Optional modulo. Return x mod y , with absent replaced by 1.

More…

predicate absent(var opt int: x)

True iff x is absent

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 $$E: deopt(var opt $$E: x)

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

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…

function var opt float: int2float(var opt int: x)

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

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…

annotation int_search(array [int] of var opt int: x,
                      ann: a1,
                      ann: a2,
                      ann: a3)

Search annotation for optional integer variables

More…

annotation int_search(array [int] of var opt int: x, ann: a1, ann: a2)

Search annotation for optional integer variables

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 int: product(array [int] of 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 int: sum(array [int] of 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.2.3. Option type support for floats

function var float: '*'(var opt float: x, var opt float: y)

Usage: x * y

Optional multiplication. Return product of x and y , with absent replaced by 1.

More…

function float: '*'(opt float: x, opt float: y)

Usage: x * y

Optional multiplication. Return product of x and y , with absent replaced by 1.

More…

function var float: '+'(var opt float: x, var opt float: y)

Usage: x + y

Optional addition. Return sum of x and y , with absent replaced by 0.

More…

function float: '+'(opt float: x, opt float: y)

Usage: x + y

Optional addition. Return sum of x and y , with absent replaced by 0.

More…

function var float: '-'(var opt float: x, var opt float: y)

Usage: x - y

Optional subtraction. Return difference of x and y , with absent replaced by 0.

More…

function float: '-'(opt float: x, opt float: y)

Usage: x - y

Optional subtraction. Return difference of x and y , with absent replaced by 0.

More…

predicate '<'(var opt float: x, var opt float: 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 float: x, opt float: 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 float: x, var opt float: 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 float: x, opt float: 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 float: x, var opt float: 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 float: x, opt float: 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 float: x, var opt float: 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 float: x, opt float: 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 float: 'div'(var opt float: x, var opt float: y)

Usage: x div y

Optional division. Return x div y , with absent replaced by 1.

More…

function float: 'div'(opt float: x, opt float: y)

Usage: x div y

Optional division. Return x div y , with absent replaced by 1.

More…

function var float: 'mod'(var opt float: x, var opt float: y)

Usage: x mod y

Optional modulo. Return x mod y , with absent replaced by 1.

More…

function float: 'mod'(opt float: x, opt float: y)

Usage: x mod y

Optional modulo. Return x mod y , with absent replaced by 1.

More…

predicate absent(var opt float: x)

True iff x is absent

More…

function var opt float: bool2float(var opt bool: x)

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

More…

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

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

More…

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

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

More…

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

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

More…

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

Return x [ idx ]

More…

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

Return x [ idx1 , idx2 ]

More…

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

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

More…

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

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

More…

predicate float_eq(var opt float: x, var opt float: y)

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

More…

predicate float_ne(var opt float: x, var opt float: y)

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

More…

annotation float_search(array [int] of var opt float: x,
                        ann: a1,
                        ann: a2,
                        ann: a3)

Search annotation for optional float variables

More…

annotation float_search(array [int] of var opt float: x,
                        ann: a1,
                        ann: a2)

Search annotation for optional float variables

More…

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

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

More…

function var opt float: min(array [int] of var opt float: 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 float: x)

True iff x is not absent

More…

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

Return product of non-absent elements of x .

More…

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

Return product of non-absent elements of x .

More…

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

Return sum of non-absent elements of x .

More…

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

Return sum of non-absent elements of x .

More…

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

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

More…

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

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

More…

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

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

More…

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

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

More…

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