4.2.2.6. Arrayrelated 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 