15.6.1 Element Constraint

We start with selection constraints over integers which is called element constraint in the literature.

Syntax and Semantics

An element constraint has has the following form:

$Z = \langle X_1,\ldots,X_n \rangle[Y]$

All a variables $Z, X_1,\ldots,X_n, Y$ denote integers. These integers may be restricted by additional finite domain constraints. The above element constraint is equivalent to

$Z = X_Y \wedge Y \in \{1,\ldots,n\}$

i.e. it says that is the -th element of the list $X_1,\ldots,X_n$ .

Example (Finite Functions)

Element constraints can used to describe applications of finite functions on integers partially. For instance,

$Y = 3^X \wedge X \in \{1,2,3\}$

is equivalently expressed through the following element constraint:

$Y = \langle 3,9,27 \rangle[X]$

This constraint says that Y=f(X) where is the finite function defined through:

$f: \{1,2,3\} \rightarrow Nat, f(Z)=3^Z \mbox{ for all } Z$

Propagation Rules

The operational semantics of element constraints can be specified through the following two propagation rules where i,j are natural numbers and a finite set of natural numbers.

$\begin{array}{rcl} i\not= Z \wedge i = X_j\wedge Z = \langle X_1,\ldots,X_n \rangle[Y] &\rightarrow& j \not= Y \\ Y \in S \wedge \bigwedge_{j\in S} i \not= X_j \wedge Z = \langle X_1,\ldots,X_n \rangle[Y] &\rightarrow& i \not= Z \end{array}$