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 #pragma once
13
14 #include <minizinc/copy.hh>
15 #include <minizinc/eval_par.hh>
16 #include <minizinc/flatten.hh>
17 #include <minizinc/optimize.hh>
18
19 #include <cmath>
20
21 // TODO: Should this be a command line option? It doesn't seem too expensive
22 // #define OUTPUT_CALLTREE
23
24 namespace MiniZinc {
25
26 /// Result of evaluation
27 class EE {
28 public:
29 /// The result value
30 KeepAlive r;
31 /// Boolean expression representing whether result is defined
32 KeepAlive b;
33 /// Constructor
EE(Expression * r0=nullptr,Expression * b0=nullptr)34 explicit EE(Expression* r0 = nullptr, Expression* b0 = nullptr) : r(r0), b(b0) {}
35 };
36
37 /// Boolean evaluation context
38 enum BCtx { C_ROOT, C_POS, C_NEG, C_MIX };
39
40 /// Evaluation context
41 struct Ctx {
42 /// Boolean context
43 BCtx b;
44 /// Integer context
45 BCtx i;
46 /// Boolen negation flag
47 bool neg;
48 /// Default constructor (root context)
CtxMiniZinc::Ctx49 Ctx() : b(C_ROOT), i(C_MIX), neg(false) {}
50 /// Copy constructor
CtxMiniZinc::Ctx51 Ctx(const Ctx& ctx) : b(ctx.b), i(ctx.i), neg(ctx.neg) {}
52 /// Assignment operator
operator =MiniZinc::Ctx53 Ctx& operator=(const Ctx& ctx) {
54 if (this != &ctx) {
55 b = ctx.b;
56 i = ctx.i;
57 neg = ctx.neg;
58 }
59 return *this;
60 }
61 };
62
63 /// Turn \a c into positive context
64 BCtx operator+(const BCtx& c);
65 /// Negate context \a c
66 BCtx operator-(const BCtx& c);
67
68 class EnvI {
69 public:
70 Model* model;
71 Model* originalModel;
72 Model* output;
73 VarOccurrences varOccurrences;
74 VarOccurrences outputVarOccurrences;
75
76 std::ostream& outstream;
77 std::ostream& errstream;
78 std::stringstream logstream;
79 std::stringstream checkerOutput;
80
81 // The current pass number (used for unifying and disabling path construction in final pass)
82 unsigned int currentPassNumber;
83 // Used for disabling path construction in final pass
84 unsigned int finalPassNumber;
85 // Used for disabling path construction past the maxPathDepth of previous passes
86 unsigned int maxPathDepth;
87
88 #ifdef OUTPUT_CALLTREE
89 // Call stack depth
90 int callDepth = 0;
91 #endif
92
93 VarOccurrences outputFlatVarOccurrences;
94 CopyMap cmap;
95 IdMap<KeepAlive> reverseMappers;
96 struct WW {
97 WeakRef r;
98 WeakRef b;
WWMiniZinc::EnvI::WW99 WW(const WeakRef& r0, const WeakRef& b0) : r(r0), b(b0) {}
100 };
101 typedef KeepAliveMap<WW> CSEMap;
102 bool ignorePartial;
103 bool ignoreUnknownIds;
104 std::vector<Expression*> callStack;
105 std::vector<std::pair<KeepAlive, bool> > errorStack;
106 std::vector<int> idStack;
107 unsigned int maxCallStack;
108 std::vector<std::string> warnings;
109 std::vector<int> modifiedVarDecls;
110 std::unordered_set<std::string> deprecationWarnings;
111 int inRedundantConstraint;
112 int inSymmetryBreakingConstraint;
113 int inMaybePartial;
114 struct {
115 int reifConstraints;
116 int impConstraints;
117 int impDel;
118 int linDel;
119 } counters;
120 bool inReverseMapVar;
121 FlatteningOptions fopts;
122 unsigned int pathUse;
123 ASTStringMap<Item*> reverseEnum;
124
125 struct PathVar {
126 KeepAlive decl;
127 unsigned int passNumber;
128 };
129 // Store mapping from path string to (VarDecl, pass_no) tuples
130 typedef std::unordered_map<std::string, PathVar> PathMap;
131 // Mapping from arbitrary Expressions to paths
132 typedef KeepAliveMap<std::string> ReversePathMap;
133 std::vector<KeepAlive> checkVars;
134
135 protected:
136 CSEMap _cseMap;
137 Model* _flat;
138 bool _failed;
139 unsigned int _ids;
140 ASTStringMap<ASTString> _reifyMap;
141 PathMap _pathMap;
142 ReversePathMap _reversePathMap;
143 ASTStringSet _filenameSet;
144 typedef std::unordered_map<VarDeclI*, unsigned int> EnumMap;
145 EnumMap _enumMap;
146 std::vector<VarDeclI*> _enumVarDecls;
147 typedef std::unordered_map<std::string, unsigned int> ArrayEnumMap;
148 ArrayEnumMap _arrayEnumMap;
149 std::vector<std::vector<unsigned int> > _arrayEnumDecls;
150 bool _collectVardecls;
151
152 public:
153 EnvI(Model* model0, std::ostream& outstream0 = std::cout, std::ostream& errstream0 = std::cerr);
154 ~EnvI();
155 long long int genId();
156 /// Set minimum new temporary id to \a i+1
minId(unsigned int i)157 void minId(unsigned int i) { _ids = std::max(_ids, i + 1); }
158 void cseMapInsert(Expression* e, const EE& ee);
159 CSEMap::iterator cseMapFind(Expression* e);
160 void cseMapRemove(Expression* e);
161 CSEMap::iterator cseMapEnd();
162 void dump();
163
164 unsigned int registerEnum(VarDeclI* vdi);
165 VarDeclI* getEnum(unsigned int i) const;
166 unsigned int registerArrayEnum(const std::vector<unsigned int>& arrayEnum);
167 const std::vector<unsigned int>& getArrayEnum(unsigned int i) const;
168 /// Check if \a t1 is a subtype of \a t2 (including enumerated types if \a strictEnum is true)
169 bool isSubtype(const Type& t1, const Type& t2, bool strictEnum) const;
hasReverseMapper(Id * ident)170 bool hasReverseMapper(Id* ident) { return reverseMappers.find(ident) != reverseMappers.end(); }
171
172 void flatAddItem(Item* i);
173 void flatRemoveItem(ConstraintI* i);
174 void flatRemoveItem(VarDeclI* i);
175 void flatRemoveExpr(Expression* e, Item* i);
176
177 void voAddExp(VarDecl* vd);
178 void annotateFromCallStack(Expression* e);
179 void fail(const std::string& msg = std::string());
180 bool failed() const;
181 Model* flat();
182 void swap();
swapOutput()183 void swapOutput() { std::swap(model, output); }
184 ASTString reifyId(const ASTString& id);
185 static ASTString halfReifyId(const ASTString& id);
186 std::ostream& dumpStack(std::ostream& os, bool errStack);
187 bool dumpPath(std::ostream& os, bool force = false);
188 void addWarning(const std::string& msg);
189 void collectVarDecls(bool b);
getPathMap()190 PathMap& getPathMap() { return _pathMap; }
getReversePathMap()191 ReversePathMap& getReversePathMap() { return _reversePathMap; }
getFilenameSet()192 ASTStringSet& getFilenameSet() { return _filenameSet; }
193
194 void copyPathMapsAndState(EnvI& env);
195 /// deprecated, use Solns2Out
196 std::ostream& evalOutput(std::ostream& os, std::ostream& log);
197 void createErrorStack();
198 Call* surroundingCall() const;
199
200 void cleanupExceptOutput();
201 };
202
203 void set_computed_domain(EnvI& envi, VarDecl* vd, Expression* domain, bool is_computed);
204 EE flat_exp(EnvI& env, const Ctx& ctx, Expression* e, VarDecl* r, VarDecl* b);
205 EE flatten_id(EnvI& env, const Ctx& ctx, Expression* e, VarDecl* r, VarDecl* b,
206 bool doNotFollowChains);
207
208 class CmpExpIdx {
209 public:
210 std::vector<KeepAlive>& x;
CmpExpIdx(std::vector<KeepAlive> & x0)211 CmpExpIdx(std::vector<KeepAlive>& x0) : x(x0) {}
operator ()(int i,int j) const212 bool operator()(int i, int j) const {
213 if (Expression::equal(x[i](), x[j]())) {
214 return false;
215 }
216 if (x[i]()->isa<Id>() && x[j]()->isa<Id>() && x[i]()->cast<Id>()->idn() != -1 &&
217 x[j]()->cast<Id>()->idn() != -1) {
218 return x[i]()->cast<Id>()->idn() < x[j]()->cast<Id>()->idn();
219 }
220 return x[i]() < x[j]();
221 }
222 };
223
224 template <class Lit>
225 class LinearTraits {};
226 template <>
227 class LinearTraits<IntLit> {
228 public:
229 typedef IntVal Val;
eval(EnvI & env,Expression * e)230 static Val eval(EnvI& env, Expression* e) { return eval_int(env, e); }
constructLinBuiltin(BinOpType bot,ASTString & callid,int & coeff_sign,Val & d)231 static void constructLinBuiltin(BinOpType bot, ASTString& callid, int& coeff_sign, Val& d) {
232 switch (bot) {
233 case BOT_LE:
234 callid = constants().ids.int_.lin_le;
235 coeff_sign = 1;
236 d += 1;
237 break;
238 case BOT_LQ:
239 callid = constants().ids.int_.lin_le;
240 coeff_sign = 1;
241 break;
242 case BOT_GR:
243 callid = constants().ids.int_.lin_le;
244 coeff_sign = -1;
245 d = -d + 1;
246 break;
247 case BOT_GQ:
248 callid = constants().ids.int_.lin_le;
249 coeff_sign = -1;
250 d = -d;
251 break;
252 case BOT_EQ:
253 callid = constants().ids.int_.lin_eq;
254 coeff_sign = 1;
255 break;
256 case BOT_NQ:
257 callid = constants().ids.int_.lin_ne;
258 coeff_sign = 1;
259 break;
260 default:
261 assert(false);
262 break;
263 }
264 }
265 // NOLINTNEXTLINE(readability-identifier-naming)
id_eq()266 static ASTString id_eq() { return constants().ids.int_.eq; }
267 typedef IntBounds Bounds;
finite(const IntBounds & ib)268 static bool finite(const IntBounds& ib) { return ib.l.isFinite() && ib.u.isFinite(); }
finite(const IntVal & v)269 static bool finite(const IntVal& v) { return v.isFinite(); }
computeBounds(EnvI & env,Expression * e)270 static Bounds computeBounds(EnvI& env, Expression* e) { return compute_int_bounds(env, e); }
271 typedef IntSetVal* Domain;
evalDomain(EnvI & env,Expression * e)272 static Domain evalDomain(EnvI& env, Expression* e) { return eval_intset(env, e); }
newDomain(Val v)273 static Expression* newDomain(Val v) {
274 return new SetLit(Location().introduce(), IntSetVal::a(v, v));
275 }
newDomain(Val v0,Val v1)276 static Expression* newDomain(Val v0, Val v1) {
277 return new SetLit(Location().introduce(), IntSetVal::a(v0, v1));
278 }
newDomain(Domain d)279 static Expression* newDomain(Domain d) { return new SetLit(Location().introduce(), d); }
domainContains(Domain dom,Val v)280 static bool domainContains(Domain dom, Val v) { return dom->contains(v); }
domainEquals(Domain dom,Val v)281 static bool domainEquals(Domain dom, Val v) {
282 return dom->size() == 1 && dom->min(0) == v && dom->max(0) == v;
283 }
domainEquals(Domain dom1,Domain dom2)284 static bool domainEquals(Domain dom1, Domain dom2) {
285 IntSetRanges d1(dom1);
286 IntSetRanges d2(dom2);
287 return Ranges::equal(d1, d2);
288 }
domainTighter(Domain dom,Bounds b)289 static bool domainTighter(Domain dom, Bounds b) {
290 return !b.valid || dom->min() > b.l || dom->max() < b.u;
291 }
domainIntersects(Domain dom,Val v0,Val v1)292 static bool domainIntersects(Domain dom, Val v0, Val v1) {
293 return (v0 > v1) || (dom->size() > 0 && dom->min(0) <= v1 && v0 <= dom->max(dom->size() - 1));
294 }
domainEmpty(Domain dom)295 static bool domainEmpty(Domain dom) { return dom->size() == 0; }
limitDomain(BinOpType bot,Domain dom,Val v)296 static Domain limitDomain(BinOpType bot, Domain dom, Val v) {
297 IntSetRanges dr(dom);
298 IntSetVal* ndomain;
299 switch (bot) {
300 case BOT_LE:
301 v -= 1;
302 // fall through
303 case BOT_LQ: {
304 Ranges::Bounded<IntVal, IntSetRanges> b =
305 Ranges::Bounded<IntVal, IntSetRanges>::maxiter(dr, v);
306 ndomain = IntSetVal::ai(b);
307 } break;
308 case BOT_GR:
309 v += 1;
310 // fall through
311 case BOT_GQ: {
312 Ranges::Bounded<IntVal, IntSetRanges> b =
313 Ranges::Bounded<IntVal, IntSetRanges>::miniter(dr, v);
314 ndomain = IntSetVal::ai(b);
315 } break;
316 case BOT_NQ: {
317 Ranges::Const<IntVal> c(v, v);
318 Ranges::Diff<IntVal, IntSetRanges, Ranges::Const<IntVal> > d(dr, c);
319 ndomain = IntSetVal::ai(d);
320 } break;
321 default:
322 assert(false);
323 return nullptr;
324 }
325 return ndomain;
326 }
intersectDomain(Domain dom,Val v0,Val v1)327 static Domain intersectDomain(Domain dom, Val v0, Val v1) {
328 IntSetRanges dr(dom);
329 Ranges::Const<IntVal> c(v0, v1);
330 Ranges::Inter<IntVal, IntSetRanges, Ranges::Const<IntVal> > inter(dr, c);
331 return IntSetVal::ai(inter);
332 }
floorDiv(Val v0,Val v1)333 static Val floorDiv(Val v0, Val v1) {
334 return static_cast<long long int>(
335 floor(static_cast<double>(v0.toInt()) / static_cast<double>(v1.toInt())));
336 }
ceilDiv(Val v0,Val v1)337 static Val ceilDiv(Val v0, Val v1) {
338 return static_cast<long long int>(
339 ceil(static_cast<double>(v0.toInt()) / static_cast<double>(v1.toInt())));
340 }
newLit(Val v)341 static IntLit* newLit(Val v) { return IntLit::a(v); }
342 };
343 template <>
344 class LinearTraits<FloatLit> {
345 public:
346 typedef FloatVal Val;
eval(EnvI & env,Expression * e)347 static Val eval(EnvI& env, Expression* e) { return eval_float(env, e); }
constructLinBuiltin(BinOpType bot,ASTString & callid,int & coeff_sign,Val & d)348 static void constructLinBuiltin(BinOpType bot, ASTString& callid, int& coeff_sign, Val& d) {
349 switch (bot) {
350 case BOT_LE:
351 callid = constants().ids.float_.lin_lt;
352 coeff_sign = 1;
353 break;
354 case BOT_LQ:
355 callid = constants().ids.float_.lin_le;
356 coeff_sign = 1;
357 break;
358 case BOT_GR:
359 callid = constants().ids.float_.lin_lt;
360 coeff_sign = -1;
361 d = -d;
362 break;
363 case BOT_GQ:
364 callid = constants().ids.float_.lin_le;
365 coeff_sign = -1;
366 d = -d;
367 break;
368 case BOT_EQ:
369 callid = constants().ids.float_.lin_eq;
370 coeff_sign = 1;
371 break;
372 case BOT_NQ:
373 callid = constants().ids.float_.lin_ne;
374 coeff_sign = 1;
375 break;
376 default:
377 assert(false);
378 break;
379 }
380 }
381 // NOLINTNEXTLINE(readability-identifier-naming)
id_eq()382 static ASTString id_eq() { return constants().ids.float_.eq; }
383 typedef FloatBounds Bounds;
finite(const FloatBounds & ib)384 static bool finite(const FloatBounds& ib) { return ib.l.isFinite() && ib.u.isFinite(); }
finite(const FloatVal & v)385 static bool finite(const FloatVal& v) { return v.isFinite(); }
computeBounds(EnvI & env,Expression * e)386 static Bounds computeBounds(EnvI& env, Expression* e) { return compute_float_bounds(env, e); }
387 typedef FloatSetVal* Domain;
evalDomain(EnvI & env,Expression * e)388 static Domain evalDomain(EnvI& env, Expression* e) { return eval_floatset(env, e); }
389
newDomain(Val v)390 static Expression* newDomain(Val v) {
391 return new SetLit(Location().introduce(), FloatSetVal::a(v, v));
392 }
newDomain(Val v0,Val v1)393 static Expression* newDomain(Val v0, Val v1) {
394 return new SetLit(Location().introduce(), FloatSetVal::a(v0, v1));
395 }
newDomain(Domain d)396 static Expression* newDomain(Domain d) { return new SetLit(Location().introduce(), d); }
domainContains(Domain dom,Val v)397 static bool domainContains(Domain dom, Val v) { return dom->contains(v); }
domainEquals(Domain dom,Val v)398 static bool domainEquals(Domain dom, Val v) {
399 return dom->size() == 1 && dom->min(0) == v && dom->max(0) == v;
400 }
401
domainTighter(Domain dom,Bounds b)402 static bool domainTighter(Domain dom, Bounds b) {
403 return !b.valid || dom->min() > b.l || dom->max() < b.u;
404 }
domainIntersects(Domain dom,Val v0,Val v1)405 static bool domainIntersects(Domain dom, Val v0, Val v1) {
406 return (v0 > v1) || (dom->size() > 0 && dom->min(0) <= v1 && v0 <= dom->max(dom->size() - 1));
407 }
domainEmpty(Domain dom)408 static bool domainEmpty(Domain dom) { return dom->size() == 0; }
409
domainEquals(Domain dom1,Domain dom2)410 static bool domainEquals(Domain dom1, Domain dom2) {
411 FloatSetRanges d1(dom1);
412 FloatSetRanges d2(dom2);
413 return Ranges::equal(d1, d2);
414 }
415
intersectDomain(Domain dom,Val v0,Val v1)416 static Domain intersectDomain(Domain dom, Val v0, Val v1) {
417 if (dom != nullptr) {
418 FloatSetRanges dr(dom);
419 Ranges::Const<FloatVal> c(v0, v1);
420 Ranges::Inter<FloatVal, FloatSetRanges, Ranges::Const<FloatVal> > inter(dr, c);
421 return FloatSetVal::ai(inter);
422 }
423 Domain d = FloatSetVal::a(v0, v1);
424 return d;
425 }
limitDomain(BinOpType bot,Domain dom,Val v)426 static Domain limitDomain(BinOpType bot, Domain dom, Val v) {
427 FloatSetRanges dr(dom);
428 FloatSetVal* ndomain;
429 switch (bot) {
430 case BOT_LE:
431 return nullptr;
432 case BOT_LQ: {
433 Ranges::Bounded<FloatVal, FloatSetRanges> b =
434 Ranges::Bounded<FloatVal, FloatSetRanges>::maxiter(dr, v);
435 ndomain = FloatSetVal::ai(b);
436 } break;
437 case BOT_GR:
438 return nullptr;
439 case BOT_GQ: {
440 Ranges::Bounded<FloatVal, FloatSetRanges> b =
441 Ranges::Bounded<FloatVal, FloatSetRanges>::miniter(dr, v);
442 ndomain = FloatSetVal::ai(b);
443 } break;
444 case BOT_NQ: {
445 Ranges::Const<FloatVal> c(v, v);
446 Ranges::Diff<FloatVal, FloatSetRanges, Ranges::Const<FloatVal> > d(dr, c);
447 ndomain = FloatSetVal::ai(d);
448 } break;
449 default:
450 assert(false);
451 return nullptr;
452 }
453 return ndomain;
454 }
floorDiv(Val v0,Val v1)455 static Val floorDiv(Val v0, Val v1) { return v0 / v1; }
ceilDiv(Val v0,Val v1)456 static Val ceilDiv(Val v0, Val v1) { return v0 / v1; }
newLit(Val v)457 static FloatLit* newLit(Val v) { return FloatLit::a(v); }
458 };
459
460 template <class Lit>
simplify_lin(std::vector<typename LinearTraits<Lit>::Val> & c,std::vector<KeepAlive> & x,typename LinearTraits<Lit>::Val & d)461 void simplify_lin(std::vector<typename LinearTraits<Lit>::Val>& c, std::vector<KeepAlive>& x,
462 typename LinearTraits<Lit>::Val& d) {
463 std::vector<int> idx(c.size());
464 for (auto i = static_cast<unsigned int>(idx.size()); i--;) {
465 idx[i] = i;
466 Expression* e = follow_id_to_decl(x[i]());
467 if (auto* vd = e->dynamicCast<VarDecl>()) {
468 if (vd->e() && vd->e()->isa<Lit>()) {
469 x[i] = vd->e();
470 } else {
471 x[i] = e->cast<VarDecl>()->id();
472 }
473 } else {
474 x[i] = e;
475 }
476 }
477 std::sort(idx.begin(), idx.end(), CmpExpIdx(x));
478 unsigned int ci = 0;
479 for (; ci < x.size(); ci++) {
480 if (Lit* il = x[idx[ci]]()->dynamicCast<Lit>()) {
481 d += c[idx[ci]] * il->v();
482 c[idx[ci]] = 0;
483 } else {
484 break;
485 }
486 }
487 for (unsigned int i = ci + 1; i < x.size(); i++) {
488 if (Expression::equal(x[idx[i]](), x[idx[ci]]())) {
489 c[idx[ci]] += c[idx[i]];
490 c[idx[i]] = 0;
491 } else if (Lit* il = x[idx[i]]()->dynamicCast<Lit>()) {
492 d += c[idx[i]] * il->v();
493 c[idx[i]] = 0;
494 } else {
495 ci = i;
496 }
497 }
498 ci = 0;
499 for (unsigned int i = 0; i < c.size(); i++) {
500 if (c[i] != 0) {
501 c[ci] = c[i];
502 x[ci] = x[i];
503 ci++;
504 }
505 }
506 c.resize(ci);
507 x.resize(ci);
508 }
509
510 } // namespace MiniZinc
511