software/minizinc/lib/optimize.cpp at develop · dekker.one/on-restart-benchmarks

this repo has no description
on-restart-benchmarks / software / minizinc / lib / optimize.cpp
at develop 70 kB view raw
   1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
   2
   3/*
   4 *  Main authors:
   5 *     Guido Tack <guido.tack@monash.edu>
   6 */
   7
   8/* This Source Code Form is subject to the terms of the Mozilla Public
   9 * License, v. 2.0. If a copy of the MPL was not distributed with this
  10 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
  11
  12#include <minizinc/astiterator.hh>
  13#include <minizinc/chain_compressor.hh>
  14#include <minizinc/eval_par.hh>
  15#include <minizinc/flatten.hh>
  16#include <minizinc/flatten_internal.hh>
  17#include <minizinc/hash.hh>
  18#include <minizinc/optimize.hh>
  19#include <minizinc/optimize_constraints.hh>
  20#include <minizinc/prettyprinter.hh>
  21
  22#include <deque>
  23#include <vector>
  24
  25namespace MiniZinc {
  26
  27void VarOccurrences::addIndex(VarDeclI* i, int idx_i) { idx.insert(i->e()->id(), idx_i); }
  28void VarOccurrences::addIndex(VarDecl* e, int idx_i) {
  29  assert(find(e) == -1);
  30  idx.insert(e->id(), idx_i);
  31}
  32int VarOccurrences::find(VarDecl* vd) {
  33  auto it = idx.find(vd->id());
  34  return it == idx.end() ? -1 : it->second;
  35}
  36void VarOccurrences::remove(VarDecl* vd) { idx.remove(vd->id()); }
  37
  38void VarOccurrences::add(VarDecl* v, Item* i) {
  39  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
  49int 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
  56void VarOccurrences::removeAllOccurrences(VarDecl* v) {
  57  auto vi = itemMap.find(v->id()->decl()->id());
  58  assert(vi != itemMap.end());
  59  vi->second.clear();
  60}
  61
  62void VarOccurrences::unify(EnvI& env, Model* m, Id* id0_0, Id* id1_0) {
  63  Id* id0 = id0_0->decl()->id();
  64  Id* id1 = id1_0->decl()->id();
  65
  66  VarDecl* v0 = id0->decl();
  67  VarDecl* v1 = id1->decl();
  68
  69  if (v0 == v1) {
  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
  92void VarOccurrences::clear() {
  93  itemMap.clear();
  94  idx.clear();
  95}
  96
  97int 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
 102std::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
 124void CollectOccurrencesI::vVarDeclI(VarDeclI* v) {
 125  CollectOccurrencesE ce(vo, v);
 126  top_down(ce, v->e());
 127}
 128void 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}
 135void 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
 143bool 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
 159void 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
 259void substitute_fixed_vars(EnvI& env, Item* ii, std::vector<VarDecl*>& deletedVarDecls);
 260void 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
 266bool simplify_constraint(EnvI& env, Item* ii, std::vector<VarDecl*>& deletedVarDecls,
 267                         std::deque<Item*>& constraintQueue,
 268                         std::deque<unsigned int>& vardeclQueue);
 269
 270void 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}
 276void 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
 280void 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
 302void 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
 965class SubstitutionVisitor : public EVisitor {
 966protected:
 967  std::vector<VarDecl*> _removed;
 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
 991public:
 992  /// Visit array literal
 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
 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
1005  static bool enter(Expression* e) { return !e->isa<Id>(); }
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
1019void 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
1041bool 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
1429int 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
1440int 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
1460void 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