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/astiterator.hh>
13#include <minizinc/chain_compressor.hh>
14#include <minizinc/eval_par.hh>
15#include <minizinc/flatten.hh>
16#include <minizinc/flatten_internal.hh>
17#include <minizinc/hash.hh>
18#include <minizinc/optimize.hh>
19#include <minizinc/optimize_constraints.hh>
20#include <minizinc/prettyprinter.hh>
21
22#include <deque>
23#include <vector>
24
25namespace MiniZinc {
26
27void VarOccurrences::add_idx(VarDeclI* i, int idx_i) { idx.insert(i->e()->id(), idx_i); }
28void VarOccurrences::add_idx(VarDecl* e, int idx_i) {
29 assert(find(e) == -1);
30 idx.insert(e->id(), idx_i);
31}
32int VarOccurrences::find(VarDecl* vd) {
33 IdMap<int>::iterator it = idx.find(vd->id());
34 return it == idx.end() ? -1 : it->second;
35}
36void VarOccurrences::remove(VarDecl* vd) { idx.remove(vd->id()); }
37
38void VarOccurrences::add(VarDecl* v, Item* i) {
39 IdMap<Items>::iterator vi = _m.find(v->id()->decl()->id());
40 if (vi == _m.end()) {
41 Items items;
42 items.insert(i);
43 _m.insert(v->id()->decl()->id(), items);
44 } else {
45 vi->second.insert(i);
46 }
47}
48
49int VarOccurrences::remove(VarDecl* v, Item* i) {
50 IdMap<Items>::iterator vi = _m.find(v->id()->decl()->id());
51 assert(vi != _m.end());
52 vi->second.erase(i);
53 return static_cast<int>(vi->second.size());
54}
55
56void VarOccurrences::removeAllOccurrences(VarDecl* v) {
57 IdMap<Items>::iterator vi = _m.find(v->id()->decl()->id());
58 assert(vi != _m.end());
59 vi->second.clear();
60}
61
62void VarOccurrences::unify(EnvI& env, Model* m, Id* id0_0, Id* id1_0) {
63 Id* id0 = id0_0->decl()->id();
64 Id* id1 = id1_0->decl()->id();
65
66 VarDecl* v0 = id0->decl();
67 VarDecl* v1 = id1->decl();
68
69 if (v0 == v1) return;
70
71 int v0idx = find(v0);
72 assert(v0idx != -1);
73 env.flat_removeItem(v0idx);
74
75 IdMap<Items>::iterator vi0 = _m.find(v0->id());
76 if (vi0 != _m.end()) {
77 IdMap<Items>::iterator vi1 = _m.find(v1->id());
78 if (vi1 == _m.end()) {
79 _m.insert(v1->id(), vi0->second);
80 } else {
81 vi1->second.insert(vi0->second.begin(), vi0->second.end());
82 }
83 _m.remove(v0->id());
84 }
85
86 remove(v0);
87 id0->redirect(id1);
88}
89
90void VarOccurrences::clear(void) {
91 _m.clear();
92 idx.clear();
93}
94
95int VarOccurrences::occurrences(VarDecl* v) {
96 IdMap<Items>::iterator vi = _m.find(v->id()->decl()->id());
97 return (vi == _m.end() ? 0 : static_cast<int>(vi->second.size()));
98}
99
100int VarOccurrences::usages(VarDecl* v) {
101 auto vi = _m.find(v->id()->decl()->id());
102 if (vi == _m.end()) {
103 return 0;
104 }
105 int count = 0;
106 for (Item* i : vi->second) {
107 auto vd = i->dyn_cast<VarDeclI>();
108 if (vd && vd->e() && vd->e() && vd->e()->e() &&
109 (vd->e()->e()->isa<ArrayLit>() || vd->e()->e()->isa<SetLit>())) {
110 count += usages(vd->e());
111 } else {
112 count++;
113 }
114 }
115 return count;
116}
117
118void CollectOccurrencesI::vVarDeclI(VarDeclI* v) {
119 CollectOccurrencesE ce(vo, v);
120 topDown(ce, v->e());
121}
122void CollectOccurrencesI::vConstraintI(ConstraintI* ci) {
123 CollectOccurrencesE ce(vo, ci);
124 topDown(ce, ci->e());
125 for (ExpressionSetIter it = ci->e()->ann().begin(); it != ci->e()->ann().end(); ++it)
126 topDown(ce, *it);
127}
128void CollectOccurrencesI::vSolveI(SolveI* si) {
129 CollectOccurrencesE ce(vo, si);
130 topDown(ce, si->e());
131 for (ExpressionSetIter it = si->ann().begin(); it != si->ann().end(); ++si) topDown(ce, *it);
132}
133
134bool isOutput(VarDecl* vd) {
135 for (ExpressionSetIter it = vd->ann().begin(); it != vd->ann().end(); ++it) {
136 if (*it) {
137 if (*it == constants().ann.output_var) return true;
138 if (Call* c = (*it)->dyn_cast<Call>()) {
139 if (c->id() == constants().ann.output_array) return true;
140 }
141 }
142 }
143 return false;
144}
145
146void unify(EnvI& env, std::vector<VarDecl*>& deletedVarDecls, Id* id0, Id* id1) {
147 if (id0->decl() != id1->decl()) {
148 if (isOutput(id0->decl())) {
149 std::swap(id0, id1);
150 }
151
152 if (id0->decl()->e() != NULL && !Expression::equal(id0->decl()->e(), id1->decl()->id())) {
153 Expression* rhs = id0->decl()->e();
154
155 VarDeclI* vdi1 = (*env.flat())[env.vo.find(id1->decl())]->cast<VarDeclI>();
156 CollectOccurrencesE ce(env.vo, vdi1);
157 topDown(ce, rhs);
158
159 id1->decl()->e(rhs);
160 id0->decl()->e(NULL);
161
162 VarDeclI* vdi0 = (*env.flat())[env.vo.find(id0->decl())]->cast<VarDeclI>();
163 CollectDecls cd(env.vo, deletedVarDecls, vdi0);
164 topDown(cd, rhs);
165 }
166 if (Expression::equal(id1->decl()->e(), id0->decl()->id())) {
167 VarDeclI* vdi1 = (*env.flat())[env.vo.find(id1->decl())]->cast<VarDeclI>();
168 CollectDecls cd(env.vo, deletedVarDecls, vdi1);
169 Expression* rhs = id1->decl()->e();
170 topDown(cd, rhs);
171 id1->decl()->e(NULL);
172 }
173 // Compute intersection of domains
174 if (id0->decl()->ti()->domain() != NULL) {
175 if (id1->decl()->ti()->domain() != NULL) {
176 if (id0->type().isint() || id0->type().isintset()) {
177 IntSetVal* isv0 = eval_intset(env, id0->decl()->ti()->domain());
178 IntSetVal* isv1 = eval_intset(env, id1->decl()->ti()->domain());
179 IntSetRanges isv0r(isv0);
180 IntSetRanges isv1r(isv1);
181 Ranges::Inter<IntVal, IntSetRanges, IntSetRanges> inter(isv0r, isv1r);
182 IntSetVal* nd = IntSetVal::ai(inter);
183 if (nd->size() == 0) {
184 env.fail();
185 } else if (nd->card() != isv1->card()) {
186 id1->decl()->ti()->domain(new SetLit(Location(), nd));
187 if (nd->card() == isv0->card()) {
188 id1->decl()->ti()->setComputedDomain(id0->decl()->ti()->computedDomain());
189 } else {
190 id1->decl()->ti()->setComputedDomain(false);
191 }
192 }
193 } else if (id0->type().isbool()) {
194 if (eval_bool(env, id0->decl()->ti()->domain()) !=
195 eval_bool(env, id1->decl()->ti()->domain())) {
196 env.fail();
197 }
198 } else {
199 // float
200 FloatSetVal* isv0 = eval_floatset(env, id0->decl()->ti()->domain());
201 FloatSetVal* isv1 = eval_floatset(env, id1->decl()->ti()->domain());
202 FloatSetRanges isv0r(isv0);
203 FloatSetRanges isv1r(isv1);
204 Ranges::Inter<FloatVal, FloatSetRanges, FloatSetRanges> inter(isv0r, isv1r);
205 FloatSetVal* nd = FloatSetVal::ai(inter);
206
207 FloatSetRanges nd_r(nd);
208 FloatSetRanges isv1r_2(isv1);
209
210 if (nd->size() == 0) {
211 env.fail();
212 } else if (!Ranges::equal(nd_r, isv1r_2)) {
213 id1->decl()->ti()->domain(new SetLit(Location(), nd));
214 FloatSetRanges nd_r_2(nd);
215 FloatSetRanges isv0r_2(isv0);
216 if (Ranges::equal(nd_r_2, isv0r_2)) {
217 id1->decl()->ti()->setComputedDomain(id0->decl()->ti()->computedDomain());
218 } else {
219 id1->decl()->ti()->setComputedDomain(false);
220 }
221 }
222 }
223
224 } else {
225 id1->decl()->ti()->domain(id0->decl()->ti()->domain());
226 }
227 }
228
229 // If both variables are output variables, unify them in the output model
230 if (isOutput(id0->decl())) {
231 assert(env.output_vo_flat.find(id0->decl()) != -1);
232 VarDecl* id0_output =
233 (*env.output)[env.output_vo_flat.find(id0->decl())]->cast<VarDeclI>()->e();
234 assert(env.output_vo_flat.find(id1->decl()) != -1);
235 VarDecl* id1_output =
236 (*env.output)[env.output_vo_flat.find(id1->decl())]->cast<VarDeclI>()->e();
237 if (id0_output->e() == NULL) {
238 id0_output->e(id1_output->id());
239 }
240 }
241
242 env.vo.unify(env, env.flat(), id0, id1);
243 }
244}
245
246void substituteFixedVars(EnvI& env, Item* ii, std::vector<VarDecl*>& deletedVarDecls);
247void simplifyBoolConstraint(EnvI& env, Item* ii, VarDecl* vd, bool& remove,
248 std::deque<int>& vardeclQueue, std::deque<Item*>& constraintQueue,
249 std::vector<Item*>& toRemove,
250 std::unordered_map<Expression*, int>& nonFixedLiteralCount);
251
252bool simplifyConstraint(EnvI& env, Item* ii, std::vector<VarDecl*>& deletedVarDecls,
253 std::deque<Item*>& constraintQueue, std::deque<int>& vardeclQueue);
254
255void pushVarDecl(EnvI& env, VarDeclI* vdi, int vd_idx, std::deque<int>& q) {
256 if (!vdi->removed() && !vdi->flag()) {
257 vdi->flag(true);
258 q.push_back(vd_idx);
259 }
260}
261void pushVarDecl(EnvI& env, int vd_idx, std::deque<int>& q) {
262 pushVarDecl(env, (*env.flat())[vd_idx]->cast<VarDeclI>(), vd_idx, q);
263}
264
265void pushDependentConstraints(EnvI& env, Id* id, std::deque<Item*>& q) {
266 IdMap<VarOccurrences::Items>::iterator it = env.vo._m.find(id->decl()->id());
267 if (it != env.vo._m.end()) {
268 for (VarOccurrences::Items::iterator item = it->second.begin(); item != it->second.end();
269 ++item) {
270 if (ConstraintI* ci = (*item)->dyn_cast<ConstraintI>()) {
271 if (!ci->removed() && !ci->flag()) {
272 ci->flag(true);
273 q.push_back(ci);
274 }
275 } else if (VarDeclI* vdi = (*item)->dyn_cast<VarDeclI>()) {
276 if (vdi->e()->id()->decl() != vdi->e()) {
277 vdi = (*env.flat())[env.vo.find(vdi->e()->id()->decl())]->cast<VarDeclI>();
278 }
279 if (!vdi->removed() && !vdi->flag() && vdi->e()->e()) {
280 vdi->flag(true);
281 q.push_back(vdi);
282 }
283 }
284 }
285 }
286}
287
288void optimize(Env& env, bool chain_compression) {
289 if (env.envi().failed()) return;
290 try {
291 EnvI& envi = env.envi();
292 Model& m = *envi.flat();
293 std::vector<int> toAssignBoolVars;
294 std::vector<int> toRemoveConstraints;
295 std::vector<VarDecl*> deletedVarDecls;
296
297 // Queue of constraint and variable items that still need to be optimised
298 std::deque<Item*> constraintQueue;
299 // Queue of variable declarations (indexes into the model) that still need to be optimised
300 std::deque<int> vardeclQueue;
301
302 std::vector<int> boolConstraints;
303
304 GCLock lock;
305
306 // Phase 0: clean up
307 // - clear flags for all constraint and variable declaration items
308 // (flags are used to indicate whether an item is already queued or not)
309 for (unsigned int i = 0; i < m.size(); i++) {
310 if (!m[i]->removed()) {
311 if (ConstraintI* ci = m[i]->dyn_cast<ConstraintI>()) {
312 ci->flag(false);
313 } else if (VarDeclI* vdi = m[i]->dyn_cast<VarDeclI>()) {
314 vdi->flag(false);
315 }
316 }
317 }
318
319 // Phase 1: initialise queues
320 // - remove equality constraints between identifiers
321 // - remove toplevel forall constraints
322 // - collect exists, clauses and reified foralls in boolConstraints
323 // - remove "constraint x" where x is a bool var
324 // - unify variables that are assigned to an identifier
325 // - push bool vars that are fixed and have a RHS (to propagate the RHS constraint)
326 // - push int vars that are fixed (either have a RHS or a singleton domain)
327 for (unsigned int i = 0; i < m.size(); i++) {
328 if (m[i]->removed()) continue;
329 if (ConstraintI* ci = m[i]->dyn_cast<ConstraintI>()) {
330 ci->flag(false);
331 if (!ci->removed()) {
332 if (Call* c = ci->e()->dyn_cast<Call>()) {
333 if ((c->id() == constants().ids.int_.eq || c->id() == constants().ids.bool_eq ||
334 c->id() == constants().ids.float_.eq || c->id() == constants().ids.set_eq) &&
335 c->arg(0)->isa<Id>() && c->arg(1)->isa<Id>() &&
336 (c->arg(0)->cast<Id>()->decl()->e() == NULL ||
337 c->arg(1)->cast<Id>()->decl()->e() == NULL)) {
338 // Equality constraint between two identifiers: unify
339
340 unify(envi, deletedVarDecls, c->arg(0)->cast<Id>(), c->arg(1)->cast<Id>());
341 {
342 VarDecl* vd = c->arg(0)->cast<Id>()->decl();
343 int v0idx = envi.vo.find(vd);
344 pushVarDecl(envi, m[v0idx]->cast<VarDeclI>(), v0idx, vardeclQueue);
345 }
346
347 pushDependentConstraints(envi, c->arg(0)->cast<Id>(), constraintQueue);
348 CollectDecls cd(envi.vo, deletedVarDecls, ci);
349 topDown(cd, c);
350 ci->e(constants().lit_true);
351 envi.flat_removeItem(i);
352 } else if (c->id() == constants().ids.int_.lin_eq &&
353 Expression::equal(c->arg(2), IntLit::a(0))) {
354 ArrayLit* al_c = follow_id(c->arg(0))->cast<ArrayLit>();
355 if (al_c->size() == 2 &&
356 (*al_c)[0]->cast<IntLit>()->v() == -(*al_c)[1]->cast<IntLit>()->v()) {
357 ArrayLit* al_x = follow_id(c->arg(1))->cast<ArrayLit>();
358 if ((*al_x)[0]->isa<Id>() && (*al_x)[1]->isa<Id>() &&
359 ((*al_x)[0]->cast<Id>()->decl()->e() == NULL ||
360 (*al_x)[1]->cast<Id>()->decl()->e() == NULL)) {
361 // Equality constraint between two identifiers: unify
362
363 unify(envi, deletedVarDecls, (*al_x)[0]->cast<Id>(), (*al_x)[1]->cast<Id>());
364 {
365 VarDecl* vd = (*al_x)[0]->cast<Id>()->decl();
366 int v0idx = envi.vo.find(vd);
367 pushVarDecl(envi, m[v0idx]->cast<VarDeclI>(), v0idx, vardeclQueue);
368 }
369
370 pushDependentConstraints(envi, (*al_x)[0]->cast<Id>(), constraintQueue);
371 CollectDecls cd(envi.vo, deletedVarDecls, ci);
372 topDown(cd, c);
373 ci->e(constants().lit_true);
374 envi.flat_removeItem(i);
375 }
376 }
377 } else if (c->id() == constants().ids.forall) {
378 // Remove forall constraints, assign variables inside the forall to true
379
380 ArrayLit* al = follow_id(c->arg(0))->cast<ArrayLit>();
381 for (unsigned int j = al->size(); j--;) {
382 if (Id* id = (*al)[j]->dyn_cast<Id>()) {
383 if (id->decl()->ti()->domain() == NULL) {
384 toAssignBoolVars.push_back(envi.vo.idx.find(id->decl()->id())->second);
385 } else if (id->decl()->ti()->domain() == constants().lit_false) {
386 env.envi().fail();
387 id->decl()->e(constants().lit_true);
388 }
389 } // todo: check else case (fixed bool inside a forall at this stage)
390 }
391 toRemoveConstraints.push_back(i);
392 } else if (c->id() == constants().ids.exists || c->id() == constants().ids.clause) {
393 // Add disjunctive constraints to the boolConstraints list
394
395 boolConstraints.push_back(i);
396 }
397 } else if (Id* id = ci->e()->dyn_cast<Id>()) {
398 if (id->decl()->ti()->domain() == constants().lit_false) {
399 env.envi().fail();
400 ci->e(constants().lit_false);
401 } else {
402 if (id->decl()->ti()->domain() == NULL) {
403 toAssignBoolVars.push_back(envi.vo.idx.find(id->decl()->id())->second);
404 }
405 toRemoveConstraints.push_back(i);
406 }
407 }
408 }
409 } else if (VarDeclI* vdi = m[i]->dyn_cast<VarDeclI>()) {
410 vdi->flag(false);
411 if (vdi->e()->e() && vdi->e()->e()->isa<Id>() && vdi->e()->type().dim() == 0) {
412 // unify variable with the identifier it's assigned to
413 Id* id1 = vdi->e()->e()->cast<Id>();
414 vdi->e()->e(NULL);
415 unify(envi, deletedVarDecls, vdi->e()->id(), id1);
416 pushDependentConstraints(envi, id1, constraintQueue);
417 }
418 if (vdi->e()->type().isbool() && vdi->e()->type().isvar() && vdi->e()->type().dim() == 0 &&
419 (vdi->e()->ti()->domain() == constants().lit_true ||
420 vdi->e()->ti()->domain() == constants().lit_false)) {
421 // push RHS onto constraint queue since this bool var is fixed
422 pushVarDecl(envi, vdi, i, vardeclQueue);
423 pushDependentConstraints(envi, vdi->e()->id(), constraintQueue);
424 }
425 if (Call* c = Expression::dyn_cast<Call>(vdi->e()->e())) {
426 if (c->id() == constants().ids.forall || c->id() == constants().ids.exists ||
427 c->id() == constants().ids.clause) {
428 // push reified foralls, exists, clauses
429 boolConstraints.push_back(i);
430 }
431 }
432 if (vdi->e()->type().isint()) {
433 if ((vdi->e()->e() && vdi->e()->e()->isa<IntLit>()) ||
434 (vdi->e()->ti()->domain() && vdi->e()->ti()->domain()->isa<SetLit>() &&
435 vdi->e()->ti()->domain()->cast<SetLit>()->isv()->size() == 1 &&
436 vdi->e()->ti()->domain()->cast<SetLit>()->isv()->min() ==
437 vdi->e()->ti()->domain()->cast<SetLit>()->isv()->max())) {
438 // Variable is assigned an integer, or has a singleton domain
439 pushVarDecl(envi, vdi, i, vardeclQueue);
440 pushDependentConstraints(envi, vdi->e()->id(), constraintQueue);
441 }
442 }
443 }
444 }
445
446 // Phase 2: handle boolean constraints
447 // - check if any boolean constraint is subsumed (e.g. a fixed false in a forall, or a fixed
448 // true in a disjunction)
449 // - check if any boolean constraint has a single non-fixed literal left, then fix that literal
450 for (unsigned int i = static_cast<unsigned int>(boolConstraints.size()); i--;) {
451 Item* bi = m[boolConstraints[i]];
452 if (bi->removed()) continue;
453 Call* c;
454
455 if (bi->isa<ConstraintI>()) {
456 c = bi->cast<ConstraintI>()->e()->dyn_cast<Call>();
457 } else {
458 c = bi->cast<VarDeclI>()->e()->e()->dyn_cast<Call>();
459 }
460 if (c == NULL) continue;
461 bool isConjunction = (c->id() == constants().ids.forall);
462 bool subsumed = false;
463 Id* finalId = NULL;
464 bool finalIdNeg = false;
465 int idCount = 0;
466 std::vector<VarDecl*> pos;
467 std::vector<VarDecl*> neg;
468 for (unsigned int j = 0; j < c->n_args(); j++) {
469 bool unit = (j == 0 ? isConjunction : !isConjunction);
470 ArrayLit* al = follow_id(c->arg(j))->cast<ArrayLit>();
471 for (unsigned int k = 0; k < al->size(); k++) {
472 if (Id* ident = (*al)[k]->dyn_cast<Id>()) {
473 if (ident->decl()->ti()->domain() ||
474 (ident->decl()->e() && ident->decl()->e()->type().ispar())) {
475 bool identValue = ident->decl()->ti()->domain()
476 ? eval_bool(envi, ident->decl()->ti()->domain())
477 : eval_bool(envi, ident->decl()->e());
478 if (identValue != unit) {
479 subsumed = true;
480 goto subsumed_check_done;
481 }
482 } else {
483 idCount++;
484 finalId = ident;
485 finalIdNeg = (j == 1);
486 if (j == 0)
487 pos.push_back(ident->decl());
488 else
489 neg.push_back(ident->decl());
490 }
491 } else {
492 if ((*al)[k]->cast<BoolLit>()->v() != unit) {
493 subsumed = true;
494 goto subsumed_check_done;
495 }
496 }
497 }
498 }
499 if (pos.size() > 0 && neg.size() > 0) {
500 std::sort(pos.begin(), pos.end());
501 std::sort(neg.begin(), neg.end());
502 unsigned int ix = 0;
503 unsigned int iy = 0;
504 for (;;) {
505 if (pos[ix] == neg[iy]) {
506 subsumed = true;
507 break;
508 }
509 if (pos[ix] < neg[iy]) {
510 ix++;
511 } else {
512 iy++;
513 }
514 if (ix == pos.size() || iy == neg.size()) break;
515 }
516 }
517
518 subsumed_check_done:
519 if (subsumed) {
520 if (isConjunction) {
521 if (bi->isa<ConstraintI>()) {
522 env.envi().fail();
523 } else {
524 if (bi->cast<VarDeclI>()->e()->ti()->domain()) {
525 if (eval_bool(envi, bi->cast<VarDeclI>()->e()->ti()->domain())) {
526 envi.fail();
527 }
528 } else {
529 CollectDecls cd(envi.vo, deletedVarDecls, bi);
530 topDown(cd, bi->cast<VarDeclI>()->e()->e());
531 bi->cast<VarDeclI>()->e()->ti()->domain(constants().lit_false);
532 bi->cast<VarDeclI>()->e()->ti()->setComputedDomain(true);
533 bi->cast<VarDeclI>()->e()->e(constants().lit_false);
534 pushVarDecl(envi, bi->cast<VarDeclI>(), boolConstraints[i], vardeclQueue);
535 pushDependentConstraints(envi, bi->cast<VarDeclI>()->e()->id(), constraintQueue);
536 }
537 }
538 } else {
539 if (bi->isa<ConstraintI>()) {
540 CollectDecls cd(envi.vo, deletedVarDecls, bi);
541 topDown(cd, bi->cast<ConstraintI>()->e());
542 env.envi().flat_removeItem(bi);
543 } else {
544 if (bi->cast<VarDeclI>()->e()->ti()->domain()) {
545 if (!eval_bool(envi, bi->cast<VarDeclI>()->e()->ti()->domain())) {
546 envi.fail();
547 }
548 } else {
549 CollectDecls cd(envi.vo, deletedVarDecls, bi);
550 topDown(cd, bi->cast<VarDeclI>()->e()->e());
551 bi->cast<VarDeclI>()->e()->ti()->domain(constants().lit_true);
552 bi->cast<VarDeclI>()->e()->ti()->setComputedDomain(true);
553 bi->cast<VarDeclI>()->e()->e(constants().lit_true);
554 pushVarDecl(envi, bi->cast<VarDeclI>(), boolConstraints[i], vardeclQueue);
555 pushDependentConstraints(envi, bi->cast<VarDeclI>()->e()->id(), constraintQueue);
556 }
557 }
558 }
559 } else if (idCount == 1 && bi->isa<ConstraintI>()) {
560 assert(finalId->decl()->ti()->domain() == NULL);
561 finalId->decl()->ti()->domain(constants().boollit(!finalIdNeg));
562 if (finalId->decl()->e() == NULL) finalId->decl()->e(constants().boollit(!finalIdNeg));
563 CollectDecls cd(envi.vo, deletedVarDecls, bi);
564 topDown(cd, bi->cast<ConstraintI>()->e());
565 env.envi().flat_removeItem(bi);
566 pushVarDecl(envi, envi.vo.idx.find(finalId->decl()->id())->second, vardeclQueue);
567 pushDependentConstraints(envi, finalId, constraintQueue);
568 } // todo: for var decls, we could unify the variable with the remaining finalId (the RHS)
569 }
570
571 // Fix all bool vars in toAssignBoolVars to true and push their declarations and constraints
572 for (unsigned int i = static_cast<int>(toAssignBoolVars.size()); i--;) {
573 if (m[toAssignBoolVars[i]]->removed()) continue;
574 VarDeclI* vdi = m[toAssignBoolVars[i]]->cast<VarDeclI>();
575 if (vdi->e()->ti()->domain() == NULL) {
576 vdi->e()->ti()->domain(constants().lit_true);
577 pushVarDecl(envi, vdi, toAssignBoolVars[i], vardeclQueue);
578 pushDependentConstraints(envi, vdi->e()->id(), constraintQueue);
579 }
580 }
581
582 // Phase 3: fixpoint of constraint and variable simplification
583
584 std::unordered_map<Expression*, int> nonFixedLiteralCount;
585 while (!vardeclQueue.empty() || !constraintQueue.empty()) {
586 while (!vardeclQueue.empty()) {
587 int var_idx = vardeclQueue.front();
588 vardeclQueue.pop_front();
589 m[var_idx]->cast<VarDeclI>()->flag(false);
590 VarDecl* vd = m[var_idx]->cast<VarDeclI>()->e();
591
592 if (vd->type().isbool() && vd->ti()->domain()) {
593 bool isTrue = vd->ti()->domain() == constants().lit_true;
594 bool remove = false;
595 if (vd->e()) {
596 if (Id* id = vd->e()->dyn_cast<Id>()) {
597 // Variable assigned to id, so fix id
598 if (id->decl()->ti()->domain() == NULL) {
599 id->decl()->ti()->domain(vd->ti()->domain());
600 pushVarDecl(envi, envi.vo.idx.find(id->decl()->id())->second, vardeclQueue);
601 } else if (id->decl()->ti()->domain() != vd->ti()->domain()) {
602 env.envi().fail();
603 }
604 remove = true;
605 } else if (Call* c = vd->e()->dyn_cast<Call>()) {
606 if (isTrue && c->id() == constants().ids.forall) {
607 // Reified forall is now fixed to true, so make all elements of the conjunction true
608 remove = true;
609 ArrayLit* al = follow_id(c->arg(0))->cast<ArrayLit>();
610 for (unsigned int i = 0; i < al->size(); i++) {
611 if (Id* id = (*al)[i]->dyn_cast<Id>()) {
612 if (id->decl()->ti()->domain() == NULL) {
613 id->decl()->ti()->domain(constants().lit_true);
614 pushVarDecl(envi, envi.vo.idx.find(id->decl()->id())->second, vardeclQueue);
615 } else if (id->decl()->ti()->domain() == constants().lit_false) {
616 env.envi().fail();
617 remove = true;
618 }
619 }
620 }
621 } else if (!isTrue &&
622 (c->id() == constants().ids.exists || c->id() == constants().ids.clause)) {
623 // Reified disjunction is now fixed to false, so make all elements of the
624 // disjunction false
625 remove = true;
626 for (unsigned int i = 0; i < c->n_args(); i++) {
627 bool ispos = i == 0;
628 ArrayLit* al = follow_id(c->arg(i))->cast<ArrayLit>();
629 for (unsigned int j = 0; j < al->size(); j++) {
630 if (Id* id = (*al)[j]->dyn_cast<Id>()) {
631 if (id->decl()->ti()->domain() == NULL) {
632 id->decl()->ti()->domain(constants().boollit(!ispos));
633 pushVarDecl(envi, envi.vo.idx.find(id->decl()->id())->second, vardeclQueue);
634 } else if (id->decl()->ti()->domain() == constants().boollit(ispos)) {
635 env.envi().fail();
636 remove = true;
637 }
638 }
639 }
640 }
641 }
642 }
643 } else {
644 // If bool variable doesn't have a RHS, just remove it
645 remove = true;
646 }
647 pushDependentConstraints(envi, vd->id(), constraintQueue);
648 std::vector<Item*> toRemove;
649 IdMap<VarOccurrences::Items>::iterator it = envi.vo._m.find(vd->id()->decl()->id());
650
651 // Handle all boolean constraints that involve this variable
652 if (it != envi.vo._m.end()) {
653 for (VarOccurrences::Items::iterator item = it->second.begin();
654 item != it->second.end(); ++item) {
655 if ((*item)->removed()) continue;
656 if (VarDeclI* vdi = (*item)->dyn_cast<VarDeclI>()) {
657 // The variable occurs in the RHS of another variable, so
658 // if that is an array variable, simplify all constraints that
659 // mention the array variable
660 if (vdi->e()->e() && vdi->e()->e()->isa<ArrayLit>()) {
661 IdMap<VarOccurrences::Items>::iterator ait =
662 envi.vo._m.find(vdi->e()->id()->decl()->id());
663 if (ait != envi.vo._m.end()) {
664 for (VarOccurrences::Items::iterator aitem = ait->second.begin();
665 aitem != ait->second.end(); ++aitem) {
666 simplifyBoolConstraint(envi, *aitem, vd, remove, vardeclQueue,
667 constraintQueue, toRemove, nonFixedLiteralCount);
668 }
669 }
670 continue;
671 }
672 }
673 // Simplify the constraint *item (which depends on this variable)
674 simplifyBoolConstraint(envi, *item, vd, remove, vardeclQueue, constraintQueue,
675 toRemove, nonFixedLiteralCount);
676 }
677 }
678 // Actually remove all items that have become unnecessary in the step above
679 for (unsigned int i = static_cast<unsigned int>(toRemove.size()); i--;) {
680 if (ConstraintI* ci = toRemove[i]->dyn_cast<ConstraintI>()) {
681 CollectDecls cd(envi.vo, deletedVarDecls, ci);
682 topDown(cd, ci->e());
683 envi.flat_removeItem(ci);
684 } else {
685 VarDeclI* vdi = toRemove[i]->cast<VarDeclI>();
686 CollectDecls cd(envi.vo, deletedVarDecls, vdi);
687 topDown(cd, vdi->e()->e());
688 vdi->e()->e(NULL);
689 }
690 }
691 if (remove) {
692 deletedVarDecls.push_back(vd);
693 } else {
694 simplifyConstraint(envi, m[var_idx], deletedVarDecls, constraintQueue, vardeclQueue);
695 }
696 } else if (vd->type().isint() && vd->ti()->domain()) {
697 IntSetVal* isv = eval_intset(envi, vd->ti()->domain());
698 if (isv->size() == 1 && isv->card() == 1) {
699 simplifyConstraint(envi, m[var_idx], deletedVarDecls, constraintQueue, vardeclQueue);
700 }
701 }
702 } // end of processing of variable queue
703
704 // Now handle all non-boolean constraints (i.e. anything except forall, clause, exists)
705 bool handledConstraint = false;
706 while (!handledConstraint && !constraintQueue.empty()) {
707 Item* item = constraintQueue.front();
708 constraintQueue.pop_front();
709 Call* c;
710 ArrayLit* al = NULL;
711 if (ConstraintI* ci = item->dyn_cast<ConstraintI>()) {
712 ci->flag(false);
713 c = Expression::dyn_cast<Call>(ci->e());
714 } else {
715 if (item->removed()) {
716 // This variable was removed because of unification, so we look up the
717 // variable it was unified to
718 item = m[envi.vo.find(item->cast<VarDeclI>()->e()->id()->decl())]->cast<VarDeclI>();
719 }
720 item->cast<VarDeclI>()->flag(false);
721 c = Expression::dyn_cast<Call>(item->cast<VarDeclI>()->e()->e());
722 al = Expression::dyn_cast<ArrayLit>(item->cast<VarDeclI>()->e()->e());
723 }
724 if (!item->removed()) {
725 if (al) {
726 // Substitute all fixed variables by their values in array literals, then
727 // push all constraints that depend on the array
728 substituteFixedVars(envi, item, deletedVarDecls);
729 pushDependentConstraints(envi, item->cast<VarDeclI>()->e()->id(), constraintQueue);
730 } else if (!c ||
731 !(c->id() == constants().ids.forall || c->id() == constants().ids.exists ||
732 c->id() == constants().ids.clause)) {
733 // For any constraint that is not forall, exists or clause,
734 // substitute fixed arguments, then simplify it
735 substituteFixedVars(envi, item, deletedVarDecls);
736 handledConstraint =
737 simplifyConstraint(envi, item, deletedVarDecls, constraintQueue, vardeclQueue);
738 }
739 }
740 }
741 }
742
743 // Clean up constraints that have been removed in the previous phase
744 for (unsigned int i = static_cast<unsigned int>(toRemoveConstraints.size()); i--;) {
745 ConstraintI* ci = m[toRemoveConstraints[i]]->cast<ConstraintI>();
746 CollectDecls cd(envi.vo, deletedVarDecls, ci);
747 topDown(cd, ci->e());
748 envi.flat_removeItem(toRemoveConstraints[i]);
749 }
750
751 // Phase 4: Chain Breaking
752 if (chain_compression) {
753 ImpCompressor imp(envi, m, deletedVarDecls, boolConstraints);
754 LECompressor le(envi, m, deletedVarDecls);
755 for (auto& item : m) {
756 imp.trackItem(item);
757 le.trackItem(item);
758 }
759 imp.compress();
760 le.compress();
761 }
762
763 // Phase 5: handle boolean constraints again (todo: check if we can
764 // refactor this into a separate function)
765 //
766 // Difference to phase 2: constraint argument arrays are actually shortened here if possible
767 for (unsigned int i = static_cast<unsigned int>(boolConstraints.size()); i--;) {
768 Item* bi = m[boolConstraints[i]];
769 if (bi->removed()) continue;
770 Call* c;
771 std::vector<VarDecl*> removedVarDecls;
772
773 if (bi->isa<ConstraintI>()) {
774 c = bi->cast<ConstraintI>()->e()->dyn_cast<Call>();
775 } else {
776 c = Expression::dyn_cast<Call>(bi->cast<VarDeclI>()->e()->e());
777 }
778 if (c == NULL) continue;
779 bool isConjunction = (c->id() == constants().ids.forall);
780 bool subsumed = false;
781 for (unsigned int j = 0; j < c->n_args(); j++) {
782 bool unit = (j == 0 ? isConjunction : !isConjunction);
783 ArrayLit* al = follow_id(c->arg(j))->cast<ArrayLit>();
784 std::vector<Expression*> compactedAl;
785 for (unsigned int k = 0; k < al->size(); k++) {
786 if (Id* ident = (*al)[k]->dyn_cast<Id>()) {
787 if (ident->decl()->ti()->domain()) {
788 if (!(ident->decl()->ti()->domain() == constants().boollit(unit))) {
789 subsumed = true;
790 }
791 removedVarDecls.push_back(ident->decl());
792 } else {
793 compactedAl.push_back(ident);
794 }
795 } else {
796 if ((*al)[k]->cast<BoolLit>()->v() != unit) {
797 subsumed = true;
798 }
799 }
800 }
801 if (compactedAl.size() < al->size()) {
802 c->arg(j, new ArrayLit(al->loc(), compactedAl));
803 c->arg(j)->type(Type::varbool(1));
804 }
805 }
806 if (subsumed) {
807 if (isConjunction) {
808 if (bi->isa<ConstraintI>()) {
809 env.envi().fail();
810 } else {
811 ArrayLit* al = follow_id(c->arg(0))->cast<ArrayLit>();
812 for (unsigned int j = 0; j < al->size(); j++) {
813 removedVarDecls.push_back((*al)[j]->cast<Id>()->decl());
814 }
815 bi->cast<VarDeclI>()->e()->ti()->domain(constants().lit_false);
816 bi->cast<VarDeclI>()->e()->ti()->setComputedDomain(true);
817 bi->cast<VarDeclI>()->e()->e(constants().lit_false);
818 }
819 } else {
820 if (bi->isa<ConstraintI>()) {
821 CollectDecls cd(envi.vo, deletedVarDecls, bi);
822 topDown(cd, bi->cast<ConstraintI>()->e());
823 env.envi().flat_removeItem(bi);
824 } else {
825 CollectDecls cd(envi.vo, deletedVarDecls, bi);
826 topDown(cd, bi->cast<VarDeclI>()->e()->e());
827 bi->cast<VarDeclI>()->e()->ti()->domain(constants().lit_true);
828 bi->cast<VarDeclI>()->e()->ti()->setComputedDomain(true);
829 bi->cast<VarDeclI>()->e()->e(constants().lit_true);
830 }
831 }
832 }
833 for (unsigned int j = 0; j < removedVarDecls.size(); j++) {
834 if (env.envi().vo.remove(removedVarDecls[j], bi) == 0) {
835 if ((removedVarDecls[j]->e() == NULL || removedVarDecls[j]->ti()->domain() == NULL ||
836 removedVarDecls[j]->ti()->computedDomain()) &&
837 !isOutput(removedVarDecls[j])) {
838 deletedVarDecls.push_back(removedVarDecls[j]);
839 }
840 }
841 }
842 if (VarDeclI* vdi = bi->dyn_cast<VarDeclI>()) {
843 if (envi.vo.occurrences(vdi->e()) == 0) {
844 if ((vdi->e()->e() == NULL || vdi->e()->ti()->domain() == NULL ||
845 vdi->e()->ti()->computedDomain()) &&
846 !isOutput(vdi->e())) {
847 deletedVarDecls.push_back(vdi->e());
848 }
849 }
850 }
851 }
852
853 // Phase 6: remove deleted variables if possible
854 while (!deletedVarDecls.empty()) {
855 VarDecl* cur = deletedVarDecls.back();
856 deletedVarDecls.pop_back();
857 if (envi.vo.occurrences(cur) == 0) {
858 IdMap<int>::iterator cur_idx = envi.vo.idx.find(cur->id());
859 if (cur_idx != envi.vo.idx.end() && !m[cur_idx->second]->removed()) {
860 if (isOutput(cur)) {
861 // We have to change the output model if we remove this variable
862 Expression* val = NULL;
863 if (cur->type().isbool() && cur->ti()->domain()) {
864 val = cur->ti()->domain();
865 } else if (cur->type().isint()) {
866 if (cur->e() && cur->e()->isa<IntLit>()) {
867 val = cur->e();
868 } else if (cur->ti()->domain() && cur->ti()->domain()->isa<SetLit>() &&
869 cur->ti()->domain()->cast<SetLit>()->isv()->size() == 1 &&
870 cur->ti()->domain()->cast<SetLit>()->isv()->min() ==
871 cur->ti()->domain()->cast<SetLit>()->isv()->max()) {
872 val = IntLit::a(cur->ti()->domain()->cast<SetLit>()->isv()->min());
873 }
874 }
875 if (val) {
876 // Find corresponding variable in output model and fix it
877 VarDecl* vd_out =
878 (*envi.output)[envi.output_vo_flat.find(cur)]->cast<VarDeclI>()->e();
879 vd_out->e(val);
880 CollectDecls cd(envi.vo, deletedVarDecls, m[cur_idx->second]->cast<VarDeclI>());
881 topDown(cd, cur->e());
882 envi.flat_removeItem(cur_idx->second);
883 }
884 } else {
885 CollectDecls cd(envi.vo, deletedVarDecls, m[cur_idx->second]->cast<VarDeclI>());
886 topDown(cd, cur->e());
887 envi.flat_removeItem(cur_idx->second);
888 }
889 }
890 }
891 }
892 } catch (ModelInconsistent&) {
893 }
894}
895
896class SubstitutionVisitor : public EVisitor {
897protected:
898 std::vector<VarDecl*> removed;
899 Expression* subst(Expression* e) {
900 if (VarDecl* vd = follow_id_to_decl(e)->dyn_cast<VarDecl>()) {
901 if (vd->type().isbool() && vd->ti()->domain()) {
902 removed.push_back(vd);
903 return vd->ti()->domain();
904 }
905 if (vd->type().isint()) {
906 if (vd->e() && vd->e()->isa<IntLit>()) {
907 removed.push_back(vd);
908 return vd->e();
909 }
910 if (vd->ti()->domain() && vd->ti()->domain()->isa<SetLit>() &&
911 vd->ti()->domain()->cast<SetLit>()->isv()->size() == 1 &&
912 vd->ti()->domain()->cast<SetLit>()->isv()->min() ==
913 vd->ti()->domain()->cast<SetLit>()->isv()->max()) {
914 removed.push_back(vd);
915 return IntLit::a(vd->ti()->domain()->cast<SetLit>()->isv()->min());
916 }
917 }
918 }
919 return e;
920 }
921
922public:
923 /// Visit array literal
924 void vArrayLit(ArrayLit& al) {
925 for (unsigned int i = 0; i < al.size(); i++) {
926 al.set(i, subst(al[i]));
927 }
928 }
929 /// Visit call
930 void vCall(Call& c) {
931 for (unsigned int i = 0; i < c.n_args(); i++) {
932 c.arg(i, subst(c.arg(i)));
933 }
934 }
935 /// Determine whether to enter node
936 bool enter(Expression* e) { return !e->isa<Id>(); }
937 void remove(EnvI& env, Item* item, std::vector<VarDecl*>& deletedVarDecls) {
938 for (unsigned int i = 0; i < removed.size(); i++) {
939 removed[i]->ann().remove(constants().ann.is_defined_var);
940 if (env.vo.remove(removed[i], item) == 0) {
941 if ((removed[i]->e() == NULL || removed[i]->ti()->domain() == NULL ||
942 removed[i]->ti()->computedDomain()) &&
943 !isOutput(removed[i])) {
944 deletedVarDecls.push_back(removed[i]);
945 }
946 }
947 }
948 }
949};
950
951void substituteFixedVars(EnvI& env, Item* ii, std::vector<VarDecl*>& deletedVarDecls) {
952 SubstitutionVisitor sv;
953 if (ConstraintI* ci = ii->dyn_cast<ConstraintI>()) {
954 topDown(sv, ci->e());
955 for (ExpressionSetIter it = ci->e()->ann().begin(); it != ci->e()->ann().end(); ++it) {
956 topDown(sv, *it);
957 }
958 } else if (VarDeclI* vdi = ii->dyn_cast<VarDeclI>()) {
959 topDown(sv, vdi->e());
960 for (ExpressionSetIter it = vdi->e()->ann().begin(); it != vdi->e()->ann().end(); ++it) {
961 topDown(sv, *it);
962 }
963 } else {
964 SolveI* si = ii->cast<SolveI>();
965 topDown(sv, si->e());
966 for (ExpressionSetIter it = si->ann().begin(); it != si->ann().end(); ++it) {
967 topDown(sv, *it);
968 }
969 }
970 sv.remove(env, ii, deletedVarDecls);
971}
972
973bool simplifyConstraint(EnvI& env, Item* ii, std::vector<VarDecl*>& deletedVarDecls,
974 std::deque<Item*>& constraintQueue, std::deque<int>& vardeclQueue) {
975 Expression* con_e;
976 bool is_true;
977 bool is_false;
978 if (ConstraintI* ci = ii->dyn_cast<ConstraintI>()) {
979 con_e = ci->e();
980 is_true = true;
981 is_false = false;
982 } else {
983 VarDeclI* vdi = ii->cast<VarDeclI>();
984 con_e = vdi->e()->e();
985 is_true = (vdi->e()->type().isbool() && vdi->e()->ti()->domain() == constants().lit_true);
986 is_false = (vdi->e()->type().isbool() && vdi->e()->ti()->domain() == constants().lit_false);
987 assert(is_true || is_false || !vdi->e()->type().isbool() || vdi->e()->ti()->domain() == NULL);
988 }
989 if (Call* c = Expression::dyn_cast<Call>(con_e)) {
990 if (c->id() == constants().ids.int_.eq || c->id() == constants().ids.bool_eq ||
991 c->id() == constants().ids.float_.eq) {
992 if (is_true && c->arg(0)->isa<Id>() && c->arg(1)->isa<Id>() &&
993 (c->arg(0)->cast<Id>()->decl()->e() == NULL ||
994 c->arg(1)->cast<Id>()->decl()->e() == NULL)) {
995 unify(env, deletedVarDecls, c->arg(0)->cast<Id>(), c->arg(1)->cast<Id>());
996 pushDependentConstraints(env, c->arg(0)->cast<Id>(), constraintQueue);
997 CollectDecls cd(env.vo, deletedVarDecls, ii);
998 topDown(cd, c);
999 env.flat_removeItem(ii);
1000 } else if (c->arg(0)->type().ispar() && c->arg(1)->type().ispar()) {
1001 Expression* e0 = eval_par(env, c->arg(0));
1002 Expression* e1 = eval_par(env, c->arg(1));
1003 bool is_equal = Expression::equal(e0, e1);
1004 if ((is_true && is_equal) || (is_false && !is_equal)) {
1005 // do nothing
1006 } else if ((is_true && !is_equal) || (is_false && is_equal)) {
1007 env.fail();
1008 } else {
1009 VarDeclI* vdi = ii->cast<VarDeclI>();
1010 CollectDecls cd(env.vo, deletedVarDecls, ii);
1011 topDown(cd, c);
1012 vdi->e()->e(constants().boollit(is_equal));
1013 vdi->e()->ti()->domain(constants().boollit(is_equal));
1014 vdi->e()->ti()->setComputedDomain(true);
1015 pushVarDecl(env, vdi, env.vo.find(vdi->e()), vardeclQueue);
1016 pushDependentConstraints(env, vdi->e()->id(), constraintQueue);
1017 }
1018 if (ii->isa<ConstraintI>()) {
1019 CollectDecls cd(env.vo, deletedVarDecls, ii);
1020 topDown(cd, c);
1021 env.flat_removeItem(ii);
1022 }
1023 } else if (is_true && ((c->arg(0)->isa<Id>() && c->arg(1)->type().ispar()) ||
1024 (c->arg(1)->isa<Id>() && c->arg(0)->type().ispar()))) {
1025 Id* ident = c->arg(0)->isa<Id>() ? c->arg(0)->cast<Id>() : c->arg(1)->cast<Id>();
1026 Expression* arg = c->arg(0)->isa<Id>() ? c->arg(1) : c->arg(0);
1027 bool canRemove = false;
1028 TypeInst* ti = ident->decl()->ti();
1029 switch (ident->type().bt()) {
1030 case Type::BT_BOOL:
1031 if (ti->domain() == NULL) {
1032 ti->domain(constants().boollit(eval_bool(env, arg)));
1033 ti->setComputedDomain(false);
1034 canRemove = true;
1035 } else {
1036 if (eval_bool(env, ti->domain()) == eval_bool(env, arg)) {
1037 canRemove = true;
1038 } else {
1039 env.fail();
1040 canRemove = true;
1041 }
1042 }
1043 break;
1044 case Type::BT_INT: {
1045 IntVal d = eval_int(env, arg);
1046 if (ti->domain() == NULL) {
1047 ti->domain(new SetLit(Location().introduce(), IntSetVal::a(d, d)));
1048 ti->setComputedDomain(false);
1049 canRemove = true;
1050 } else {
1051 IntSetVal* isv = eval_intset(env, ti->domain());
1052 if (isv->contains(d)) {
1053 ident->decl()->ti()->domain(new SetLit(Location().introduce(), IntSetVal::a(d, d)));
1054 ident->decl()->ti()->setComputedDomain(false);
1055 canRemove = true;
1056 } else {
1057 env.fail();
1058 canRemove = true;
1059 }
1060 }
1061 } break;
1062 case Type::BT_FLOAT: {
1063 if (ti->domain() == NULL) {
1064 ti->domain(new BinOp(Location().introduce(), arg, BOT_DOTDOT, arg));
1065 ti->setComputedDomain(false);
1066 canRemove = true;
1067 } else {
1068 FloatVal value = eval_float(env, arg);
1069 if (LinearTraits<FloatLit>::domain_contains(eval_floatset(env, ti->domain()),
1070 value)) {
1071 ti->domain(new BinOp(Location().introduce(), arg, BOT_DOTDOT, arg));
1072 ti->setComputedDomain(false);
1073 canRemove = true;
1074 } else {
1075 env.fail();
1076 canRemove = true;
1077 }
1078 }
1079 } break;
1080 default:
1081 break;
1082 }
1083 if (ident->decl()->e() == NULL) {
1084 ident->decl()->e(c->arg(0)->isa<Id>() ? c->arg(1) : c->arg(0));
1085 ti->setComputedDomain(true);
1086 canRemove = true;
1087 }
1088
1089 if (ident->decl()->e()->isa<Call>())
1090 constraintQueue.push_back((*env.flat())[env.vo.find(ident->decl())]);
1091 pushDependentConstraints(env, ident, constraintQueue);
1092 if (canRemove) {
1093 CollectDecls cd(env.vo, deletedVarDecls, ii);
1094 topDown(cd, c);
1095 env.flat_removeItem(ii);
1096 }
1097 }
1098 } else if ((is_true || is_false) && c->id() == constants().ids.int_.le &&
1099 ((c->arg(0)->isa<Id>() && c->arg(1)->type().ispar()) ||
1100 (c->arg(1)->isa<Id>() && c->arg(0)->type().ispar()))) {
1101 // todo: does this every happen? int_le shouldn't be generated any more
1102 Id* ident = c->arg(0)->isa<Id>() ? c->arg(0)->cast<Id>() : c->arg(1)->cast<Id>();
1103 Expression* arg = c->arg(0)->isa<Id>() ? c->arg(1) : c->arg(0);
1104 IntSetVal* domain =
1105 ident->decl()->ti()->domain() ? eval_intset(env, ident->decl()->ti()->domain()) : NULL;
1106 if (domain) {
1107 BinOpType bot =
1108 c->arg(0)->isa<Id>() ? (is_true ? BOT_LQ : BOT_GR) : (is_true ? BOT_GQ : BOT_LE);
1109 IntSetVal* newDomain = LinearTraits<IntLit>::limit_domain(bot, domain, eval_int(env, arg));
1110 ident->decl()->ti()->domain(new SetLit(Location().introduce(), newDomain));
1111 ident->decl()->ti()->setComputedDomain(false);
1112
1113 if (newDomain->min() == newDomain->max()) {
1114 pushDependentConstraints(env, ident, constraintQueue);
1115 }
1116 CollectDecls cd(env.vo, deletedVarDecls, ii);
1117 topDown(cd, c);
1118
1119 if (VarDeclI* vdi = ii->dyn_cast<VarDeclI>()) {
1120 vdi->e()->e(constants().boollit(is_true));
1121 pushDependentConstraints(env, vdi->e()->id(), constraintQueue);
1122 if (env.vo.occurrences(vdi->e()) == 0) {
1123 if (isOutput(vdi->e())) {
1124 VarDecl* vd_out =
1125 (*env.output)[env.output_vo_flat.find(vdi->e())]->cast<VarDeclI>()->e();
1126 vd_out->e(constants().boollit(is_true));
1127 }
1128 env.flat_removeItem(vdi);
1129 }
1130 } else {
1131 env.flat_removeItem(ii);
1132 }
1133 }
1134 } else if (c->id() == constants().ids.bool2int) {
1135 VarDeclI* vdi = ii->dyn_cast<VarDeclI>();
1136 VarDecl* vd;
1137 bool fixed = false;
1138 bool b_val = false;
1139 if (vdi) {
1140 vd = vdi->e();
1141 } else if (Id* ident = c->arg(1)->dyn_cast<Id>()) {
1142 vd = ident->decl();
1143 } else {
1144 vd = NULL;
1145 }
1146 IntSetVal* vd_dom = NULL;
1147 if (vd) {
1148 if (vd->ti()->domain()) {
1149 vd_dom = eval_intset(env, vd->ti()->domain());
1150 if (vd_dom->max() < 0 || vd_dom->min() > 1) {
1151 env.fail();
1152 return true;
1153 }
1154 fixed = vd_dom->min() == vd_dom->max();
1155 b_val = (vd_dom->min() == 1);
1156 }
1157 } else {
1158 fixed = true;
1159 b_val = (eval_int(env, c->arg(1)) == 1);
1160 }
1161 if (fixed) {
1162 if (c->arg(0)->type().ispar()) {
1163 bool b2i_val = eval_bool(env, c->arg(0));
1164 if (b2i_val != b_val) {
1165 env.fail();
1166 } else {
1167 CollectDecls cd(env.vo, deletedVarDecls, ii);
1168 topDown(cd, c);
1169 env.flat_removeItem(ii);
1170 }
1171 } else {
1172 Id* ident = c->arg(0)->cast<Id>();
1173 TypeInst* ti = ident->decl()->ti();
1174 if (ti->domain() == NULL) {
1175 ti->domain(constants().boollit(b_val));
1176 ti->setComputedDomain(false);
1177 } else if (eval_bool(env, ti->domain()) != b_val) {
1178 env.fail();
1179 }
1180 CollectDecls cd(env.vo, deletedVarDecls, ii);
1181 topDown(cd, c);
1182 if (vd) {
1183 vd->e(IntLit::a(b_val));
1184 vd->ti()->setComputedDomain(true);
1185 }
1186 pushDependentConstraints(env, ident, constraintQueue);
1187 if (vdi) {
1188 if (env.vo.occurrences(vd) == 0) {
1189 env.flat_removeItem(vdi);
1190 }
1191 } else {
1192 env.flat_removeItem(ii);
1193 }
1194 }
1195 } else {
1196 IntVal v = -1;
1197 if (BoolLit* bl = c->arg(0)->dyn_cast<BoolLit>()) {
1198 v = bl->v() ? 1 : 0;
1199 } else if (Id* ident = c->arg(0)->dyn_cast<Id>()) {
1200 if (ident->decl()->ti()->domain()) {
1201 v = eval_bool(env, ident->decl()->ti()->domain()) ? 1 : 0;
1202 }
1203 }
1204 if (v != -1) {
1205 if (vd_dom && !vd_dom->contains(v)) {
1206 env.fail();
1207 } else {
1208 CollectDecls cd(env.vo, deletedVarDecls, ii);
1209 topDown(cd, c);
1210 vd->e(IntLit::a(v));
1211 vd->ti()->domain(new SetLit(Location().introduce(), IntSetVal::a(v, v)));
1212 vd->ti()->setComputedDomain(true);
1213 pushVarDecl(env, env.vo.find(vd), vardeclQueue);
1214 pushDependentConstraints(env, vd->id(), constraintQueue);
1215 }
1216 }
1217 }
1218
1219 } else {
1220 // General propagation: call a propagator registered for this constraint type
1221 Expression* rewrite = NULL;
1222 GCLock lock;
1223 switch (OptimizeRegistry::registry().process(env, ii, c, rewrite)) {
1224 case OptimizeRegistry::CS_NONE:
1225 return false;
1226 case OptimizeRegistry::CS_OK:
1227 return true;
1228 case OptimizeRegistry::CS_FAILED:
1229 if (is_true) {
1230 env.fail();
1231 return true;
1232 } else if (is_false) {
1233 if (ii->isa<ConstraintI>()) {
1234 CollectDecls cd(env.vo, deletedVarDecls, ii);
1235 topDown(cd, c);
1236 env.flat_removeItem(ii);
1237 } else {
1238 deletedVarDecls.push_back(ii->cast<VarDeclI>()->e());
1239 }
1240 return true;
1241 } else {
1242 VarDeclI* vdi = ii->cast<VarDeclI>();
1243 vdi->e()->ti()->domain(constants().lit_false);
1244 pushVarDecl(env, vdi, env.vo.find(vdi->e()), vardeclQueue);
1245 return true;
1246 }
1247 case OptimizeRegistry::CS_ENTAILED:
1248 if (is_true) {
1249 if (ii->isa<ConstraintI>()) {
1250 CollectDecls cd(env.vo, deletedVarDecls, ii);
1251 topDown(cd, c);
1252 env.flat_removeItem(ii);
1253 } else {
1254 deletedVarDecls.push_back(ii->cast<VarDeclI>()->e());
1255 }
1256 return true;
1257 } else if (is_false) {
1258 env.fail();
1259 return true;
1260 } else {
1261 VarDeclI* vdi = ii->cast<VarDeclI>();
1262 vdi->e()->ti()->domain(constants().lit_true);
1263 pushVarDecl(env, vdi, env.vo.find(vdi->e()), vardeclQueue);
1264 return true;
1265 }
1266 case OptimizeRegistry::CS_REWRITE: {
1267 std::vector<VarDecl*> tdv;
1268 CollectDecls cd(env.vo, tdv, ii);
1269 topDown(cd, c);
1270
1271 CollectOccurrencesE ce(env.vo, ii);
1272 topDown(ce, rewrite);
1273
1274 for (unsigned int i = 0; i < tdv.size(); i++) {
1275 if (env.vo.occurrences(tdv[i]) == 0) deletedVarDecls.push_back(tdv[i]);
1276 }
1277
1278 assert(rewrite != NULL);
1279 if (ConstraintI* ci = ii->dyn_cast<ConstraintI>()) {
1280 ci->e(rewrite);
1281 constraintQueue.push_back(ii);
1282 } else {
1283 VarDeclI* vdi = ii->cast<VarDeclI>();
1284 vdi->e()->e(rewrite);
1285 if (vdi->e()->e() && vdi->e()->e()->isa<Id>() && vdi->e()->type().dim() == 0) {
1286 Id* id1 = vdi->e()->e()->cast<Id>();
1287 vdi->e()->e(NULL);
1288 unify(env, deletedVarDecls, vdi->e()->id(), id1);
1289 pushDependentConstraints(env, id1, constraintQueue);
1290 }
1291 if (vdi->e()->e() && vdi->e()->e()->type().ispar() && vdi->e()->ti()->domain()) {
1292 if (vdi->e()->e()->type().isint()) {
1293 IntVal iv = eval_int(env, vdi->e()->e());
1294 IntSetVal* dom = eval_intset(env, vdi->e()->ti()->domain());
1295 if (!dom->contains(iv)) env.fail();
1296 } else if (vdi->e()->e()->type().isintset()) {
1297 IntSetVal* isv = eval_intset(env, vdi->e()->e());
1298 IntSetVal* dom = eval_intset(env, vdi->e()->ti()->domain());
1299 IntSetRanges isv_r(isv);
1300 IntSetRanges dom_r(dom);
1301 if (!Ranges::subset(isv_r, dom_r)) env.fail();
1302 } else if (vdi->e()->e()->type().isfloat()) {
1303 FloatVal fv = eval_float(env, vdi->e()->e());
1304 FloatSetVal* dom = eval_floatset(env, vdi->e()->ti()->domain());
1305 if (!dom->contains(fv)) env.fail();
1306 }
1307 }
1308 if (vdi->e()->ti()->type() != Type::varbool() || vdi->e()->ti()->domain() == NULL)
1309 pushVarDecl(env, vdi, env.vo.find(vdi->e()), vardeclQueue);
1310
1311 if (is_true) {
1312 constraintQueue.push_back(ii);
1313 }
1314 }
1315 return true;
1316 }
1317 }
1318 }
1319 }
1320 return false;
1321}
1322
1323int boolState(EnvI& env, Expression* e) {
1324 if (e->type().ispar()) {
1325 return eval_bool(env, e);
1326 } else {
1327 Id* id = e->cast<Id>();
1328 if (id->decl()->ti()->domain() == NULL) return 2;
1329 return id->decl()->ti()->domain() == constants().lit_true;
1330 }
1331}
1332
1333int decrementNonFixedVars(std::unordered_map<Expression*, int>& nonFixedLiteralCount, Call* c) {
1334 std::unordered_map<Expression*, int>::iterator it = nonFixedLiteralCount.find(c);
1335 if (it == nonFixedLiteralCount.end()) {
1336 int nonFixedVars = 0;
1337 for (unsigned int i = 0; i < c->n_args(); i++) {
1338 ArrayLit* al = follow_id(c->arg(i))->cast<ArrayLit>();
1339 nonFixedVars += al->size();
1340 for (unsigned int j = al->size(); j--;) {
1341 if ((*al)[j]->type().ispar()) nonFixedVars--;
1342 }
1343 }
1344 nonFixedVars--; // for the identifier we're currently processing
1345 nonFixedLiteralCount.insert(std::make_pair(c, nonFixedVars));
1346 return nonFixedVars;
1347 } else {
1348 it->second--;
1349 return it->second;
1350 }
1351}
1352
1353void simplifyBoolConstraint(EnvI& env, Item* ii, VarDecl* vd, bool& remove,
1354 std::deque<int>& vardeclQueue, std::deque<Item*>& constraintQueue,
1355 std::vector<Item*>& toRemove,
1356 std::unordered_map<Expression*, int>& nonFixedLiteralCount) {
1357 if (ii->isa<SolveI>()) {
1358 remove = false;
1359 return;
1360 }
1361 bool isTrue = vd->ti()->domain() == constants().lit_true;
1362 Expression* e = NULL;
1363 ConstraintI* ci = ii->dyn_cast<ConstraintI>();
1364 VarDeclI* vdi = ii->dyn_cast<VarDeclI>();
1365 if (ci) {
1366 e = ci->e();
1367 } else if (vdi) {
1368 e = vdi->e()->e();
1369 if (e == NULL) return;
1370 if (Id* id = e->dyn_cast<Id>()) {
1371 assert(id->decl() == vd);
1372 if (vdi->e()->ti()->domain() == NULL) {
1373 vdi->e()->ti()->domain(constants().boollit(isTrue));
1374 vardeclQueue.push_back(env.vo.idx.find(vdi->e()->id())->second);
1375 } else if (id->decl()->ti()->domain() == constants().boollit(!isTrue)) {
1376 env.fail();
1377 remove = false;
1378 }
1379 return;
1380 }
1381 }
1382 if (Id* ident = e->dyn_cast<Id>()) {
1383 assert(ident->decl() == vd);
1384 return;
1385 }
1386 if (e->isa<BoolLit>()) {
1387 if (e == constants().lit_true && ci) {
1388 toRemove.push_back(ci);
1389 }
1390 return;
1391 }
1392 Call* c = e->cast<Call>();
1393 if (c->id() == constants().ids.bool_eq) {
1394 Expression* b0 = c->arg(0);
1395 Expression* b1 = c->arg(1);
1396 int b0s = boolState(env, b0);
1397 int b1s = boolState(env, b1);
1398 if (b0s == 2) {
1399 std::swap(b0, b1);
1400 std::swap(b0s, b1s);
1401 }
1402 assert(b0s != 2);
1403 if (ci || vdi->e()->ti()->domain() == constants().lit_true) {
1404 if (b0s != b1s) {
1405 if (b1s == 2) {
1406 b1->cast<Id>()->decl()->ti()->domain(constants().boollit(isTrue));
1407 vardeclQueue.push_back(env.vo.idx.find(b1->cast<Id>()->decl()->id())->second);
1408 if (ci) toRemove.push_back(ci);
1409 } else {
1410 env.fail();
1411 remove = false;
1412 }
1413 } else {
1414 if (ci) toRemove.push_back(ci);
1415 }
1416 } else if (vdi && vdi->e()->ti()->domain() == constants().lit_false) {
1417 if (b0s != b1s) {
1418 if (b1s == 2) {
1419 b1->cast<Id>()->decl()->ti()->domain(constants().boollit(isTrue));
1420 vardeclQueue.push_back(env.vo.idx.find(b1->cast<Id>()->decl()->id())->second);
1421 }
1422 } else {
1423 env.fail();
1424 remove = false;
1425 }
1426 } else {
1427 remove = false;
1428 }
1429 } else if (c->id() == constants().ids.forall || c->id() == constants().ids.exists ||
1430 c->id() == constants().ids.clause) {
1431 if (isTrue && c->id() == constants().ids.exists) {
1432 if (ci) {
1433 toRemove.push_back(ci);
1434 } else {
1435 if (vdi->e()->ti()->domain() == NULL) {
1436 vdi->e()->ti()->domain(constants().lit_true);
1437 vardeclQueue.push_back(env.vo.idx.find(vdi->e()->id())->second);
1438 } else if (vdi->e()->ti()->domain() != constants().lit_true) {
1439 env.fail();
1440 vdi->e()->e(constants().lit_true);
1441 }
1442 }
1443 } else if (!isTrue && c->id() == constants().ids.forall) {
1444 if (ci) {
1445 env.fail();
1446 toRemove.push_back(ci);
1447 } else {
1448 if (vdi->e()->ti()->domain() == NULL) {
1449 vdi->e()->ti()->domain(constants().lit_false);
1450 vardeclQueue.push_back(env.vo.idx.find(vdi->e()->id())->second);
1451 } else if (vdi->e()->ti()->domain() != constants().lit_false) {
1452 env.fail();
1453 vdi->e()->e(constants().lit_false);
1454 }
1455 }
1456 } else {
1457 int nonfixed = decrementNonFixedVars(nonFixedLiteralCount, c);
1458 bool isConjunction = (c->id() == constants().ids.forall);
1459 assert(nonfixed >= 0);
1460 if (nonfixed <= 1) {
1461 bool subsumed = false;
1462 int nonfixed_i = -1;
1463 int nonfixed_j = -1;
1464 int realNonFixed = 0;
1465 for (unsigned int i = 0; i < c->n_args(); i++) {
1466 bool unit = (i == 0 ? isConjunction : !isConjunction);
1467 ArrayLit* al = follow_id(c->arg(i))->cast<ArrayLit>();
1468 realNonFixed += al->size();
1469 for (unsigned int j = al->size(); j--;) {
1470 if ((*al)[j]->type().ispar() || (*al)[j]->cast<Id>()->decl()->ti()->domain())
1471 realNonFixed--;
1472 if ((*al)[j]->type().ispar() && eval_bool(env, (*al)[j]) != unit) {
1473 subsumed = true;
1474 i = 2; // break out of outer loop
1475 break;
1476 } else if (Id* id = (*al)[j]->dyn_cast<Id>()) {
1477 if (id->decl()->ti()->domain()) {
1478 bool idv = (id->decl()->ti()->domain() == constants().lit_true);
1479 if (unit != idv) {
1480 subsumed = true;
1481 i = 2; // break out of outer loop
1482 break;
1483 }
1484 } else {
1485 nonfixed_i = i;
1486 nonfixed_j = j;
1487 }
1488 }
1489 }
1490 }
1491
1492 if (subsumed) {
1493 if (ci) {
1494 if (isConjunction) {
1495 env.fail();
1496 ci->e(constants().lit_false);
1497 } else {
1498 toRemove.push_back(ci);
1499 }
1500 } else {
1501 if (vdi->e()->ti()->domain() == NULL) {
1502 vdi->e()->ti()->domain(constants().boollit(!isConjunction));
1503 vardeclQueue.push_back(env.vo.idx.find(vdi->e()->id())->second);
1504 } else if (vdi->e()->ti()->domain() != constants().boollit(!isConjunction)) {
1505 env.fail();
1506 vdi->e()->e(constants().boollit(!isConjunction));
1507 }
1508 }
1509 } else if (realNonFixed == 0) {
1510 if (ci) {
1511 if (isConjunction) {
1512 toRemove.push_back(ci);
1513 } else {
1514 env.fail();
1515 ci->e(constants().lit_false);
1516 }
1517 } else {
1518 if (vdi->e()->ti()->domain() == NULL) {
1519 vdi->e()->ti()->domain(constants().boollit(isConjunction));
1520 vardeclQueue.push_back(env.vo.idx.find(vdi->e()->id())->second);
1521 } else if (vdi->e()->ti()->domain() != constants().boollit(isConjunction)) {
1522 env.fail();
1523 vdi->e()->e(constants().boollit(isConjunction));
1524 }
1525 toRemove.push_back(vdi);
1526 }
1527 } else {
1528 // not subsumed, nonfixed==1
1529 assert(nonfixed_i != -1);
1530 ArrayLit* al = follow_id(c->arg(nonfixed_i))->cast<ArrayLit>();
1531 Id* id = (*al)[nonfixed_j]->cast<Id>();
1532 if (ci || vdi->e()->ti()->domain()) {
1533 bool result = nonfixed_i == 0;
1534 if (vdi && vdi->e()->ti()->domain() == constants().lit_false) result = !result;
1535 VarDecl* vd = id->decl();
1536 if (vd->ti()->domain() == NULL) {
1537 vd->ti()->domain(constants().boollit(result));
1538 vardeclQueue.push_back(env.vo.idx.find(vd->id())->second);
1539 } else if (vd->ti()->domain() != constants().boollit(result)) {
1540 env.fail();
1541 vd->e(constants().lit_true);
1542 }
1543 } else {
1544 remove = false;
1545 }
1546 }
1547
1548 } else if (c->id() == constants().ids.clause) {
1549 int posOrNeg = isTrue ? 0 : 1;
1550 ArrayLit* al = follow_id(c->arg(posOrNeg))->cast<ArrayLit>();
1551 ArrayLit* al_other = follow_id(c->arg(1 - posOrNeg))->cast<ArrayLit>();
1552
1553 if (ci && al->size() == 1 && (*al)[0] != vd->id() && al_other->size() == 1) {
1554 // simple implication
1555 assert((*al_other)[0] == vd->id());
1556 if (ci) {
1557 if ((*al)[0]->type().ispar()) {
1558 if (eval_bool(env, (*al)[0]) == isTrue) {
1559 toRemove.push_back(ci);
1560 } else {
1561 env.fail();
1562 remove = false;
1563 }
1564 } else {
1565 Id* id = (*al)[0]->cast<Id>();
1566 if (id->decl()->ti()->domain() == NULL) {
1567 id->decl()->ti()->domain(constants().boollit(isTrue));
1568 vardeclQueue.push_back(env.vo.idx.find(id->decl()->id())->second);
1569 } else {
1570 if (id->decl()->ti()->domain() == constants().boollit(isTrue)) {
1571 toRemove.push_back(ci);
1572 } else {
1573 env.fail();
1574 remove = false;
1575 }
1576 }
1577 }
1578 }
1579 } else {
1580 // proper clause
1581 for (unsigned int i = 0; i < al->size(); i++) {
1582 if ((*al)[i] == vd->id()) {
1583 if (ci) {
1584 toRemove.push_back(ci);
1585 } else {
1586 if (vdi->e()->ti()->domain() == NULL) {
1587 vdi->e()->ti()->domain(constants().lit_true);
1588 vardeclQueue.push_back(env.vo.idx.find(vdi->e()->id())->second);
1589 } else if (vdi->e()->ti()->domain() != constants().lit_true) {
1590 env.fail();
1591 vdi->e()->e(constants().lit_true);
1592 }
1593 }
1594 break;
1595 }
1596 }
1597 }
1598 }
1599 }
1600 } else {
1601 remove = false;
1602 }
1603}
1604
1605} // namespace MiniZinc