# 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