this repo has no description
dekker.one
1%-----------------------------------------------------------------------------%
2% A 'table' constraint table(x, T) represents the constraint x in T where we
3% consider each row in T to be a tuple and T as a set of tuples.
4%
5% Linear version.
6%
7% See also the equality encoding of the 'element' constraint.
8%-----------------------------------------------------------------------------%
9
10predicate table_int(array[int] of var int: x, array[int, int] of int: t) =
11 assert(index_set_2of2(t) = index_set(x),
12 "The second dimension of the table must equal the number of " ++
13 "variables in the first argument",
14 let { set of int: it = index_set_1of2(t),
15 array[it] of var 0..1: lambda }
16 in
17 sum(lambda) = 1
18 /\
19 forall(j in index_set(x))( sum(i in it)( t[i,j]*lambda[i] ) = x[j] ) );
20
21%-----------------------------------------------------------------------------%