4.2.2.3. Sorting constraints

In this section: arg_sort, decreasing, increasing, sort, strictly_decreasing, strictly_increasing.

arg_sort

1.  predicate arg_sort(array [$$E] of var $$T: xs,
                       array [int] of var $$E: permutation)

2.  predicate arg_sort(array [$$E] of var float: xs,
                       array [int] of var $$E: permutation)

3.  function array [int] of var $$E: arg_sort(array [$$E] of var $$T: xs)

4.  function array [int] of var $$E: arg_sort(array [$$E] of var float: xs)
1, 2.

Constrains permutation to be the permutation which causes xs to be in sorted order hence xs[permutation[i]] <= xs[permutation[i+1]].

The permutation is the stable sort hence xs[permutation[i]] = xs[permutation[i+1]] \(\rightarrow\) permutation[i] < permutation[i+1].

3, 4.

Returns the permutation permutation which causes xs to be in sorted order hence xs[permutation[i]] <= xs[permutation[i+1]].

The permutation is the stable sort hence xs[permutation[i]] = xs[permutation[i+1]] \(\rightarrow\) permutation[i] < permutation[i+1].

decreasing

predicate decreasing(array [$X] of var bool: xs)
predicate decreasing(array [$X] of var opt float: xs)
predicate decreasing(array [$X] of var opt $$E: xs)
predicate decreasing(array [$X] of var set of $$E: xs)

Requires that the array xs is in decreasing order (duplicates are allowed).

increasing

predicate increasing(array [$X] of var bool: xs)
predicate increasing(array [$X] of var float: xs)
predicate increasing(array [$X] of var opt float: xs)
predicate increasing(array [$X] of var $$E: xs)
predicate increasing(array [$X] of var opt $$E: xs)
predicate increasing(array [$X] of var set of $$E: xs)

Requires that the array xs is in increasing order (duplicates are allowed).

sort

1.  predicate sort(array [$$E] of var $$T: xs, array [$$F] of var $$T: ys)

2.  function array [$$E] of var $$T: sort(array [$$E] of var $$T: xs)

  1. Requires that the multiset of values in xs are the same as the multiset of values in ys but ys is in sorted order.

  2. Return a multiset of values that is the same as the multiset of values in xs but in sorted order.

strictly_decreasing

predicate strictly_decreasing(array [$X] of var opt $$E: xs)
predicate strictly_decreasing(array [$X] of var opt float: xs)
predicate strictly_decreasing(array [$X] of var set of $$E: xs)

Requires that the array xs is in a strictly decreasing order (duplicates are not allowed).

strictly_increasing

1.  predicate strictly_increasing(array [$X] of var $$E: xs)

2.  predicate strictly_increasing(array [$X] of var opt $$E: xs)

3.  predicate strictly_increasing(array [$X] of var float: xs)

4.  predicate strictly_increasing(array [$X] of var opt float: xs)

5.  predicate strictly_increasing(array [$X] of var set of $$E: xs)
1, 2.

Requires that the array xs is in a strictly increasing order (duplicates are not allowed).

3-5.

Requires that the array xs is in increasing order (duplicates are allowed).