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