( C x = 1) x 0#1where it is assumed that x does not occur free in C.

The operational semantics of a propagator for the reification of a constraint C with respect to x is given by the following rules:

- If the constraint store entails x = 1, the propagator for the reification reduces to a propagator for C.
- If the constraint store entails x = 0, the propagator for the reification reduces to a propagator for C.
- If a propagator for C would realize that the constraint store entails C, the propagator for the reification tells x = 1 and ceases to exist.
- If a propagator for C would realize that the constraint store is inconsistent with C, the propagator for the reification tells x = 0 and ceases to exist.

- Reified.intvar (s, dom, b)

Returns an FD variable freshly created in s. Also, a propagator is created to ensure b is true if and only if the intvar returned is in dom. - Reified.intvarVec (s, n, dom, b)

Returns a vector of FD variables freshly created in s. Also, a propagator is created to ensure b is true if and only if all the intvars returned are in dom. - Reified.dom (s, x, dom, b)

Creates a propagator in s to ensure b is true if and only if x is in dom. - Reified.rel (s, x, rel, y, b),Reified.relI (s, x, rel, n, b)

Creates a propagator in s to ensure b is true if and only if x is in rel with y (or n). - Reified.linear (s, v, rel, n, b, level)

Creates a propagator in s to ensure b is true if and only if the regular linear constraint holds for the arguments.

Andreas Rossberg 2006-08-28