this repo has no description
dekker.one
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
16EE flatten_let(EnvI& env, const Ctx& ctx, Expression* e, VarDecl* r, VarDecl* b) {
17 CallStackItem _csi(env, e);
18 EE ret;
19 Let* let = e->cast<Let>();
20 std::vector<EE> cs;
21 std::vector<KeepAlive> flatmap;
22 let->pushbindings();
23 for (unsigned int i = 0; i < let->let().size(); i++) {
24 Expression* le = let->let()[i];
25 if (auto* vd = le->dynamicCast<VarDecl>()) {
26 Expression* let_e = nullptr;
27 if (vd->e() != nullptr) {
28 Ctx nctx = ctx;
29 nctx.neg = false;
30 if (vd->e()->type().bt() == Type::BT_BOOL) {
31 nctx.b = C_MIX;
32 }
33
34 EE ee = flat_exp(env, nctx, vd->e(), nullptr, nullptr);
35 let_e = ee.r();
36 cs.push_back(ee);
37 if (vd->ti()->domain() != nullptr) {
38 GCLock lock;
39 std::vector<Expression*> domargs(2);
40 domargs[0] = ee.r();
41 if (vd->ti()->type().isfloat()) {
42 FloatSetVal* fsv = eval_floatset(env, vd->ti()->domain());
43 if (fsv->size() == 1) {
44 domargs[1] = FloatLit::a(fsv->min());
45 domargs.push_back(FloatLit::a(fsv->max()));
46 } else {
47 domargs[1] = vd->ti()->domain();
48 }
49 } else {
50 domargs[1] = vd->ti()->domain();
51 }
52 Call* c = new Call(vd->ti()->loc().introduce(), "var_dom", domargs);
53 c->type(Type::varbool());
54 c->decl(env.model->matchFn(env, c, false));
55 if (c->decl() == nullptr) {
56 throw InternalError("no matching declaration found for var_dom");
57 }
58 VarDecl* b_b = (nctx.b == C_ROOT && b == constants().varTrue) ? b : nullptr;
59 VarDecl* r_r = (nctx.b == C_ROOT && b == constants().varTrue) ? b : nullptr;
60 ee = flat_exp(env, nctx, c, r_r, b_b);
61 cs.push_back(ee);
62 ee.b = ee.r;
63 cs.push_back(ee);
64 }
65 if (vd->type().dim() > 0) {
66 check_index_sets(env, vd, let_e);
67 }
68 } else {
69 if ((ctx.b == C_NEG || ctx.b == C_MIX) &&
70 !vd->ann().contains(constants().ann.promise_total)) {
71 CallStackItem csi_vd(env, vd);
72 throw FlatteningError(env, vd->loc(), "free variable in non-positive context");
73 }
74 CallStackItem csi_vd(env, vd);
75 GCLock lock;
76 TypeInst* ti = eval_typeinst(env, ctx, vd);
77 VarDecl* nvd = new_vardecl(env, ctx, ti, nullptr, vd, nullptr);
78 let_e = nvd->id();
79 }
80 vd->e(let_e);
81 flatmap.emplace_back(vd->flat());
82 if (Id* id = Expression::dynamicCast<Id>(let_e)) {
83 vd->flat(id->decl());
84 } else {
85 vd->flat(vd);
86 }
87 } else {
88 if (ctx.b == C_ROOT || le->ann().contains(constants().ann.promise_total)) {
89 (void)flat_exp(env, Ctx(), le, constants().varTrue, constants().varTrue);
90 } else {
91 EE ee = flat_exp(env, ctx, le, nullptr, constants().varTrue);
92 ee.b = ee.r;
93 cs.push_back(ee);
94 }
95 }
96 }
97 if (r == constants().varTrue && ctx.b == C_ROOT && !ctx.neg) {
98 ret.b = bind(env, Ctx(), b, constants().literalTrue);
99 (void)flat_exp(env, ctx, let->in(), r, b);
100 ret.r = conj(env, r, Ctx(), cs);
101 } else {
102 Ctx nctx = ctx;
103 nctx.neg = false;
104 VarDecl* bb = b;
105 for (EE& ee : cs) {
106 if (ee.b() != constants().literalTrue) {
107 bb = nullptr;
108 break;
109 }
110 }
111 EE ee = flat_exp(env, nctx, let->in(), nullptr, bb);
112 if (let->type().isbool() && !let->type().isOpt()) {
113 ee.b = ee.r;
114 cs.push_back(ee);
115 ret.r = conj(env, r, ctx, cs);
116 ret.b = bind(env, Ctx(), b, constants().literalTrue);
117 } else {
118 cs.push_back(ee);
119 ret.r = bind(env, Ctx(), r, ee.r());
120 ret.b = conj(env, b, Ctx(), cs);
121 }
122 }
123 let->popbindings();
124 // Restore previous mapping
125 for (unsigned int i = 0; i < let->let().size(); i++) {
126 if (auto* vd = let->let()[i]->dynamicCast<VarDecl>()) {
127 vd->flat(Expression::cast<VarDecl>(flatmap.back()()));
128 flatmap.pop_back();
129 }
130 }
131 return ret;
132}
133} // namespace MiniZinc