this repo has no description
dekker.one
1predicate fzn_value_precede_set(int: s, int: t, array[int] of var set of 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 = (s in x[i] /\ not (t in x[i]))
10 } in
11 (xis -> (b[i + 1] == true))
12 /\ ((not xis) -> (b[i] == b[i + 1]))
13 /\ ((not b[i]) -> (s in x[i] \/ not (t in x[i])))
14 )
15 /\ b[imin] == false
16 );