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