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_comp(EnvI& env, const Ctx& ctx, Expression* e, VarDecl* r, VarDecl* b) {
17 CallStackItem _csi(env, e);
18 EE ret;
19 auto* c = e->cast<Comprehension>();
20 KeepAlive c_ka(c);
21
22 bool isvarset = false;
23 if (c->set()) {
24 for (int i = 0; i < c->numberOfGenerators(); i++) {
25 Expression* g_in = c->in(i);
26 if (g_in != nullptr) {
27 const Type& ty_in = g_in->type();
28 if (ty_in == Type::varsetint()) {
29 isvarset = true;
30 break;
31 }
32 if (c->where(i) != nullptr) {
33 if (c->where(i)->type() == Type::varbool()) {
34 isvarset = true;
35 break;
36 }
37 }
38 }
39 }
40 }
41
42 if (c->type().isOpt() || isvarset) {
43 std::vector<Expression*> in(c->numberOfGenerators());
44 std::vector<Expression*> orig_where(c->numberOfGenerators());
45 std::vector<Expression*> where;
46 GCLock lock;
47 for (int i = 0; i < c->numberOfGenerators(); i++) {
48 if (c->in(i) == nullptr) {
49 in[i] = nullptr;
50 orig_where[i] = c->where(i);
51 } else {
52 if (c->in(i)->type().isvar() && c->in(i)->type().dim() == 0) {
53 std::vector<Expression*> args(1);
54 args[0] = c->in(i);
55 Call* ub = new Call(Location().introduce(), "ub", args);
56 ub->type(Type::parsetint());
57 ub->decl(env.model->matchFn(env, ub, false));
58 in[i] = ub;
59 for (int j = 0; j < c->numberOfDecls(i); j++) {
60 auto* bo = new BinOp(Location().introduce(), c->decl(i, j)->id(), BOT_IN, c->in(i));
61 bo->type(Type::varbool());
62 where.push_back(bo);
63 }
64 } else {
65 in[i] = c->in(i);
66 }
67 if ((c->where(i) != nullptr) && c->where(i)->type().isvar()) {
68 // This is a generalised where clause. Split into par and var part.
69 // The par parts can remain in where clause. The var parts are translated
70 // into optionality constraints.
71 if (c->where(i)->isa<BinOp>() && c->where(i)->cast<BinOp>()->op() == BOT_AND) {
72 std::vector<Expression*> parWhere;
73 std::vector<BinOp*> todo;
74 todo.push_back(c->where(i)->cast<BinOp>());
75 while (!todo.empty()) {
76 BinOp* bo = todo.back();
77 todo.pop_back();
78 if (bo->rhs()->type().isPar()) {
79 parWhere.push_back(bo->rhs());
80 } else if (bo->rhs()->isa<BinOp>() && bo->rhs()->cast<BinOp>()->op() == BOT_AND) {
81 todo.push_back(bo->rhs()->cast<BinOp>());
82 } else {
83 where.push_back(bo->rhs());
84 }
85 if (bo->lhs()->type().isPar()) {
86 parWhere.push_back(bo->lhs());
87 } else if (bo->lhs()->isa<BinOp>() && bo->lhs()->cast<BinOp>()->op() == BOT_AND) {
88 todo.push_back(bo->lhs()->cast<BinOp>());
89 } else {
90 where.push_back(bo->lhs());
91 }
92 }
93 switch (parWhere.size()) {
94 case 0:
95 orig_where[i] = nullptr;
96 break;
97 case 1:
98 orig_where[i] = parWhere[0];
99 break;
100 case 2:
101 orig_where[i] = new BinOp(c->where(i)->loc(), parWhere[0], BOT_AND, parWhere[1]);
102 orig_where[i]->type(Type::parbool());
103 break;
104 default: {
105 auto* parWhereAl = new ArrayLit(c->where(i)->loc(), parWhere);
106 parWhereAl->type(Type::parbool(1));
107 Call* forall = new Call(c->where(i)->loc(), constants().ids.forall, {parWhereAl});
108 forall->type(Type::parbool());
109 forall->decl(env.model->matchFn(env, forall, false));
110 orig_where[i] = forall;
111 break;
112 }
113 }
114 } else {
115 orig_where[i] = nullptr;
116 where.push_back(c->where(i));
117 }
118 } else {
119 orig_where[i] = c->where(i);
120 }
121 }
122 }
123 if (!where.empty()) {
124 Generators gs;
125 for (int i = 0; i < c->numberOfGenerators(); i++) {
126 std::vector<VarDecl*> vds(c->numberOfDecls(i));
127 for (int j = 0; j < c->numberOfDecls(i); j++) {
128 vds[j] = c->decl(i, j);
129 }
130 gs.g.emplace_back(vds, in[i], orig_where[i]);
131 }
132 Expression* cond;
133 if (where.size() > 1) {
134 auto* al = new ArrayLit(Location().introduce(), where);
135 al->type(Type::varbool(1));
136 std::vector<Expression*> args(1);
137 args[0] = al;
138 Call* forall = new Call(Location().introduce(), constants().ids.forall, args);
139 forall->type(Type::varbool());
140 forall->decl(env.model->matchFn(env, forall, false));
141 cond = forall;
142 } else {
143 cond = where[0];
144 }
145
146 Expression* new_e;
147
148 Call* surround = env.surroundingCall();
149
150 Type ntype = c->type();
151 if ((surround != nullptr) && surround->id() == constants().ids.forall) {
152 new_e = new BinOp(Location().introduce(), cond, BOT_IMPL, c->e());
153 new_e->type(Type::varbool());
154 ntype.ot(Type::OT_PRESENT);
155 } else if ((surround != nullptr) && surround->id() == constants().ids.exists) {
156 new_e = new BinOp(Location().introduce(), cond, BOT_AND, c->e());
157 new_e->type(Type::varbool());
158 ntype.ot(Type::OT_PRESENT);
159 } else if ((surround != nullptr) && surround->id() == constants().ids.sum) {
160 ITE* if_b_else_zero = new ITE(c->loc().introduce(), {cond, c->e()}, IntLit::a(0));
161 Type tt;
162 tt = c->e()->type();
163 tt.ti(Type::TI_VAR);
164 tt.ot(Type::OT_PRESENT);
165 if_b_else_zero->type(tt);
166 new_e = if_b_else_zero;
167 ntype.ot(Type::OT_PRESENT);
168 } else {
169 ITE* if_b_else_absent = new ITE(c->loc().introduce(), {cond, c->e()}, constants().absent);
170 Type tt;
171 tt = c->e()->type();
172 tt.ti(Type::TI_VAR);
173 tt.ot(Type::OT_OPTIONAL);
174 if_b_else_absent->type(tt);
175 new_e = if_b_else_absent;
176 }
177 auto* nc = new Comprehension(c->loc(), new_e, gs, c->set());
178 nc->type(ntype);
179 c = nc;
180 c_ka = c;
181 }
182 }
183
184 class EvalF : public EvalBase {
185 public:
186 Ctx ctx;
187 EvalF(const Ctx& ctx0) : ctx(ctx0) {}
188 typedef EE ArrayVal;
189 EE e(EnvI& env, Expression* e0) const {
190 VarDecl* b = ctx.b == C_ROOT ? constants().varTrue : nullptr;
191 VarDecl* r = (ctx.b == C_ROOT && e0->type().isbool() && !e0->type().isOpt())
192 ? constants().varTrue
193 : nullptr;
194 return flat_exp(env, ctx, e0, r, b);
195 }
196 static Expression* flatten(EnvI& env, Expression* e0) {
197 return flat_exp(env, Ctx(), e0, nullptr, constants().varTrue).r();
198 }
199 } _evalf(ctx);
200 std::vector<EE> elems_ee;
201 bool wasUndefined = false;
202 try {
203 elems_ee = eval_comp<EvalF>(env, _evalf, c);
204 } catch (ResultUndefinedError&) {
205 wasUndefined = true;
206 }
207 std::vector<Expression*> elems(elems_ee.size());
208 Type elemType = Type::bot();
209 bool allPar = true;
210 bool someOpt = false;
211 for (auto i = static_cast<unsigned int>(elems.size()); (i--) != 0U;) {
212 elems[i] = elems_ee[i].r();
213 if (elemType == Type::bot()) {
214 elemType = elems[i]->type();
215 }
216 if (!elems[i]->type().isPar()) {
217 allPar = false;
218 }
219 if (elems[i]->type().isOpt()) {
220 someOpt = true;
221 }
222 }
223 if (elemType.isbot()) {
224 elemType = c->type();
225 elemType.ti(Type::TI_PAR);
226 }
227 if (!allPar) {
228 elemType.ti(Type::TI_VAR);
229 }
230 if (someOpt) {
231 elemType.ot(Type::OT_OPTIONAL);
232 }
233 if (c->set()) {
234 elemType.st(Type::ST_SET);
235 } else {
236 elemType.dim(c->type().dim());
237 }
238 KeepAlive ka;
239 {
240 GCLock lock;
241 if (c->set()) {
242 if (c->type().isPar() && allPar) {
243 auto* sl = new SetLit(c->loc(), elems);
244 sl->type(elemType);
245 Expression* slr = eval_par(env, sl);
246 slr->type(elemType);
247 ka = slr;
248 } else {
249 auto* alr = new ArrayLit(Location().introduce(), elems);
250 elemType.st(Type::ST_PLAIN);
251 elemType.dim(1);
252 alr->type(elemType);
253 alr->flat(true);
254 Call* a2s = new Call(Location().introduce(), "array2set", {alr});
255 a2s->decl(env.model->matchFn(env, a2s, false));
256 a2s->type(a2s->decl()->rtype(env, {alr}, false));
257 EE ee = flat_exp(env, Ctx(), a2s, nullptr, constants().varTrue);
258 ka = ee.r();
259 }
260 } else {
261 auto* alr = new ArrayLit(Location().introduce(), elems);
262 alr->type(elemType);
263 alr->flat(true);
264 ka = alr;
265 }
266 }
267 assert(!ka()->type().isbot());
268 if (wasUndefined) {
269 ret.b = bind(env, Ctx(), b, constants().literalFalse);
270 } else {
271 ret.b = conj(env, b, Ctx(), elems_ee);
272 }
273 ret.r = bind(env, Ctx(), r, ka());
274 return ret;
275}
276
277} // namespace MiniZinc