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…

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

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

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…

predicate set_in(var opt int: x, set of int: S)

Constrains x \(\in\) S

More…

predicate set_in(var opt int: x, var set of int: S)

Constrains x \(\in\) S

More…