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