this repo has no description
dekker.one
1%% New annotations
2annotation assume(array[int] of var bool: b);
3annotation int_priority(array[int] of var int: xs,
4 array[int] of ann: br, ann: sel);
5annotation bool_priority(array[int] of var bool: xs,
6 array[int] of ann: br, ann: sel);
7
8%% Half Reifications
9predicate int_eq_imp(var int: a, var int: b, var bool: r);
10predicate int_ne_imp(var int: a, var int: b, var bool: r);
11predicate int_le_imp(var int: a, var int: b, var bool: r);
12predicate int_lt_imp(var int: a, var int: b, var bool: r);
13
14predicate int_lin_eq_imp(array [int] of int: as, array [int] of var int: bs,
15 int: c, var bool: r);
16predicate int_lin_ne_imp(array [int] of int: as, array [int] of var int: bs,
17 int: c, var bool: r);
18predicate int_lin_le_imp(array [int] of int: as, array [int] of var int: bs,
19 int: c, var bool: r);
20
21predicate bool_eq_imp(var bool: a, var bool: b, var bool: r);
22predicate bool_ne_imp(var bool: a, var bool: b, var bool: r);
23predicate bool_le_imp(var bool: a, var bool: b, var bool: r);
24predicate bool_lt_imp(var bool: a, var bool: b, var bool: r);
25
26predicate bool_or_imp(var bool: a, var bool: b, var bool: r);
27predicate bool_and_imp(var bool: a, var bool: b, var bool: r);
28predicate bool_xor_imp(var bool: a, var bool: b, var bool: r);
29
30predicate bool_clause_imp(array [int] of var bool: as, array [int] of var bool: bs,
31 var bool: b);
32predicate array_bool_or_imp(array [int] of var bool: as, var bool: r);
33predicate array_bool_and_imp(array [int] of var bool: as, var bool: r);
34
35predicate bool_lin_eq_imp(array [int] of int: as, array [int] of var bool: bs,
36 var int: c, var bool: r);
37predicate bool_lin_le_imp(array [int] of int: as, array [int] of var bool: bs,
38 var int: c, var bool: r);
39predicate bool_lin_lt_imp(array [int] of int: as, array [int] of var bool: bs,
40 var int: c, var bool: r);
41predicate bool_lin_ne_imp(array [int] of int: as, array [int] of var bool: bs,
42 var int: c, var bool: r);
43
44%% Special cases for binary-ish x, y.
45predicate int_lin_eq_reif(
46 array [int] of int: cs, array [int] of var int: xs, int: k, var bool: r) =
47 let { var bool: a; var bool: b } in
48 (r <-> (a /\ b)) /\ int_lin_le_reif(cs, xs, k, a)
49 /\ int_lin_le_reif([-c | c in cs], xs, -k, b);
50
51predicate bool_xor(var bool: x, var bool: y, var bool: r) =
52 bool_clause([x,y],[r])
53 /\ bool_clause([],[x,y,r])
54 /\ bool_clause([x, r], [y])
55 /\ bool_clause([y, r], [x]);
56
57predicate set_in_reif(var int: x, set of int: s, var bool: r) =
58 if card(s) = max(s) - min(s) + 1 then
59 r <-> (x >= min(s) /\ x <= max(s))
60 else
61 bool_clause([x = k | k in s], [r]) /\ forall (k in s) (x = k -> r)
62 endif;
63
64predicate int_pow(var int: x, var int: y, var int: z) =
65 let {
66 array [dom(x), dom(y)] of int: A = array2d(
67 dom(x),
68 dom(y),
69 [ pow(a, b) | a in dom(x), b in dom(y) ]
70 );
71 } in z = A[x, y];
72
73predicate int_pow(var int: x, int: y, var int: z) =
74 if y = 0 then z = 1
75 elseif y = 1 then z = x
76 else
77 let { var int: zp ::is_defined_var ;
78 constraint int_pow(x, y div 2, zp) :: defines_var(zp); } in
79 if y mod 2 = 0 then
80 z = zp * zp
81 else
82 z = x * zp * zp
83 endif
84 endif;