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 * Gleb Belov <gleb.belov@monash.edu>
7 */
8
9/* This Source Code Form is subject to the terms of the Mozilla Public
10 * License, v. 2.0. If a copy of the MPL was ! distributed with this
11 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
12
13#ifdef _MSC_VER
14#define _CRT_SECURE_NO_WARNINGS
15#endif
16
17#include <minizinc/solns2out.hh>
18#include <minizinc/solver.hh>
19
20#include <fstream>
21
22using namespace std;
23using namespace MiniZinc;
24
25void Solns2Out::printHelp(ostream& os) {
26 os << "Solution output options:" << std::endl
27 << " --ozn-file <file>\n Read output specification from ozn file." << std::endl
28 << " -o <file>, --output-to-file <file>\n Filename for generated output." << std::endl
29 << " -i <n>, --ignore-lines <n>, --ignore-leading-lines <n>\n Ignore the first <n> lines "
30 "in the FlatZinc solution stream."
31 << std::endl
32 << " --soln-sep <s>, --soln-separator <s>, --solution-separator <s>\n Specify the string "
33 "printed after each solution (as a separate line).\n The default is to use the same as "
34 "FlatZinc, \"----------\"."
35 << std::endl
36 << " --soln-comma <s>, --solution-comma <s>\n Specify the string used to separate "
37 "solutions.\n The default is the empty string."
38 << std::endl
39 << " --unsat-msg (--unsatisfiable-msg), --unbounded-msg, --unsatorunbnd-msg,\n"
40 " --unknown-msg, --error-msg, --search-complete-msg <msg>\n"
41 " Specify solution status messages. The defaults:\n"
42 " \"=====UNSATISFIABLE=====\", \"=====UNSATorUNBOUNDED=====\", "
43 "\"=====UNBOUNDED=====\",\n"
44 " \"=====UNKNOWN=====\", \"=====ERROR=====\", \"==========\", respectively."
45 << std::endl
46 << " --non-unique\n Allow duplicate solutions.\n"
47 << " -c, --canonicalize\n Canonicalize the output solution stream (i.e., buffer and "
48 "sort).\n"
49 << " --output-non-canonical <file>\n Non-buffered solution output file in case of "
50 "canonicalization.\n"
51 << " --output-raw <file>\n File to dump the solver's raw output (not for hard-linked "
52 "solvers)\n"
53 // Unclear how to exit then:
54 // << " --number-output <n>\n Maximal number of different solutions printed." <<
55 // std::endl
56 << " --no-output-comments\n Do not print comments in the FlatZinc solution stream."
57 << std::endl
58 << " --output-time\n Print timing information in the FlatZinc solution stream."
59 << std::endl
60 << " --no-flush-output\n Don't flush output stream after every line." << std::endl;
61}
62
63bool Solns2Out::processOption(int& i, std::vector<std::string>& argv) {
64 CLOParser cop(i, argv);
65 std::string oznfile;
66 if (cop.getOption("--ozn-file", &oznfile)) {
67 initFromOzn(oznfile);
68 } else if (cop.getOption("-o --output-to-file", &_opt.flag_output_file)) {
69 } else if (cop.getOption("--no-flush-output")) {
70 _opt.flag_output_flush = false;
71 } else if (cop.getOption("--no-output-comments")) {
72 _opt.flag_output_comments = false;
73 } else if (cop.getOption("-i --ignore-lines --ignore-leading-lines", &_opt.flag_ignore_lines)) {
74 } else if (cop.getOption("--output-time")) {
75 _opt.flag_output_time = true;
76 } else if (cop.getOption("--soln-sep --soln-separator --solution-separator",
77 &_opt.solution_separator)) {
78 } else if (cop.getOption("--soln-comma --solution-comma", &_opt.solution_comma)) {
79 } else if (cop.getOption("--unsat-msg --unsatisfiable-msg", &_opt.unsatisfiable_msg)) {
80 } else if (cop.getOption("--unbounded-msg", &_opt.unbounded_msg)) {
81 } else if (cop.getOption("--unsatorunbnd-msg", &_opt.unsatorunbnd_msg)) {
82 } else if (cop.getOption("--unknown-msg", &_opt.unknown_msg)) {
83 } else if (cop.getOption("--error-msg", &_opt.error_msg)) {
84 } else if (cop.getOption("--search-complete-msg", &_opt.search_complete_msg)) {
85 } else if (cop.getOption("--unique")) {
86 _opt.flag_unique = true;
87 } else if (cop.getOption("--non-unique")) {
88 _opt.flag_unique = false;
89 } else if (cop.getOption("-c --canonicalize")) {
90 _opt.flag_canonicalize = true;
91 } else if (cop.getOption("--output-non-canonical --output-non-canon",
92 &_opt.flag_output_noncanonical)) {
93 } else if (cop.getOption("--output-raw", &_opt.flag_output_raw)) {
94 // } else if ( cop.getOption( "--number-output", &_opt.flag_number_output ) ) {
95 } else if (_opt.flag_standaloneSolns2Out) {
96 std::string oznfile(argv[i]);
97 if (oznfile.length() <= 4) {
98 return false;
99 }
100 size_t last_dot = oznfile.find_last_of('.');
101 if (last_dot == string::npos) {
102 return false;
103 }
104 std::string extension = oznfile.substr(last_dot, string::npos);
105 if (extension == ".ozn") {
106 initFromOzn(oznfile);
107 return true;
108 }
109 return false;
110 } else {
111 return false;
112 }
113 return true;
114}
115
116bool Solns2Out::initFromEnv(Env* pE) {
117 assert(pE);
118 pEnv = pE;
119 init();
120 return true;
121}
122
123void Solns2Out::initFromOzn(const std::string& filename) {
124 std::vector<string> filenames(1, filename);
125
126 includePaths.push_back(stdlibDir + "/std/");
127
128 for (unsigned int i = 0; i < includePaths.size(); i++) {
129 if (!FileUtils::directory_exists(includePaths[i])) {
130 std::cerr << "solns2out: cannot access include directory " << includePaths[i] << "\n";
131 std::exit(EXIT_FAILURE);
132 }
133 }
134
135 {
136 pEnv = new Env();
137 std::stringstream errstream;
138 if ((pOutput = parse(*pEnv, filenames, std::vector<std::string>(), "", "", includePaths, false,
139 false, false, errstream))) {
140 std::vector<TypeError> typeErrors;
141 pEnv->model(pOutput);
142 MZN_ASSERT_HARD_MSG(pEnv, "solns2out: could not allocate Env");
143 pEnv_guard.reset(pEnv);
144 MiniZinc::typecheck(*pEnv, pOutput, typeErrors, false, false);
145 MiniZinc::registerBuiltins(*pEnv);
146 pEnv->envi().swap_output();
147 init();
148 } else {
149 throw Error(errstream.str());
150 }
151 }
152}
153
154void Solns2Out::createOutputMap() {
155 for (unsigned int i = 0; i < getModel()->size(); i++) {
156 if (VarDeclI* vdi = (*getModel())[i]->dyn_cast<VarDeclI>()) {
157 GCLock lock;
158 declmap.insert(
159 pair<std::string, DE>(vdi->e()->id()->str().str(), DE(vdi->e(), vdi->e()->e())));
160 } else if (OutputI* oi = (*getModel())[i]->dyn_cast<OutputI>()) {
161 MZN_ASSERT_HARD_MSG(outputExpr == oi->e(),
162 "solns2out_base: <=1 output items allowed currently TODO?");
163 }
164 }
165}
166
167Solns2Out::DE& Solns2Out::findOutputVar(ASTString id) {
168 declNewOutput();
169 if (declmap.empty()) createOutputMap();
170 auto it = declmap.find(id.str());
171 MZN_ASSERT_HARD_MSG(declmap.end() != it, "solns2out_base: unexpected id in output: " << id);
172 return it->second;
173}
174
175void Solns2Out::restoreDefaults() {
176 for (unsigned int i = 0; i < getModel()->size(); i++) {
177 if (VarDeclI* vdi = (*getModel())[i]->dyn_cast<VarDeclI>()) {
178 GCLock lock;
179 auto& de = findOutputVar(vdi->e()->id()->str());
180 vdi->e()->e(de.second());
181 vdi->e()->evaluated(false);
182 }
183 }
184 fNewSol2Print = false;
185}
186
187void Solns2Out::parseAssignments(string& solution) {
188 std::vector<SyntaxError> se;
189 unique_ptr<Model> sm(parseFromString(*pEnv, solution, "solution received from solver",
190 includePaths, true, false, false, log, se));
191 if (sm.get() == NULL) throw Error("solns2out_base: could not parse solution");
192 solution = "";
193 for (unsigned int i = 0; i < sm->size(); i++) {
194 if (AssignI* ai = (*sm)[i]->dyn_cast<AssignI>()) {
195 auto& de = findOutputVar(ai->id());
196 ai->e()->type(de.first->type());
197 ai->decl(de.first);
198 typecheck(*pEnv, getModel(), ai);
199 if (Call* c = ai->e()->dyn_cast<Call>()) {
200 // This is an arrayXd call, make sure we get the right builtin
201 assert(c->arg(c->n_args() - 1)->isa<ArrayLit>());
202 for (unsigned int i = 0; i < c->n_args(); i++) c->arg(i)->type(Type::parsetint());
203 c->arg(c->n_args() - 1)->type(de.first->type());
204 c->decl(getModel()->matchFn(pEnv->envi(), c, false));
205 }
206 de.first->e(ai->e());
207 }
208 }
209 declNewOutput();
210}
211
212void Solns2Out::declNewOutput() {
213 fNewSol2Print = true;
214 status = SolverInstance::SAT;
215}
216
217bool Solns2Out::evalOutput(const string& s_ExtraInfo) {
218 if (!fNewSol2Print) return true;
219 ostringstream oss;
220 if (!__evalOutput(oss)) return false;
221 if (!checkerModel.empty()) checkSolution(oss);
222 bool fNew = true;
223 if (_opt.flag_unique || _opt.flag_canonicalize) {
224 auto res = sSolsCanon.insert(oss.str());
225 if (!res.second) // repeated solution
226 fNew = false;
227 }
228 if (fNew) {
229 ++nSolns;
230 if (_opt.flag_canonicalize) {
231 if (pOfs_non_canon.get())
232 if (pOfs_non_canon->good()) {
233 (*pOfs_non_canon) << oss.str();
234 (*pOfs_non_canon) << comments;
235 if (s_ExtraInfo.size()) {
236 (*pOfs_non_canon) << s_ExtraInfo;
237 if ('\n' != s_ExtraInfo.back()) /// TODO is this enough to check EOL?
238 (*pOfs_non_canon) << '\n';
239 }
240 if (_opt.flag_output_time)
241 (*pOfs_non_canon) << "% time elapsed: " << starttime.stoptime() << "\n";
242 if (!_opt.solution_separator.empty())
243 (*pOfs_non_canon) << _opt.solution_separator << '\n';
244 if (_opt.flag_output_flush) pOfs_non_canon->flush();
245 }
246 } else {
247 if (_opt.solution_comma.size() && nSolns > 1) getOutput() << _opt.solution_comma << '\n';
248 getOutput() << oss.str();
249 }
250 }
251 getOutput() << comments; // print them now ????
252 comments = "";
253 if (s_ExtraInfo.size()) {
254 getOutput() << s_ExtraInfo;
255 if ('\n' != s_ExtraInfo.back()) /// TODO is this enough to check EOL?
256 getOutput() << '\n';
257 }
258 if (fNew && _opt.flag_output_time)
259 getOutput() << "% time elapsed: " << starttime.stoptime() << "\n";
260 if (fNew && !_opt.flag_canonicalize && !_opt.solution_separator.empty())
261 getOutput() << _opt.solution_separator << '\n';
262 if (_opt.flag_output_flush) getOutput().flush();
263 restoreDefaults(); // cleans data. evalOutput() should not be called again w/o assigning new
264 // data.
265 return true;
266}
267
268void Solns2Out::checkSolution(std::ostream& os) {
269#ifdef HAS_GECODE
270
271 std::ostringstream checker;
272 checker << checkerModel;
273 {
274 GCLock lock;
275 for (unsigned int i = 0; i < getModel()->size(); i++) {
276 if (VarDeclI* vdi = (*getModel())[i]->dyn_cast<VarDeclI>()) {
277 if (vdi->e()->ann().contains(constants().ann.mzn_check_var)) {
278 if (Call* cev = vdi->e()->ann().getCall(constants().ann.mzn_check_enum_var)) {
279 checker << vdi->e()->id()->str() << "= to_enum(" << *cev->arg(0)->cast<Id>() << ","
280 << *eval_par(getEnv()->envi(), vdi->e()->e()) << ");";
281 } else {
282 checker << vdi->e()->id()->str() << "=" << *eval_par(getEnv()->envi(), vdi->e()->e())
283 << ";";
284 }
285 }
286 }
287 }
288 }
289
290 std::ostringstream oss_err;
291 assert(false);
292 MznSolver slv;
293 slv.s2out._opt.solution_separator = "";
294 try {
295 std::vector<std::string> args({"--solver", "org.minizinc.gecode_presolver"});
296 // slv.run(args, checker.str(), "minizinc", "checker.mzc");
297 } catch (const LocationException& e) {
298 oss_err << e.loc() << ":" << std::endl;
299 oss_err << e.what() << ": " << e.msg() << std::endl;
300 } catch (const Exception& e) {
301 std::string what = e.what();
302 oss_err << what << (what.empty() ? "" : ": ") << e.msg() << std::endl;
303 } catch (const exception& e) {
304 oss_err << e.what() << std::endl;
305 } catch (...) {
306 oss_err << " UNKNOWN EXCEPTION." << std::endl;
307 }
308 std::istringstream iss(oss_err.str());
309 std::string line;
310 os << "% Solution checker report:\n";
311 while (std::getline(iss, line)) {
312 os << "% " << line << "\n";
313 }
314
315#else
316 os << "% solution checking not supported (need built-in Gecode)" << std::endl;
317#endif
318}
319
320bool Solns2Out::__evalOutput(ostream& fout) {
321 if (0 != outputExpr) {
322 pEnv->envi().evalOutput(fout);
323 }
324 return true;
325}
326
327bool Solns2Out::evalStatus(SolverInstance::Status status) {
328 if (_opt.flag_canonicalize) __evalOutputFinal(_opt.flag_output_flush);
329 __evalStatusMsg(status);
330 fStatusPrinted = 1;
331 return true;
332}
333
334bool Solns2Out::__evalOutputFinal(bool) {
335 /// Print the canonical list
336 for (auto& sol : sSolsCanon) {
337 if (_opt.solution_comma.size() && &sol != &*sSolsCanon.begin())
338 getOutput() << _opt.solution_comma << '\n';
339 getOutput() << sol;
340 if (!_opt.solution_separator.empty()) getOutput() << _opt.solution_separator << '\n';
341 }
342 return true;
343}
344
345bool Solns2Out::__evalStatusMsg(SolverInstance::Status status) {
346 std::map<SolverInstance::Status, string> stat2msg;
347 stat2msg[SolverInstance::OPT] = _opt.search_complete_msg;
348 stat2msg[SolverInstance::UNSAT] = _opt.unsatisfiable_msg;
349 stat2msg[SolverInstance::UNBND] = _opt.unbounded_msg;
350 stat2msg[SolverInstance::UNSATorUNBND] = _opt.unsatorunbnd_msg;
351 stat2msg[SolverInstance::UNKNOWN] = _opt.unknown_msg;
352 stat2msg[SolverInstance::ERROR] = _opt.error_msg;
353 stat2msg[SolverInstance::NONE] = "";
354 auto it = stat2msg.find(status);
355 if (stat2msg.end() != it) {
356 getOutput() << comments;
357 if (!it->second.empty()) getOutput() << it->second << '\n';
358 if (_opt.flag_output_time) getOutput() << "% time elapsed: " << starttime.stoptime() << "\n";
359 if (_opt.flag_output_flush) getOutput().flush();
360 Solns2Out::status = status;
361 } else {
362 getOutput() << comments;
363 if (_opt.flag_output_flush) getOutput().flush();
364 MZN_ASSERT_HARD_MSG(SolverInstance::SAT == status, // which is ignored
365 "solns2out_base: undefined solution status code " << status);
366 Solns2Out::status = SolverInstance::SAT;
367 }
368 comments = "";
369 return true;
370}
371
372void Solns2Out::init() {
373 for (unsigned int i = 0; i < getModel()->size(); i++) {
374 if (OutputI* oi = (*getModel())[i]->dyn_cast<OutputI>()) {
375 outputExpr = oi->e();
376 break;
377 }
378 if (VarDeclI* vdi = (*getModel())[i]->dyn_cast<VarDeclI>()) {
379 if (vdi->e()->id()->idn() == -1 && vdi->e()->id()->v() == "_mzn_solution_checker") {
380 checkerModel = eval_string(getEnv()->envi(), vdi->e()->e());
381 if (checkerModel.size() > 0 && checkerModel[0] == '@') {
382 checkerModel = FileUtils::decodeBase64(checkerModel);
383 FileUtils::inflateString(checkerModel);
384 }
385 }
386 }
387 }
388
389 /// Main output file
390 if (0 == pOut) {
391 if (_opt.flag_output_file.size()) {
392 pOut.reset(new ofstream(_opt.flag_output_file));
393 MZN_ASSERT_HARD_MSG(pOut.get(),
394 "solns2out_base: could not allocate stream object for file output into "
395 << _opt.flag_output_file);
396 checkIOStatus(pOut->good(), _opt.flag_output_file);
397 }
398 }
399 /// Non-canonical output
400 if (_opt.flag_canonicalize && _opt.flag_output_noncanonical.size()) {
401 pOfs_non_canon.reset(new ofstream(_opt.flag_output_noncanonical));
402 MZN_ASSERT_HARD_MSG(pOfs_non_canon.get(),
403 "solns2out_base: could not allocate stream object for non-canon output");
404 checkIOStatus(pOfs_non_canon->good(), _opt.flag_output_noncanonical, 0);
405 }
406 /// Raw output
407 if (_opt.flag_output_raw.size()) {
408 pOfs_raw.reset(new ofstream(_opt.flag_output_raw));
409 MZN_ASSERT_HARD_MSG(pOfs_raw.get(),
410 "solns2out_base: could not allocate stream object for raw output");
411 checkIOStatus(pOfs_raw->good(), _opt.flag_output_raw, 0);
412 }
413 /// Assume all options are set before
414 nLinesIgnore = _opt.flag_ignore_lines;
415}
416
417Solns2Out::Solns2Out(std::ostream& os0, std::ostream& log0, const std::string& stdlibDir0)
418 : os(os0), log(log0), stdlibDir(stdlibDir0) {}
419
420Solns2Out::~Solns2Out() {
421 getOutput() << comments;
422 if (_opt.flag_output_flush) getOutput() << flush;
423}
424
425ostream& Solns2Out::getOutput() { return ((pOut.get() && pOut->good()) ? *pOut : os); }
426
427ostream& Solns2Out::getLog() { return log; }
428
429bool Solns2Out::feedRawDataChunk(const char* data) {
430 istringstream solstream(data);
431 while (solstream.good()) {
432 string line;
433 getline(solstream, line);
434 if (line_part.size()) {
435 line = line_part + line;
436 line_part.clear();
437 }
438 if (solstream.eof()) { // wait next chunk
439 line_part = line;
440 break; // to get to raw output
441 }
442 if (line.size())
443 if ('\r' == line.back()) line.pop_back(); // For WIN files
444 if (nLinesIgnore > 0) {
445 --nLinesIgnore;
446 continue;
447 }
448 if (mapInputStatus.empty()) createInputMap();
449 auto it = mapInputStatus.find(line);
450 if (mapInputStatus.end() != it) {
451 if (SolverInstance::SAT == it->second) {
452 parseAssignments(solution);
453 // evalOutput();
454 } else {
455 evalStatus(it->second);
456 }
457 } else {
458 solution += line + '\n';
459 if (_opt.flag_output_comments) {
460 std::istringstream iss(line);
461 char c = '_';
462 iss >> skipws >> c;
463 if (iss.good() && '%' == c) {
464 // Feed comments directly
465 getOutput() << line << '\n';
466 if (_opt.flag_output_flush) getOutput().flush();
467 if (pOfs_non_canon.get())
468 if (pOfs_non_canon->good()) (*pOfs_non_canon) << line << '\n';
469 }
470 }
471 }
472 }
473 if (pOfs_raw.get()) {
474 (*pOfs_raw.get()) << data;
475 if (_opt.flag_output_flush) pOfs_raw->flush();
476 }
477 return true;
478}
479
480void Solns2Out::createInputMap() {
481 mapInputStatus[_opt.search_complete_msg_00] = SolverInstance::OPT;
482 mapInputStatus[_opt.solution_separator_00] = SolverInstance::SAT;
483 mapInputStatus[_opt.unsatisfiable_msg_00] = SolverInstance::UNSAT;
484 mapInputStatus[_opt.unbounded_msg_00] = SolverInstance::UNBND;
485 mapInputStatus[_opt.unsatorunbnd_msg_00] = SolverInstance::UNSATorUNBND;
486 mapInputStatus[_opt.unknown_msg_00] = SolverInstance::UNKNOWN;
487 mapInputStatus[_opt.error_msg] = SolverInstance::ERROR;
488}
489
490void Solns2Out::printStatistics(ostream& os) { os << "%%%mzn-stat: nSolutions=" << nSolns << "\n"; }