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/eval_par.hh>
13#include <minizinc/solver_instance_base.hh>
14
15#ifdef _MSC_VER
16#define _CRT_SECURE_NO_WARNINGS
17#endif
18
19namespace MiniZinc {
20
21SolverInstanceBase::Status SolverInstanceBase::solve() { return SolverInstance__ERROR; }
22
23void SolverInstanceBase::reset() { assert(false); }
24
25void SolverInstanceBase::resetWithConstraints(Model::iterator begin, Model::iterator end) {
26 assert(false);
27}
28
29void SolverInstanceBase::processPermanentConstraints(Model::iterator begin, Model::iterator end) {
30 assert(false);
31}
32
33void Registry::add(const ASTString name, poster p) { _registry.insert(std::make_pair(name, p)); }
34void Registry::add(const std::string& name, poster p) {
35 GCLock lock;
36 ASTString str(name);
37 return add(str, p);
38}
39void Registry::post(Call* c) {
40 auto it = _registry.find(c->id());
41 if (it == _registry.end()) {
42 std::ostringstream ss;
43 ss << "Error: solver backend cannot handle constraint: " << c->id();
44 throw InternalError(ss.str());
45 }
46 it->second(_base, c);
47}
48
49void SolverInstanceBase::printSolution() {
50 std::ostringstream oss;
51
52 if (_options->printStatistics) {
53 printStatistics(); // Insert stats before sol separator
54 }
55 if (nullptr == _pS2Out) {
56 getEnv()->evalOutput(std::cout, std::cerr); // deprecated
57 std::cout << oss.str();
58 if ((!oss.str().empty()) && '\n' != oss.str().back()) {
59 std::cout << '\n';
60 }
61 std::cout << "----------" << std::endl;
62 } else {
63 getSolns2Out()->evalOutput(oss.str());
64 }
65}
66
67void SolverInstanceBase2::printSolution() {
68 GCLock lock;
69 assignSolutionToOutput();
70 SolverInstanceBase::printSolution();
71}
72
73// void
74// SolverInstanceBase::assignSolutionToOutput() {
75// for (VarDeclIterator it = getEnv()->output()->vardecls().begin(); it !=
76// getEnv()->output()->vardecls().end(); ++it) {
77// if (it->e()->e() == NULL) {
78// it->e()->e(getSolutionValue(it->e()->id()));
79// }
80// }
81// }
82
83void SolverInstanceBase2::assignSolutionToOutput() {
84 GCLock lock;
85
86 MZN_ASSERT_HARD_MSG(
87 nullptr != _pS2Out,
88 "Setup a Solns2Out object to use default solution extraction/reporting procs");
89
90 if (_varsWithOutput.empty()) {
91 for (VarDeclIterator it = getEnv()->flat()->vardecls().begin();
92 it != getEnv()->flat()->vardecls().end(); ++it) {
93 if (!it->removed()) {
94 VarDecl* vd = it->e();
95 if (!vd->ann().isEmpty()) {
96 if (vd->ann().containsCall(constants().ann.output_array.aststr()) ||
97 vd->ann().contains(constants().ann.output_var)) {
98 _varsWithOutput.push_back(vd);
99 }
100 }
101 }
102 }
103 }
104
105 _pS2Out->declNewOutput(); // Even for empty output decl
106
107 // iterate over set of ids that have an output annotation && obtain their right hand side from the
108 // flat model
109 for (auto* vd : _varsWithOutput) {
110 // std::cout << "DEBUG: Looking at var-decl with output-annotation: " << *vd << std::endl;
111 if (Call* output_array_ann = Expression::dynamicCast<Call>(
112 get_annotation(vd->ann(), constants().ann.output_array.aststr()))) {
113 assert(vd->e());
114
115 if (auto* al = vd->e()->dynamicCast<ArrayLit>()) {
116 std::vector<Expression*> array_elems;
117 ArrayLit& array = *al;
118 for (unsigned int j = 0; j < array.size(); j++) {
119 if (Id* id = array[j]->dynamicCast<Id>()) {
120 // std::cout << "DEBUG: getting solution value from " << *id << " : " << id->v() <<
121 // std::endl;
122 array_elems.push_back(getSolutionValue(id));
123 } else if (auto* floatLit = array[j]->dynamicCast<FloatLit>()) {
124 array_elems.push_back(floatLit);
125 } else if (auto* intLit = array[j]->dynamicCast<IntLit>()) {
126 array_elems.push_back(intLit);
127 } else if (auto* boolLit = array[j]->dynamicCast<BoolLit>()) {
128 array_elems.push_back(boolLit);
129 } else if (auto* setLit = array[j]->dynamicCast<SetLit>()) {
130 array_elems.push_back(setLit);
131 } else if (auto* strLit = array[j]->dynamicCast<StringLit>()) {
132 array_elems.push_back(strLit);
133 } else {
134 std::ostringstream oss;
135 oss << "Error: array element " << *array[j] << " is not an id nor a literal";
136 throw InternalError(oss.str());
137 }
138 }
139 GCLock lock;
140 ArrayLit* dims;
141 Expression* e = output_array_ann->arg(0);
142 if (auto* al = e->dynamicCast<ArrayLit>()) {
143 dims = al;
144 } else if (Id* id = e->dynamicCast<Id>()) {
145 dims = id->decl()->e()->cast<ArrayLit>();
146 } else {
147 throw -1;
148 }
149 std::vector<std::pair<int, int> > dims_v;
150 for (int i = 0; i < dims->length(); i++) {
151 IntSetVal* isv = eval_intset(getEnv()->envi(), (*dims)[i]);
152 if (isv->size() == 0) {
153 dims_v.emplace_back(1, 0);
154 } else {
155 dims_v.emplace_back(static_cast<int>(isv->min().toInt()),
156 static_cast<int>(isv->max().toInt()));
157 }
158 }
159 auto* array_solution = new ArrayLit(Location(), array_elems, dims_v);
160 KeepAlive ka(array_solution);
161 auto& de = getSolns2Out()->findOutputVar(vd->id()->str());
162 de.first->e(array_solution);
163 }
164 } else if (vd->ann().contains(constants().ann.output_var)) {
165 Expression* sol = getSolutionValue(vd->id());
166 vd->e(sol);
167 auto& de = getSolns2Out()->findOutputVar(vd->id()->str());
168 de.first->e(sol);
169 }
170 }
171}
172
173void SolverInstanceBase::flattenSearchAnnotations(const Annotation& ann,
174 std::vector<Expression*>& out) {
175 for (ExpressionSetIter i = ann.begin(); i != ann.end(); ++i) {
176 Expression* e = *i;
177 if (e->isa<Call>() &&
178 (e->cast<Call>()->id() == "seq_search" || e->cast<Call>()->id() == "warm_start_array")) {
179 Call* c = e->cast<Call>();
180 auto* anns = c->arg(0)->cast<ArrayLit>();
181 for (unsigned int i = 0; i < anns->size(); i++) {
182 Annotation subann;
183 subann.add((*anns)[i]);
184 flattenSearchAnnotations(subann, out);
185 }
186 } else {
187 out.push_back(*i);
188 }
189 }
190}
191
192void SolverInstanceBase::flattenMultipleObjectives(const Annotation& ann,
193 MultipleObjectives& mo) const {
194 int nGoalH = 0;
195 for (ExpressionSetIter i = ann.begin(); i != ann.end(); ++i) {
196 MZN_ASSERT_HARD_MSG(0 == nGoalH++, "Several goal hierarchies provided");
197 Expression* e = *i;
198 if (e->isa<Call>() && (e->cast<Call>()->id() == "goal_hierarchy")) {
199 MZN_ASSERT_HARD_MSG(getEnv()->flat()->solveItem()->st() == SolveI::SolveType::ST_SAT,
200 "goal_hierarchy provided but solve item is not SAT");
201 Call* c = e->cast<Call>();
202 auto* anns = c->arg(0)->cast<ArrayLit>();
203 for (unsigned int i = 0; i < anns->size(); i++) {
204 Annotation subann;
205 subann.add((*anns)[i]);
206 MultipleObjectives::Objective obj;
207 flattenMultObjComponent(subann, obj);
208 mo.add(obj);
209 }
210 }
211 }
212}
213
214void SolverInstanceBase::flattenMultObjComponent(const Annotation& ann,
215 MultipleObjectives::Objective& obj) {
216 MZN_ASSERT_HARD(!ann.isEmpty());
217 Expression* e = *ann.begin();
218 MZN_ASSERT_HARD(e->isa<Call>());
219 Call* c = e->cast<Call>();
220 obj.setVariable(c->arg(0));
221 const auto id = c->id();
222 if (id == "min_goal" || id == "int_min_goal" || id == "float_min_goal") {
223 obj.setWeight(-1.0);
224 } else if (id == "sat_goal" || id == "max_goal" || id == "int_max_goal" ||
225 id == "float_max_goal") {
226 obj.setWeight(1.0);
227 } else {
228 MZN_ASSERT_HARD_MSG(false, "unknown goal: " << id);
229 }
230}
231
232} // namespace MiniZinc