4.2.2.4. Channeling constraints

In this section: int_set_channel, inverse, inverse_in_range, inverse_set, link_set_to_booleans.

int_set_channel

predicate int_set_channel(array [$$I] of var $$J: ints,
                          array [$$J] of var set of $$I: sets)

Requires that array of int variables ints and array of set variables sets are related such that (ints[i] = j) \(\leftrightarrow\) (i in sets[j]).

inverse

1.  predicate inverse(array [$$X] of var $$Y: f,
                      array [$$Y] of var $$X: invf)

2.  function array [$$E] of var $$F: inverse(array [$$F] of var $$E: f)

3.  function array [$$E] of var opt $$F: inverse(array [$$F] of var opt $$E: f)

4.  function array [$$E] of $$F: inverse(array [$$F] of $$E: f)

  1. Constrains two arrays of int variables, f and invf, to represent inverse functions. All the values in each array must be within the index set of the other array.

2-4.

Given a function f represented as an array, return the inverse function.

inverse_in_range

predicate inverse_in_range(array [$$A] of var $$B: xs,
                           array [$$B] of var $$A: ys)

If the i th variable of the collection xs is assigned to j and if j is in the index set of ys then the j th variable of the collection ys is assigned to i.

Conversely, if the j th variable of the collection ys is assigned to i and if i is in the index set of xs then the i th variable of the collection xs is assigned to j.

inverse_set

predicate inverse_set(array [$$X] of var set of $$Y: f,
                      array [$$Y] of var set of $$X: invf)

Constrains two arrays of set of int variables, f and invf, so that a j in f[i] iff i in invf[j]. All the values in each array’s sets must be within the index set of the other array.