this repo has no description
dekker.one
1/*
2% FlatZinc built-in redefinitions for linear solvers.
3%
4% AUTHORS
5% Sebastian Brand
6% Gleb Belov
7*/
8
9%-----------------------------------------------------------------------------%
10% Auxiliary: indicator constraints
11% p -> x # 0 where p is a 0/1 variable and # is a comparison
12
13% Base cases
14
15%% used e.g. in element
16predicate aux_float_eq_if_1(var float: x, var float: y, var int: p) =
17 if is_fixed(p) then
18 if 1==fix(p) then x==y else true endif
19 elseif is_fixed(x) /\ is_fixed(y) then %%% Needed to avoid constant domain var
20 if fix(x)!=fix(y) then p==0 else true endif
21 elseif is_fixed(x-y) then %%% Hypothetically possible to land here
22 if 0.0!=fix(x-y) then p==0 else true endif
23 elseif fPostprocessDomains /\ fPostproDom_AUX /\ fPostproDom_DIFF then
24 aux_float_eq_zero_if_1__POST(x - y, p, p)
25 elseif fMZN__UseIndicators then
26 aux_float_eq_if_1__IND(x, y, p)
27 else
28 aux_float_le_if_1(x, y, p) /\
29 aux_float_ge_if_1(x, y, p)
30 endif;
31
32predicate aux_int_eq_if_1(var int: x, var int: y, var int: p) =
33 if is_fixed(p) then
34 if fix(p) = 1 then (x = y) else true endif
35 elseif is_fixed(x) /\ is_fixed(y) then
36 if fix(x) != fix(y) then (p = 0) else true endif
37 % elseif is_fixed(x-y) then % TODO: Necessary for integers??
38 % if 0.0!=fix(x-y) then p==0 else true endif
39 % elseif fPostprocessDomains /\ fPostproDom_AUX /\ fPostproDom_DIFF then
40 % % TODO MIPDomains
41 % elseif fMZN__UseIndicators then % TODO: Necessary for integers??
42 % aux_float_eq_if_1__IND(x, y, p)
43 else
44 aux_int_le_if_1(x, y, p) /\
45 aux_int_ge_if_1(x, y, p)
46 endif;
47
48predicate aux_float_ne_if_1(var float: x, var float: y, var int: p) =
49 if is_fixed(p) then
50 if fix(p) = 1 then (x = y) else true endif
51 elseif is_fixed(x) /\ is_fixed(y) then %%% Needed to avoid constant domain var
52 if (fix(x) = fix(y)) then (p = 0) else true endif
53 elseif is_fixed(x-y) then %%% Hypothetically possible to land here
54 if (0.0 = fix(x-y)) then (p = 0) else true endif
55 % TODO: What is necessary for not equals?
56 % elseif fPostprocessDomains /\ fPostproDom_AUX /\ fPostproDom_DIFF then
57 % aux_float_ne_zero_if_1__POST(x - y, p, p)
58 % elseif fMZN__UseIndicators then
59 % aux_float_ne_if_1__IND(x, y, p)
60 else
61 let { array[1..2] of var bool: q } in
62 ( q[1] -> (x < y) ) /\
63 ( q[2] -> (x > y) ) /\
64 (sum(q) = p)
65 endif;
66
67predicate aux_int_ne_if_1(var int: x, var int: y, var int: p) =
68 if is_fixed(p) then
69 if fix(p) = 1 then (x != y) else true endif
70 elseif is_fixed(x) /\ is_fixed(y) then
71 if fix(x) = fix(y) then (p = 0) else true endif
72 % elseif is_fixed(x-y) then % TODO: Necessary for integers??
73 % if 0.0!=fix(x-y) then p==0 else true endif
74 % elseif fPostprocessDomains /\ fPostproDom_AUX /\ fPostproDom_DIFF then
75 % % TODO MIPDomains
76 % elseif fMZN__UseIndicators then % TODO: Necessary for integers??
77 % aux_float_eq_if_1__IND(x, y, p)
78 else
79 let { array[1..2] of var bool: q } in
80 ( q[1] -> (x < y) ) /\
81 ( q[2] -> (x > y) ) /\
82 (sum(q) = p)
83 endif;
84
85predicate aux_int_le_zero_if_0(var int: x, var int: p) =
86 if is_fixed(p) then
87 if 0==fix(p) then x<=0 else true endif %% 0==fix !!
88 elseif lb(x)>0 then
89 p==1
90 elseif not (0 in dom(x)) then
91 let {
92 constraint assert( ub(x) < infinity,
93 "aux_int_le_zero_if_0: variable \(x)'s domain: dom(\(x)) = \(dom(x)), should have finite upper bound\n" ),
94 set of int: sDomNeg = dom(x) intersect -infinity..-1,
95 constraint assert( card( sDomNeg ) > 0,
96 "Variable \(x): dom(\(x)) = \(dom(x)), but dom() intersect -inf..-1: \(sDomNeg)\n" ),
97 } in
98 aux_int_le_if_0( x, max( sDomNeg ), p )
99 elseif fPostprocessDomains /\ fPostproDom_AUX then
100 aux_int_le_zero_if_1__POST(x, 1-p)
101 elseif fMZN__UseIndicators then
102 aux_int_le_zero_if_0__IND(x, p)
103 else
104 assert( ub(x)<infinity, "Variable \(x) needs finite upper bound for a big-M constraint, current domain \(dom(x))" ) /\
105 x <= ub(x) * p
106 endif;
107
108predicate aux_float_le_zero_if_0(var float: x, var int: p) =
109 %% TODO actually only need has_ub(x) in ub(x)*p but lb/ub fail on var float (not on var -infinity..const) 22.2.19
110 assert( has_bounds(x), "Variable \(x) needs finite bounds for a big-M constraint" ) /\
111 if is_fixed(p) then
112 if 0==fix(p) then x<=0.0 else true endif
113 elseif lb(x)>0.0 then
114 p==1
115 elseif fPostprocessDomains /\ fPostproDom_AUX then
116 aux_float_le_zero_if_1__POST(x, 1-p, 1-p)
117 elseif fMZN__UseIndicators then
118 aux_float_le_zero_if_0__IND(x, p)
119 else
120 x <= ub(x) * p
121 endif;
122
123predicate aux_float_lt_zero_if_0(var float: x, var int: p) =
124 assert( has_bounds(x), "Variable \(x) needs finite bounds for a big-M constraint" ) /\
125 if is_fixed(p) then
126 if 0==fix(p) then x<0.0 else true endif
127 elseif lb(x)>=0.0 then
128 p==1
129 elseif fPostprocessDomains /\ fPostproDom_AUX then
130 aux_float_lt_zero_if_1__POST(x, 1-p, 1-p, float_lt_EPS)
131 elseif fMZN__UseIndicators then
132 aux_float_le_zero_if_0__IND(x+float_lt_EPS, p) %% Here just absolute EPS, TODO
133 else
134%% let { float: rho = float_lt_EPS_coef__ * max(abs(ub(x)), abs(lb(x))) } % same order of magnitude as ub(x)
135 let { float: rho = float_lt_EPS } % absolute eps
136 in
137 %%% This one causes 2x- derivation of EPS:
138 %% x < (ub(x) + rho) * p
139 %%% Better?
140 x <= (ub(x) + rho) * p - rho
141 %%% This just uses absolute eps:
142 %% x < (ub(x) + float_lt_EPS) * p
143 endif;
144
145
146% Derived cases
147predicate aux_int_le_if_0(var int: x, var int: y, var int: p) =
148 aux_int_le_zero_if_0(x - y, p);
149
150predicate aux_int_ge_if_0(var int: x, var int: y, var int: p) =
151 aux_int_le_zero_if_0(y - x, p);
152
153predicate aux_int_le_if_1(var int: x, var int: y, var int: p) =
154 aux_int_le_zero_if_0(x - y, 1 - p);
155
156predicate aux_int_ge_if_1(var int: x, var int: y, var int: p) =
157 aux_int_le_zero_if_0(y - x, 1 - p);
158
159predicate aux_int_lt_if_0(var int: x, var int: y, var int: p) =
160 aux_int_le_zero_if_0(x - y + 1, p);
161
162predicate aux_int_gt_if_0(var int: x, var int: y, var int: p) =
163 aux_int_le_zero_if_0(y - x + 1, p);
164
165predicate aux_int_lt_if_1(var int: x, var int: y, var int: p) =
166 aux_int_le_zero_if_0(x - y + 1, 1 - p);
167
168predicate aux_int_gt_if_1(var int: x, var int: y, var int: p) =
169 aux_int_le_zero_if_0(y - x + 1, 1 - p);
170
171%% int: switching differences to float to avoid creating integer vars
172/* Used anywhere?
173predicate aux_int_le_if_0(var float: x, var float: y, var int: p) =
174 aux_float_le_zero_if_0(x - y, p);
175
176predicate aux_int_ge_if_0(var float: x, var float: y, var int: p) =
177 aux_float_le_zero_if_0(y - x, p);
178
179predicate aux_int_le_if_1(var float: x, var float: y, var int: p) =
180 aux_float_le_zero_if_0(x - y, 1 - p);
181
182predicate aux_int_ge_if_1(var float: x, var float: y, var int: p) =
183 aux_float_le_zero_if_0(y - x, 1 - p);
184
185predicate aux_int_lt_if_0(var float: x, var float: y, var int: p) =
186 aux_float_le_zero_if_0(x - y + 1.0, p);
187
188predicate aux_int_gt_if_0(var float: x, var float: y, var int: p) =
189 aux_float_le_zero_if_0(y - x + 1.0, p);
190
191predicate aux_int_lt_if_1(var float: x, float: y, var int: p) =
192 aux_float_le_zero_if_0(x - y + 1.0, 1 - p);
193*/
194
195predicate aux_float_le_if_0(var float: x, var float: y, var int: p) =
196 aux_float_le_zero_if_0(x - y, p);
197
198predicate aux_float_ge_if_0(var float: x, var float: y, var int: p) =
199 aux_float_le_zero_if_0(y - x, p);
200
201predicate aux_float_le_if_1(var float: x, var float: y, var int: p) =
202 aux_float_le_zero_if_0(x - y, 1 - p);
203
204predicate aux_float_ge_if_1(var float: x, var float: y, var int: p) =
205 aux_float_le_zero_if_0(y - x, 1 - p);
206
207predicate aux_float_lt_if_0(var float: x, var float: y, var int: p) =
208 aux_float_lt_zero_if_0(x - y, p);
209
210predicate aux_float_gt_if_0(var float: x, var float: y, var int: p) =
211 aux_float_lt_zero_if_0(y - x, p);
212
213predicate aux_float_lt_if_1(var float: x, var float: y, var int: p) =
214 aux_float_lt_zero_if_0(x - y, 1 - p);
215
216predicate aux_float_gt_if_1(var float: x, var float: y, var int: p) =
217 aux_float_lt_zero_if_0(y - x, 1 - p);
218
219
220% -------------------------- Domains postpro ---------------------------
221 %% To avoid looking if an original int var x-y exists and has eq_encode:
222 %% Passing both int and float version of the indicator for flexibility:
223predicate aux_float_eq_zero_if_1__POST(var float: x, var int: pI, var float: p);
224
225predicate aux_int_le_zero_if_1__POST(var int: x, var int: p);
226predicate aux_float_le_zero_if_1__POST(var float: x, var int: pI, var float: p);
227predicate aux_float_lt_zero_if_1__POST(var float: x, var int: pI, var float: p, float: eps);