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

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