this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2
3/*
4 * Main authors:
5 * Guido Tack <guido.tack@monash.edu>
6 */
7
8/* This Source Code Form is subject to the terms of the Mozilla Public
9 * License, v. 2.0. If a copy of the MPL was not distributed with this
10 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
11
12#include <minizinc/eval_par.hh>
13#include <minizinc/flatten_internal.hh>
14#include <minizinc/optimize_constraints.hh>
15
16namespace MiniZinc {
17
18void OptimizeRegistry::reg(const MiniZinc::ASTString& call, optimizer opt) {
19 _m.insert(std::make_pair(call, opt));
20}
21
22OptimizeRegistry::ConstraintStatus OptimizeRegistry::process(EnvI& env, MiniZinc::Item* i,
23 MiniZinc::Call* c,
24 Expression*& rewrite) {
25 auto it = _m.find(c->id());
26 if (it != _m.end()) {
27 return it->second(env, i, c, rewrite);
28 }
29 return CS_NONE;
30}
31
32OptimizeRegistry& OptimizeRegistry::registry() {
33 static OptimizeRegistry reg;
34 return reg;
35}
36
37namespace Optimizers {
38
39OptimizeRegistry::ConstraintStatus o_linear(EnvI& env, Item* ii, Call* c, Expression*& rewrite) {
40 ArrayLit* al_c = eval_array_lit(env, c->arg(0));
41 std::vector<IntVal> coeffs(al_c->size());
42 for (unsigned int i = 0; i < al_c->size(); i++) {
43 coeffs[i] = eval_int(env, (*al_c)[i]);
44 }
45 ArrayLit* al_x = eval_array_lit(env, c->arg(1));
46 std::vector<KeepAlive> x(al_x->size());
47 for (unsigned int i = 0; i < al_x->size(); i++) {
48 x[i] = (*al_x)[i];
49 }
50 IntVal d = 0;
51 simplify_lin<IntLit>(coeffs, x, d);
52 if (coeffs.empty()) {
53 bool failed;
54 if (c->id() == constants().ids.int_.lin_le) {
55 failed = (d > eval_int(env, c->arg(2)));
56 } else if (c->id() == constants().ids.int_.lin_eq) {
57 failed = (d != eval_int(env, c->arg(2)));
58 } else {
59 failed = (d == eval_int(env, c->arg(2)));
60 }
61 if (failed) {
62 return OptimizeRegistry::CS_FAILED;
63 }
64 return OptimizeRegistry::CS_ENTAILED;
65 }
66 if (coeffs.size() == 1 && (ii->isa<ConstraintI>() || ii->cast<VarDeclI>()->e()->ti()->domain() ==
67 constants().literalTrue)) {
68 VarDecl* vd = x[0]()->cast<Id>()->decl();
69 IntSetVal* domain =
70 vd->ti()->domain() != nullptr ? eval_intset(env, vd->ti()->domain()) : nullptr;
71 if (c->id() == constants().ids.int_.lin_eq) {
72 IntVal rd = eval_int(env, c->arg(2)) - d;
73 if (rd % coeffs[0] == 0) {
74 IntVal nd = rd / coeffs[0];
75 if ((domain != nullptr) && !domain->contains(nd)) {
76 return OptimizeRegistry::CS_FAILED;
77 }
78 std::vector<Expression*> args(2);
79 args[0] = x[0]();
80 args[1] = IntLit::a(nd);
81 Call* nc = new Call(Location(), constants().ids.int_.eq, args);
82 nc->type(Type::varbool());
83 rewrite = nc;
84 return OptimizeRegistry::CS_REWRITE;
85 }
86 return OptimizeRegistry::CS_FAILED;
87 }
88 if (c->id() == constants().ids.int_.lin_le) {
89 IntVal ac = std::abs(coeffs[0]);
90 IntVal rd = eval_int(env, c->arg(2)) - d;
91 IntVal ad = std::abs(rd);
92 IntVal nd;
93 if (ad % ac == 0) {
94 nd = rd / coeffs[0];
95 } else {
96 double nd_d = static_cast<double>(ad.toInt()) / static_cast<double>(ac.toInt());
97 if (coeffs[0] >= 0 && rd >= 0) {
98 nd = static_cast<long long int>(std::floor(nd_d));
99 } else if (rd >= 0) {
100 nd = -static_cast<long long int>(std::floor(nd_d));
101 } else if (coeffs[0] >= 0) {
102 nd = -static_cast<long long int>(std::ceil(nd_d));
103 } else {
104 nd = static_cast<long long int>(std::ceil(nd_d));
105 }
106 }
107 bool swapSign = coeffs[0] < 0;
108 if (domain != nullptr) {
109 if (swapSign) {
110 if (domain->max() < nd) {
111 return OptimizeRegistry::CS_FAILED;
112 }
113 if (domain->min() >= nd) {
114 return OptimizeRegistry::CS_ENTAILED;
115 }
116 } else {
117 if (domain->min() > nd) {
118 return OptimizeRegistry::CS_FAILED;
119 }
120 if (domain->max() <= nd) {
121 return OptimizeRegistry::CS_ENTAILED;
122 }
123 }
124 std::vector<Expression*> args(2);
125 args[0] = x[0]();
126 args[1] = IntLit::a(nd);
127 if (swapSign) {
128 std::swap(args[0], args[1]);
129 }
130 Call* nc = new Call(Location(), constants().ids.int_.le, args);
131 nc->type(Type::varbool());
132 rewrite = nc;
133 return OptimizeRegistry::CS_REWRITE;
134 }
135 }
136 } else if (c->id() == constants().ids.int_.lin_eq && coeffs.size() == 2 &&
137 ((coeffs[0] == 1 && coeffs[1] == -1) || (coeffs[1] == 1 && coeffs[0] == -1)) &&
138 eval_int(env, c->arg(2)) - d == 0) {
139 std::vector<Expression*> args(2);
140 args[0] = x[0]();
141 args[1] = x[1]();
142 Call* nc = new Call(Location(), constants().ids.int_.eq, args);
143 rewrite = nc;
144 return OptimizeRegistry::CS_REWRITE;
145 }
146 if (coeffs.size() < al_c->size()) {
147 std::vector<Expression*> coeffs_e(coeffs.size());
148 std::vector<Expression*> x_e(coeffs.size());
149 for (unsigned int i = 0; i < coeffs.size(); i++) {
150 coeffs_e[i] = IntLit::a(coeffs[i]);
151 x_e[i] = x[i]();
152 }
153 auto* al_c_new = new ArrayLit(al_c->loc(), coeffs_e);
154 al_c_new->type(Type::parint(1));
155 auto* al_x_new = new ArrayLit(al_x->loc(), x_e);
156 al_x_new->type(al_x->type());
157
158 std::vector<Expression*> args(3);
159 args[0] = al_c_new;
160 args[1] = al_x_new;
161 args[2] = IntLit::a(eval_int(env, c->arg(2)) - d);
162 Call* nc = new Call(Location(), c->id(), args);
163 nc->type(Type::varbool());
164 for (ExpressionSetIter it = c->ann().begin(); it != c->ann().end(); ++it) {
165 nc->addAnnotation(*it);
166 }
167
168 rewrite = nc;
169 return OptimizeRegistry::CS_REWRITE;
170 }
171 return OptimizeRegistry::CS_OK;
172}
173
174OptimizeRegistry::ConstraintStatus o_lin_exp(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
175 if (c->type().isint()) {
176 ArrayLit* al_c = eval_array_lit(env, c->arg(0));
177 std::vector<IntVal> coeffs(al_c->size());
178 for (unsigned int j = 0; j < al_c->size(); j++) {
179 coeffs[j] = eval_int(env, (*al_c)[j]);
180 }
181 ArrayLit* al_x = eval_array_lit(env, c->arg(1));
182 std::vector<KeepAlive> x(al_x->size());
183 for (unsigned int j = 0; j < al_x->size(); j++) {
184 x[j] = (*al_x)[j];
185 }
186 IntVal d = eval_int(env, c->arg(2));
187 simplify_lin<IntLit>(coeffs, x, d);
188 if (coeffs.empty()) {
189 rewrite = IntLit::a(d);
190 return OptimizeRegistry::CS_REWRITE;
191 }
192 if (coeffs.size() < al_c->size()) {
193 if (coeffs.size() == 1 && coeffs[0] == 1 && d == 0) {
194 rewrite = x[0]();
195 return OptimizeRegistry::CS_REWRITE;
196 }
197
198 std::vector<Expression*> coeffs_e(coeffs.size());
199 std::vector<Expression*> x_e(coeffs.size());
200 for (unsigned int j = 0; j < coeffs.size(); j++) {
201 coeffs_e[j] = IntLit::a(coeffs[j]);
202 x_e[j] = x[j]();
203 }
204 auto* al_c_new = new ArrayLit(al_c->loc(), coeffs_e);
205 al_c_new->type(Type::parint(1));
206 auto* al_x_new = new ArrayLit(al_x->loc(), x_e);
207 al_x_new->type(al_x->type());
208
209 std::vector<Expression*> args(3);
210 args[0] = al_c_new;
211 args[1] = al_x_new;
212 args[2] = IntLit::a(d);
213 Call* nc = new Call(Location(), c->id(), args);
214 nc->type(c->type());
215 for (ExpressionSetIter it = c->ann().begin(); it != c->ann().end(); ++it) {
216 nc->addAnnotation(*it);
217 }
218 rewrite = nc;
219 return OptimizeRegistry::CS_REWRITE;
220 }
221 }
222 return OptimizeRegistry::CS_OK;
223}
224
225OptimizeRegistry::ConstraintStatus o_element(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
226 if (c->arg(0)->isa<IntLit>()) {
227 IntVal idx = eval_int(env, c->arg(0));
228 ArrayLit* al = eval_array_lit(env, c->arg(1));
229 if (idx < 1 || idx > al->size()) {
230 return OptimizeRegistry::CS_FAILED;
231 }
232 Expression* result = (*al)[static_cast<int>(idx.toInt()) - 1];
233 std::vector<Expression*> args(2);
234 args[0] = result;
235 args[1] = c->arg(2);
236 Call* eq = new Call(Location(), constants().ids.int_.eq, args);
237 rewrite = eq;
238 return OptimizeRegistry::CS_REWRITE;
239 }
240 return OptimizeRegistry::CS_OK;
241}
242
243OptimizeRegistry::ConstraintStatus o_clause(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
244 std::vector<VarDecl*> pos;
245 std::vector<VarDecl*> neg;
246 ArrayLit* al_pos = eval_array_lit(env, c->arg(0));
247 for (unsigned int j = 0; j < al_pos->size(); j++) {
248 if (Id* ident = (*al_pos)[j]->dynamicCast<Id>()) {
249 if (ident->decl()->ti()->domain() == nullptr) {
250 pos.push_back(ident->decl());
251 }
252 }
253 }
254 ArrayLit* al_neg = eval_array_lit(env, c->arg(1));
255 for (unsigned int j = 0; j < al_neg->size(); j++) {
256 if (Id* ident = (*al_neg)[j]->dynamicCast<Id>()) {
257 if (ident->decl()->ti()->domain() == nullptr) {
258 neg.push_back(ident->decl());
259 }
260 }
261 }
262 bool subsumed = false;
263 if (!pos.empty() && !neg.empty()) {
264 std::sort(pos.begin(), pos.end());
265 std::sort(neg.begin(), neg.end());
266 unsigned int ix = 0;
267 unsigned int iy = 0;
268 for (;;) {
269 if (pos[ix] == neg[iy]) {
270 subsumed = true;
271 break;
272 }
273 if (pos[ix] < neg[iy]) {
274 ix++;
275 } else {
276 iy++;
277 }
278 if (ix == pos.size() || iy == neg.size()) {
279 break;
280 }
281 }
282 }
283 if (subsumed) {
284 return OptimizeRegistry::CS_ENTAILED;
285 }
286 return OptimizeRegistry::CS_OK;
287}
288
289OptimizeRegistry::ConstraintStatus o_not(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
290 if (c->argCount() == 2) {
291 Expression* e0 = c->arg(0);
292 Expression* e1 = c->arg(1);
293 if (e0->type().isPar() && e1->type().isPar()) {
294 return eval_bool(env, e0) == eval_bool(env, e1) ? OptimizeRegistry::CS_FAILED
295 : OptimizeRegistry::CS_ENTAILED;
296 }
297 if (e1->type().isPar()) {
298 std::swap(e0, e1);
299 }
300 if (e0->type().isPar()) {
301 Call* eq = new Call(Location(), constants().ids.bool_eq,
302 {e1, constants().boollit(!eval_bool(env, e0))});
303 rewrite = eq;
304 return OptimizeRegistry::CS_REWRITE;
305 }
306 }
307 return OptimizeRegistry::CS_OK;
308}
309
310OptimizeRegistry::ConstraintStatus o_div(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
311 if (c->arg(1)->type().isPar()) {
312 IntVal c1v = eval_int(env, c->arg(1));
313 if (c->arg(0)->type().isPar() && c->argCount() == 3 && c->arg(2)->type().isPar()) {
314 IntVal c0v = eval_int(env, c->arg(0));
315 IntVal c2v = eval_int(env, c->arg(2));
316 return (c0v / c1v == c2v) ? OptimizeRegistry::CS_ENTAILED : OptimizeRegistry::CS_FAILED;
317 }
318 }
319 return OptimizeRegistry::CS_OK;
320}
321
322OptimizeRegistry::ConstraintStatus o_times(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
323 Expression* result = nullptr;
324 Expression* arg0 = c->arg(0);
325 Expression* arg1 = c->arg(1);
326 if (arg0->type().isPar() && arg1->type().isPar()) {
327 IntVal c0v = eval_int(env, arg0);
328 IntVal c1v = eval_int(env, arg1);
329 result = IntLit::a(c0v * c1v);
330 } else if (arg0->type().isPar()) {
331 IntVal c0v = eval_int(env, arg0);
332 if (c0v == 0) {
333 result = IntLit::a(0);
334 } else if (c0v == 1) {
335 result = arg1;
336 }
337 } else if (arg1->type().isPar()) {
338 IntVal c1v = eval_int(env, arg1);
339 if (c1v == 0) {
340 result = IntLit::a(0);
341 }
342 if (c1v == 1) {
343 result = arg0;
344 }
345 }
346
347 if (result != nullptr) {
348 if (c->argCount() == 2) {
349 // this is the functional version of times
350 rewrite = result;
351 return OptimizeRegistry::CS_REWRITE;
352 } // this is the relational version of times
353 assert(c->argCount() == 3);
354 rewrite = new Call(Location().introduce(), constants().ids.int_.eq, {c->arg(2), result});
355 return OptimizeRegistry::CS_REWRITE;
356 }
357 return OptimizeRegistry::CS_OK;
358}
359
360OptimizeRegistry::ConstraintStatus o_set_in(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
361 if (c->arg(1)->type().isPar()) {
362 if (c->arg(0)->type().isPar()) {
363 IntSetVal* isv = eval_intset(env, c->arg(1));
364 return isv->contains(eval_int(env, c->arg(0))) ? OptimizeRegistry::CS_ENTAILED
365 : OptimizeRegistry::CS_FAILED;
366 }
367 if (Id* ident = c->arg(0)->dynamicCast<Id>()) {
368 VarDecl* vd = ident->decl();
369 IntSetVal* isv = eval_intset(env, c->arg(1));
370 if (vd->ti()->domain() != nullptr) {
371 IntSetVal* dom = eval_intset(env, vd->ti()->domain());
372 {
373 IntSetRanges isv_r(isv);
374 IntSetRanges dom_r(dom);
375 if (Ranges::subset(dom_r, isv_r)) {
376 return OptimizeRegistry::CS_ENTAILED;
377 }
378 }
379 {
380 IntSetRanges isv_r(isv);
381 IntSetRanges dom_r(dom);
382 if (Ranges::disjoint(dom_r, isv_r)) {
383 return OptimizeRegistry::CS_FAILED;
384 }
385 }
386 } else if (isv->min() == isv->max()) {
387 std::vector<Expression*> args(2);
388 args[0] = vd->id();
389 args[1] = IntLit::a(isv->min());
390 Call* eq = new Call(Location(), constants().ids.int_.eq, args);
391 rewrite = eq;
392 return OptimizeRegistry::CS_REWRITE;
393 }
394 }
395 }
396 return OptimizeRegistry::CS_OK;
397}
398
399OptimizeRegistry::ConstraintStatus o_int_ne(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
400 Expression* e0 = c->arg(0);
401 Expression* e1 = c->arg(1);
402 if (e0->type().isPar() && e1->type().isPar()) {
403 return eval_int(env, e0) != eval_int(env, e1) ? OptimizeRegistry::CS_ENTAILED
404 : OptimizeRegistry::CS_FAILED;
405 }
406 if (e1->isa<Id>()) {
407 std::swap(e0, e1);
408 }
409 if (Id* ident = e0->dynamicCast<Id>()) {
410 if (e1->type().isPar()) {
411 if (ident->decl()->ti()->domain() != nullptr) {
412 IntVal e1v = eval_int(env, e1);
413 IntSetVal* isv = eval_intset(env, ident->decl()->ti()->domain());
414 if (!isv->contains(e1v)) {
415 return OptimizeRegistry::CS_ENTAILED;
416 }
417 if (e1v == isv->min() && e1v == isv->max()) {
418 return OptimizeRegistry::CS_FAILED;
419 }
420 }
421 }
422 }
423
424 return OptimizeRegistry::CS_OK;
425}
426
427OptimizeRegistry::ConstraintStatus o_int_le(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
428 Expression* e0 = c->arg(0);
429 Expression* e1 = c->arg(1);
430 if (e0->type().isPar() && e1->type().isPar()) {
431 return eval_int(env, e0) <= eval_int(env, e1) ? OptimizeRegistry::CS_ENTAILED
432 : OptimizeRegistry::CS_FAILED;
433 }
434 bool swapped = false;
435 if (e1->isa<Id>()) {
436 std::swap(e0, e1);
437 swapped = true;
438 }
439 if (Id* ident = e0->dynamicCast<Id>()) {
440 if (e1->type().isPar()) {
441 if (ident->decl()->ti()->domain() != nullptr) {
442 IntVal e1v = eval_int(env, e1);
443 IntSetVal* isv = eval_intset(env, ident->decl()->ti()->domain());
444 if (!swapped) {
445 if (isv->max() <= e1v) {
446 return OptimizeRegistry::CS_ENTAILED;
447 }
448 if (isv->min() > e1v) {
449 return OptimizeRegistry::CS_FAILED;
450 }
451 } else {
452 if (e1v <= isv->min()) {
453 return OptimizeRegistry::CS_ENTAILED;
454 }
455 if (e1v > isv->max()) {
456 return OptimizeRegistry::CS_FAILED;
457 }
458 }
459 }
460 }
461 }
462
463 return OptimizeRegistry::CS_OK;
464}
465
466class Register {
467private:
468 Model* _keepAliveModel;
469
470public:
471 Register() {
472 GCLock lock;
473 _keepAliveModel = new Model;
474 ASTString id_element("array_int_element");
475 ASTString id_var_element("array_var_int_element");
476 std::vector<Expression*> e;
477 e.push_back(new StringLit(Location(), id_element));
478 e.push_back(new StringLit(Location(), id_var_element));
479 _keepAliveModel->addItem(new ConstraintI(Location(), new ArrayLit(Location(), e)));
480 OptimizeRegistry::registry().reg(constants().ids.int_.lin_eq, o_linear);
481 OptimizeRegistry::registry().reg(constants().ids.int_.lin_le, o_linear);
482 OptimizeRegistry::registry().reg(constants().ids.int_.lin_ne, o_linear);
483 OptimizeRegistry::registry().reg(constants().ids.int_.div, o_div);
484 OptimizeRegistry::registry().reg(constants().ids.int_.times, o_times);
485 OptimizeRegistry::registry().reg(id_element, o_element);
486 OptimizeRegistry::registry().reg(constants().ids.lin_exp, o_lin_exp);
487 OptimizeRegistry::registry().reg(id_var_element, o_element);
488 OptimizeRegistry::registry().reg(constants().ids.clause, o_clause);
489 OptimizeRegistry::registry().reg(constants().ids.bool_clause, o_clause);
490 OptimizeRegistry::registry().reg(constants().ids.bool_not, o_not);
491 OptimizeRegistry::registry().reg(constants().ids.set_in, o_set_in);
492 OptimizeRegistry::registry().reg(constants().ids.int_.ne, o_int_ne);
493 OptimizeRegistry::registry().reg(constants().ids.int_.le, o_int_le);
494 }
495 ~Register() { delete _keepAliveModel; }
496} _r;
497
498} // namespace Optimizers
499
500} // namespace MiniZinc