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