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 [$X] of var bool: x, var bool: y)

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

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

 predicate member(array [$X] 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

1.  predicate write(array [$$E] of var $$T: I,
                    var $$E: i,
                    var $$T: v,
                    array [$$E] of var $$T: O)

2.  function array [$$E] of var $$T: write(array [$$E] of var $$T: I,
                                           var $$E: i,
                                           var $$T: v)

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 values O is an array of values with same index set as I i is an index for I v is the value to write
Return the input array I with a change at position i to take value v

I is an array of values i is an index for I v is the value to write

writes

1.  predicate writes(array [$$X] of var $$T: I,
                     array [$$Y] of var $$X: P,
                     array [$$Y] of var $$T: V,
                     array [$$X] of var $$T: O)

2.  function array [$$X] of var $$T: writes(array [$$X] of var $$T: I,
                                            array [$$Y] of var $$X: P,
                                            array [$$Y] of var $$T: 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 input values 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 values to write
Returns a new array from an input array I with a simultaneous change at positions P to values V

I is an array of input values P is an array of index values in I V is an array of values to write

writes_seq

1.  predicate writes_seq(array [$$X] of var $$T: I,
                         array [$$Y] of var $$X: P,
                         array [$$Y] of var $$T: V,
                         array [$$X] of var $$T: O)

2.  function array [$$X] of var $$T: writes_seq(array [$$X] of var $$T: I,
                                                array [$$Y] of var $$X: P,
                                                array [$$Y] of var $$T: V)

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 input values O is an array of output values with same index set as I P is an array of indices in I V is an array of values to write
Return the input array I with a sequence of changes at positions P to take values V

I is an array of input values P is an array of index values in I V is an array of values to write