1/*
2% FlatZinc built-in redefinitions for linear solvers.
3%
4% AUTHORS
5% Sebastian Brand
6% Gleb Belov
7*/
8
9%-----------------------------------------------------------------------------%
10%
11% Logic operations
12% Use indicators for reifs (CPLEX)?  Seems weak.
13%
14%-----------------------------------------------------------------------------%
15
16predicate bool_not(var bool: p) = bool2int(p)=0;
17
18predicate bool_not(var bool: p, var bool: q) =
19    bool2int(p) + bool2int(q) = 1;
20
21predicate bool_and(var bool: p, var bool: q, var bool: r) =
22%  my_trace("  bool_and: \(p) /\\ \(q) <-> \(r) \n") /\
23  if false then
24      int_lin_le_reif__IND( [-1, -1], [p, q], -2, r)
25  else
26    array_bool_and( [p, q], r )
27%    bool_and__INT(bool2int(p), bool2int(q), bool2int(r))
28  endif;
29
30predicate bool_and__INT(var int: x, var int: y, var int: z) =
31    x + y <= z + 1 /\
32    %% x + y >= z * 2;         % weak
33    x >= z /\ y >= z;     % strong
34
35
36predicate bool_or(var bool: p, var bool: q, var bool: r) =
37  if false then
38      int_lin_le_reif__IND( [-1, -1], [p, q], -1, r)
39  elseif true then
40    array_bool_or( [p, q], r )
41  else
42    let { var int: x = bool2int(p),
43          var int: y = bool2int(q),
44          var int: z = bool2int(r) }
45    in
46    x + y >= z /\
47    % x + y <= z * 2;       % weak
48    x <= z /\ y <= z   % strong
49  endif;
50
51predicate bool_xor(var bool: p, var bool: q) =
52  1==p+q;
53
54predicate bool_xor(var bool: p, var bool: q, var bool: r) =
55  if false then
56%      int_lin_eq_reif__IND( [1, 1], [p, q], 1, r) /\
57    true
58  else
59    let { var int: x = bool2int(p),
60          var int: y = bool2int(q),
61          var int: z = bool2int(r) }
62    in
63    x <= y + z /\
64    y <= x + z /\
65    z <= x + y /\
66    x + y + z <= 2
67  endif;
68
69
70predicate bool_eq_reif(var bool: p, var bool: q, var bool: r) =
71%%    trace(" bool_eq_reif: \(p), \(q), \(r) \n") /\
72    if is_fixed(r) then   % frequent case
73        if fix(r) = true then p = q else bool_not(p,q) endif
74    elseif is_fixed(q) then
75        if fix(q) = true then p = r
76        else bool_not(p,r) endif
77    elseif is_fixed(p) then
78        if fix(p) = true then q = r
79        else bool_not(q,r) endif
80    elseif false then
81%      int_lin_eq_reif__IND( [1, -1], [p, q], 0, r) /\
82      true
83    else
84      let { var int: x = bool2int(p),
85            var int: y = bool2int(q),
86            var int: z = bool2int(r) }
87      in
88      x + y <= z + 1 /\
89      x + z <= y + 1 /\
90      y + z <= x + 1 /\
91      x + y + z >= 1
92    endif;
93
94
95predicate bool_ne_reif(var bool: p, var bool: q, var bool: r) =
96    bool_xor(p, q, r);
97
98
99predicate bool_le(var bool: p, var bool: q) =
100    let { var int: x = bool2int(p),
101          var int: y = bool2int(q) }
102    in
103    x <= y;
104
105
106predicate bool_le_reif(var bool: p, var bool: q, var bool: r) =
107  if false then
108%      int_lin_le_reif__IND( [1, -1], [p, q], 0, r) /\
109    true
110  else
111    let { var int: x = bool2int(p),
112          var int: y = bool2int(q),
113          var int: z = bool2int(r) }
114    in
115    1 - x + y >= z /\
116      %% /\ 1 - x + y <= z * 2      not needed
117    1 - x <= z /\ y <= z % strong
118  endif;
119
120
121predicate bool_lt(var bool: p, var bool: q) =
122    not p /\ q;
123
124
125predicate bool_lt_reif(var bool: p, var bool: q, var bool: r) =
126    (not p /\ q) <-> r;
127
128%-----------------------------------------------------------------------------%
129
130%% Reified disjunction
131predicate array_bool_or(array[int] of var bool: a, var bool: b) =
132    if exists( i in index_set( a ) )( is_fixed(a[i]) /\ fix(a[i]) ) then
133      b
134    elseif is_fixed(b) then   % frequent case
135        if fix(b) = true then
136            sum(i in index_set(a))( bool2int(a[i]) ) >= 1       %% >=1 seems better for MIPDomains... 5.4.19
137        else
138            forall(i in index_set(a))( not a[i] )
139        endif
140    else
141      let { var int: x = bool2int(b),
142          array[1..length(a)] of var int: c =
143              [ bool2int(a[i]) | i in index_set(a) ] }
144    in
145        sum(c) >= x /\
146          %  sum(c) <= x * length(a)                     % weak
147        forall (i in index_set(a)) (x >= c[i])        % strong
148    endif;
149
150%% Reified conjunction
151predicate array_bool_and(array[int] of var bool: a, var bool: b) =
152    if exists( i in index_set( a ) )( is_fixed(a[i]) /\ not fix(a[i]) ) then
153      not b
154    elseif is_fixed(b) then            % frequent case
155        if fix(b) = false then
156            sum(i in index_set(a))( bool2int(a[i]) ) <= length(a)-1
157        else
158            forall(i in index_set(a))( a[i] )
159        endif
160    else
161      let { var int: x = bool2int(b),
162          array[1..length(a)] of var int: c =
163              [ bool2int(a[i]) | i in index_set(a) ] }
164      in
165      length(a) - sum(c) >=  1 - x /\
166        % length(a) - sum(c) <= (1 - x) * length(a);     % weak
167      forall (i in index_set(a)) (x <= c[i])        % strong
168    endif;
169
170% predicate array_bool_xor(array[int] of var bool: a) = .. sum(a) is odd ..
171predicate array_bool_xor(array[int] of var bool: a) =
172     let { var 0..(length(a)-1) div 2: m,
173           var 1..((length(a)-1) div 2)*2+1: ss = sum(i in index_set(a))( bool2int(a[i]) ) }
174     in
175       ss == 1 + 2 * m;
176
177predicate bool_clause(array[int] of var bool: p, array[int] of var bool: n) =
178      sum(i in index_set(p))( bool2int(p[i]) )
179    - sum(i in index_set(n))( bool2int(n[i]) )
180    + length(n)
181    >= 1;
182
183predicate bool_lin_eq(array[int] of int: c, array[int] of var bool: x, var int: d) :: promise_total =
184  sum(i in index_set(x))( c[i]*bool2int(x[i]) ) == d;
185
186predicate bool_lin_eq_reif(array[int] of int: c, array[int] of var bool: x,
187                          int: d, var bool: b) =                                %% No var int d, sorry
188    aux_int_eq_iff_1(sum(i in index_set(x))( c[i]*bool2int(x[i]) ), d, bool2int(b));
189
190
191