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

this repo has no description
on-restart-benchmarks / software / minizinc / lib / flatten / flatten_call.cpp
at develop 49 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/flat_exp.hh>
  13
  14namespace MiniZinc {
  15
  16std::vector<Expression*> to_exp_vec(std::vector<KeepAlive>& v) {
  17  std::vector<Expression*> r(v.size());
  18  for (auto i = static_cast<unsigned int>(v.size()); (i--) != 0U;) {
  19    r[i] = v[i]();
  20  }
  21  return r;
  22}
  23
  24bool is_total(FunctionI* fi) { return fi->ann().contains(constants().ann.promise_total); }
  25
  26Call* same_call(EnvI& env, Expression* e, const ASTString& id) {
  27  assert(GC::locked());
  28  Expression* ce = follow_id(e);
  29  Call* c = Expression::dynamicCast<Call>(ce);
  30  if (c != nullptr) {
  31    if (c->id() == id) {
  32      return ce->cast<Call>();
  33    }
  34    if (c->id() == constants().ids.int2float) {
  35      Expression* i2f = follow_id(c->arg(0));
  36      Call* i2fc = Expression::dynamicCast<Call>(i2f);
  37      if ((i2fc != nullptr) && i2fc->id() == id && id == constants().ids.lin_exp) {
  38        ArrayLit* coeffs = eval_array_lit(env, i2fc->arg(0));
  39        std::vector<Expression*> ncoeff_v(coeffs->size());
  40        for (unsigned int i = 0; i < coeffs->size(); i++) {
  41          ncoeff_v[i] = FloatLit::a(eval_int(env, (*coeffs)[i]));
  42        }
  43        auto* ncoeff = new ArrayLit(coeffs->loc().introduce(), ncoeff_v);
  44        ncoeff->type(Type::parfloat(1));
  45        ArrayLit* vars = eval_array_lit(env, i2fc->arg(1));
  46        std::vector<Expression*> n_vars_v(vars->size());
  47        for (unsigned int i = 0; i < vars->size(); i++) {
  48          Call* f2i =
  49              new Call((*vars)[i]->loc().introduce(), constants().ids.int2float, {(*vars)[i]});
  50          f2i->decl(env.model->matchFn(env, f2i, false));
  51          assert(f2i->decl());
  52          f2i->type(Type::varfloat());
  53          EE ee = flat_exp(env, Ctx(), f2i, nullptr, constants().varTrue);
  54          n_vars_v[i] = ee.r();
  55        }
  56        auto* nvars = new ArrayLit(vars->loc().introduce(), n_vars_v);
  57        nvars->type(Type::varfloat(1));
  58        FloatVal c = eval_int(env, i2fc->arg(2));
  59        Call* nlinexp = new Call(i2fc->loc().introduce(), constants().ids.lin_exp,
  60                                 {ncoeff, nvars, FloatLit::a(c)});
  61        nlinexp->decl(env.model->matchFn(env, nlinexp, false));
  62        assert(nlinexp->decl());
  63        nlinexp->type(Type::varfloat());
  64        return nlinexp;
  65      }
  66    }
  67  }
  68  return nullptr;
  69}
  70
  71class CmpExp {
  72public:
  73  bool operator()(const KeepAlive& i, const KeepAlive& j) const {
  74    if (Expression::equal(i(), j())) {
  75      return false;
  76    }
  77    return i() < j();
  78  }
  79};
  80
  81bool remove_dups(std::vector<KeepAlive>& x, bool identity) {
  82  for (auto& i : x) {
  83    i = follow_id_to_value(i());
  84  }
  85  std::sort(x.begin(), x.end(), CmpExp());
  86  int ci = 0;
  87  Expression* prev = nullptr;
  88  for (unsigned int i = 0; i < x.size(); i++) {
  89    if (!Expression::equal(x[i](), prev)) {
  90      prev = x[i]();
  91      if (x[i]()->isa<BoolLit>()) {
  92        if (x[i]()->cast<BoolLit>()->v() == identity) {
  93          // skip
  94        } else {
  95          return true;
  96        }
  97      } else {
  98        x[ci++] = x[i];
  99      }
 100    }
 101  }
 102  x.resize(ci);
 103  return false;
 104}
 105bool contains_dups(std::vector<KeepAlive>& x, std::vector<KeepAlive>& y) {
 106  if (x.empty() || y.empty()) {
 107    return false;
 108  }
 109  unsigned int ix = 0;
 110  unsigned int iy = 0;
 111  for (;;) {
 112    if (x[ix]() == y[iy]()) {
 113      return true;
 114    }
 115    if (x[ix]() < y[iy]()) {
 116      ix++;
 117    } else {
 118      iy++;
 119    }
 120    if (ix == x.size() || iy == y.size()) {
 121      return false;
 122    }
 123  }
 124}
 125
 126template <class Lit>
 127void flatten_linexp_call(EnvI& env, Ctx ctx, const Ctx& nctx, ASTString& cid, Call* c, EE& ret,
 128                         VarDecl* b, VarDecl* r, std::vector<EE>& args_ee,
 129                         std::vector<KeepAlive>& args) {
 130  typedef typename LinearTraits<Lit>::Val Val;
 131  Expression* al_arg = (cid == constants().ids.sum ? args_ee[0].r() : args_ee[1].r());
 132  EE flat_al = flat_exp(env, nctx, al_arg, nullptr, nullptr);
 133  auto* al = follow_id(flat_al.r())->template cast<ArrayLit>();
 134  KeepAlive al_ka = al;
 135  if (al->dims() > 1) {
 136    Type alt = al->type();
 137    alt.dim(1);
 138    GCLock lock;
 139    al = new ArrayLit(al->loc(), *al);
 140    al->type(alt);
 141    al_ka = al;
 142  }
 143  Val d = (cid == constants().ids.sum ? Val(0) : LinearTraits<Lit>::eval(env, args_ee[2].r()));
 144
 145  std::vector<Val> c_coeff(al->size());
 146  if (cid == constants().ids.sum) {
 147    for (unsigned int i = al->size(); i--;) {
 148      c_coeff[i] = 1;
 149    }
 150  } else {
 151    EE flat_coeff = flat_exp(env, nctx, args_ee[0].r(), nullptr, nullptr);
 152    auto* coeff = follow_id(flat_coeff.r())->template cast<ArrayLit>();
 153    for (unsigned int i = coeff->size(); i--;) {
 154      c_coeff[i] = LinearTraits<Lit>::eval(env, (*coeff)[i]);
 155    }
 156  }
 157  cid = constants().ids.lin_exp;
 158  std::vector<Val> coeffv;
 159  std::vector<KeepAlive> alv;
 160  for (unsigned int i = 0; i < al->size(); i++) {
 161    GCLock lock;
 162    if (Call* sc = Expression::dynamicCast<Call>(same_call(env, (*al)[i], cid))) {
 163      if (auto* alvi_decl = follow_id_to_decl((*al)[i])->template dynamicCast<VarDecl>()) {
 164        if (alvi_decl->ti()->domain()) {
 165          // Test if the variable has tighter declared bounds than what can be inferred
 166          // from its RHS. If yes, keep the variable (don't aggregate), because the tighter
 167          // bounds are actually a constraint
 168          typename LinearTraits<Lit>::Domain sc_dom =
 169              LinearTraits<Lit>::evalDomain(env, alvi_decl->ti()->domain());
 170          typename LinearTraits<Lit>::Bounds sc_bounds = LinearTraits<Lit>::computeBounds(env, sc);
 171          if (LinearTraits<Lit>::domainTighter(sc_dom, sc_bounds)) {
 172            coeffv.push_back(c_coeff[i]);
 173            alv.emplace_back((*al)[i]);
 174            continue;
 175          }
 176        }
 177      }
 178
 179      Val cd = c_coeff[i];
 180      ArrayLit* sc_coeff = eval_array_lit(env, sc->arg(0));
 181      ArrayLit* sc_al = eval_array_lit(env, sc->arg(1));
 182      Val sc_d = LinearTraits<Lit>::eval(env, sc->arg(2));
 183      assert(sc_coeff->size() == sc_al->size());
 184      for (unsigned int j = 0; j < sc_coeff->size(); j++) {
 185        coeffv.push_back(cd * LinearTraits<Lit>::eval(env, (*sc_coeff)[j]));
 186        alv.emplace_back((*sc_al)[j]);
 187      }
 188      d += cd * sc_d;
 189    } else {
 190      coeffv.push_back(c_coeff[i]);
 191      alv.emplace_back((*al)[i]);
 192    }
 193  }
 194  simplify_lin<Lit>(coeffv, alv, d);
 195  if (coeffv.empty()) {
 196    GCLock lock;
 197    ret.b = conj(env, b, Ctx(), args_ee);
 198    ret.r = bind(env, ctx, r, LinearTraits<Lit>::newLit(d));
 199    return;
 200  }
 201  if (coeffv.size() == 1 && coeffv[0] == 1 && d == 0) {
 202    ret.b = conj(env, b, Ctx(), args_ee);
 203    ret.r = bind(env, ctx, r, alv[0]());
 204    return;
 205  }
 206  GCLock lock;
 207  std::vector<Expression*> coeff_ev(coeffv.size());
 208  for (auto i = static_cast<unsigned int>(coeff_ev.size()); i--;) {
 209    coeff_ev[i] = LinearTraits<Lit>::newLit(coeffv[i]);
 210  }
 211  auto* ncoeff = new ArrayLit(Location().introduce(), coeff_ev);
 212  Type t = coeff_ev[0]->type();
 213  t.dim(1);
 214  ncoeff->type(t);
 215  args.emplace_back(ncoeff);
 216  std::vector<Expression*> alv_e(alv.size());
 217  bool al_same_as_before = alv.size() == al->size();
 218  for (auto i = static_cast<unsigned int>(alv.size()); i--;) {
 219    alv_e[i] = alv[i]();
 220    al_same_as_before = al_same_as_before && Expression::equal(alv_e[i], (*al)[i]);
 221  }
 222  if (al_same_as_before) {
 223    Expression* rd = follow_id_to_decl(flat_al.r());
 224    if (rd->isa<VarDecl>()) {
 225      rd = rd->cast<VarDecl>()->id();
 226    }
 227    if (rd->type().dim() > 1) {
 228      ArrayLit* al = eval_array_lit(env, rd);
 229      std::vector<std::pair<int, int> > dims(1);
 230      dims[0].first = 1;
 231      dims[0].second = al->size();
 232      rd = new ArrayLit(al->loc(), *al, dims);
 233      Type t = al->type();
 234      t.dim(1);
 235      rd->type(t);
 236    }
 237    args.emplace_back(rd);
 238  } else {
 239    auto* nal = new ArrayLit(al->loc(), alv_e);
 240    nal->type(al->type());
 241    args.emplace_back(nal);
 242  }
 243  Lit* il = LinearTraits<Lit>::newLit(d);
 244  args.push_back(il);
 245}
 246
 247/// Special form of disjunction for SCIP
 248bool is_totaladd_bounds_disj(EnvI& env, Expression* arg, Call* c_orig) {
 249  auto* pArrayLit = arg->dynamicCast<ArrayLit>();
 250  if (nullptr == pArrayLit) {
 251    return false;
 252  }
 253  // integer bounds and vars
 254  std::vector<Expression*> isUBI;
 255  std::vector<Expression*> bndI;
 256  std::vector<Expression*> varI;
 257  // float bounds and vars
 258  std::vector<Expression*> isUBF;
 259  std::vector<Expression*> bndF;
 260  std::vector<Expression*> varF;
 261  for (unsigned int i = pArrayLit->size(); (i--) != 0U;) {
 262    auto* pId = pArrayLit->operator[](i)->dynamicCast<Id>();
 263    if (nullptr == pId) {
 264      return false;
 265    }
 266    auto* pDecl = follow_id_to_decl(pId)->dynamicCast<VarDecl>();
 267    /// Checking the rhs
 268    auto* pRhs = pDecl->e();
 269    if (nullptr == pRhs) {
 270      return false;  // not checking this boolean
 271    }
 272    auto* pCall = pRhs->dynamicCast<Call>();
 273    if (nullptr == pCall) {
 274      return false;
 275    }
 276    if (constants().ids.int_.le != pCall->id() && constants().ids.float_.le != pCall->id()) {
 277      return false;
 278    }
 279    /// See if one is a constant and one a variable
 280    Expression* pConst = nullptr;
 281    Expression* pVar = nullptr;
 282    bool fFloat = false;
 283    bool isUB = false;
 284    for (unsigned int j = pCall->argCount(); (j--) != 0U;) {
 285      if (auto* pF = pCall->arg(j)->dynamicCast<FloatLit>()) {
 286        pConst = pF;
 287        fFloat = true;
 288        isUB = (1 == j);
 289      } else if (auto* pF = pCall->arg(j)->dynamicCast<IntLit>()) {
 290        pConst = pF;
 291        fFloat = false;
 292        isUB = (1 == j);
 293      } else if (auto* pId = pCall->arg(j)->dynamicCast<Id>()) {
 294        if (nullptr != pVar) {
 295          return false;  // 2 variables, exit
 296        }
 297        pVar = pId;
 298      }
 299    }
 300    /// All good, add them
 301    if (fFloat) {
 302      isUBF.push_back(constants().boollit(isUB));
 303      bndF.push_back(pConst);
 304      varF.push_back(pVar);
 305    } else {
 306      isUBI.push_back(constants().boollit(isUB));
 307      bndI.push_back(pConst);
 308      varI.push_back(pVar);
 309    }
 310  }
 311  /// Create new call
 312  GCLock lock;
 313  auto loc = c_orig->loc().introduce();
 314  std::vector<Expression*> args = {new ArrayLit(loc, isUBI), new ArrayLit(loc, bndI),
 315                                   new ArrayLit(loc, varI),  new ArrayLit(loc, isUBF),
 316                                   new ArrayLit(loc, bndF),  new ArrayLit(loc, varF)};
 317
 318  Call* c =
 319      new Call(c_orig->loc().introduce(), env.model->getFnDecls().boundsDisj.second->id(), args);
 320  c->type(Type::varbool());
 321  c->decl(env.model->getFnDecls().boundsDisj.second);
 322  env.flatAddItem(new ConstraintI(c_orig->loc().introduce(), c));
 323  return true;
 324}
 325
 326class IgnorePartial {
 327public:
 328  EnvI& env;
 329  bool ignorePartial;
 330  IgnorePartial(EnvI& env0, Call* c) : env(env0), ignorePartial(env.ignorePartial) {
 331    if (c->id().endsWith("_reif") || c->id().endsWith("_imp")) {
 332      env.ignorePartial = true;
 333    }
 334  }
 335  ~IgnorePartial() { env.ignorePartial = ignorePartial; }
 336};
 337
 338// NOLINTNEXTLINE(readability-function-size): TODO??
 339EE flatten_call(EnvI& env, const Ctx& input_ctx, Expression* e, VarDecl* r, VarDecl* b) {
 340  EE ret;
 341  Call* c = e->cast<Call>();
 342  IgnorePartial ignorePartial(env, c);
 343  if (c->id().endsWith("_reif")) {
 344    env.counters.reifConstraints++;
 345  } else if (c->id().endsWith("_imp")) {
 346    env.counters.impConstraints++;
 347  }
 348  FunctionI* decl = env.model->matchFn(env, c, false);
 349  if (decl == nullptr) {
 350    std::ostringstream ss;
 351    ss << "undeclared function or predicate " << c->id();
 352    throw InternalError(ss.str());
 353  }
 354
 355  Ctx ctx = input_ctx;
 356  Ctx nctx = ctx;
 357  nctx.neg = false;
 358  ASTString cid = c->id();
 359  CallStackItem _csi(env, e);
 360
 361  if (cid == constants().ids.bool2int && c->type().dim() == 0) {
 362    if (ctx.neg) {
 363      ctx.neg = false;
 364      nctx.neg = true;
 365      nctx.b = -ctx.i;
 366    } else {
 367      nctx.b = ctx.i;
 368    }
 369  } else if (cid == constants().ids.forall) {
 370    nctx.b = +nctx.b;
 371    if (ctx.neg) {
 372      ctx.neg = false;
 373      nctx.neg = true;
 374      cid = constants().ids.exists;
 375    }
 376  } else if (cid == constants().ids.exists) {
 377    nctx.b = +nctx.b;
 378    if (ctx.neg) {
 379      ctx.neg = false;
 380      nctx.neg = true;
 381      cid = constants().ids.forall;
 382    }
 383  } else if (decl->e() == nullptr &&
 384             (cid == constants().ids.assert || cid == constants().ids.trace ||
 385              cid == constants().ids.mzn_symmetry_breaking_constraint ||
 386              cid == constants().ids.mzn_redundant_constraint ||
 387              cid == constants().ids.mzn_deprecate)) {
 388    if (cid == constants().ids.assert && c->argCount() == 2) {
 389      (void)decl->builtins.b(env, c);
 390      ret = flat_exp(env, ctx, constants().literalTrue, r, b);
 391    } else {
 392      KeepAlive callres = decl->builtins.e(env, c);
 393      ret = flat_exp(env, ctx, callres(), r, b);
 394      // This is all we need to do for assert, so break out of the E_CALL
 395    }
 396    return ret;
 397  } else if ((decl->e() != nullptr) && ctx.b == C_ROOT && decl->e()->isa<BoolLit>() &&
 398             eval_bool(env, decl->e())) {
 399    bool allBool = true;
 400    for (unsigned int i = 0; i < c->argCount(); i++) {
 401      if (c->arg(i)->type().bt() != Type::BT_BOOL) {
 402        allBool = false;
 403        break;
 404      }
 405    }
 406    if (allBool) {
 407      ret.r = bind(env, ctx, r, constants().literalTrue);
 408      ret.b = bind(env, ctx, b, constants().literalTrue);
 409      return ret;
 410    }
 411  }
 412
 413  if (ctx.b == C_ROOT && decl->e() == nullptr && cid == constants().ids.forall &&
 414      r == constants().varTrue) {
 415    ret.b = bind(env, ctx, b, constants().literalTrue);
 416    ArrayLit* al;
 417    if (c->arg(0)->isa<ArrayLit>()) {
 418      al = c->arg(0)->cast<ArrayLit>();
 419    } else {
 420      EE flat_al = flat_exp(env, Ctx(), c->arg(0), constants().varIgnore, constants().varTrue);
 421      al = follow_id(flat_al.r())->cast<ArrayLit>();
 422    }
 423    nctx.b = C_ROOT;
 424    for (unsigned int i = 0; i < al->size(); i++) {
 425      (void)flat_exp(env, nctx, (*al)[i], r, b);
 426    }
 427    ret.r = bind(env, ctx, r, constants().literalTrue);
 428  } else {
 429    if ((decl->e() != nullptr) && decl->params().size() == 1 && decl->e()->isa<Id>() &&
 430        decl->params()[0]->ti()->domain() == nullptr &&
 431        decl->e()->cast<Id>()->decl() == decl->params()[0]) {
 432      Expression* arg = c->arg(0);
 433      for (ExpressionSetIter esi = decl->e()->ann().begin(); esi != decl->e()->ann().end(); ++esi) {
 434        arg->addAnnotation(*esi);
 435      }
 436      for (ExpressionSetIter esi = c->ann().begin(); esi != c->ann().end(); ++esi) {
 437        arg->addAnnotation(*esi);
 438      }
 439      ret = flat_exp(env, ctx, c->arg(0), r, b);
 440      return ret;
 441    }
 442
 443    std::vector<EE> args_ee(c->argCount());
 444    bool isPartial = false;
 445
 446    if (cid == constants().ids.lin_exp && c->type().isint()) {
 447      // Linear expressions need special context handling:
 448      // the context of a variable expression depends on the corresponding coefficient
 449
 450      // flatten the coefficient array
 451      Expression* tmp = follow_id_to_decl(c->arg(0));
 452      ArrayLit* coeffs;
 453      if (auto* vd = tmp->dynamicCast<VarDecl>()) {
 454        tmp = vd->id();
 455      }
 456      {
 457        CallArgItem cai(env);
 458        args_ee[0] = flat_exp(env, nctx, tmp, nullptr, nullptr);
 459        isPartial |= isfalse(env, args_ee[0].b());
 460        coeffs = eval_array_lit(env, args_ee[0].r());
 461      }
 462
 463      ArrayLit* vars = eval_array_lit(env, c->arg(1));
 464      if (vars->flat()) {
 465        args_ee[1].r = vars;
 466        args_ee[1].b = constants().varTrue;
 467      } else {
 468        CallArgItem cai(env);
 469        CallStackItem _csi(env, c->arg(1));
 470        std::vector<EE> elems_ee(vars->size());
 471        for (unsigned int i = vars->size(); (i--) != 0U;) {
 472          Ctx argctx = nctx;
 473          argctx.i = eval_int(env, (*coeffs)[i]) < 0 ? -nctx.i : +nctx.i;
 474          elems_ee[i] = flat_exp(env, argctx, (*vars)[i], nullptr, nullptr);
 475        }
 476        std::vector<Expression*> elems(elems_ee.size());
 477        for (auto i = static_cast<unsigned int>(elems.size()); (i--) != 0U;) {
 478          elems[i] = elems_ee[i].r();
 479        }
 480        KeepAlive ka;
 481        {
 482          GCLock lock;
 483          auto* alr = new ArrayLit(Location().introduce(), elems);
 484          alr->type(vars->type());
 485          alr->flat(true);
 486          ka = alr;
 487        }
 488        args_ee[1].r = ka();
 489        args_ee[1].b = conj(env, b, Ctx(), elems_ee);
 490      }
 491
 492      {
 493        Expression* constant = follow_id_to_decl(c->arg(2));
 494        if (auto* vd = constant->dynamicCast<VarDecl>()) {
 495          constant = vd->id();
 496        }
 497        CallArgItem cai(env);
 498        args_ee[2] = flat_exp(env, nctx, constant, nullptr, nullptr);
 499        isPartial |= isfalse(env, args_ee[2].b());
 500      }
 501
 502    } else {
 503      bool mixContext =
 504          (cid != constants().ids.forall && cid != constants().ids.exists &&
 505           (cid != constants().ids.bool2int || c->type().dim() > 0) && cid != constants().ids.sum &&
 506           cid != "assert" && cid != constants().varRedef->id() && cid != "mzn_reverse_map_var");
 507      if (cid == "mzn_reverse_map_var") {
 508        env.inReverseMapVar = true;
 509      }
 510      if (cid == constants().ids.clause && c->arg(0)->isa<ArrayLit>() &&
 511          c->arg(1)->isa<ArrayLit>()) {
 512        Ctx argctx = nctx;
 513
 514        // handle negated args first, try to make them positive
 515
 516        if (mixContext) {
 517          argctx.b = -nctx.b;
 518        }
 519        std::vector<KeepAlive> neg_args;
 520        std::vector<KeepAlive> pos_args;
 521        std::vector<KeepAlive> newPositives;
 522        bool is_subsumed = false;
 523        auto* al_neg = c->arg(1)->cast<ArrayLit>();
 524        {
 525          CallArgItem cai(env);
 526          for (unsigned int i = 0; i < al_neg->size(); i++) {
 527            auto* bo = (*al_neg)[i]->dynamicCast<BinOp>();
 528            Call* co = (*al_neg)[i]->dynamicCast<Call>();
 529            if ((bo != nullptr) || ((co != nullptr) && (co->id() == constants().ids.forall ||
 530                                                        co->id() == constants().ids.exists ||
 531                                                        co->id() == constants().ids.clause))) {
 532              GCLock lock;
 533              UnOp* notBoe0 = new UnOp(Location().introduce(), UOT_NOT, (*al_neg)[i]);
 534              notBoe0->type(Type::varbool());
 535              newPositives.emplace_back(notBoe0);
 536            } else {
 537              EE res = flat_exp(env, argctx, (*al_neg)[i], nullptr, constants().varTrue);
 538              if (res.r()->type().isPar()) {
 539                if (eval_bool(env, res.r())) {
 540                  // this element is irrelevant
 541                } else {
 542                  // this element subsumes all other elements
 543                  neg_args = {res.r()};
 544                  pos_args = {};
 545                  is_subsumed = true;
 546                  break;
 547                }
 548              } else {
 549                neg_args.emplace_back(res.r());
 550              }
 551            }
 552          }
 553        }
 554
 555        // Now process new and previous positive arguments
 556        if (mixContext) {
 557          argctx.b = +nctx.b;
 558        }
 559        auto* al_pos = c->arg(0)->cast<ArrayLit>();
 560        for (unsigned int i = 0; i < al_pos->size(); i++) {
 561          newPositives.emplace_back((*al_pos)[i]);
 562        }
 563        {
 564          CallArgItem cai(env);
 565          for (auto& newPositive : newPositives) {
 566            EE res = flat_exp(env, argctx, newPositive(), nullptr, constants().varTrue);
 567            if (res.r()->type().isPar()) {
 568              if (!eval_bool(env, res.r())) {
 569                // this element is irrelevant
 570              } else {
 571                // this element subsumes all other elements
 572                pos_args = {res.r()};
 573                neg_args = {};
 574                is_subsumed = true;
 575                break;
 576              }
 577            } else {
 578              pos_args.emplace_back(res.r());
 579            }
 580          }
 581        }
 582
 583        GCLock lock;
 584        auto* al_new_pos = new ArrayLit(al_pos->loc(), to_exp_vec(pos_args));
 585        al_new_pos->type(Type::varbool(1));
 586        al_new_pos->flat(true);
 587        args_ee[0] = EE(al_new_pos, constants().literalTrue);
 588        auto* al_new_neg = new ArrayLit(al_neg->loc(), to_exp_vec(neg_args));
 589        al_new_neg->flat(true);
 590        al_new_neg->type(Type::varbool(1));
 591        args_ee[1] = EE(al_new_neg, constants().literalTrue);
 592      } else if ((cid == constants().ids.forall || cid == constants().ids.exists) &&
 593                 c->arg(0)->isa<ArrayLit>()) {
 594        bool is_conj = (cid == constants().ids.forall);
 595        Ctx argctx = nctx;
 596        if (mixContext) {
 597          argctx.b = C_MIX;
 598        }
 599        auto* al = c->arg(0)->cast<ArrayLit>();
 600        ArrayLit* al_new;
 601        if (al->flat()) {
 602          al_new = al;
 603        } else {
 604          std::vector<KeepAlive> flat_args;
 605          CallArgItem cai(env);
 606          for (unsigned int i = 0; i < al->size(); i++) {
 607            EE res = flat_exp(env, argctx, (*al)[i], nullptr, constants().varTrue);
 608            if (res.r()->type().isPar()) {
 609              if (eval_bool(env, res.r()) == is_conj) {
 610                // this element is irrelevant
 611              } else {
 612                // this element subsumes all other elements
 613                flat_args = {res.r()};
 614                break;
 615              }
 616            } else {
 617              flat_args.emplace_back(res.r());
 618            }
 619          }
 620          GCLock lock;
 621          al_new = new ArrayLit(al->loc(), to_exp_vec(flat_args));
 622          al_new->type(Type::varbool(1));
 623          al_new->flat(true);
 624        }
 625        args_ee[0] = EE(al_new, constants().literalTrue);
 626      } else {
 627        for (unsigned int i = c->argCount(); (i--) != 0U;) {
 628          Ctx argctx = nctx;
 629          if (mixContext) {
 630            if (cid == constants().ids.clause) {
 631              argctx.b = (i == 0 ? +nctx.b : -nctx.b);
 632            } else if (c->arg(i)->type().bt() == Type::BT_BOOL) {
 633              argctx.b = C_MIX;
 634            } else if (c->arg(i)->type().bt() == Type::BT_INT) {
 635              argctx.i = C_MIX;
 636            }
 637          } else if (cid == constants().ids.sum && c->arg(i)->type().bt() == Type::BT_BOOL) {
 638            argctx.b = argctx.i;
 639          }
 640          Expression* tmp = follow_id_to_decl(c->arg(i));
 641          if (auto* vd = tmp->dynamicCast<VarDecl>()) {
 642            tmp = vd->id();
 643          }
 644          CallArgItem cai(env);
 645          args_ee[i] = flat_exp(env, argctx, tmp, nullptr, nullptr);
 646          isPartial |= isfalse(env, args_ee[i].b());
 647        }
 648      }
 649    }
 650    if (isPartial && c->type().isbool() && !c->type().isOpt()) {
 651      ret.b = bind(env, Ctx(), b, constants().literalTrue);
 652      args_ee.resize(1);
 653      args_ee[0] = EE(nullptr, constants().literalFalse);
 654      ret.r = conj(env, r, ctx, args_ee);
 655      return ret;
 656    }
 657
 658    std::vector<KeepAlive> args;
 659    if (decl->e() == nullptr && (cid == constants().ids.exists || cid == constants().ids.clause)) {
 660      std::vector<KeepAlive> pos_alv;
 661      std::vector<KeepAlive> neg_alv;
 662
 663      std::vector<Expression*> pos_stack;
 664      std::vector<Expression*> neg_stack;
 665
 666      auto* al_pos = follow_id(args_ee[0].r())->cast<ArrayLit>();
 667      for (unsigned int i = 0; i < al_pos->size(); i++) {
 668        pos_stack.push_back((*al_pos)[i]);
 669      }
 670      if (cid == constants().ids.clause) {
 671        auto* al_neg = follow_id(args_ee[1].r())->cast<ArrayLit>();
 672        for (unsigned int i = 0; i < al_neg->size(); i++) {
 673          neg_stack.push_back((*al_neg)[i]);
 674        }
 675      }
 676
 677      std::unordered_set<Expression*> seen;
 678
 679      while (!pos_stack.empty() || !neg_stack.empty()) {
 680        while (!pos_stack.empty()) {
 681          Expression* cur = pos_stack.back();
 682          pos_stack.pop_back();
 683          if (cur->isa<Id>() && seen.find(cur) != seen.end()) {
 684            pos_alv.emplace_back(cur);
 685          } else {
 686            seen.insert(cur);
 687            GCLock lock;
 688            if (Call* sc =
 689                    Expression::dynamicCast<Call>(same_call(env, cur, constants().ids.exists))) {
 690              GCLock lock;
 691              ArrayLit* sc_c = eval_array_lit(env, sc->arg(0));
 692              for (unsigned int j = 0; j < sc_c->size(); j++) {
 693                pos_stack.push_back((*sc_c)[j]);
 694              }
 695            } else if (Call* sc = Expression::dynamicCast<Call>(
 696                           same_call(env, cur, constants().ids.clause))) {
 697              GCLock lock;
 698              ArrayLit* sc_c = eval_array_lit(env, sc->arg(0));
 699              for (unsigned int j = 0; j < sc_c->size(); j++) {
 700                pos_stack.push_back((*sc_c)[j]);
 701              }
 702              sc_c = eval_array_lit(env, sc->arg(1));
 703              for (unsigned int j = 0; j < sc_c->size(); j++) {
 704                neg_stack.push_back((*sc_c)[j]);
 705              }
 706            } else {
 707              Call* eq_call =
 708                  Expression::dynamicCast<Call>(same_call(env, cur, constants().ids.bool_eq));
 709              Call* not_call =
 710                  Expression::dynamicCast<Call>(same_call(env, cur, constants().ids.bool_not));
 711              if ((eq_call != nullptr) &&
 712                  Expression::equal(eq_call->arg(1), constants().literalFalse)) {
 713                neg_stack.push_back(eq_call->arg(0));
 714              } else if ((eq_call != nullptr) &&
 715                         Expression::equal(eq_call->arg(0), constants().literalFalse)) {
 716                neg_stack.push_back(eq_call->arg(1));
 717              } else if ((eq_call != nullptr) &&
 718                         Expression::equal(eq_call->arg(1), constants().literalTrue)) {
 719                pos_stack.push_back(eq_call->arg(0));
 720              } else if ((eq_call != nullptr) &&
 721                         Expression::equal(eq_call->arg(0), constants().literalTrue)) {
 722                pos_stack.push_back(eq_call->arg(1));
 723              } else if ((not_call != nullptr) && not_call->argCount() == 1) {
 724                neg_stack.push_back(not_call->arg(0));
 725              } else if (Id* ident = cur->dynamicCast<Id>()) {
 726                if (ident->decl()->ti()->domain() != constants().literalFalse) {
 727                  pos_alv.emplace_back(ident);
 728                }
 729              } else {
 730                pos_alv.emplace_back(cur);
 731              }
 732            }
 733          }
 734        }
 735
 736        while (!neg_stack.empty()) {
 737          GCLock lock;
 738          Expression* cur = neg_stack.back();
 739          neg_stack.pop_back();
 740          if (cur->isa<Id>() && seen.find(cur) != seen.end()) {
 741            neg_alv.emplace_back(cur);
 742          } else {
 743            seen.insert(cur);
 744            if (Call* sc =
 745                    Expression::dynamicCast<Call>(same_call(env, cur, constants().ids.forall))) {
 746              GCLock lock;
 747              ArrayLit* sc_c = eval_array_lit(env, sc->arg(0));
 748              for (unsigned int j = 0; j < sc_c->size(); j++) {
 749                neg_stack.push_back((*sc_c)[j]);
 750              }
 751            } else {
 752              Call* eq_call =
 753                  Expression::dynamicCast<Call>(same_call(env, cur, constants().ids.bool_eq));
 754              Call* not_call =
 755                  Expression::dynamicCast<Call>(same_call(env, cur, constants().ids.bool_not));
 756              if ((eq_call != nullptr) &&
 757                  Expression::equal(eq_call->arg(1), constants().literalFalse)) {
 758                pos_stack.push_back(eq_call->arg(0));
 759              } else if ((eq_call != nullptr) &&
 760                         Expression::equal(eq_call->arg(0), constants().literalFalse)) {
 761                pos_stack.push_back(eq_call->arg(1));
 762              } else if ((eq_call != nullptr) &&
 763                         Expression::equal(eq_call->arg(1), constants().literalTrue)) {
 764                neg_stack.push_back(eq_call->arg(0));
 765              } else if ((eq_call != nullptr) &&
 766                         Expression::equal(eq_call->arg(0), constants().literalTrue)) {
 767                neg_stack.push_back(eq_call->arg(1));
 768              } else if ((not_call != nullptr) && not_call->argCount() == 1) {
 769                pos_stack.push_back(not_call->arg(0));
 770              } else if (Id* ident = cur->dynamicCast<Id>()) {
 771                if (ident->decl()->ti()->domain() != constants().literalTrue) {
 772                  neg_alv.emplace_back(ident);
 773                }
 774              } else {
 775                neg_alv.emplace_back(cur);
 776              }
 777            }
 778          }
 779        }
 780      }
 781
 782      bool subsumed = remove_dups(pos_alv, false);
 783      subsumed = subsumed || remove_dups(neg_alv, true);
 784      subsumed = subsumed || contains_dups(pos_alv, neg_alv);
 785      if (subsumed) {
 786        ret.b = bind(env, Ctx(), b, constants().literalTrue);
 787        ret.r = bind(env, ctx, r, constants().literalTrue);
 788        return ret;
 789      }
 790      if (neg_alv.empty()) {
 791        if (pos_alv.empty()) {
 792          ret.b = bind(env, Ctx(), b, constants().literalTrue);
 793          ret.r = bind(env, ctx, r, constants().literalFalse);
 794          return ret;
 795        }
 796        if (pos_alv.size() == 1) {
 797          ret.b = bind(env, Ctx(), b, constants().literalTrue);
 798          ret.r = bind(env, ctx, r, pos_alv[0]());
 799          return ret;
 800        }
 801        GCLock lock;
 802        auto* nal = new ArrayLit(Location().introduce(), to_exp_vec(pos_alv));
 803        nal->type(Type::varbool(1));
 804        args.emplace_back(nal);
 805        cid = constants().ids.exists;
 806      } else {
 807        if (pos_alv.empty() && neg_alv.size() == 1) {
 808          ret.b = bind(env, Ctx(), b, constants().literalTrue);
 809          Ctx nctx = ctx;
 810          nctx.neg = !nctx.neg;
 811          nctx.b = -nctx.b;
 812          ret.r = bind(env, nctx, r, neg_alv[0]());
 813          return ret;
 814        }
 815        GCLock lock;
 816        auto* pos_al = new ArrayLit(Location().introduce(), to_exp_vec(pos_alv));
 817        pos_al->type(Type::varbool(1));
 818        auto* neg_al = new ArrayLit(Location().introduce(), to_exp_vec(neg_alv));
 819        neg_al->type(Type::varbool(1));
 820        cid = constants().ids.clause;
 821        args.emplace_back(pos_al);
 822        args.emplace_back(neg_al);
 823      }
 824      if (C_ROOT == ctx.b && cid == constants().ids.exists) {
 825        /// Check the special bounds disjunction for SCIP
 826        /// Only in root context
 827        if (!env.model->getFnDecls().boundsDisj.first) {
 828          env.model->getFnDecls().boundsDisj.first = true;
 829          std::vector<Type> bj_t = {Type::parbool(1), Type::parint(1),   Type::varint(1),
 830                                    Type::parbool(1), Type::parfloat(1), Type::varfloat(1)};
 831          GCLock lock;
 832          env.model->getFnDecls().boundsDisj.second =
 833              env.model->matchFn(env, ASTString("bounds_disj"), bj_t, false);
 834        }
 835        /// When the SCIP predicate is declared only
 836        bool fBoundsDisj_Maybe = (nullptr != env.model->getFnDecls().boundsDisj.second);
 837        if (fBoundsDisj_Maybe) {
 838          if (is_totaladd_bounds_disj(env, args[0](), c)) {
 839            ret.b = bind(env, Ctx(), b, constants().literalTrue);
 840            ret.r = bind(env, ctx, r, constants().literalTrue);
 841            return ret;
 842          }
 843        }
 844      }
 845
 846    } else if (decl->e() == nullptr && cid == constants().ids.forall) {
 847      auto* al = follow_id(args_ee[0].r())->cast<ArrayLit>();
 848      std::vector<KeepAlive> alv;
 849      for (unsigned int i = 0; i < al->size(); i++) {
 850        GCLock lock;
 851        if (Call* sc = Expression::dynamicCast<Call>(same_call(env, (*al)[i], cid))) {
 852          GCLock lock;
 853          ArrayLit* sc_c = eval_array_lit(env, sc->arg(0));
 854          for (unsigned int j = 0; j < sc_c->size(); j++) {
 855            alv.emplace_back((*sc_c)[j]);
 856          }
 857        } else {
 858          alv.emplace_back((*al)[i]);
 859        }
 860      }
 861      bool subsumed = remove_dups(alv, true);
 862      if (subsumed) {
 863        ret.b = bind(env, Ctx(), b, constants().literalTrue);
 864        ret.r = bind(env, ctx, r, constants().literalFalse);
 865        return ret;
 866      }
 867      if (alv.empty()) {
 868        ret.b = bind(env, Ctx(), b, constants().literalTrue);
 869        ret.r = bind(env, ctx, r, constants().literalTrue);
 870        return ret;
 871      }
 872      if (alv.size() == 1) {
 873        ret.b = bind(env, Ctx(), b, constants().literalTrue);
 874        ret.r = bind(env, ctx, r, alv[0]());
 875        return ret;
 876      }
 877      GCLock lock;
 878      auto* nal = new ArrayLit(al->loc(), to_exp_vec(alv));
 879      nal->type(al->type());
 880      args.emplace_back(nal);
 881    } else if (decl->e() == nullptr &&
 882               (cid == constants().ids.lin_exp || cid == constants().ids.sum)) {
 883      if (e->type().isint()) {
 884        flatten_linexp_call<IntLit>(env, ctx, nctx, cid, c, ret, b, r, args_ee, args);
 885      } else {
 886        flatten_linexp_call<FloatLit>(env, ctx, nctx, cid, c, ret, b, r, args_ee, args);
 887      }
 888      if (args.empty()) {
 889        return ret;
 890      }
 891    } else {
 892      for (auto& i : args_ee) {
 893        args.emplace_back(i.r());
 894      }
 895    }
 896    bool hadImplementation = (decl->e() != nullptr);
 897    KeepAlive cr;
 898    {
 899      GCLock lock;
 900      std::vector<Expression*> e_args = to_exp_vec(args);
 901      Call* cr_c = new Call(c->loc().introduce(), cid, e_args);
 902      decl = env.model->matchFn(env, cr_c, false);
 903      if (decl == nullptr) {
 904        throw FlatteningError(env, cr_c->loc(), "cannot find matching declaration");
 905      }
 906      cr_c->type(decl->rtype(env, e_args, false));
 907      assert(decl);
 908      cr_c->decl(decl);
 909      cr = cr_c;
 910    }
 911    if (hadImplementation && decl->e() == nullptr &&
 912        (cid == constants().ids.lin_exp || cid == constants().ids.sum)) {
 913      args.clear();
 914      if (e->type().isint()) {
 915        flatten_linexp_call<IntLit>(env, ctx, nctx, cid, cr()->cast<Call>(), ret, b, r, args_ee,
 916                                    args);
 917      } else {
 918        flatten_linexp_call<FloatLit>(env, ctx, nctx, cid, cr()->cast<Call>(), ret, b, r, args_ee,
 919                                      args);
 920      }
 921      if (args.empty()) {
 922        return ret;
 923      }
 924      GCLock lock;
 925      std::vector<Expression*> e_args = to_exp_vec(args);
 926      Call* cr_c = new Call(c->loc().introduce(), cid, e_args);
 927      decl = env.model->matchFn(env, cr_c, false);
 928      if (decl == nullptr) {
 929        throw FlatteningError(env, cr_c->loc(), "cannot find matching declaration");
 930      }
 931      cr_c->type(decl->rtype(env, e_args, false));
 932      assert(decl);
 933      cr_c->decl(decl);
 934      cr = cr_c;
 935    }
 936    auto cit = env.cseMapFind(cr());
 937    if (cit != env.cseMapEnd()) {
 938      if (env.ignorePartial) {
 939        ret.b = bind(env, Ctx(), b, constants().literalTrue);
 940      } else {
 941        args_ee.emplace_back(nullptr, cit->second.b());
 942        ret.b = conj(env, b, Ctx(), args_ee);
 943      }
 944      ret.r = bind(env, ctx, r, cit->second.r());
 945    } else {
 946      for (unsigned int i = 0; i < decl->params().size(); i++) {
 947        if (decl->params()[i]->type().dim() > 0) {
 948          // Check array index sets
 949          auto* al = follow_id(args[i]())->cast<ArrayLit>();
 950          VarDecl* pi = decl->params()[i];
 951          for (unsigned int j = 0; j < pi->ti()->ranges().size(); j++) {
 952            TypeInst* range_ti = pi->ti()->ranges()[j];
 953            if ((range_ti->domain() != nullptr) && !range_ti->domain()->isa<TIId>()) {
 954              GCLock lock;
 955              IntSetVal* isv = eval_intset(env, range_ti->domain());
 956              if (isv->min() != al->min(j) || isv->max() != al->max(j)) {
 957                std::ostringstream oss;
 958                oss << "array index set " << (j + 1) << " of argument " << (i + 1)
 959                    << " does not match declared index set";
 960                throw FlatteningError(env, e->loc(), oss.str());
 961              }
 962            }
 963          }
 964        }
 965        if (Expression* dom = decl->params()[i]->ti()->domain()) {
 966          if (!dom->isa<TIId>()) {
 967            // May have to constrain actual argument
 968            if (args[i]()->type().bt() == Type::BT_INT) {
 969              GCLock lock;
 970              IntSetVal* isv = eval_intset(env, dom);
 971              BinOpType bot;
 972              bool needToConstrain;
 973              if (args[i]()->type().st() == Type::ST_SET) {
 974                bot = BOT_SUBSET;
 975                needToConstrain = true;
 976              } else {
 977                bot = BOT_IN;
 978                if (args[i]()->type().dim() > 0) {
 979                  needToConstrain = true;
 980                } else {
 981                  IntBounds ib = compute_int_bounds(env, args[i]());
 982                  needToConstrain = !ib.valid || isv->size() == 0 || ib.l < isv->min(0) ||
 983                                    ib.u > isv->max(isv->size() - 1);
 984                }
 985              }
 986              if (needToConstrain) {
 987                GCLock lock;
 988                Expression* domconstraint;
 989                if (args[i]()->type().dim() > 0) {
 990                  std::vector<Expression*> domargs(2);
 991                  domargs[0] = args[i]();
 992                  domargs[1] = dom;
 993                  Call* c = new Call(Location().introduce(), "var_dom", domargs);
 994                  c->type(Type::varbool());
 995                  c->decl(env.model->matchFn(env, c, false));
 996                  if (c->decl() == nullptr) {
 997                    throw InternalError("no matching declaration found for var_dom");
 998                  }
 999                  domconstraint = c;
1000                } else {
1001                  domconstraint = new BinOp(Location().introduce(), args[i](), bot, dom);
1002                }
1003                domconstraint->type(args[i]()->type().isPar() ? Type::parbool() : Type::varbool());
1004                if (ctx.b == C_ROOT) {
1005                  (void)flat_exp(env, Ctx(), domconstraint, constants().varTrue,
1006                                 constants().varTrue);
1007                } else {
1008                  EE ee = flat_exp(env, Ctx(), domconstraint, nullptr, constants().varTrue);
1009                  ee.b = ee.r;
1010                  args_ee.push_back(ee);
1011                }
1012              }
1013            } else if (args[i]()->type().bt() == Type::BT_FLOAT) {
1014              GCLock lock;
1015
1016              FloatSetVal* fsv = eval_floatset(env, dom);
1017              bool needToConstrain;
1018              if (args[i]()->type().dim() > 0) {
1019                needToConstrain = true;
1020              } else {
1021                FloatBounds fb = compute_float_bounds(env, args[i]());
1022                needToConstrain = !fb.valid || fsv->size() == 0 || fb.l < fsv->min(0) ||
1023                                  fb.u > fsv->max(fsv->size() - 1);
1024              }
1025
1026              if (needToConstrain) {
1027                GCLock lock;
1028                Expression* domconstraint;
1029                if (args[i]()->type().dim() > 0) {
1030                  std::vector<Expression*> domargs(2);
1031                  domargs[0] = args[i]();
1032                  domargs[1] = dom;
1033                  Call* c = new Call(Location().introduce(), "var_dom", domargs);
1034                  c->type(Type::varbool());
1035                  c->decl(env.model->matchFn(env, c, false));
1036                  if (c->decl() == nullptr) {
1037                    throw InternalError("no matching declaration found for var_dom");
1038                  }
1039                  domconstraint = c;
1040                } else {
1041                  domconstraint = new BinOp(Location().introduce(), args[i](), BOT_IN, dom);
1042                }
1043                domconstraint->type(args[i]()->type().isPar() ? Type::parbool() : Type::varbool());
1044                if (ctx.b == C_ROOT) {
1045                  (void)flat_exp(env, Ctx(), domconstraint, constants().varTrue,
1046                                 constants().varTrue);
1047                } else {
1048                  EE ee = flat_exp(env, Ctx(), domconstraint, nullptr, constants().varTrue);
1049                  ee.b = ee.r;
1050                  args_ee.push_back(ee);
1051                }
1052              }
1053            } else if (args[i]()->type().bt() == Type::BT_BOT) {
1054              // Nothing to be done for empty arrays/sets
1055            } else {
1056              throw EvalError(env, decl->params()[i]->loc(),
1057                              "domain restrictions other than int and float not supported yet");
1058            }
1059          }
1060        }
1061      }
1062      if (cr()->type().isbool() && !cr()->type().isPar() && !cr()->type().isOpt() &&
1063          (ctx.b != C_ROOT || r != constants().varTrue)) {
1064        std::vector<Type> argtypes(args.size());
1065        for (unsigned int i = 0; i < args.size(); i++) {
1066          argtypes[i] = args[i]()->type();
1067        }
1068        argtypes.push_back(Type::varbool());
1069        GCLock lock;
1070        ASTString r_cid = env.reifyId(cid);
1071        FunctionI* reif_decl = env.model->matchFn(env, r_cid, argtypes, false);
1072        if ((reif_decl != nullptr) && (reif_decl->e() != nullptr)) {
1073          add_path_annotation(env, reif_decl->e());
1074          VarDecl* reif_b;
1075          if (r == nullptr || (r != nullptr && r->e() != nullptr)) {
1076            reif_b = new_vardecl(env, Ctx(), new TypeInst(Location().introduce(), Type::varbool()),
1077                                 nullptr, nullptr, nullptr);
1078            add_ctx_ann(reif_b, ctx.b);
1079            if (reif_b->ti()->domain() != nullptr) {
1080              if (reif_b->ti()->domain() == constants().literalTrue) {
1081                bind(env, ctx, r, constants().literalTrue);
1082                r = constants().varTrue;
1083                ctx.b = C_ROOT;
1084                goto call_nonreif;
1085              } else {
1086                std::vector<Expression*> args_e(args.size() + 1);
1087                for (unsigned int i = 0; i < args.size(); i++) {
1088                  args_e[i] = args[i]();
1089                }
1090                args_e[args.size()] = constants().literalFalse;
1091                Call* reif_call = new Call(Location().introduce(), r_cid, args_e);
1092                reif_call->type(Type::varbool());
1093                reif_call->decl(reif_decl);
1094                flat_exp(env, Ctx(), reif_call, constants().varTrue, constants().varTrue);
1095                args_ee.emplace_back(nullptr, constants().literalFalse);
1096                ret.r = conj(env, r, ctx, args_ee);
1097                ret.b = bind(env, ctx, b, constants().literalTrue);
1098                return ret;
1099              }
1100            }
1101          } else {
1102            reif_b = r;
1103          }
1104          // Annotate cr() with get_path()
1105          add_path_annotation(env, cr());
1106          reif_b->e(cr());
1107          if (r != nullptr && r->e() != nullptr) {
1108            Ctx reif_ctx;
1109            reif_ctx.neg = ctx.neg;
1110            bind(env, reif_ctx, r, reif_b->id());
1111          }
1112          env.voAddExp(reif_b);
1113          ret.b = bind(env, Ctx(), b, constants().literalTrue);
1114          args_ee.emplace_back(nullptr, reif_b->id());
1115          ret.r = conj(env, nullptr, ctx, args_ee);
1116          if (!ctx.neg && !cr()->type().isAnn()) {
1117            env.cseMapInsert(cr(), ret);
1118          }
1119          return ret;
1120        }
1121      }
1122    call_nonreif:
1123      if (decl->e() == nullptr ||
1124          (cr()->type().isPar() && !cr()->type().isAnn() && !decl->e()->type().cv())) {
1125        Call* cr_c = cr()->cast<Call>();
1126        /// All builtins are total
1127        std::vector<Type> argt(cr_c->argCount());
1128        for (auto i = static_cast<unsigned int>(argt.size()); (i--) != 0U;) {
1129          argt[i] = cr_c->arg(i)->type();
1130        }
1131        Type callt = decl->rtype(env, argt, false);
1132        if (callt.isPar() && callt.bt() != Type::BT_ANN) {
1133          GCLock lock;
1134          try {
1135            ret.r = bind(env, ctx, r, eval_par(env, cr_c));
1136            ret.b = conj(env, b, Ctx(), args_ee);
1137          } catch (ResultUndefinedError&) {
1138            ret.r = create_dummy_value(env, cr_c->type());
1139            ret.b = bind(env, Ctx(), b, constants().literalFalse);
1140            return ret;
1141          }
1142          // Do not insert into map, since par results will quickly become
1143          // garbage anyway and then disappear from the map
1144        } else if (decl->builtins.e != nullptr) {
1145          KeepAlive callres;
1146          {
1147            GCLock lock;
1148            callres = decl->builtins.e(env, cr_c);
1149          }
1150          EE res = flat_exp(env, ctx, callres(), r, b);
1151          args_ee.push_back(res);
1152          ret.b = conj(env, b, Ctx(), args_ee);
1153          add_path_annotation(env, res.r());
1154          ret.r = bind(env, ctx, r, res.r());
1155          if (!ctx.neg && !cr_c->type().isAnn()) {
1156            env.cseMapInsert(cr_c, ret);
1157          }
1158        } else {
1159          GCLock lock;
1160          ret.b = conj(env, b, Ctx(), args_ee);
1161          add_path_annotation(env, cr_c);
1162          ret.r = bind(env, ctx, r, cr_c);
1163          if (!ctx.neg && !cr_c->type().isAnn()) {
1164            env.cseMapInsert(cr_c, ret);
1165          }
1166        }
1167      } else {
1168        std::vector<KeepAlive> previousParameters(decl->params().size());
1169        for (unsigned int i = decl->params().size(); (i--) != 0U;) {
1170          VarDecl* vd = decl->params()[i];
1171          previousParameters[i] = vd->e();
1172          vd->flat(vd);
1173          vd->e(args[i]());
1174        }
1175
1176        if (decl->e()->type().isbool() && !decl->e()->type().isOpt()) {
1177          ret.b = bind(env, Ctx(), b, constants().literalTrue);
1178          if (ctx.b == C_ROOT && r == constants().varTrue) {
1179            (void)flat_exp(env, Ctx(), decl->e(), r, constants().varTrue);
1180          } else {
1181            Ctx nctx;
1182            if (!is_total(decl)) {
1183              nctx = ctx;
1184              nctx.neg = false;
1185            }
1186            EE ee = flat_exp(env, nctx, decl->e(), nullptr, constants().varTrue);
1187            ee.b = ee.r;
1188            args_ee.push_back(ee);
1189          }
1190          ret.r = conj(env, r, ctx, args_ee);
1191        } else {
1192          if (is_total(decl)) {
1193            EE ee = flat_exp(env, Ctx(), decl->e(), r, constants().varTrue);
1194            ret.r = bind(env, ctx, r, ee.r());
1195          } else {
1196            ret = flat_exp(env, ctx, decl->e(), r, nullptr);
1197            args_ee.push_back(ret);
1198            if (decl->e()->type().dim() > 0) {
1199              auto* al = follow_id(ret.r())->cast<ArrayLit>();
1200              assert(al->dims() == decl->e()->type().dim());
1201              for (unsigned int i = 0; i < decl->ti()->ranges().size(); i++) {
1202                if ((decl->ti()->ranges()[i]->domain() != nullptr) &&
1203                    !decl->ti()->ranges()[i]->domain()->isa<TIId>()) {
1204                  GCLock lock;
1205                  IntSetVal* isv = eval_intset(env, decl->ti()->ranges()[i]->domain());
1206                  if (al->min(i) != isv->min() || al->max(i) != isv->max()) {
1207                    EE ee;
1208                    ee.b = constants().literalFalse;
1209                    args_ee.push_back(ee);
1210                  }
1211                }
1212              }
1213            }
1214            if ((decl->ti()->domain() != nullptr) && !decl->ti()->domain()->isa<TIId>()) {
1215              BinOpType bot;
1216              if (ret.r()->type().st() == Type::ST_SET) {
1217                bot = BOT_SUBSET;
1218              } else {
1219                bot = BOT_IN;
1220              }
1221
1222              KeepAlive domconstraint;
1223              if (decl->e()->type().dim() > 0) {
1224                GCLock lock;
1225                std::vector<Expression*> domargs(2);
1226                domargs[0] = ret.r();
1227                domargs[1] = decl->ti()->domain();
1228                Call* c = new Call(Location().introduce(), "var_dom", domargs);
1229                c->type(Type::varbool());
1230                c->decl(env.model->matchFn(env, c, false));
1231                if (c->decl() == nullptr) {
1232                  throw InternalError("no matching declaration found for var_dom");
1233                }
1234                domconstraint = c;
1235              } else {
1236                GCLock lock;
1237                domconstraint =
1238                    new BinOp(Location().introduce(), ret.r(), bot, decl->ti()->domain());
1239              }
1240              domconstraint()->type(ret.r()->type().isPar() ? Type::parbool() : Type::varbool());
1241              if (ctx.b == C_ROOT) {
1242                (void)flat_exp(env, Ctx(), domconstraint(), constants().varTrue,
1243                               constants().varTrue);
1244              } else {
1245                EE ee = flat_exp(env, Ctx(), domconstraint(), nullptr, constants().varTrue);
1246                ee.b = ee.r;
1247                args_ee.push_back(ee);
1248              }
1249            }
1250          }
1251          ret.b = conj(env, b, Ctx(), args_ee);
1252        }
1253        if (!ctx.neg && !cr()->type().isAnn()) {
1254          env.cseMapInsert(cr(), ret);
1255        }
1256
1257        // Restore previous mapping
1258        for (unsigned int i = decl->params().size(); (i--) != 0U;) {
1259          VarDecl* vd = decl->params()[i];
1260          vd->e(previousParameters[i]());
1261          vd->flat(vd->e() != nullptr ? vd : nullptr);
1262        }
1263      }
1264    }
1265  }
1266  if (cid == "mzn_reverse_map_var") {
1267    env.inReverseMapVar = false;
1268  }
1269  return ret;
1270}
1271}  // namespace MiniZinc