4.2.2.6. Array-related constraints
In this section: element, member, write, writes, writes_seq.
element
predicate element(var $$E: i, array [$$E] of var bool: x, var bool: y)
predicate element(var $$E: i,
array [$$E] of var float: x,
var float: y)
predicate element(var $$E: i, array [$$E] of var $$T: x, var $$T: y)
predicate element(var $$E: i,
array [$$E] of var set of $$T: x,
var set of $$T: y)
|
Constrains i to be the index of the element y in the array x. |
member
1. predicate member(array [int] of var bool: x, var bool: y)
2. predicate member(array [int] of var float: x, var float: y)
3. predicate member(array [int] of var $$E: x, var $$E: y)
4. predicate member(array [int] of var set of $$E: x, var set of $$E: y)
5. predicate member(var set of $$E: x, var $$E: y)
|
|
write
predicate write(array [$$E] of var int: I,
var int: i,
var int: v,
array [$$E] of var int: O)
|
Creates a new array O from an input array I with a change at position i to take value v I is an array of integers O is an array of integers with same index set as I i is an index for I v is an integer value |
writes
1. predicate writes(array [$$X] of var int: I,
array [$$Y] of var int: P,
array [$$Y] of var int: V,
array [$$X] of var int: O)
2. function array [$$X] of var int: writes(array [$$X] of var int: I,
array [$$Y] of var int: P,
array [$$Y] of var int: V)
|
|
writes_seq
predicate writes_seq(array [$$X] of var int: I,
array [$$Y] of var int: P,
array [$$Y] of var int: V,
array [$$X] of var int: O)
|
Creates a new array O from an input array I with a sequence of changes at positions P to take values V I is an array of integers O is an array of integers with same index set as I P is an array of index values in I V is an array of integer values |