this repo has no description
dekker.one
1%-----------------------------------------------------------------------------%
2% Reflect an array of comparison values onto a comparison value variable using
3% a lexicographic interpretation of the array. The comparison values are
4% encoded as follows: > | = | < as -1 | 0 | +1.
5% Uses of this constraint are generated by Cadmium transformations that
6% simplify ordering constraints on expressions of complex types.
7%-----------------------------------------------------------------------------%
8predicate comparison_rel_array(array[int] of var -1..1: rels, var -1..1: rel) =
9 let { int: l = min(index_set(rels)),
10 int: u = max(index_set(rels)),
11 array[l-1..u] of var -1..1: r }
12 in
13 r[l-1] = 0 % initial state (before first array position) is 'equal'
14 /\
15 forall (i in l..u) (
16 % new state: as given array at current position if
17 % previous state is 'equal', otherwise previous state
18 %
19 % r[i] = (if r[i-1] = 0 then rels[i] else r[i-1] endif)
20 (r[i-1] = 0 -> r[i] = rels[i])
21 /\
22 (r[i-1] != 0 -> r[i] = r[i-1])
23 )
24 /\
25 r[u] = rel; % final state (at last array position)
26