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

this repo has no description
on-restart-benchmarks / software / minizinc / lib / output.cpp
at develop 50 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/output.hh>
  14#include <minizinc/typecheck.hh>
  15
  16namespace MiniZinc {
  17
  18namespace {
  19
  20// Test if all parameters and the return type are par
  21bool is_completely_par(EnvI& env, FunctionI* fi, const std::vector<Type>& tv) {
  22  if (fi->e() != nullptr) {
  23    // This is not a builtin, so check parameters
  24    for (auto* p : fi->params()) {
  25      if (p->type().isvar()) {
  26        return false;
  27      }
  28    }
  29  }
  30  return fi->rtype(env, tv, false).isPar();
  31}
  32
  33}  // namespace
  34
  35void check_output_par_fn(EnvI& env, Call* rhs) {
  36  std::vector<Type> tv(rhs->argCount());
  37  for (unsigned int i = rhs->argCount(); (i--) != 0U;) {
  38    tv[i] = rhs->arg(i)->type();
  39    tv[i].ti(Type::TI_PAR);
  40  }
  41  FunctionI* decl = env.output->matchFn(env, rhs->id(), tv, false);
  42  if (decl == nullptr) {
  43    FunctionI* origdecl = env.model->matchFn(env, rhs->id(), tv, false);
  44    if (origdecl == nullptr || !is_completely_par(env, origdecl, tv)) {
  45      std::ostringstream ss;
  46      ss << "function " << rhs->id() << " is used in output, par version needed";
  47      throw FlatteningError(env, rhs->loc(), ss.str());
  48    }
  49    if (!origdecl->fromStdLib()) {
  50      decl = copy(env, env.cmap, origdecl)->cast<FunctionI>();
  51      CollectOccurrencesE ce(env.outputVarOccurrences, decl);
  52      top_down(ce, decl->e());
  53      top_down(ce, decl->ti());
  54      for (unsigned int i = decl->params().size(); (i--) != 0U;) {
  55        top_down(ce, decl->params()[i]);
  56      }
  57      (void)env.output->registerFn(env, decl, true);
  58      env.output->addItem(decl);
  59    } else {
  60      decl = origdecl;
  61    }
  62  }
  63  rhs->type(decl->rtype(env, tv, false));
  64  rhs->decl(decl);
  65}
  66
  67bool cannot_use_rhs_for_output(EnvI& env, Expression* e,
  68                               std::unordered_set<FunctionI*>& seen_functions) {
  69  if (e == nullptr) {
  70    return true;
  71  }
  72
  73  class V : public EVisitor {
  74  public:
  75    EnvI& env;
  76    std::unordered_set<FunctionI*>& seenFunctions;
  77    bool success;
  78    V(EnvI& env0, std::unordered_set<FunctionI*>& seenFunctions0)
  79        : env(env0), seenFunctions(seenFunctions0), success(true) {}
  80    /// Visit anonymous variable
  81    void vAnonVar(const AnonVar& /*v*/) { success = false; }
  82    /// Visit array literal
  83    void vArrayLit(const ArrayLit& /*al*/) {}
  84    /// Visit array access
  85    void vArrayAccess(const ArrayAccess& /*aa*/) {}
  86    /// Visit array comprehension
  87    void vComprehension(const Comprehension& /*c*/) {}
  88    /// Visit if-then-else
  89    void vITE(const ITE& /*ite*/) {}
  90    /// Visit binary operator
  91    void vBinOp(const BinOp& /*bo*/) {}
  92    /// Visit unary operator
  93    void vUnOp(const UnOp& /*uo*/) {}
  94    /// Visit call
  95    void vCall(Call& c) {
  96      std::vector<Type> tv(c.argCount());
  97      for (unsigned int i = c.argCount(); (i--) != 0U;) {
  98        tv[i] = c.arg(i)->type();
  99        tv[i].ti(Type::TI_PAR);
 100      }
 101      FunctionI* decl = env.output->matchFn(env, c.id(), tv, false);
 102      Type t;
 103      if (decl == nullptr) {
 104        FunctionI* origdecl = env.model->matchFn(env, c.id(), tv, false);
 105        if (origdecl == nullptr) {
 106          std::ostringstream ss;
 107          ss << "function " << c.id() << " is used in output, par version needed";
 108          throw FlatteningError(env, c.loc(), ss.str());
 109        }
 110        bool seen = (seenFunctions.find(origdecl) != seenFunctions.end());
 111        if (seen) {
 112          success = false;
 113        } else {
 114          seenFunctions.insert(origdecl);
 115          if ((origdecl->e() != nullptr) &&
 116              cannot_use_rhs_for_output(env, origdecl->e(), seenFunctions)) {
 117            success = false;
 118          } else {
 119            if (!origdecl->fromStdLib()) {
 120              decl = copy(env, env.cmap, origdecl)->cast<FunctionI>();
 121              CollectOccurrencesE ce(env.outputVarOccurrences, decl);
 122              top_down(ce, decl->e());
 123              top_down(ce, decl->ti());
 124              for (unsigned int i = decl->params().size(); (i--) != 0U;) {
 125                top_down(ce, decl->params()[i]);
 126              }
 127              (void)env.output->registerFn(env, decl, true);
 128              env.output->addItem(decl);
 129              output_vardecls(env, origdecl, decl->e());
 130              output_vardecls(env, origdecl, decl->ti());
 131            } else {
 132              decl = origdecl;
 133            }
 134            c.decl(decl);
 135          }
 136        }
 137      }
 138      if (success) {
 139        t = decl->rtype(env, tv, false);
 140        if (!t.isPar()) {
 141          success = false;
 142        }
 143      }
 144    }
 145    void vId(const Id& /*id*/) {}
 146    /// Visit let
 147    void vLet(const Let& /*let*/) { success = false; }
 148    /// Visit variable declaration
 149    void vVarDecl(const VarDecl& /*vd*/) {}
 150    /// Visit type inst
 151    void vTypeInst(const TypeInst& /*ti*/) {}
 152    /// Visit TIId
 153    void vTIId(const TIId& /*tiid*/) {}
 154    /// Determine whether to enter node
 155    bool enter(Expression* /*e*/) const { return success; }
 156  } _v(env, seen_functions);
 157  top_down(_v, e);
 158
 159  return !_v.success;
 160}
 161
 162bool cannot_use_rhs_for_output(EnvI& env, Expression* e) {
 163  std::unordered_set<FunctionI*> seen_functions;
 164  return cannot_use_rhs_for_output(env, e, seen_functions);
 165}
 166
 167void remove_is_output(VarDecl* vd) {
 168  if (vd == nullptr) {
 169    return;
 170  }
 171  vd->ann().remove(constants().ann.output_var);
 172  vd->ann().removeCall(constants().ann.output_array);
 173}
 174
 175void copy_output(EnvI& e) {
 176  struct CopyOutput : public EVisitor {
 177    EnvI& env;
 178    CopyOutput(EnvI& env0) : env(env0) {}
 179    static void vId(Id& _id) { _id.decl(_id.decl()->flat()); }
 180    void vCall(Call& c) {
 181      std::vector<Type> tv(c.argCount());
 182      for (unsigned int i = c.argCount(); (i--) != 0U;) {
 183        tv[i] = c.arg(i)->type();
 184        tv[i].ti(Type::TI_PAR);
 185      }
 186      FunctionI* decl = c.decl();
 187      if (!decl->fromStdLib()) {
 188        env.flatAddItem(decl);
 189      }
 190    }
 191  };
 192
 193  if (OutputI* oi = e.model->outputItem()) {
 194    GCLock lock;
 195    auto* noi = copy(e, oi)->cast<OutputI>();
 196    CopyOutput co(e);
 197    top_down(co, noi->e());
 198    e.flatAddItem(noi);
 199  }
 200}
 201
 202void cleanup_output(EnvI& env) {
 203  for (auto& i : *env.output) {
 204    if (auto* vdi = i->dynamicCast<VarDeclI>()) {
 205      vdi->e()->flat(nullptr);
 206    }
 207  }
 208}
 209
 210void make_par(EnvI& env, Expression* e) {
 211  class OutputJSON : public EVisitor {
 212  public:
 213    EnvI& env;
 214    OutputJSON(EnvI& env0) : env(env0) {}
 215    void vCall(Call& c) {
 216      if (c.id() == "outputJSON") {
 217        bool outputObjective = (c.argCount() == 1 && eval_bool(env, c.arg(0)));
 218        c.id(ASTString("array1d"));
 219        Expression* json =
 220            copy(env, env.cmap, create__json_output(env, outputObjective, false, false));
 221        std::vector<Expression*> new_args({json});
 222        new_args[0]->type(Type::parstring(1));
 223        c.args(new_args);
 224      }
 225    }
 226  } _outputJSON(env);
 227  top_down(_outputJSON, e);
 228  class Par : public EVisitor {
 229  public:
 230    /// Visit variable declaration
 231    static void vVarDecl(VarDecl& vd) { vd.ti()->type(vd.type()); }
 232    /// Determine whether to enter node
 233    static bool enter(Expression* e) {
 234      Type t = e->type();
 235      t.ti(Type::TI_PAR);
 236      t.cv(false);
 237      e->type(t);
 238      return true;
 239    }
 240  } _par;
 241  top_down(_par, e);
 242  class Decls : public EVisitor {
 243  public:
 244    EnvI& env;
 245    Decls(EnvI& env0) : env(env0) {}
 246    void vCall(Call& c) {
 247      if (c.id() == "format" || c.id() == "show" || c.id() == "showDzn" || c.id() == "showJSON") {
 248        unsigned int enumId = c.arg(c.argCount() - 1)->type().enumId();
 249        if (enumId != 0U && c.arg(c.argCount() - 1)->type().dim() != 0) {
 250          const std::vector<unsigned int>& enumIds = env.getArrayEnum(enumId);
 251          enumId = enumIds[enumIds.size() - 1];
 252        }
 253        if (enumId > 0) {
 254          GCLock lock;
 255          Expression* obj = c.arg(c.argCount() - 1);
 256          Id* ti_id = env.getEnum(enumId)->e()->id();
 257          std::string enumName = create_enum_to_string_name(ti_id, "_toString_");
 258          bool is_json = c.id() == "showJSON";
 259          const int dimensions = obj->type().dim();
 260          if (is_json && dimensions > 1) {
 261            // Create generators for dimensions selection
 262            std::vector<Expression*> slice_dimensions(dimensions);
 263            std::vector<Generator> generators;
 264            generators.reserve(dimensions - 1);
 265            auto* idx_ti = new TypeInst(Location().introduce(), Type::parint());
 266            for (int i = 0; i < dimensions - 1; ++i) {
 267              auto* idx_i = new VarDecl(Location().introduce(), idx_ti, env.genId());
 268              idx_i->toplevel(false);
 269              Call* index_set_xx = new Call(
 270                  Location().introduce(),
 271                  "index_set_" + std::to_string(i + 1) + "of" + std::to_string(dimensions), {obj});
 272              index_set_xx->type(Type::parsetint());
 273              generators.push_back(Generator({idx_i}, index_set_xx, nullptr));
 274              slice_dimensions[i] =
 275                  new BinOp(Location().introduce(), idx_i->id(), BOT_DOTDOT, idx_i->id());
 276              slice_dimensions[i]->type(Type::parsetint());
 277            }
 278
 279            // Construct innermost slicing operation
 280            Call* index_set_n = new Call(
 281                Location().introduce(),
 282                "index_set_" + std::to_string(dimensions) + "of" + std::to_string(dimensions),
 283                {obj});
 284            index_set_n->type(Type::parsetint());
 285            slice_dimensions[dimensions - 1] = index_set_n;
 286            auto* al_slice_dim = new ArrayLit(Location().introduce(), slice_dimensions);
 287            al_slice_dim->type(Type::parsetint(1));
 288
 289            auto* slice_call =
 290                new Call(Location().introduce(), "slice_1d", {obj, al_slice_dim, index_set_n});
 291            Type tt = obj->type();
 292            tt.dim(1);
 293            slice_call->type(tt);
 294            Call* _toString_ENUM =
 295                new Call(Location().introduce(), enumName,
 296                         {slice_call, constants().boollit(false), constants().boollit(true)});
 297            _toString_ENUM->type(Type::parstring());
 298
 299            // Build multi-level JSON Array string
 300            auto* comma = new StringLit(Location().introduce(), ", ");
 301            comma->type(Type::parstring());
 302            auto join = [&](Expression* expr, Generator gen) -> Expression* {
 303              Generators generators;
 304              generators.g.push_back(gen);
 305              auto* comp = new Comprehension(Location().introduce(), expr, generators, false);
 306              comp->type(Type::parstring(1));
 307              Call* cc = new Call(Location().introduce(), "join", {comma, comp});
 308              cc->type(Type::parstring());
 309              return cc;
 310            };
 311            auto* sl_open = new StringLit(Location().introduce(), "[");
 312            sl_open->type(Type::parstring());
 313            auto* sl_close = new StringLit(Location().introduce(), "]");
 314            sl_close->type(Type::parstring());
 315
 316            auto* al_concat = new ArrayLit(
 317                Location().introduce(),
 318                std::vector<Expression*>(
 319                    {sl_open, join(_toString_ENUM, generators[dimensions - 2]), sl_close}));
 320            al_concat->type(Type::parstring(1));
 321            for (int i = dimensions - 3; i >= 0; --i) {
 322              Call* concat = new Call(Location().introduce(), "concat", {al_concat});
 323              concat->type(Type::parstring());
 324              al_concat = new ArrayLit(
 325                  Location().introduce(),
 326                  std::vector<Expression*>({sl_open, join(concat, generators[i]), sl_close}));
 327              al_concat->type(Type::parstring(1));
 328            }
 329            std::vector<Expression*> args = {al_concat};
 330            c.args(args);
 331            c.id(ASTString("concat"));
 332          } else {
 333            std::vector<Expression*> args = {obj, constants().boollit(c.id() == "showDzn"),
 334                                             constants().boollit(is_json)};
 335            c.args(args);
 336            c.id(ASTString(enumName));
 337          }
 338        }
 339        if (c.id() == "showDzn" || (c.id() == "showJSON" && enumId > 0)) {
 340          c.id(constants().ids.show);
 341        }
 342      }
 343      c.decl(env.model->matchFn(env, &c, false));
 344    }
 345    void vBinOp(BinOp& bo) {
 346      std::vector<Expression*> args = {bo.lhs(), bo.rhs()};
 347      bo.decl(env.model->matchFn(env, bo.opToString(), args, false));
 348    }
 349    void vUnop(UnOp& uo) {
 350      std::vector<Expression*> args = {uo.e()};
 351      uo.decl(env.model->matchFn(env, uo.opToString(), args, false));
 352    }
 353  } _decls(env);
 354  top_down(_decls, e);
 355}
 356
 357void check_rename_var(EnvI& e, VarDecl* vd) {
 358  if (vd->id()->idn() != vd->flat()->id()->idn()) {
 359    auto* vd_rename_ti = copy(e, e.cmap, vd->ti())->cast<TypeInst>();
 360    auto* vd_rename =
 361        new VarDecl(Location().introduce(), vd_rename_ti, vd->flat()->id()->idn(), nullptr);
 362    vd_rename->flat(vd->flat());
 363    make_par(e, vd_rename);
 364    vd->e(vd_rename->id());
 365    e.output->addItem(new VarDeclI(Location().introduce(), vd_rename));
 366  }
 367}
 368
 369class ClearAnnotations {
 370public:
 371  /// Push all elements of \a v onto \a stack
 372  template <class E>
 373  static void pushVec(std::vector<Expression*>& stack, ASTExprVec<E> v) {
 374    for (unsigned int i = 0; i < v.size(); i++) {
 375      stack.push_back(v[i]);
 376    }
 377  }
 378
 379  static void run(Expression* root) {
 380    std::vector<Expression*> stack;
 381    stack.push_back(root);
 382    while (!stack.empty()) {
 383      Expression* e = stack.back();
 384      stack.pop_back();
 385      if (e == nullptr) {
 386        continue;
 387      }
 388      e->ann().clear();
 389      switch (e->eid()) {
 390        case Expression::E_INTLIT:
 391        case Expression::E_FLOATLIT:
 392        case Expression::E_BOOLLIT:
 393        case Expression::E_STRINGLIT:
 394        case Expression::E_ID:
 395        case Expression::E_ANON:
 396        case Expression::E_TIID:
 397          break;
 398        case Expression::E_SETLIT:
 399          pushVec(stack, e->template cast<SetLit>()->v());
 400          break;
 401        case Expression::E_ARRAYLIT:
 402          for (unsigned int i = 0; i < e->cast<ArrayLit>()->size(); i++) {
 403            stack.push_back((*e->cast<ArrayLit>())[i]);
 404          }
 405          break;
 406        case Expression::E_ARRAYACCESS:
 407          pushVec(stack, e->template cast<ArrayAccess>()->idx());
 408          stack.push_back(e->template cast<ArrayAccess>()->v());
 409          break;
 410        case Expression::E_COMP: {
 411          auto* comp = e->template cast<Comprehension>();
 412          for (unsigned int i = comp->numberOfGenerators(); (i--) != 0U;) {
 413            stack.push_back(comp->where(i));
 414            stack.push_back(comp->in(i));
 415            for (unsigned int j = comp->numberOfDecls(i); (j--) != 0U;) {
 416              stack.push_back(comp->decl(i, j));
 417            }
 418          }
 419          stack.push_back(comp->e());
 420        } break;
 421        case Expression::E_ITE: {
 422          ITE* ite = e->template cast<ITE>();
 423          stack.push_back(ite->elseExpr());
 424          for (int i = 0; i < ite->size(); i++) {
 425            stack.push_back(ite->ifExpr(i));
 426            stack.push_back(ite->thenExpr(i));
 427          }
 428        } break;
 429        case Expression::E_BINOP:
 430          stack.push_back(e->template cast<BinOp>()->rhs());
 431          stack.push_back(e->template cast<BinOp>()->lhs());
 432          break;
 433        case Expression::E_UNOP:
 434          stack.push_back(e->template cast<UnOp>()->e());
 435          break;
 436        case Expression::E_CALL:
 437          for (unsigned int i = 0; i < e->template cast<Call>()->argCount(); i++) {
 438            stack.push_back(e->template cast<Call>()->arg(i));
 439          }
 440          break;
 441        case Expression::E_VARDECL:
 442          stack.push_back(e->template cast<VarDecl>()->e());
 443          stack.push_back(e->template cast<VarDecl>()->ti());
 444          break;
 445        case Expression::E_LET:
 446          stack.push_back(e->template cast<Let>()->in());
 447          pushVec(stack, e->template cast<Let>()->let());
 448          break;
 449        case Expression::E_TI:
 450          stack.push_back(e->template cast<TypeInst>()->domain());
 451          pushVec(stack, e->template cast<TypeInst>()->ranges());
 452          break;
 453      }
 454    }
 455  }
 456};
 457
 458void output_vardecls(EnvI& env, Item* ci, Expression* e) {
 459  class O : public EVisitor {
 460  public:
 461    EnvI& env;
 462    Item* ci;
 463    O(EnvI& env0, Item* ci0) : env(env0), ci(ci0) {}
 464    void vId(Id& id) {
 465      if (&id == constants().absent) {
 466        return;
 467      }
 468      if (!id.decl()->toplevel()) {
 469        return;
 470      }
 471      VarDecl* vd = id.decl();
 472      VarDecl* reallyFlat = vd->flat();
 473      while (reallyFlat != nullptr && reallyFlat != reallyFlat->flat()) {
 474        reallyFlat = reallyFlat->flat();
 475      }
 476      auto idx = reallyFlat != nullptr ? env.outputFlatVarOccurrences.idx.find(reallyFlat->id())
 477                                       : env.outputFlatVarOccurrences.idx.end();
 478      auto idx2 = env.outputVarOccurrences.idx.find(vd->id());
 479      if (idx == env.outputFlatVarOccurrences.idx.end() &&
 480          idx2 == env.outputVarOccurrences.idx.end()) {
 481        auto* nvi = new VarDeclI(Location().introduce(), copy(env, env.cmap, vd)->cast<VarDecl>());
 482        Type t = nvi->e()->ti()->type();
 483        if (t.ti() != Type::TI_PAR) {
 484          t.ti(Type::TI_PAR);
 485        }
 486        make_par(env, nvi->e());
 487        nvi->e()->ti()->domain(nullptr);
 488        nvi->e()->flat(vd->flat());
 489        ClearAnnotations::run(nvi->e());
 490        nvi->e()->introduced(false);
 491        if (reallyFlat != nullptr) {
 492          env.outputFlatVarOccurrences.addIndex(reallyFlat, static_cast<int>(env.output->size()));
 493        }
 494        env.outputVarOccurrences.addIndex(nvi, static_cast<int>(env.output->size()));
 495        env.outputVarOccurrences.add(nvi->e(), ci);
 496        env.output->addItem(nvi);
 497
 498        IdMap<KeepAlive>::iterator it;
 499        if ((it = env.reverseMappers.find(nvi->e()->id())) != env.reverseMappers.end()) {
 500          Call* rhs = copy(env, env.cmap, it->second())->cast<Call>();
 501          check_output_par_fn(env, rhs);
 502          output_vardecls(env, nvi, it->second());
 503          nvi->e()->e(rhs);
 504        } else if ((reallyFlat != nullptr) && cannot_use_rhs_for_output(env, reallyFlat->e())) {
 505          assert(nvi->e()->flat());
 506          nvi->e()->e(nullptr);
 507          if (nvi->e()->type().dim() == 0) {
 508            reallyFlat->addAnnotation(constants().ann.output_var);
 509          } else {
 510            std::vector<Expression*> args(reallyFlat->e()->type().dim());
 511            for (unsigned int i = 0; i < args.size(); i++) {
 512              if (nvi->e()->ti()->ranges()[i]->domain() == nullptr) {
 513                args[i] = new SetLit(Location().introduce(),
 514                                     eval_intset(env, reallyFlat->ti()->ranges()[i]->domain()));
 515              } else {
 516                args[i] = new SetLit(Location().introduce(),
 517                                     eval_intset(env, nvi->e()->ti()->ranges()[i]->domain()));
 518              }
 519            }
 520            auto* al = new ArrayLit(Location().introduce(), args);
 521            args.resize(1);
 522            args[0] = al;
 523            reallyFlat->addAnnotation(
 524                new Call(Location().introduce(), constants().ann.output_array, args));
 525          }
 526          check_rename_var(env, nvi->e());
 527        } else {
 528          output_vardecls(env, nvi, nvi->e()->ti());
 529          output_vardecls(env, nvi, nvi->e()->e());
 530        }
 531        CollectOccurrencesE ce(env.outputVarOccurrences, nvi);
 532        top_down(ce, nvi->e());
 533      }
 534    }
 535  } _o(env, ci);
 536  top_down(_o, e);
 537}
 538
 539void process_deletions(EnvI& e) {
 540  std::vector<VarDecl*> deletedVarDecls;
 541  for (unsigned int i = 0; i < e.output->size(); i++) {
 542    if (auto* vdi = (*e.output)[i]->dynamicCast<VarDeclI>()) {
 543      if (!vdi->removed() && e.outputVarOccurrences.occurrences(vdi->e()) == 0 &&
 544          !vdi->e()->ann().contains(constants().ann.mzn_check_var) &&
 545          !(vdi->e()->id()->idn() == -1 && (vdi->e()->id()->v() == "_mzn_solution_checker" ||
 546                                            vdi->e()->id()->v() == "_mzn_stats_checker"))) {
 547        CollectDecls cd(e.outputVarOccurrences, deletedVarDecls, vdi);
 548        top_down(cd, vdi->e()->e());
 549        remove_is_output(vdi->e()->flat());
 550        if (e.outputVarOccurrences.find(vdi->e()) != -1) {
 551          e.outputVarOccurrences.remove(vdi->e());
 552        }
 553        vdi->remove();
 554      }
 555    }
 556  }
 557  while (!deletedVarDecls.empty()) {
 558    VarDecl* cur = deletedVarDecls.back();
 559    deletedVarDecls.pop_back();
 560    if (e.outputVarOccurrences.occurrences(cur) == 0) {
 561      auto cur_idx = e.outputVarOccurrences.idx.find(cur->id());
 562      if (cur_idx != e.outputVarOccurrences.idx.end()) {
 563        auto* vdi = (*e.output)[cur_idx->second]->cast<VarDeclI>();
 564        if (!vdi->removed()) {
 565          CollectDecls cd(e.outputVarOccurrences, deletedVarDecls, vdi);
 566          top_down(cd, cur->e());
 567          remove_is_output(vdi->e()->flat());
 568          if (e.outputVarOccurrences.find(vdi->e()) != -1) {
 569            e.outputVarOccurrences.remove(vdi->e());
 570          }
 571          vdi->remove();
 572        }
 573      }
 574    }
 575  }
 576
 577  for (auto& it : e.outputVarOccurrences.itemMap) {
 578    std::vector<Item*> toRemove;
 579    for (auto* iit : it.second) {
 580      if (iit->removed()) {
 581        toRemove.push_back(iit);
 582      }
 583    }
 584    for (auto& i : toRemove) {
 585      it.second.erase(i);
 586    }
 587  }
 588}
 589
 590void create_dzn_output_item(EnvI& e, bool outputObjective, bool includeOutputItem, bool hasChecker,
 591                            bool outputForChecker) {
 592  std::vector<Expression*> outputVars;
 593
 594  class DZNOVisitor : public ItemVisitor {
 595  protected:
 596    EnvI& _e;
 597    bool _outputObjective;
 598    bool _includeOutputItem;
 599    bool _outputForChecker;
 600    std::vector<Expression*>& _outputVars;
 601    bool _hadAddToOutput;
 602
 603  public:
 604    DZNOVisitor(EnvI& e, bool outputObjective, bool includeOutputItem, bool outputForChecker,
 605                std::vector<Expression*>& outputVars)
 606        : _e(e),
 607          _outputObjective(outputObjective),
 608          _includeOutputItem(includeOutputItem),
 609          _outputForChecker(outputForChecker),
 610          _outputVars(outputVars),
 611          _hadAddToOutput(false) {}
 612    void vVarDeclI(VarDeclI* vdi) {
 613      VarDecl* vd = vdi->e();
 614      bool process_var = false;
 615      if (_outputForChecker) {
 616        if (vd->ann().contains(constants().ann.mzn_check_var)) {
 617          process_var = true;
 618        }
 619      } else {
 620        if (_outputObjective && vd->id()->idn() == -1 && vd->id()->v() == "_objective") {
 621          process_var = true;
 622        } else {
 623          if (vd->ann().contains(constants().ann.add_to_output)) {
 624            if (!_hadAddToOutput) {
 625              _outputVars.clear();
 626            }
 627            _hadAddToOutput = true;
 628            process_var = true;
 629          } else {
 630            if (!_hadAddToOutput) {
 631              process_var = false;
 632              if (vd->type().isvar()) {
 633                if (vd->e() != nullptr) {
 634                  if (auto* al = vd->e()->dynamicCast<ArrayLit>()) {
 635                    for (unsigned int i = 0; i < al->size(); i++) {
 636                      if ((*al)[i]->isa<AnonVar>()) {
 637                        process_var = true;
 638                        break;
 639                      }
 640                    }
 641                  } else if (vd->ann().contains(constants().ann.rhs_from_assignment)) {
 642                    process_var = true;
 643                  }
 644                } else {
 645                  process_var = true;
 646                }
 647              }
 648            }
 649          }
 650        }
 651      }
 652      if (process_var) {
 653        std::ostringstream s;
 654        s << vd->id()->str() << " = ";
 655        bool needArrayXd = false;
 656        if (vd->type().dim() > 0) {
 657          ArrayLit* al = nullptr;
 658          if ((vd->flat() != nullptr) && (vd->flat()->e() != nullptr)) {
 659            al = eval_array_lit(_e, vd->flat()->e());
 660          } else if (vd->e() != nullptr) {
 661            al = eval_array_lit(_e, vd->e());
 662          }
 663          if (al->size() > 0) {
 664            needArrayXd = true;
 665            s << "array" << vd->type().dim() << "d(";
 666            for (int i = 0; i < vd->type().dim(); i++) {
 667              unsigned int enumId =
 668                  (vd->type().enumId() != 0 ? _e.getArrayEnum(vd->type().enumId())[i] : 0);
 669              if (enumId != 0) {
 670                s << _e.getEnum(enumId)->e()->id()->str() << ", ";
 671              } else if (al != nullptr) {
 672                s << al->min(i) << ".." << al->max(i) << ", ";
 673              } else {
 674                IntSetVal* idxset = eval_intset(_e, vd->ti()->ranges()[i]->domain());
 675                s << *idxset << ", ";
 676              }
 677            }
 678          }
 679        }
 680        auto* sl = new StringLit(Location().introduce(), s.str());
 681        _outputVars.push_back(sl);
 682
 683        std::vector<Expression*> showArgs(1);
 684        showArgs[0] = vd->id();
 685        Call* show = new Call(Location().introduce(), ASTString("showDzn"), showArgs);
 686        show->type(Type::parstring());
 687        FunctionI* fi = _e.model->matchFn(_e, show, false);
 688        assert(fi);
 689        show->decl(fi);
 690        _outputVars.push_back(show);
 691        std::string ends = needArrayXd ? ")" : "";
 692        ends += ";\n";
 693        auto* eol = new StringLit(Location().introduce(), ends);
 694        _outputVars.push_back(eol);
 695      }
 696    }
 697    void vOutputI(OutputI* oi) {
 698      if (_includeOutputItem) {
 699        _outputVars.push_back(new StringLit(Location().introduce(), "_output = "));
 700        Call* concat = new Call(Location().introduce(), ASTString("concat"), {oi->e()});
 701        concat->type(Type::parstring());
 702        FunctionI* fi = _e.model->matchFn(_e, concat, false);
 703        assert(fi);
 704        concat->decl(fi);
 705        Call* show = new Call(Location().introduce(), ASTString("showDzn"), {concat});
 706        show->type(Type::parstring());
 707        fi = _e.model->matchFn(_e, show, false);
 708        assert(fi);
 709        show->decl(fi);
 710        _outputVars.push_back(show);
 711        _outputVars.push_back(new StringLit(Location().introduce(), ";\n"));
 712      }
 713
 714      oi->remove();
 715    }
 716  } dznov(e, outputObjective, includeOutputItem, outputForChecker, outputVars);
 717
 718  iter_items(dznov, e.model);
 719
 720  if (hasChecker && !outputForChecker) {
 721    outputVars.push_back(new StringLit(Location().introduce(), "_checker = "));
 722    auto* checker_output = new Call(Location().introduce(), ASTString("showCheckerOutput"), {});
 723    checker_output->type(Type::parstring());
 724    FunctionI* fi = e.model->matchFn(e, checker_output, false);
 725    assert(fi);
 726    checker_output->decl(fi);
 727    auto* show = new Call(Location().introduce(), ASTString("showDzn"), {checker_output});
 728    show->type(Type::parstring());
 729    fi = e.model->matchFn(e, show, false);
 730    assert(fi);
 731    show->decl(fi);
 732    outputVars.push_back(show);
 733    outputVars.push_back(new StringLit(Location().introduce(), ";\n"));
 734  }
 735
 736  auto* newOutputItem =
 737      new OutputI(Location().introduce(), new ArrayLit(Location().introduce(), outputVars));
 738  e.model->addItem(newOutputItem);
 739}
 740
 741ArrayLit* create__json_output(EnvI& e, bool outputObjective, bool includeOutputItem,
 742                              bool hasChecker) {
 743  std::vector<Expression*> outputVars;
 744  outputVars.push_back(new StringLit(Location().introduce(), "{\n"));
 745
 746  class JSONOVisitor : public ItemVisitor {
 747  protected:
 748    EnvI& _e;
 749    bool _outputObjective;
 750    bool _includeOutputItem;
 751    std::vector<Expression*>& _outputVars;
 752    bool _hadAddToOutput;
 753
 754  public:
 755    bool firstVar;
 756    JSONOVisitor(EnvI& e, bool outputObjective, bool includeOutputItem,
 757                 std::vector<Expression*>& outputVars)
 758        : _e(e),
 759          _outputObjective(outputObjective),
 760          _outputVars(outputVars),
 761          _includeOutputItem(includeOutputItem),
 762          _hadAddToOutput(false),
 763          firstVar(true) {}
 764    void vVarDeclI(VarDeclI* vdi) {
 765      VarDecl* vd = vdi->e();
 766      bool process_var = false;
 767      if (_outputObjective && vd->id()->idn() == -1 && vd->id()->v() == "_objective") {
 768        process_var = true;
 769      } else {
 770        if (vd->ann().contains(constants().ann.add_to_output)) {
 771          if (!_hadAddToOutput) {
 772            _outputVars.clear();
 773            _outputVars.push_back(new StringLit(Location().introduce(), "{\n"));
 774            firstVar = true;
 775          }
 776          _hadAddToOutput = true;
 777          process_var = true;
 778        } else {
 779          if (!_hadAddToOutput) {
 780            process_var =
 781                vd->type().isvar() &&
 782                (vd->e() == nullptr || vd->ann().contains(constants().ann.rhs_from_assignment));
 783          }
 784        }
 785      }
 786      if (process_var) {
 787        std::ostringstream s;
 788        if (firstVar) {
 789          firstVar = false;
 790        } else {
 791          s << ",\n";
 792        }
 793        s << "  \"" << vd->id()->str() << "\""
 794          << " : ";
 795        auto* sl = new StringLit(Location().introduce(), s.str());
 796        _outputVars.push_back(sl);
 797
 798        std::vector<Expression*> showArgs(1);
 799        showArgs[0] = vd->id();
 800        Call* show = new Call(Location().introduce(), "showJSON", showArgs);
 801        show->type(Type::parstring());
 802        FunctionI* fi = _e.model->matchFn(_e, show, false);
 803        assert(fi);
 804        show->decl(fi);
 805        _outputVars.push_back(show);
 806      }
 807    }
 808    void vOutputI(OutputI* oi) {
 809      if (_includeOutputItem) {
 810        std::ostringstream s;
 811        if (firstVar) {
 812          firstVar = false;
 813        } else {
 814          s << ",\n";
 815        }
 816        s << "  \"_output\""
 817          << " : ";
 818        auto* sl = new StringLit(Location().introduce(), s.str());
 819        _outputVars.push_back(sl);
 820        Call* concat = new Call(Location().introduce(), ASTString("concat"), {oi->e()});
 821        concat->type(Type::parstring());
 822        FunctionI* fi = _e.model->matchFn(_e, concat, false);
 823        assert(fi);
 824        concat->decl(fi);
 825        Call* show = new Call(Location().introduce(), ASTString("showJSON"), {concat});
 826        show->type(Type::parstring());
 827        fi = _e.model->matchFn(_e, show, false);
 828        assert(fi);
 829        show->decl(fi);
 830        _outputVars.push_back(show);
 831      }
 832
 833      oi->remove();
 834    }
 835  } jsonov(e, outputObjective, includeOutputItem, outputVars);
 836
 837  iter_items(jsonov, e.model);
 838
 839  if (hasChecker) {
 840    std::ostringstream s;
 841    if (jsonov.firstVar) {
 842      jsonov.firstVar = false;
 843    } else {
 844      s << ",\n";
 845    }
 846    s << "  \"_checker\""
 847      << " : ";
 848    auto* sl = new StringLit(Location().introduce(), s.str());
 849    outputVars.push_back(sl);
 850    Call* checker_output = new Call(Location().introduce(), ASTString("showCheckerOutput"), {});
 851    checker_output->type(Type::parstring());
 852    FunctionI* fi = e.model->matchFn(e, checker_output, false);
 853    assert(fi);
 854    checker_output->decl(fi);
 855    Call* show = new Call(Location().introduce(), ASTString("showJSON"), {checker_output});
 856    show->type(Type::parstring());
 857    fi = e.model->matchFn(e, show, false);
 858    assert(fi);
 859    show->decl(fi);
 860    outputVars.push_back(show);
 861  }
 862
 863  outputVars.push_back(new StringLit(Location().introduce(), "\n}\n"));
 864  return new ArrayLit(Location().introduce(), outputVars);
 865}
 866void create_json_output_item(EnvI& e, bool outputObjective, bool includeOutputItem,
 867                             bool hasChecker) {
 868  auto* newOutputItem =
 869      new OutputI(Location().introduce(),
 870                  create__json_output(e, outputObjective, includeOutputItem, hasChecker));
 871  e.model->addItem(newOutputItem);
 872}
 873
 874void create_output(EnvI& e, FlatteningOptions::OutputMode outputMode, bool outputObjective,
 875                   bool includeOutputItem, bool hasChecker) {
 876  // Create new output model
 877  OutputI* outputItem = nullptr;
 878  GCLock lock;
 879
 880  switch (outputMode) {
 881    case FlatteningOptions::OUTPUT_DZN:
 882      create_dzn_output_item(e, outputObjective, includeOutputItem, hasChecker, false);
 883      break;
 884    case FlatteningOptions::OUTPUT_JSON:
 885      create_json_output_item(e, outputObjective, includeOutputItem, hasChecker);
 886      break;
 887    case FlatteningOptions::OUTPUT_CHECKER:
 888      create_dzn_output_item(e, outputObjective, includeOutputItem, hasChecker, true);
 889      break;
 890    default:
 891      if (e.model->outputItem() == nullptr) {
 892        create_dzn_output_item(e, outputObjective, false, false, false);
 893      }
 894      break;
 895  }
 896
 897  // Copy output item from model into output model
 898  outputItem = copy(e, e.cmap, e.model->outputItem())->cast<OutputI>();
 899  make_par(e, outputItem->e());
 900  e.output->addItem(outputItem);
 901
 902  // Copy all function definitions that are required for output into the output model
 903  class CollectFunctions : public EVisitor {
 904  public:
 905    EnvI& env;
 906    CollectFunctions(EnvI& env0) : env(env0) {}
 907    static bool enter(Expression* e) {
 908      if (e->type().isvar()) {
 909        Type t = e->type();
 910        t.ti(Type::TI_PAR);
 911        e->type(t);
 912      }
 913      return true;
 914    }
 915    void vId(Id& i) {
 916      // Also collect functions from output_only variables we depend on
 917      if ((i.decl() != nullptr) && i.decl()->ann().contains(constants().ann.output_only)) {
 918        top_down(*this, i.decl()->e());
 919      }
 920    }
 921    void vCall(Call& c) {
 922      std::vector<Type> tv(c.argCount());
 923      for (unsigned int i = c.argCount(); (i--) != 0U;) {
 924        tv[i] = c.arg(i)->type();
 925        tv[i].ti(Type::TI_PAR);
 926      }
 927      FunctionI* decl = env.output->matchFn(env, c.id(), tv, false);
 928      FunctionI* origdecl = env.model->matchFn(env, c.id(), tv, false);
 929      bool canReuseDecl = (decl != nullptr);
 930      if (canReuseDecl && (origdecl != nullptr)) {
 931        // Check if this is the exact same overloaded declaration as in the model
 932        for (unsigned int i = 0; i < decl->params().size(); i++) {
 933          if (decl->params()[i]->type() != origdecl->params()[i]->type()) {
 934            // no, the types don't match, so we have to copy the original decl
 935            canReuseDecl = false;
 936            break;
 937          }
 938        }
 939      }
 940      Type t;
 941      if (!canReuseDecl) {
 942        if (origdecl == nullptr || !is_completely_par(env, origdecl, tv)) {
 943          std::ostringstream ss;
 944          ss << "function " << c.id() << " is used in output, par version needed";
 945          throw FlatteningError(env, c.loc(), ss.str());
 946        }
 947        if (!origdecl->fromStdLib()) {
 948          auto* decl_copy = copy(env, env.cmap, origdecl)->cast<FunctionI>();
 949          if (decl_copy != decl) {
 950            decl = decl_copy;
 951            (void)env.output->registerFn(env, decl, true);
 952            env.output->addItem(decl);
 953            if (decl->e() != nullptr) {
 954              make_par(env, decl->e());
 955              top_down(*this, decl->e());
 956            }
 957            CollectOccurrencesE ce(env.outputVarOccurrences, decl);
 958            top_down(ce, decl->e());
 959            top_down(ce, decl->ti());
 960            for (unsigned int i = decl->params().size(); (i--) != 0U;) {
 961              top_down(ce, decl->params()[i]);
 962            }
 963          }
 964        } else {
 965          decl = origdecl;
 966        }
 967      }
 968      c.decl(decl);
 969    }
 970  } _cf(e);
 971  top_down(_cf, outputItem->e());
 972
 973  // If we are checking solutions using a checker model, all parameters of the checker model
 974  // have to be made available in the output model
 975  class OV1 : public ItemVisitor {
 976  public:
 977    EnvI& env;
 978    CollectFunctions& cf;
 979    OV1(EnvI& env0, CollectFunctions& cf0) : env(env0), cf(cf0) {}
 980    void vVarDeclI(VarDeclI* vdi) {
 981      if (vdi->e()->ann().contains(constants().ann.mzn_check_var)) {
 982        auto* output_vd = copy(env, env.cmap, vdi->e())->cast<VarDecl>();
 983        top_down(cf, output_vd);
 984      }
 985    }
 986  } _ov1(e, _cf);
 987  iter_items(_ov1, e.model);
 988
 989  // Copying the output item and the functions it depends on has created copies
 990  // of all dependent VarDecls. However the output model does not contain VarDeclIs for
 991  // these VarDecls yet. This iterator processes all variable declarations of the
 992  // original model, and if they were copied (i.e., if the output model depends on them),
 993  // the corresponding VarDeclI is created in the output model.
 994  class OV2 : public ItemVisitor {
 995  public:
 996    EnvI& env;
 997    OV2(EnvI& env0) : env(env0) {}
 998    void vVarDeclI(VarDeclI* vdi) {
 999      auto idx = env.outputVarOccurrences.idx.find(vdi->e()->id());
1000      if (idx != env.outputVarOccurrences.idx.end()) {
1001        return;
1002      }
1003      if (Expression* vd_e = env.cmap.find(vdi->e())) {
1004        // We found a copied VarDecl, now need to create a VarDeclI
1005        auto* vd = vd_e->cast<VarDecl>();
1006        auto* vdi_copy = copy(env, env.cmap, vdi)->cast<VarDeclI>();
1007
1008        Type t = vdi_copy->e()->ti()->type();
1009        t.ti(Type::TI_PAR);
1010        vdi_copy->e()->ti()->domain(nullptr);
1011        vdi_copy->e()->flat(vdi->e()->flat());
1012        bool isCheckVar = vdi_copy->e()->ann().contains(constants().ann.mzn_check_var);
1013        Call* checkVarEnum = vdi_copy->e()->ann().getCall(constants().ann.mzn_check_enum_var);
1014        vdi_copy->e()->ann().clear();
1015        if (isCheckVar) {
1016          vdi_copy->e()->ann().add(constants().ann.mzn_check_var);
1017        }
1018        if (checkVarEnum != nullptr) {
1019          vdi_copy->e()->ann().add(checkVarEnum);
1020        }
1021        vdi_copy->e()->introduced(false);
1022        IdMap<KeepAlive>::iterator it;
1023        if (!vdi->e()->type().isPar()) {
1024          if (vd->flat() == nullptr && vdi->e()->e() != nullptr && vdi->e()->e()->type().isPar()) {
1025            // Don't have a flat version of this variable, but the original has a right hand
1026            // side that is par, so we can use that.
1027            Expression* flate = eval_par(env, vdi->e()->e());
1028            output_vardecls(env, vdi_copy, flate);
1029            vd->e(flate);
1030          } else {
1031            vd = follow_id_to_decl(vd->id())->cast<VarDecl>();
1032            VarDecl* reallyFlat = vd->flat();
1033            while ((reallyFlat != nullptr) && reallyFlat != reallyFlat->flat()) {
1034              reallyFlat = reallyFlat->flat();
1035            }
1036            if (reallyFlat == nullptr) {
1037              // The variable doesn't have a flat version. This can only happen if
1038              // the original variable had type-inst var, but a right-hand-side that
1039              // was par, so follow_id_to_decl lead to a par variable.
1040              assert(vd->e() && vd->e()->type().isPar());
1041              Expression* flate = eval_par(env, vd->e());
1042              output_vardecls(env, vdi_copy, flate);
1043              vd->e(flate);
1044            } else if ((vd->flat()->e() != nullptr) && vd->flat()->e()->type().isPar()) {
1045              // We can use the right hand side of the flat version of this variable
1046              Expression* flate = copy(env, env.cmap, follow_id(reallyFlat->id()));
1047              output_vardecls(env, vdi_copy, flate);
1048              vd->e(flate);
1049            } else if ((it = env.reverseMappers.find(vd->id())) != env.reverseMappers.end()) {
1050              // Found a reverse mapper, so we need to add the mapping function to the
1051              // output model to map the FlatZinc value back to the model variable.
1052              Call* rhs = copy(env, env.cmap, it->second())->cast<Call>();
1053              check_output_par_fn(env, rhs);
1054              output_vardecls(env, vdi_copy, rhs);
1055              vd->e(rhs);
1056            } else if (cannot_use_rhs_for_output(env, vd->e())) {
1057              // If the VarDecl does not have a usable right hand side, it needs to be
1058              // marked as output in the FlatZinc
1059              vd->e(nullptr);
1060              assert(vd->flat());
1061              if (vd->type().dim() == 0) {
1062                vd->flat()->addAnnotation(constants().ann.output_var);
1063                check_rename_var(env, vd);
1064              } else {
1065                bool needOutputAnn = true;
1066                if ((reallyFlat->e() != nullptr) && reallyFlat->e()->isa<ArrayLit>()) {
1067                  auto* al = reallyFlat->e()->cast<ArrayLit>();
1068                  for (unsigned int i = 0; i < al->size(); i++) {
1069                    if (Id* id = (*al)[i]->dynamicCast<Id>()) {
1070                      if (env.reverseMappers.find(id) != env.reverseMappers.end()) {
1071                        needOutputAnn = false;
1072                        break;
1073                      }
1074                    }
1075                  }
1076                  if (!needOutputAnn) {
1077                    output_vardecls(env, vdi_copy, al);
1078                    vd->e(copy(env, env.cmap, al));
1079                  }
1080                }
1081                if (needOutputAnn) {
1082                  std::vector<Expression*> args(vdi->e()->type().dim());
1083                  for (unsigned int i = 0; i < args.size(); i++) {
1084                    if (vdi->e()->ti()->ranges()[i]->domain() == nullptr) {
1085                      args[i] =
1086                          new SetLit(Location().introduce(),
1087                                     eval_intset(env, vd->flat()->ti()->ranges()[i]->domain()));
1088                    } else {
1089                      args[i] = new SetLit(Location().introduce(),
1090                                           eval_intset(env, vd->ti()->ranges()[i]->domain()));
1091                    }
1092                  }
1093                  auto* al = new ArrayLit(Location().introduce(), args);
1094                  args.resize(1);
1095                  args[0] = al;
1096                  vd->flat()->addAnnotation(
1097                      new Call(Location().introduce(), constants().ann.output_array, args));
1098                  check_rename_var(env, vd);
1099                }
1100              }
1101            }
1102            if ((reallyFlat != nullptr) && env.outputFlatVarOccurrences.find(reallyFlat) == -1) {
1103              env.outputFlatVarOccurrences.addIndex(reallyFlat,
1104                                                    static_cast<int>(env.output->size()));
1105            }
1106          }
1107        } else {
1108          if (vd->flat() == nullptr && vdi->e()->e() != nullptr) {
1109            // Need to process right hand side of variable, since it may contain
1110            // identifiers that are only in the FlatZinc and that we would
1111            // therefore fail to copy into the output model
1112            output_vardecls(env, vdi_copy, vdi->e()->e());
1113          }
1114        }
1115        make_par(env, vdi_copy->e());
1116        env.outputVarOccurrences.addIndex(vdi_copy, static_cast<int>(env.output->size()));
1117        CollectOccurrencesE ce(env.outputVarOccurrences, vdi_copy);
1118        top_down(ce, vdi_copy->e());
1119        env.output->addItem(vdi_copy);
1120      }
1121    }
1122  } _ov2(e);
1123  iter_items(_ov2, e.model);
1124
1125  CollectOccurrencesE ce(e.outputVarOccurrences, outputItem);
1126  top_down(ce, outputItem->e());
1127
1128  e.model->mergeStdLib(e, e.output);
1129  process_deletions(e);
1130}
1131
1132Expression* is_fixed_domain(EnvI& env, VarDecl* vd) {
1133  if (vd->type() != Type::varbool() && vd->type() != Type::varint() &&
1134      vd->type() != Type::varfloat()) {
1135    return nullptr;
1136  }
1137  Expression* e = vd->ti()->domain();
1138  if (e == constants().literalTrue || e == constants().literalFalse) {
1139    return e;
1140  }
1141  if (auto* sl = Expression::dynamicCast<SetLit>(e)) {
1142    if (sl->type().bt() == Type::BT_INT) {
1143      IntSetVal* isv = eval_intset(env, sl);
1144      return isv->min() == isv->max() ? IntLit::a(isv->min()) : nullptr;
1145    }
1146    if (sl->type().bt() == Type::BT_FLOAT) {
1147      FloatSetVal* fsv = eval_floatset(env, sl);
1148      return fsv->min() == fsv->max() ? FloatLit::a(fsv->min()) : nullptr;
1149    }
1150  }
1151  return nullptr;
1152}
1153
1154void finalise_output(EnvI& e) {
1155  if (e.output->size() > 0) {
1156    // Adapt existing output model
1157    // (generated by repeated flattening)
1158    e.outputVarOccurrences.clear();
1159    for (unsigned int i = 0; i < e.output->size(); i++) {
1160      Item* item = (*e.output)[i];
1161      if (item->removed()) {
1162        continue;
1163      }
1164      switch (item->iid()) {
1165        case Item::II_VD: {
1166          VarDecl* vd = item->cast<VarDeclI>()->e();
1167          IdMap<KeepAlive>::iterator it;
1168          GCLock lock;
1169          VarDecl* reallyFlat = vd->flat();
1170          while ((reallyFlat != nullptr) && reallyFlat != reallyFlat->flat()) {
1171            reallyFlat = reallyFlat->flat();
1172          }
1173          if (vd->e() == nullptr) {
1174            if (((vd->flat()->e() != nullptr) && vd->flat()->e()->type().isPar()) ||
1175                (is_fixed_domain(e, vd->flat()) != nullptr)) {
1176              VarDecl* reallyFlat = vd->flat();
1177              while (reallyFlat != reallyFlat->flat()) {
1178                reallyFlat = reallyFlat->flat();
1179              }
1180              remove_is_output(reallyFlat);
1181              Expression* flate;
1182              if (Expression* fd = is_fixed_domain(e, vd->flat())) {
1183                flate = fd;
1184              } else {
1185                flate = copy(e, e.cmap, follow_id(reallyFlat->id()));
1186              }
1187              output_vardecls(e, item, flate);
1188              vd->e(flate);
1189            } else if ((it = e.reverseMappers.find(vd->id())) != e.reverseMappers.end()) {
1190              Call* rhs = copy(e, e.cmap, it->second())->cast<Call>();
1191              check_output_par_fn(e, rhs);
1192              remove_is_output(reallyFlat);
1193
1194              output_vardecls(e, item, it->second()->cast<Call>());
1195              vd->e(rhs);
1196
1197              if (e.varOccurrences.occurrences(reallyFlat) == 0 && reallyFlat->e() == nullptr) {
1198                auto it = e.varOccurrences.idx.find(reallyFlat->id());
1199                assert(it != e.varOccurrences.idx.end());
1200                e.flatRemoveItem((*e.flat())[it->second]->cast<VarDeclI>());
1201              }
1202            } else {
1203              // If the VarDecl does not have a usable right hand side, it needs to be
1204              // marked as output in the FlatZinc
1205              assert(vd->flat());
1206
1207              bool needOutputAnn = true;
1208              if ((reallyFlat->e() != nullptr) && reallyFlat->e()->isa<Id>()) {
1209                Id* ident = reallyFlat->e()->cast<Id>();
1210                if (e.reverseMappers.find(ident) != e.reverseMappers.end()) {
1211                  needOutputAnn = false;
1212                  remove_is_output(vd);
1213                  remove_is_output(reallyFlat);
1214
1215                  vd->e(copy(e, e.cmap, ident));
1216                  Type al_t(vd->e()->type());
1217                  al_t.ti(Type::TI_PAR);
1218                  vd->e()->type(al_t);
1219
1220                  output_vardecls(e, item, ident);
1221
1222                  if (e.varOccurrences.occurrences(reallyFlat) == 0) {
1223                    auto it = e.varOccurrences.idx.find(reallyFlat->id());
1224                    assert(it != e.varOccurrences.idx.end());
1225                    e.flatRemoveItem((*e.flat())[it->second]->cast<VarDeclI>());
1226                  }
1227                }
1228              } else if ((reallyFlat->e() != nullptr) && reallyFlat->e()->isa<ArrayLit>()) {
1229                auto* al = reallyFlat->e()->cast<ArrayLit>();
1230                for (unsigned int i = 0; i < al->size(); i++) {
1231                  if (Id* ident = follow_id_to_value((*al)[i])->dynamicCast<Id>()) {
1232                    if (e.reverseMappers.find(ident) != e.reverseMappers.end()) {
1233                      needOutputAnn = false;
1234                      break;
1235                    }
1236                  }
1237                }
1238                if (!needOutputAnn) {
1239                  remove_is_output(vd);
1240                  remove_is_output(reallyFlat);
1241                  if (e.varOccurrences.occurrences(reallyFlat) == 0) {
1242                    auto it = e.varOccurrences.idx.find(reallyFlat->id());
1243                    assert(it != e.varOccurrences.idx.end());
1244                    e.flatRemoveItem((*e.flat())[it->second]->cast<VarDeclI>());
1245                  }
1246
1247                  output_vardecls(e, item, al);
1248                  vd->e(copy(e, e.cmap, al));
1249                  Type al_t(vd->e()->type());
1250                  al_t.ti(Type::TI_PAR);
1251                  vd->e()->type(al_t);
1252                }
1253              }
1254              if (needOutputAnn) {
1255                if (!is_output(vd->flat())) {
1256                  GCLock lock;
1257                  if (vd->type().dim() == 0) {
1258                    vd->flat()->addAnnotation(constants().ann.output_var);
1259                  } else {
1260                    std::vector<Expression*> args(vd->type().dim());
1261                    for (unsigned int i = 0; i < args.size(); i++) {
1262                      if (vd->ti()->ranges()[i]->domain() == nullptr) {
1263                        args[i] =
1264                            new SetLit(Location().introduce(),
1265                                       eval_intset(e, vd->flat()->ti()->ranges()[i]->domain()));
1266                      } else {
1267                        args[i] = new SetLit(Location().introduce(),
1268                                             eval_intset(e, vd->ti()->ranges()[i]->domain()));
1269                      }
1270                    }
1271                    auto* al = new ArrayLit(Location().introduce(), args);
1272                    args.resize(1);
1273                    args[0] = al;
1274                    vd->flat()->addAnnotation(
1275                        new Call(Location().introduce(), constants().ann.output_array, args));
1276                  }
1277                  check_rename_var(e, vd);
1278                }
1279              }
1280            }
1281            vd->flat(nullptr);
1282            // Remove enum type
1283            Type vdt = vd->type();
1284            vdt.enumId(0);
1285            vd->type(vdt);
1286            vd->ti()->type(vdt);
1287          }
1288          e.outputVarOccurrences.addIndex(item->cast<VarDeclI>(), static_cast<int>(i));
1289          CollectOccurrencesE ce(e.outputVarOccurrences, item);
1290          top_down(ce, vd);
1291        } break;
1292        case Item::II_OUT: {
1293          CollectOccurrencesE ce(e.outputVarOccurrences, item);
1294          top_down(ce, item->cast<OutputI>()->e());
1295        } break;
1296        case Item::II_FUN: {
1297          CollectOccurrencesE ce(e.outputVarOccurrences, item);
1298          top_down(ce, item->cast<FunctionI>()->e());
1299          top_down(ce, item->cast<FunctionI>()->ti());
1300          for (unsigned int i = item->cast<FunctionI>()->params().size(); (i--) != 0U;) {
1301            top_down(ce, item->cast<FunctionI>()->params()[i]);
1302          }
1303        } break;
1304        default:
1305          throw FlatteningError(e, item->loc(), "invalid item in output model");
1306      }
1307    }
1308  }
1309  process_deletions(e);
1310}
1311}  // namespace MiniZinc