this repo has no description
dekker.one
1predicate fzn_value_precede_int(int: s, int: t, array[int] of var int: x) =
2 let {
3 int: imin = min(index_set(x)),
4 int: imax = max(index_set(x)),
5 array[imin..imax+1] of var bool: b
6 } in (
7 forall (i in imin..imax) (
8 let {
9 var bool: xis = (x[i] == s)
10 } in
11 (xis -> (b[i+1] == true))
12 /\ ((not xis) -> (b[i] == b[i+1]))
13 /\ ((not b[i]) -> (x[i] != t))
14 )
15 /\ b[imin] == false
16 );