this repo has no description
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_id(EnvI& env, const Ctx& ctx, Expression* e, VarDecl* r, VarDecl* b,
17 bool doNotFollowChains) {
18 CallStackItem _csi(env, e);
19 EE ret;
20 Id* id = e->cast<Id>();
21 if (id->decl() == nullptr) {
22 if (id->type().isAnn()) {
23 ret.b = bind(env, Ctx(), b, constants().literalTrue);
24 ret.r = bind(env, ctx, r, e);
25 return ret;
26 }
27 throw FlatteningError(env, e->loc(), "undefined identifier");
28 }
29 if (!doNotFollowChains) {
30 Expression* id_f = follow_id_to_decl(id);
31 if (id_f == constants().absent) {
32 ret.b = bind(env, Ctx(), b, constants().literalTrue);
33 ret.r = bind(env, ctx, r, id_f);
34 } else {
35 id = id_f->cast<VarDecl>()->id();
36 }
37 }
38 if (ctx.neg && id->type().dim() > 0) {
39 if (id->type().dim() > 1) {
40 throw InternalError("multi-dim arrays in negative positions not supported yet");
41 }
42 KeepAlive ka;
43 {
44 GCLock lock;
45 std::vector<VarDecl*> gen_id(1);
46 gen_id[0] = new VarDecl(id->loc(), new TypeInst(id->loc(), Type::parint()), env.genId(),
47 IntLit::a(0));
48
49 /// TODO: support arbitrary dimensions
50 std::vector<Expression*> idxsetargs(1);
51 idxsetargs[0] = id;
52 Call* idxset = new Call(id->loc().introduce(), "index_set", idxsetargs);
53 idxset->decl(env.model->matchFn(env, idxset, false));
54 idxset->type(idxset->decl()->rtype(env, idxsetargs, false));
55 Generator gen(gen_id, idxset, nullptr);
56 std::vector<Expression*> idx(1);
57 Generators gens;
58 gens.g.push_back(gen);
59 UnOp* aanot = new UnOp(id->loc(), UOT_NOT, nullptr);
60 auto* cp = new Comprehension(id->loc(), aanot, gens, false);
61 Id* bodyidx = cp->decl(0, 0)->id();
62 idx[0] = bodyidx;
63 auto* aa = new ArrayAccess(id->loc(), id, idx);
64 aanot->e(aa);
65 Type tt = id->type();
66 tt.dim(0);
67 aa->type(tt);
68 aanot->type(aa->type());
69 cp->type(id->type());
70 ka = cp;
71 }
72 Ctx nctx = ctx;
73 nctx.neg = false;
74 ret = flat_exp(env, nctx, ka(), r, b);
75 } else {
76 GCLock lock;
77 VarDecl* vd = id->decl()->flat();
78 Expression* rete = nullptr;
79 if (vd == nullptr) {
80 if (id->decl()->e() == nullptr || id->decl()->e()->type().isAnn() ||
81 id->decl()->e()->type().isvar() || id->decl()->e()->type().cv() ||
82 id->decl()->e()->type().dim() > 0) {
83 // New top-level id, need to copy into env.m
84 vd = flat_exp(env, Ctx(), id->decl(), nullptr, constants().varTrue).r()->cast<Id>()->decl();
85 } else {
86 vd = id->decl();
87 }
88 }
89 ret.b = bind(env, Ctx(), b, constants().literalTrue);
90 if (vd->e() != nullptr) {
91 if (vd->e()->type().isPar() && vd->e()->type().dim() == 0) {
92 rete = eval_par(env, vd->e());
93 if (vd->toplevel() && (vd->ti()->domain() != nullptr) && !vd->ti()->computedDomain()) {
94 // need to check if domain includes RHS value
95 if (vd->type() == Type::varbool()) {
96 if (!Expression::equal(rete, vd->ti()->domain())) {
97 env.fail();
98 }
99 vd->ti()->domain(rete);
100 } else if (vd->type() == Type::varint()) {
101 IntSetVal* isv = eval_intset(env, vd->ti()->domain());
102 IntVal v = eval_int(env, rete);
103 if (!isv->contains(v)) {
104 env.fail();
105 }
106 vd->ti()->domain(new SetLit(Location().introduce(), IntSetVal::a(v, v)));
107 } else if (vd->type() == Type::varfloat()) {
108 FloatSetVal* fsv = eval_floatset(env, vd->ti()->domain());
109 FloatVal v = eval_float(env, rete);
110 if (!fsv->contains(v)) {
111 env.fail();
112 }
113 vd->ti()->domain(new SetLit(Location().introduce(), FloatSetVal::a(v, v)));
114 } else if (vd->type() == Type::varsetint()) {
115 IntSetVal* isv = eval_intset(env, vd->ti()->domain());
116 IntSetVal* v = eval_intset(env, rete);
117 IntSetRanges isv_r(isv);
118 IntSetRanges v_r(v);
119 if (!Ranges::subset(v_r, isv_r)) {
120 env.fail();
121 }
122 vd->ti()->domain(new SetLit(Location().introduce(), v));
123 }
124 // If we made it to here, the new domain is equal to the RHS
125 vd->ti()->setComputedDomain(true);
126 }
127 } else if (vd->e()->isa<Id>()) {
128 rete = vd->e();
129 }
130 } else if (vd->ti()->ranges().size() == 0 && (vd->ti()->domain() != nullptr) &&
131 vd->type().st() == Type::ST_PLAIN && vd->type().ot() == Type::OT_PRESENT) {
132 if (vd->type().bt() == Type::BT_BOOL) {
133 rete = vd->ti()->domain();
134 } else if (vd->type().bt() == Type::BT_INT && vd->ti()->domain()->isa<SetLit>() &&
135 (vd->ti()->domain()->cast<SetLit>()->isv() != nullptr) &&
136 vd->ti()->domain()->cast<SetLit>()->isv()->card() == 1) {
137 rete = IntLit::a(vd->ti()->domain()->cast<SetLit>()->isv()->min());
138 }
139 } else if (vd->ti()->ranges().size() > 0) {
140 // create fresh variables and array literal
141 std::vector<std::pair<int, int> > dims;
142 IntVal asize = 1;
143 for (unsigned int i = 0; i < vd->ti()->ranges().size(); i++) {
144 TypeInst* ti = vd->ti()->ranges()[i];
145 if (ti->domain() == nullptr) {
146 throw FlatteningError(env, ti->loc(), "array dimensions unknown");
147 }
148 IntSetVal* isv = eval_intset(env, ti->domain());
149 if (isv->size() == 0) {
150 dims.emplace_back(1, 0);
151 asize = 0;
152 } else {
153 if (isv->size() != 1) {
154 throw FlatteningError(env, ti->loc(), "invalid array index set");
155 }
156 asize *= (isv->max(0) - isv->min(0) + 1);
157 dims.emplace_back(static_cast<int>(isv->min(0).toInt()),
158 static_cast<int>(isv->max(0).toInt()));
159 }
160 }
161 Type tt = vd->ti()->type();
162 tt.dim(0);
163
164 if (asize > Constants::max_array_size) {
165 std::ostringstream oss;
166 oss << "array size (" << asize << ") exceeds maximum allowed size ("
167 << Constants::max_array_size << ")";
168 throw FlatteningError(env, vd->loc(), oss.str());
169 }
170
171 std::vector<Expression*> elems(static_cast<int>(asize.toInt()));
172 for (int i = 0; i < static_cast<int>(asize.toInt()); i++) {
173 CallStackItem csi(env, IntLit::a(i));
174 auto* vti = new TypeInst(Location().introduce(), tt, vd->ti()->domain());
175 VarDecl* nvd = new_vardecl(env, Ctx(), vti, nullptr, vd, nullptr);
176 elems[i] = nvd->id();
177 }
178 // After introducing variables for each array element, the original domain can be
179 // set to "computed" (since it is a consequence of the individual variable domains)
180 vd->ti()->setComputedDomain(true);
181
182 auto* al = new ArrayLit(Location().introduce(), elems, dims);
183 al->type(vd->type());
184 vd->e(al);
185 env.voAddExp(vd);
186 EE ee;
187 ee.r = vd;
188 env.cseMapInsert(vd->e(), ee);
189 }
190 if (rete == nullptr) {
191 if (!vd->toplevel()) {
192 // create new VarDecl in toplevel, if decl doesnt exist yet
193 auto it = env.cseMapFind(vd->e());
194 if (it == env.cseMapEnd()) {
195 Expression* vde = follow_id(vd->e());
196 ArrayLit* vdea = vde != nullptr ? vde->dynamicCast<ArrayLit>() : nullptr;
197 if ((vdea != nullptr) && vdea->size() == 0) {
198 // Do not create names for empty arrays but return array literal directly
199 rete = vdea;
200 } else {
201 VarDecl* nvd = new_vardecl(env, ctx, eval_typeinst(env, ctx, vd), nullptr, vd, nullptr);
202
203 if (vd->e() != nullptr) {
204 (void)flat_exp(env, Ctx(), vd->e(), nvd, constants().varTrue);
205 }
206 vd = nvd;
207 EE ee(vd, nullptr);
208 if (vd->e() != nullptr) {
209 env.cseMapInsert(vd->e(), ee);
210 }
211 }
212 } else {
213 if (it->second.r()->isa<VarDecl>()) {
214 vd = it->second.r()->cast<VarDecl>();
215 } else {
216 rete = it->second.r();
217 }
218 }
219 }
220 if (rete == nullptr) {
221 if (id->type().bt() == Type::BT_ANN && (vd->e() != nullptr)) {
222 rete = vd->e();
223 } else {
224 auto* vda = vd->dynamicCast<ArrayLit>();
225 if ((vda != nullptr) && vda->size() == 0) {
226 // Do not create names for empty arrays but return array literal directly
227 rete = vda;
228 } else {
229 rete = vd->id();
230 }
231 }
232 }
233 }
234 ret.r = bind(env, ctx, r, rete);
235 }
236 return ret;
237}
238
239EE flatten_id(EnvI& env, const Ctx& ctx, Expression* e, VarDecl* r, VarDecl* b) {
240 return flatten_id(env, ctx, e, r, b, false);
241}
242
243} // namespace MiniZinc