this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Christian Schulte <schulte@gecode.org>
5 *
6 * Copyright:
7 * Christian Schulte, 2006
8 *
9 * This file is part of Gecode, the generic constraint
10 * development environment:
11 * http://www.gecode.org
12 *
13 * Permission is hereby granted, free of charge, to any person obtaining
14 * a copy of this software and associated documentation files (the
15 * "Software"), to deal in the Software without restriction, including
16 * without limitation the rights to use, copy, modify, merge, publish,
17 * distribute, sublicense, and/or sell copies of the Software, and to
18 * permit persons to whom the Software is furnished to do so, subject to
19 * the following conditions:
20 *
21 * The above copyright notice and this permission notice shall be
22 * included in all copies or substantial portions of the Software.
23 *
24 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
25 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
26 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
27 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
28 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
29 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
30 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
31 *
32 */
33
34#include <gecode/minimodel.hh>
35
36namespace Gecode { namespace MiniModel {
37
38 /// Non-linear arithmetic expressions over integer variables
39 class GECODE_MINIMODEL_EXPORT ArithNonLinIntExpr : public NonLinIntExpr {
40 public:
41 /// The expression type
42 enum ArithNonLinIntExprType {
43 ANLE_ABS, ///< Absolute value expression
44 ANLE_MIN, ///< Minimum expression
45 ANLE_MAX, ///< Maximum expression
46 ANLE_MULT, ///< Multiplication expression
47 ANLE_DIV, ///< Division expression
48 ANLE_MOD, ///< Modulo expression
49 ANLE_SQR, ///< Square expression
50 ANLE_SQRT, ///< Square root expression
51 ANLE_POW, ///< Pow expression
52 ANLE_NROOT, ///< Nroot expression
53 ANLE_ELMNT, ///< Element expression
54 ANLE_ITE ///< If-then-else expression
55 } t;
56 /// Expressions
57 LinIntExpr* a;
58 /// Size of variable array
59 int n;
60 /// Integer argument (used in nroot for example)
61 int aInt;
62 /// Boolean expression argument (used in ite for example)
63 BoolExpr b;
64 /// Constructor
65 ArithNonLinIntExpr(ArithNonLinIntExprType t0, int n0)
66 : t(t0), a(heap.alloc<LinIntExpr>(n0)), n(n0) {}
67 /// Constructor
68 ArithNonLinIntExpr(ArithNonLinIntExprType t0, int n0, int a0)
69 : t(t0), a(heap.alloc<LinIntExpr>(n0)), n(n0), aInt(a0) {}
70 /// Constructor
71 ArithNonLinIntExpr(ArithNonLinIntExprType t0, int n0, const BoolExpr& b0)
72 : t(t0), a(heap.alloc<LinIntExpr>(n0)), n(n0), b(b0) {}
73 /// Destructor
74 ~ArithNonLinIntExpr(void) {
75 heap.free<LinIntExpr>(a,n);
76 }
77 /// Post expression
78 virtual IntVar post(Home home, IntVar* ret,
79 const IntPropLevels& ipls) const {
80 IntVar y;
81 switch (t) {
82 case ANLE_ABS:
83 {
84 IntVar x = a[0].post(home, ipls);
85 if (x.min() >= 0)
86 y = result(home,ret,x);
87 else {
88 y = result(home,ret);
89 abs(home, x, y, ipls.abs());
90 }
91 }
92 break;
93 case ANLE_MIN:
94 if (n==1) {
95 y = result(home,ret, a[0].post(home, ipls));
96 } else if (n==2) {
97 IntVar x0 = a[0].post(home, ipls);
98 IntVar x1 = a[1].post(home, ipls);
99 if (x0.max() <= x1.min())
100 y = result(home,ret,x0);
101 else if (x1.max() <= x0.min())
102 y = result(home,ret,x1);
103 else {
104 y = result(home,ret);
105 min(home, x0, x1, y, ipls.min2());
106 }
107 } else {
108 IntVarArgs x(n);
109 for (int i=n; i--;)
110 x[i] = a[i].post(home, ipls);
111 y = result(home,ret);
112 min(home, x, y, ipls.min());
113 }
114 break;
115 case ANLE_MAX:
116 if (n==1) {
117 y = result(home,ret,a[0].post(home, ipls));
118 } else if (n==2) {
119 IntVar x0 = a[0].post(home, ipls);
120 IntVar x1 = a[1].post(home, ipls);
121 if (x0.max() <= x1.min())
122 y = result(home,ret,x1);
123 else if (x1.max() <= x0.min())
124 y = result(home,ret,x0);
125 else {
126 y = result(home,ret);
127 max(home, x0, x1, y, ipls.max2());
128 }
129 } else {
130 IntVarArgs x(n);
131 for (int i=n; i--;)
132 x[i] = a[i].post(home, ipls);
133 y = result(home,ret);
134 max(home, x, y, ipls.max());
135 }
136 break;
137 case ANLE_MULT:
138 {
139 assert(n == 2);
140 IntVar x0 = a[0].post(home, ipls);
141 IntVar x1 = a[1].post(home, ipls);
142 if (x0.assigned() && (x0.val() == 0))
143 y = result(home,ret,x0);
144 else if (x0.assigned() && (x0.val() == 1))
145 y = result(home,ret,x1);
146 else if (x1.assigned() && (x1.val() == 0))
147 y = result(home,ret,x1);
148 else if (x1.assigned() && (x1.val() == 1))
149 y = result(home,ret,x0);
150 else {
151 y = result(home,ret);
152 mult(home, x0, x1, y, ipls.mult());
153 }
154 }
155 break;
156 case ANLE_DIV:
157 {
158 assert(n == 2);
159 IntVar x0 = a[0].post(home, ipls);
160 IntVar x1 = a[1].post(home, ipls);
161 rel(home, x1, IRT_NQ, 0);
162 if (x1.assigned() && (x1.val() == 1))
163 y = result(home,ret,x0);
164 else if (x0.assigned() && (x0.val() == 0))
165 y = result(home,ret,x0);
166 else {
167 y = result(home,ret);
168 div(home, x0, x1, y, ipls.div());
169 }
170 }
171 break;
172 case ANLE_MOD:
173 {
174 assert(n == 2);
175 IntVar x0 = a[0].post(home, ipls);
176 IntVar x1 = a[1].post(home, ipls);
177 y = result(home,ret);
178 mod(home, x0, x1, y, ipls.mod());
179 }
180 break;
181 case ANLE_SQR:
182 {
183 assert(n == 1);
184 IntVar x = a[0].post(home, ipls);
185 if (x.assigned() && ((x.val() == 0) || (x.val() == 1)))
186 y = result(home,ret,x);
187 else {
188 y = result(home,ret);
189 sqr(home, x, y, ipls.sqr());
190 }
191 }
192 break;
193 case ANLE_SQRT:
194 {
195 assert(n == 1);
196 IntVar x = a[0].post(home, ipls);
197 if (x.assigned() && ((x.val() == 0) || (x.val() == 1)))
198 y = result(home,ret,x);
199 else {
200 y = result(home,ret);
201 sqrt(home, x, y, ipls.sqrt());
202 }
203 }
204 break;
205 case ANLE_POW:
206 {
207 assert(n == 1);
208 IntVar x = a[0].post(home, ipls);
209 if (x.assigned() && (aInt > 0) &&
210 ((x.val() == 0) || (x.val() == 1)))
211 y = result(home,ret,x);
212 else {
213 y = result(home,ret);
214 pow(home, x, aInt, y, ipls.pow());
215 }
216 }
217 break;
218 case ANLE_NROOT:
219 {
220 assert(n == 1);
221 IntVar x = a[0].post(home, ipls);
222 if (x.assigned() && (aInt > 0) &&
223 ((x.val() == 0) || (x.val() == 1)))
224 y = result(home,ret,x);
225 else {
226 y = result(home,ret);
227 nroot(home, x, aInt, y, ipls.nroot());
228 }
229 }
230 break;
231 case ANLE_ELMNT:
232 {
233 IntVar z = a[n-1].post(home, ipls);
234 if (z.assigned() && z.val() >= 0 && z.val() < n-1) {
235 y = result(home,ret,a[z.val()].post(home, ipls));
236 } else {
237 IntVarArgs x(n-1);
238 bool assigned = true;
239 for (int i=n-1; i--;) {
240 x[i] = a[i].post(home, ipls);
241 if (!x[i].assigned())
242 assigned = false;
243 }
244 y = result(home,ret);
245 if (assigned) {
246 IntArgs xa(n-1);
247 for (int i=n-1; i--;)
248 xa[i] = x[i].val();
249 element(home, xa, z, y, ipls.element());
250 } else {
251 element(home, x, z, y, ipls.element());
252 }
253 }
254 }
255 break;
256 case ANLE_ITE:
257 {
258 assert(n == 2);
259 BoolVar c = b.expr(home, ipls);
260 IntVar x0 = a[0].post(home, ipls);
261 IntVar x1 = a[1].post(home, ipls);
262 y = result(home,ret);
263 ite(home, c, x0, x1, y, ipls.ite());
264 }
265 break;
266 default:
267 GECODE_NEVER;
268 }
269 return y;
270 }
271 virtual void post(Home home, IntRelType irt, int c,
272 const IntPropLevels& ipls) const {
273 if ((t == ANLE_MIN && (irt == IRT_GQ || irt == IRT_GR)) ||
274 (t == ANLE_MAX && (irt == IRT_LQ || irt == IRT_LE)) ) {
275 IntVarArgs x(n);
276 for (int i=n; i--;)
277 x[i] = a[i].post(home, ipls);
278 rel(home, x, irt, c);
279 } else {
280 rel(home, post(home,nullptr,ipls), irt, c);
281 }
282 }
283 virtual void post(Home home, IntRelType irt, int c, BoolVar b,
284 const IntPropLevels& ipls) const {
285 rel(home, post(home,nullptr,ipls), irt, c, b);
286 }
287 };
288 /// Check if \a e is of type \a t
289 bool hasType(const LinIntExpr& e, ArithNonLinIntExpr::ArithNonLinIntExprType t) {
290 return e.nle() &&
291 dynamic_cast<ArithNonLinIntExpr*>(e.nle()) != nullptr &&
292 dynamic_cast<ArithNonLinIntExpr*>(e.nle())->t == t;
293 }
294
295}}
296
297namespace Gecode {
298
299 LinIntExpr
300 abs(const LinIntExpr& e) {
301 using namespace MiniModel;
302 if (hasType(e, ArithNonLinIntExpr::ANLE_ABS))
303 return e;
304 ArithNonLinIntExpr* ae =
305 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_ABS,1);
306 ae->a[0] = e;
307 return LinIntExpr(ae);
308 }
309
310 LinIntExpr
311 min(const LinIntExpr& e0, const LinIntExpr& e1) {
312 using namespace MiniModel;
313 int n = 0;
314 if (hasType(e0, ArithNonLinIntExpr::ANLE_MIN))
315 n += static_cast<ArithNonLinIntExpr*>(e0.nle())->n;
316 else
317 n += 1;
318 if (hasType(e1, ArithNonLinIntExpr::ANLE_MIN))
319 n += static_cast<ArithNonLinIntExpr*>(e1.nle())->n;
320 else
321 n += 1;
322 ArithNonLinIntExpr* ae =
323 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_MIN,n);
324 int i=0;
325 if (hasType(e0, ArithNonLinIntExpr::ANLE_MIN)) {
326 ArithNonLinIntExpr* e0e = static_cast<ArithNonLinIntExpr*>(e0.nle());
327 for (; i<e0e->n; i++)
328 ae->a[i] = e0e->a[i];
329 } else {
330 ae->a[i++] = e0;
331 }
332 if (hasType(e1, ArithNonLinIntExpr::ANLE_MIN)) {
333 ArithNonLinIntExpr* e1e = static_cast<ArithNonLinIntExpr*>(e1.nle());
334 int curN = i;
335 for (; i<curN+e1e->n; i++)
336 ae->a[i] = e1e->a[i-curN];
337 } else {
338 ae->a[i++] = e1;
339 }
340 return LinIntExpr(ae);
341 }
342
343 LinIntExpr
344 max(const LinIntExpr& e0, const LinIntExpr& e1) {
345 using namespace MiniModel;
346 int n = 0;
347 if (hasType(e0, ArithNonLinIntExpr::ANLE_MAX))
348 n += static_cast<ArithNonLinIntExpr*>(e0.nle())->n;
349 else
350 n += 1;
351 if (hasType(e1, ArithNonLinIntExpr::ANLE_MAX))
352 n += static_cast<ArithNonLinIntExpr*>(e1.nle())->n;
353 else
354 n += 1;
355 ArithNonLinIntExpr* ae =
356 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_MAX,n);
357 int i=0;
358 if (hasType(e0, ArithNonLinIntExpr::ANLE_MAX)) {
359 ArithNonLinIntExpr* e0e = static_cast<ArithNonLinIntExpr*>(e0.nle());
360 for (; i<e0e->n; i++)
361 ae->a[i] = e0e->a[i];
362 } else {
363 ae->a[i++] = e0;
364 }
365 if (hasType(e1, ArithNonLinIntExpr::ANLE_MAX)) {
366 ArithNonLinIntExpr* e1e = static_cast<ArithNonLinIntExpr*>(e1.nle());
367 int curN = i;
368 for (; i<curN+e1e->n; i++)
369 ae->a[i] = e1e->a[i-curN];
370 } else {
371 ae->a[i++] = e1;
372 }
373 return LinIntExpr(ae);
374 }
375
376 LinIntExpr
377 min(const IntVarArgs& x) {
378 using namespace MiniModel;
379 ArithNonLinIntExpr* ae =
380 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_MIN,x.size());
381 for (int i=x.size(); i--;)
382 ae->a[i] = x[i];
383 return LinIntExpr(ae);
384 }
385
386 LinIntExpr
387 max(const IntVarArgs& x) {
388 using namespace MiniModel;
389 ArithNonLinIntExpr* ae =
390 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_MAX,x.size());
391 for (int i=x.size(); i--;)
392 ae->a[i] = x[i];
393 return LinIntExpr(ae);
394 }
395
396 LinIntExpr
397 operator *(const LinIntExpr& e0, const LinIntExpr& e1) {
398 using namespace MiniModel;
399 ArithNonLinIntExpr* ae =
400 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_MULT,2);
401 ae->a[0] = e0;
402 ae->a[1] = e1;
403 return LinIntExpr(ae);
404 }
405
406 LinIntExpr
407 sqr(const LinIntExpr& e) {
408 using namespace MiniModel;
409 ArithNonLinIntExpr* ae =
410 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_SQR,1);
411 ae->a[0] = e;
412 return LinIntExpr(ae);
413 }
414
415 LinIntExpr
416 sqrt(const LinIntExpr& e) {
417 using namespace MiniModel;
418 ArithNonLinIntExpr* ae =
419 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_SQRT,1);
420 ae->a[0] = e;
421 return LinIntExpr(ae);
422 }
423
424 LinIntExpr
425 pow(const LinIntExpr& e, int n) {
426 using namespace MiniModel;
427 ArithNonLinIntExpr* ae =
428 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_POW,1,n);
429 ae->a[0] = e;
430 return LinIntExpr(ae);
431 }
432
433 LinIntExpr
434 nroot(const LinIntExpr& e, int n) {
435 using namespace MiniModel;
436 ArithNonLinIntExpr* ae =
437 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_NROOT,1,n);
438 ae->a[0] = e;
439 return LinIntExpr(ae);
440 }
441
442 LinIntExpr
443 operator /(const LinIntExpr& e0, const LinIntExpr& e1) {
444 using namespace MiniModel;
445 ArithNonLinIntExpr* ae =
446 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_DIV,2);
447 ae->a[0] = e0;
448 ae->a[1] = e1;
449 return LinIntExpr(ae);
450 }
451
452 LinIntExpr
453 operator %(const LinIntExpr& e0, const LinIntExpr& e1) {
454 using namespace MiniModel;
455 ArithNonLinIntExpr* ae =
456 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_MOD,2);
457 ae->a[0] = e0;
458 ae->a[1] = e1;
459 return LinIntExpr(ae);
460 }
461
462 LinIntExpr
463 element(const IntVarArgs& x, const LinIntExpr& e) {
464 using namespace MiniModel;
465 ArithNonLinIntExpr* ae =
466 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_ELMNT,x.size()+1);
467 for (int i=x.size(); i--;)
468 ae->a[i] = x[i];
469 ae->a[x.size()] = e;
470 return LinIntExpr(ae);
471 }
472
473 LinIntExpr
474 element(const IntArgs& x, const LinIntExpr& e) {
475 using namespace MiniModel;
476 ArithNonLinIntExpr* ae =
477 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_ELMNT,x.size()+1);
478 for (int i=x.size(); i--;)
479 ae->a[i] = x[i];
480 ae->a[x.size()] = e;
481 return LinIntExpr(ae);
482 }
483
484 LinIntExpr
485 ite(const BoolExpr& b, const LinIntExpr& e0, const LinIntExpr& e1) {
486 using namespace MiniModel;
487 ArithNonLinIntExpr* ae =
488 new ArithNonLinIntExpr(ArithNonLinIntExpr::ANLE_ITE,2,b);
489 ae->a[0] = e0;
490 ae->a[1] = e1;
491 return LinIntExpr(ae);
492 }
493
494}
495
496// STATISTICS: minimodel-any