Constraint element
The constraint element [vHC88] ensures that value is element of list, i.e., equal to one value among those (assigned to variables) of list. The optional attribute startIndex gives the number used for indexing the first variable in list (0, by default). The optional element index gives the index (position) of one occurrence of value inside list. The optional attribute rank of index indicates if index is the first index, the last index or any index of a variable of list with the specified value (any, by default).
We give the semantics for rank=any, with indexing assumed to start at 1 for simplicity.
- element($X$, $v$) with $X=\langle x_1,x_2,\ldots \rangle$, iff $\exists i : 1 \leq i \leq |X| \land x_i = v$
- element($X$, $i$, $v$) with $X=\langle x_1,x_2,\ldots \rangle$, iff $x_i = v$
Syntax
<element>
<list [ startIndex="integer" ]> (intVal wspace)2+ | (intVar wspace)2+ </list>
[ <index [ rank="rankType" ]> intVar </index> ]
<value> intVal | intVar </value>
</element>
Below, the first constraint states that the ith variable of $\langle$ x1,x2,x3,x4 $\rangle$ must be equal to v. For example, if i is equal to 2, then x2 must be equal to v. The second constraint ensures that z is element (member) of the 1-dimensional array y.
Example
<element>
<list startIndex="1"> x1 x2 x3 x4 </list>
<index> i </index>
<value> v </value>
</element>
<element>
<list> y[] </list>
<value> z </value>
</element>