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¶

 predicate member(array [int] of var bool: x, var bool: y)

 predicate member(array [int] of var float: x, var float: y)

 predicate member(array [int] of var $$E: x, var $$E: y)

 predicate member(array [int] of var set of $$E: x, var set of $$E: y)

 predicate member(var set of $$E: x, var $$E: y)

1-4.: Requires that y occurs in the array x.

Requires that y occurs in the set x.

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)

Creates a new array O from an input array I with a simultaneous change at positions P to 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
Returns a new array from an input array I with a simultaneous change at positions P to values V

I is an array of integers P is an array of index values in I V is an array of integer values

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