## 5.10 Reified Constraints

Reified constraints reflect the validity of a constraint C into a 0/1-valued finite domain integer. The propagator realizing a reified constraint is called the reification propagator. The reification propagators wait in the same way as their non-reified counterparts. All reification propagators constrain their last argument to a 0/1-valued finite domain integer.

Let C be a constraint and P the corresponding propagator. Reifying C into a 0/1-valued variable `D` is defined by

This is implemented by

> `D::0#1
> or` `P` `D=1
> [] P^N D=0
> end`

Here, denotes the negation of P (i. e. a propagator for the negation of the denotational semantics of P).

If P is one of `{FD.reified.int Spec X}` and `{FD.reified.dom Spec Xv}`, then denotes `{FD.reified.int ComplSpec X}` and `{FD.reified.dom ComplSpec Xv}`, respectively (where `ComplSpec = compl(Spec)` if `Spec` is a simple domain specification, and `ComplSpec = SSpec` if `Spec = compl(SSpec)`).

For the propagators P wich are parameterized by a relation symbol A, the symbol of the negated relation occurs in . For instance, if P is `{FD.sum Ds '<:' X Y}`, then is `{FD.sum Ds '>=:' X Y}`.

`reified.int`

  > > `{FD.reified.int` `+Spec``` `*D1``` `D2``}`

  reifies `{FD.int Spec D1}` into `D2`.

`reified.dom`

  > > `{FD.reified.dom` `+Spec``` `Dv``` `D``}`

  reifies `{FD.dom Spec Dv}` into `D`.

`reified.sum`

  > > `{FD.reified.sum` `*Dv``` `+A``` `*D1``` `D2``}`

  reifies `{FD.sum Dv A D1}` into `D2`.

`reified.sumC`

  > > `{FD.reified.sumC` `+Iv``` `*Dv``` `+A``` `*D1``` `D2``}`

  reifies `{FD.sumC Iv Dv A D1}` into `D2`.

`reified.sumCN`

  > > `{FD.reified.sumCN` `+Iv``` `*Dvv``` `+A``` `*D1``` `D2``}`

  reifies `{FD.sumCN Iv Dvv A D1}` into `D2`.

`reified.sumAC`

  > > `{FD.reified.sumAC` `+Iv``` `*Dv``` `+A``` `*D1``` `D2``}`

  reifies `{FD.sumAC Iv Dv A D1}` into `D2`.

`reified.sumACN`

  > > `{FD.reified.sumACN` `+Iv``` `*Dvv``` `+A``` `*D1``` `D2``}`

  reifies `{FD.sumACN Iv Dvv A D1}` into `D2`.

`reified.distance`

  > > `{FD.reified.distance` `*D1``` `*D2``` `+A``` `*D3``` `D4``}`

  reifies `{FD.distance D1 D2 A D3}` into `D4`.

`reified.card`

  > > `{FD.reified.card` `*D1``` `*Dv``` `*D2``` `D3``}`

  Dv is a vector of Boolean variables. `FD.reified.card` creates a propagator for

  which reifies into `D3` the conjunction

  > `D1 =<: D1 + ... + Dn
  > D1 + ... + Dn =<: D2`

  More specifically, its operational semantics is defined through

  > `D3 :: 0#1
  > or D1 =<: D1 + ... + Dn
  > D1 + ... + Dn =<: D2
  > D3 = 1
  > [] or D1 >: D1 + ... + Dn
  > [] D1 + ... + Dn >: D2
  > end
  > D3 = 0
  > end`