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 ASTStringMap<optimizer>::t::iterator 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(void) {
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.size() == 0) {
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 } else {
64 return OptimizeRegistry::CS_ENTAILED;
65 }
66 } else if (coeffs.size() == 1 &&
67 (ii->isa<ConstraintI>() ||
68 ii->cast<VarDeclI>()->e()->ti()->domain() == constants().lit_true)) {
69 VarDecl* vd = x[0]()->cast<Id>()->decl();
70 IntSetVal* domain = vd->ti()->domain() ? eval_intset(env, vd->ti()->domain()) : NULL;
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 && !domain->contains(nd)) return OptimizeRegistry::CS_FAILED;
76 std::vector<Expression*> args(2);
77 args[0] = x[0]();
78 args[1] = IntLit::a(nd);
79 Call* c = new Call(Location(), constants().ids.int_.eq, args);
80 c->type(Type::varbool());
81 rewrite = c;
82 return OptimizeRegistry::CS_REWRITE;
83 } else {
84 return OptimizeRegistry::CS_FAILED;
85 }
86 } else if (c->id() == constants().ids.int_.lin_le) {
87 IntVal ac = std::abs(coeffs[0]);
88 IntVal rd = eval_int(env, c->arg(2)) - d;
89 IntVal ad = std::abs(rd);
90 IntVal nd;
91 if (ad % ac == 0) {
92 nd = rd / coeffs[0];
93 } else {
94 double nd_d = static_cast<double>(ad.toInt()) / static_cast<double>(ac.toInt());
95 if (coeffs[0] >= 0 && rd >= 0) {
96 nd = static_cast<long long int>(std::floor(nd_d));
97 } else if (rd >= 0) {
98 nd = -static_cast<long long int>(std::floor(nd_d));
99 } else if (coeffs[0] >= 0) {
100 nd = -static_cast<long long int>(std::ceil(nd_d));
101 } else {
102 nd = static_cast<long long int>(std::ceil(nd_d));
103 }
104 }
105 bool swapSign = coeffs[0] < 0;
106 if (domain) {
107 if (swapSign) {
108 if (domain->max() < nd) {
109 return OptimizeRegistry::CS_FAILED;
110 } else if (domain->min() >= nd)
111 return OptimizeRegistry::CS_ENTAILED;
112 } else {
113 if (domain->min() > nd) {
114 return OptimizeRegistry::CS_FAILED;
115 } else if (domain->max() <= nd)
116 return OptimizeRegistry::CS_ENTAILED;
117 }
118 std::vector<Expression*> args(2);
119 args[0] = x[0]();
120 args[1] = IntLit::a(nd);
121 if (swapSign) std::swap(args[0], args[1]);
122 Call* nc = new Call(Location(), constants().ids.int_.le, args);
123 nc->type(Type::varbool());
124 rewrite = nc;
125 return OptimizeRegistry::CS_REWRITE;
126 }
127 }
128 } else if (c->id() == constants().ids.int_.lin_eq && coeffs.size() == 2 &&
129 ((coeffs[0] == 1 && coeffs[1] == -1) || (coeffs[1] == 1 && coeffs[0] == -1)) &&
130 eval_int(env, c->arg(2)) - d == 0) {
131 std::vector<Expression*> args(2);
132 args[0] = x[0]();
133 args[1] = x[1]();
134 Call* c = new Call(Location(), constants().ids.int_.eq, args);
135 rewrite = c;
136 return OptimizeRegistry::CS_REWRITE;
137 }
138 if (coeffs.size() < al_c->size()) {
139 std::vector<Expression*> coeffs_e(coeffs.size());
140 std::vector<Expression*> x_e(coeffs.size());
141 for (unsigned int i = 0; i < coeffs.size(); i++) {
142 coeffs_e[i] = IntLit::a(coeffs[i]);
143 x_e[i] = x[i]();
144 }
145 ArrayLit* al_c_new = new ArrayLit(al_c->loc(), coeffs_e);
146 al_c_new->type(Type::parint(1));
147 ArrayLit* al_x_new = new ArrayLit(al_x->loc(), x_e);
148 al_x_new->type(al_x->type());
149
150 std::vector<Expression*> args(3);
151 args[0] = al_c_new;
152 args[1] = al_x_new;
153 args[2] = IntLit::a(eval_int(env, c->arg(2)) - d);
154 Call* nc = new Call(Location(), c->id(), args);
155 nc->type(Type::varbool());
156 for (ExpressionSetIter it = c->ann().begin(); it != c->ann().end(); ++it) {
157 nc->addAnnotation(*it);
158 }
159
160 rewrite = nc;
161 return OptimizeRegistry::CS_REWRITE;
162 }
163 return OptimizeRegistry::CS_OK;
164}
165
166OptimizeRegistry::ConstraintStatus o_lin_exp(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
167 if (c->type().isint()) {
168 ArrayLit* al_c = eval_array_lit(env, c->arg(0));
169 std::vector<IntVal> coeffs(al_c->size());
170 for (unsigned int i = 0; i < al_c->size(); i++) {
171 coeffs[i] = eval_int(env, (*al_c)[i]);
172 }
173 ArrayLit* al_x = eval_array_lit(env, c->arg(1));
174 std::vector<KeepAlive> x(al_x->size());
175 for (unsigned int i = 0; i < al_x->size(); i++) {
176 x[i] = (*al_x)[i];
177 }
178 IntVal d = eval_int(env, c->arg(2));
179 simplify_lin<IntLit>(coeffs, x, d);
180 if (coeffs.size() == 0) {
181 rewrite = IntLit::a(d);
182 return OptimizeRegistry::CS_REWRITE;
183 } else if (coeffs.size() < al_c->size()) {
184 if (coeffs.size() == 1 && coeffs[0] == 1 && d == 0) {
185 rewrite = x[0]();
186 return OptimizeRegistry::CS_REWRITE;
187 }
188
189 std::vector<Expression*> coeffs_e(coeffs.size());
190 std::vector<Expression*> x_e(coeffs.size());
191 for (unsigned int i = 0; i < coeffs.size(); i++) {
192 coeffs_e[i] = IntLit::a(coeffs[i]);
193 x_e[i] = x[i]();
194 }
195 ArrayLit* al_c_new = new ArrayLit(al_c->loc(), coeffs_e);
196 al_c_new->type(Type::parint(1));
197 ArrayLit* al_x_new = new ArrayLit(al_x->loc(), x_e);
198 al_x_new->type(al_x->type());
199
200 std::vector<Expression*> args(3);
201 args[0] = al_c_new;
202 args[1] = al_x_new;
203 args[2] = IntLit::a(d);
204 Call* nc = new Call(Location(), c->id(), args);
205 nc->type(c->type());
206 for (ExpressionSetIter it = c->ann().begin(); it != c->ann().end(); ++it) {
207 nc->addAnnotation(*it);
208 }
209 rewrite = nc;
210 return OptimizeRegistry::CS_REWRITE;
211 }
212 }
213 return OptimizeRegistry::CS_OK;
214}
215
216OptimizeRegistry::ConstraintStatus o_element(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
217 if (c->arg(0)->isa<IntLit>()) {
218 IntVal idx = eval_int(env, c->arg(0));
219 ArrayLit* al = eval_array_lit(env, c->arg(1));
220 if (idx < 1 || idx > al->size()) {
221 return OptimizeRegistry::CS_FAILED;
222 }
223 Expression* result = (*al)[static_cast<int>(idx.toInt()) - 1];
224 std::vector<Expression*> args(2);
225 args[0] = result;
226 args[1] = c->arg(2);
227 Call* eq = new Call(Location(), constants().ids.int_.eq, args);
228 rewrite = eq;
229 return OptimizeRegistry::CS_REWRITE;
230 }
231 return OptimizeRegistry::CS_OK;
232}
233
234OptimizeRegistry::ConstraintStatus o_clause(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
235 std::vector<VarDecl*> pos;
236 std::vector<VarDecl*> neg;
237 ArrayLit* al_pos = eval_array_lit(env, c->arg(0));
238 for (unsigned int i = 0; i < al_pos->size(); i++) {
239 if (Id* ident = (*al_pos)[i]->dyn_cast<Id>()) {
240 if (ident->decl()->ti()->domain() == NULL) pos.push_back(ident->decl());
241 }
242 }
243 ArrayLit* al_neg = eval_array_lit(env, c->arg(1));
244 for (unsigned int i = 0; i < al_neg->size(); i++) {
245 if (Id* ident = (*al_neg)[i]->dyn_cast<Id>()) {
246 if (ident->decl()->ti()->domain() == NULL) neg.push_back(ident->decl());
247 }
248 }
249 bool subsumed = false;
250 if (pos.size() > 0 && neg.size() > 0) {
251 std::sort(pos.begin(), pos.end());
252 std::sort(neg.begin(), neg.end());
253 unsigned int ix = 0;
254 unsigned int iy = 0;
255 for (;;) {
256 if (pos[ix] == neg[iy]) {
257 subsumed = true;
258 break;
259 }
260 if (pos[ix] < neg[iy]) {
261 ix++;
262 } else {
263 iy++;
264 }
265 if (ix == pos.size() || iy == neg.size()) break;
266 }
267 }
268 if (subsumed) {
269 return OptimizeRegistry::CS_ENTAILED;
270 } else {
271 return OptimizeRegistry::CS_OK;
272 }
273}
274
275OptimizeRegistry::ConstraintStatus o_div(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
276 if (c->arg(1)->type().ispar()) {
277 IntVal c1v = eval_int(env, c->arg(1));
278 if (c->arg(0)->type().ispar() && c->n_args() == 3 && c->arg(2)->type().ispar()) {
279 IntVal c0v = eval_int(env, c->arg(0));
280 IntVal c2v = eval_int(env, c->arg(2));
281 return (c0v / c1v == c2v) ? OptimizeRegistry::CS_ENTAILED : OptimizeRegistry::CS_FAILED;
282 }
283 }
284 return OptimizeRegistry::CS_OK;
285}
286
287OptimizeRegistry::ConstraintStatus o_set_in(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
288 if (c->arg(1)->type().ispar()) {
289 if (c->arg(0)->type().ispar()) {
290 IntSetVal* isv = eval_intset(env, c->arg(1));
291 return isv->contains(eval_int(env, c->arg(0))) ? OptimizeRegistry::CS_ENTAILED
292 : OptimizeRegistry::CS_FAILED;
293 } else if (Id* ident = c->arg(0)->dyn_cast<Id>()) {
294 VarDecl* vd = ident->decl();
295 IntSetVal* isv = eval_intset(env, c->arg(1));
296 if (vd->ti()->domain()) {
297 IntSetVal* dom = eval_intset(env, vd->ti()->domain());
298 {
299 IntSetRanges isv_r(isv);
300 IntSetRanges dom_r(dom);
301 if (Ranges::subset(dom_r, isv_r)) return OptimizeRegistry::CS_ENTAILED;
302 }
303 {
304 IntSetRanges isv_r(isv);
305 IntSetRanges dom_r(dom);
306 if (Ranges::disjoint(dom_r, isv_r)) return OptimizeRegistry::CS_FAILED;
307 }
308 } else if (isv->min() == isv->max()) {
309 std::vector<Expression*> args(2);
310 args[0] = vd->id();
311 args[1] = IntLit::a(isv->min());
312 Call* eq = new Call(Location(), constants().ids.int_.eq, args);
313 rewrite = eq;
314 return OptimizeRegistry::CS_REWRITE;
315 }
316 }
317 }
318 return OptimizeRegistry::CS_OK;
319}
320
321OptimizeRegistry::ConstraintStatus o_int_ne(EnvI& env, Item* i, Call* c, Expression*& rewrite) {
322 Expression* e0 = c->arg(0);
323 Expression* e1 = c->arg(1);
324 if (e0->type().ispar() && e1->type().ispar()) {
325 return eval_int(env, e0) != eval_int(env, e1) ? OptimizeRegistry::CS_ENTAILED
326 : OptimizeRegistry::CS_FAILED;
327 }
328 if (e1->isa<Id>()) {
329 std::swap(e0, e1);
330 }
331 if (Id* ident = e0->dyn_cast<Id>()) {
332 if (e1->type().ispar()) {
333 if (ident->decl()->ti()->domain()) {
334 IntVal e1v = eval_int(env, e1);
335 IntSetVal* isv = eval_intset(env, ident->decl()->ti()->domain());
336 if (!isv->contains(e1v)) return OptimizeRegistry::CS_ENTAILED;
337 if (e1v == isv->min() && e1v == isv->max()) return OptimizeRegistry::CS_FAILED;
338 }
339 }
340 }
341
342 return OptimizeRegistry::CS_OK;
343}
344
345class Register {
346private:
347 Model* _keepAliveModel;
348
349public:
350 Register(void) {
351 GCLock lock;
352 _keepAliveModel = new Model;
353 ASTString id_element("array_int_element");
354 ASTString id_var_element("array_var_int_element");
355 std::vector<Expression*> e;
356 e.push_back(new StringLit(Location(), id_element));
357 e.push_back(new StringLit(Location(), id_var_element));
358 _keepAliveModel->addItem(new ConstraintI(Location(), new ArrayLit(Location(), e)));
359 OptimizeRegistry::registry().reg(constants().ids.int_.lin_eq, o_linear);
360 OptimizeRegistry::registry().reg(constants().ids.int_.lin_le, o_linear);
361 OptimizeRegistry::registry().reg(constants().ids.int_.lin_ne, o_linear);
362 OptimizeRegistry::registry().reg(constants().ids.int_.div, o_div);
363 OptimizeRegistry::registry().reg(id_element, o_element);
364 OptimizeRegistry::registry().reg(constants().ids.lin_exp, o_lin_exp);
365 OptimizeRegistry::registry().reg(id_var_element, o_element);
366 OptimizeRegistry::registry().reg(constants().ids.clause, o_clause);
367 OptimizeRegistry::registry().reg(constants().ids.bool_clause, o_clause);
368 OptimizeRegistry::registry().reg(constants().ids.set_in, o_set_in);
369 OptimizeRegistry::registry().reg(constants().ids.int_.ne, o_int_ne);
370 }
371 ~Register(void) { delete _keepAliveModel; }
372} _r;
373
374} // namespace Optimizers
375
376} // namespace MiniZinc