this repo has no description
dekker.one
1/***
2!Test
3solvers: [gecode]
4expected:
5- !Result
6 solution: !Solution
7 x: 2
8***/
9
10% Test a simple equality constraint after creating a encoding with a reverse mapper.
11% The correct behaviour is that this needs to be posted as a constraints.
12% Previously an optimisation would simply change the domain, which is incorrect once the encoding has been created.
13var 1..2: x;
14array[int] of var bool: x_enc = unary_encode(x);
15constraint x = 2;
16
17% Simple unary SAT encoding for integers with two options
18function array[int] of var bool: unary_encode(var int: x) ::promise_total =
19 let {
20 array[lb(x)..ub(x)] of var bool: x_enc::expression_name("unary_encoding");
21 constraint ub(x) - lb(x) = 1;
22 constraint bool_not(x_enc[lb(x)], x_enc[ub(x)]);
23 constraint (x = reverse_unary(x_enc))::is_reverse_map;
24 } in x_enc;
25
26predicate int_eq(var int: x, int: y) =
27 let {
28 array[int] of var bool: x_enc = unary_encode(x);
29 } in x_enc[y];
30
31% Reverse mappings (unary to integer)
32function var int: reverse_unary(array[int] of var bool: x_enc);
33function int: reverse_unary(array[int] of bool: x_enc) = arg_max(x_enc);