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#include <utility>
22
23using namespace std;
24using namespace MiniZinc;
25
26void Solns2Out::printHelp(ostream& os) {
27 os << "Solution output options:" << std::endl
28 << " --ozn-file <file>\n Read output specification from ozn file." << std::endl
29 << " -o <file>, --output-to-file <file>\n Filename for generated output." << std::endl
30 << " -i <n>, --ignore-lines <n>, --ignore-leading-lines <n>\n Ignore the first <n> lines "
31 "in the FlatZinc solution stream."
32 << std::endl
33 << " --soln-sep <s>, --soln-separator <s>, --solution-separator <s>\n Specify the string "
34 "printed after each solution (as a separate line).\n The default is to use the same as "
35 "FlatZinc, \"----------\"."
36 << std::endl
37 << " --soln-comma <s>, --solution-comma <s>\n Specify the string used to separate "
38 "solutions.\n The default is the empty string."
39 << std::endl
40 << " --unsat-msg (--unsatisfiable-msg), --unbounded-msg, --unsatorunbnd-msg,\n"
41 " --unknown-msg, --error-msg, --search-complete-msg <msg>\n"
42 " Specify solution status messages. The defaults:\n"
43 " \"=====UNSATISFIABLE=====\", \"=====UNSATorUNBOUNDED=====\", "
44 "\"=====UNBOUNDED=====\",\n"
45 " \"=====UNKNOWN=====\", \"=====ERROR=====\", \"==========\", respectively."
46 << std::endl
47 << " --non-unique\n Allow duplicate solutions.\n"
48 << " -c, --canonicalize\n Canonicalize the output solution stream (i.e., buffer and "
49 "sort).\n"
50 << " --output-non-canonical <file>\n Non-buffered solution output file in case of "
51 "canonicalization.\n"
52 << " --output-raw <file>\n File to dump the solver's raw output (not for hard-linked "
53 "solvers)\n"
54 // Unclear how to exit then:
55 // << " --number-output <n>\n Maximal number of different solutions printed." <<
56 // std::endl
57 << " --no-output-comments\n Do not print comments in the FlatZinc solution stream."
58 << std::endl
59 << " --output-time\n Print timing information in the FlatZinc solution stream."
60 << std::endl
61 << " --no-flush-output\n Don't flush output stream after every line." << std::endl;
62}
63
64bool Solns2Out::processOption(int& i, std::vector<std::string>& argv,
65 const std::string& workingDir) {
66 CLOParser cop(i, argv);
67 std::string buffer;
68 if (cop.getOption("--ozn-file", &buffer)) {
69 initFromOzn(FileUtils::file_path(buffer, workingDir));
70 } else if (cop.getOption("-o --output-to-file", &buffer)) {
71 opt.flagOutputFile = buffer;
72 } else if (cop.getOption("--no-flush-output")) {
73 opt.flagOutputFlush = false;
74 } else if (cop.getOption("--no-output-comments")) {
75 opt.flagOutputComments = false;
76 } else if (cop.getOption("-i --ignore-lines --ignore-leading-lines",
77 &opt.flagIgnoreLines)) { // NOLINT: Allow repeated empty if
78 // Parsed by reference
79 } else if (cop.getOption("--output-time")) {
80 opt.flagOutputTime = true;
81 } else if (cop.getOption("--soln-sep --soln-separator --solution-separator",
82 &opt.solutionSeparator)) { // NOLINT: Allow repeated empty if
83 // Parsed by reference
84 } else if (cop.getOption("--soln-comma --solution-comma",
85 &opt.solutionComma)) { // NOLINT: Allow repeated empty if
86 // Parsed by reference
87 } else if (cop.getOption("--unsat-msg --unsatisfiable-msg",
88 &opt.unsatisfiableMsg)) { // NOLINT: Allow repeated empty if
89 // Parsed by reference
90 } else if (cop.getOption("--unbounded-msg",
91 &opt.unboundedMsg)) { // NOLINT: Allow repeated empty if
92 // Parsed by reference
93 } else if (cop.getOption("--unsatorunbnd-msg",
94 &opt.unsatorunbndMsg)) { // NOLINT: Allow repeated empty if
95 // Parsed by reference
96 } else if (cop.getOption("--unknown-msg", &opt.unknownMsg)) { // NOLINT: Allow repeated empty if
97 // Parsed by reference
98 } else if (cop.getOption("--error-msg", &opt.errorMsg)) { // NOLINT: Allow repeated empty if
99 // Parsed by reference
100 } else if (cop.getOption("--search-complete-msg",
101 &opt.searchCompleteMsg)) { // NOLINT: Allow repeated empty if
102 // Parsed by reference
103 } else if (cop.getOption("--unique")) {
104 opt.flagUnique = true;
105 } else if (cop.getOption("--non-unique")) {
106 opt.flagUnique = false;
107 } else if (cop.getOption("-c --canonicalize")) {
108 opt.flagCanonicalize = true;
109 } else if (cop.getOption("--output-non-canonical --output-non-canon",
110 &opt.flagOutputNoncanonical)) { // NOLINT: Allow repeated empty if
111 // Parsed by reference
112 } else if (cop.getOption("--output-raw",
113 &opt.flagOutputRaw)) { // NOLINT: Allow repeated empty if
114 // Parsed by reference
115 } else if (opt.flagStandaloneSolns2Out) {
116 std::string oznfile(argv[i]);
117 if (oznfile.length() <= 4) {
118 return false;
119 }
120 size_t last_dot = oznfile.find_last_of('.');
121 if (last_dot == string::npos) {
122 return false;
123 }
124 std::string extension = oznfile.substr(last_dot, string::npos);
125 if (extension == ".ozn") {
126 initFromOzn(oznfile);
127 return true;
128 }
129 return false;
130 } else {
131 return false;
132 }
133 return true;
134}
135
136bool Solns2Out::initFromEnv(Env* pE) {
137 assert(pE);
138 _env = pE;
139 _includePaths.push_back(_stdlibDir + "/std/");
140 init();
141 return true;
142}
143
144void Solns2Out::initFromOzn(const std::string& filename) {
145 std::vector<string> filenames(1, filename);
146
147 _includePaths.push_back(_stdlibDir + "/std/");
148
149 for (auto& includePath : _includePaths) {
150 if (!FileUtils::directory_exists(includePath)) {
151 std::cerr << "solns2out: cannot access include directory " << includePath << "\n";
152 std::exit(EXIT_FAILURE);
153 }
154 }
155
156 {
157 _env = new Env();
158 std::stringstream errstream;
159 if ((_outputModel = parse(*_env, filenames, std::vector<std::string>(), "", "", _includePaths,
160 false, false, false, false, errstream)) != nullptr) {
161 std::vector<TypeError> typeErrors;
162 _env->model(_outputModel);
163 MZN_ASSERT_HARD_MSG(_env, "solns2out: could not allocate Env");
164 _envGuard.reset(_env);
165 MiniZinc::typecheck(*_env, _outputModel, typeErrors, false, false);
166 MiniZinc::register_builtins(*_env);
167 _env->envi().swapOutput();
168 init();
169 } else {
170 throw Error(errstream.str());
171 }
172 }
173}
174
175Solns2Out::DE& Solns2Out::findOutputVar(const ASTString& name) {
176 declNewOutput();
177 auto it = _declmap.find(name);
178 MZN_ASSERT_HARD_MSG(_declmap.end() != it, "solns2out_base: unexpected id in output: " << name);
179 return it->second;
180}
181
182void Solns2Out::restoreDefaults() {
183 for (auto& i : *getModel()) {
184 if (auto* vdi = i->dynamicCast<VarDeclI>()) {
185 if (vdi->e()->id()->idn() != -1 || (vdi->e()->id()->v() != "_mzn_solution_checker" &&
186 vdi->e()->id()->v() != "_mzn_stats_checker")) {
187 GCLock lock;
188 auto& de = findOutputVar(vdi->e()->id()->str());
189 vdi->e()->e(de.second());
190 vdi->e()->evaluated(false);
191 }
192 }
193 }
194 _fNewSol2Print = false;
195}
196
197void Solns2Out::parseAssignments(string& solution) {
198 std::vector<SyntaxError> se;
199 unique_ptr<Model> sm(parse_from_string(*_env, solution, "solution received from solver",
200 _includePaths, false, true, false, false, _log, se));
201 if (sm == nullptr) {
202 throw Error("solns2out_base: could not parse solution");
203 }
204 solution = "";
205 for (unsigned int i = 0; i < sm->size(); i++) {
206 if (auto* ai = (*sm)[i]->dynamicCast<AssignI>()) {
207 auto& de = findOutputVar(ai->id());
208 if (!ai->e()->isa<BoolLit>() && !ai->e()->isa<IntLit>() && !ai->e()->isa<FloatLit>()) {
209 Type de_t = de.first->type();
210 de_t.cv(false);
211 ai->e()->type(de_t);
212 }
213 ai->decl(de.first);
214 typecheck(*_env, getModel(), ai);
215 if (Call* c = ai->e()->dynamicCast<Call>()) {
216 // This is an arrayXd call, make sure we get the right builtin
217 assert(c->arg(c->argCount() - 1)->isa<ArrayLit>());
218 for (unsigned int i = 0; i < c->argCount(); i++) {
219 c->arg(i)->type(Type::parsetint());
220 }
221 c->arg(c->argCount() - 1)->type(de.first->type());
222 c->decl(getModel()->matchFn(_env->envi(), c, false));
223 }
224 de.first->e(ai->e());
225 }
226 }
227 declNewOutput();
228}
229
230void Solns2Out::declNewOutput() {
231 _fNewSol2Print = true;
232 status = SolverInstance::SAT;
233}
234
235bool Solns2Out::evalOutput(const string& s_ExtraInfo) {
236 if (!_fNewSol2Print) {
237 return true;
238 }
239 ostringstream oss;
240 if (!_checkerModel.empty()) {
241 auto& checkerStream = _env->envi().checkerOutput;
242 checkerStream.clear();
243 checkerStream.str("");
244 checkSolution(checkerStream);
245 }
246 if (!evalOutputInternal(oss)) {
247 return false;
248 }
249 bool fNew = true;
250 if (opt.flagUnique || opt.flagCanonicalize) {
251 auto res = _sSolsCanon.insert(oss.str());
252 if (!res.second) { // repeated solution
253 fNew = false;
254 }
255 }
256 if (fNew) {
257 {
258 auto& checkerStream = _env->envi().checkerOutput;
259 checkerStream.flush();
260 std::string line;
261 if (std::getline(checkerStream, line)) {
262 _os << "% Solution checker report:\n";
263 _os << "% " << line << "\n";
264 while (std::getline(checkerStream, line)) {
265 _os << "% " << line << "\n";
266 }
267 }
268 }
269 ++stats.nSolns;
270 if (opt.flagCanonicalize) {
271 if (_outStreamNonCanon != nullptr) {
272 if (_outStreamNonCanon->good()) {
273 (*_outStreamNonCanon) << oss.str();
274 (*_outStreamNonCanon) << comments;
275 if (!s_ExtraInfo.empty()) {
276 (*_outStreamNonCanon) << s_ExtraInfo;
277 if ('\n' != s_ExtraInfo.back()) { /// TODO is this enough to check EOL?
278 (*_outStreamNonCanon) << '\n';
279 }
280 }
281 if (opt.flagOutputTime) {
282 (*_outStreamNonCanon) << "% time elapsed: " << _starttime.stoptime() << "\n";
283 }
284 if (!opt.solutionSeparator.empty()) {
285 (*_outStreamNonCanon) << opt.solutionSeparator << '\n';
286 }
287 if (opt.flagOutputFlush) {
288 _outStreamNonCanon->flush();
289 }
290 }
291 }
292 } else {
293 if ((!opt.solutionComma.empty()) && stats.nSolns > 1) {
294 getOutput() << opt.solutionComma << '\n';
295 }
296 getOutput() << oss.str();
297 }
298 }
299 getOutput() << comments; // print them now ????
300 comments = "";
301 if (!s_ExtraInfo.empty()) {
302 getOutput() << s_ExtraInfo;
303 if ('\n' != s_ExtraInfo.back()) { /// TODO is this enough to check EOL?
304 getOutput() << '\n';
305 }
306 }
307 if (fNew && opt.flagOutputTime) {
308 getOutput() << "% time elapsed: " << _starttime.stoptime() << "\n";
309 }
310 if (fNew && !opt.flagCanonicalize && !opt.solutionSeparator.empty()) {
311 getOutput() << opt.solutionSeparator << '\n';
312 }
313 if (opt.flagOutputFlush) {
314 getOutput().flush();
315 }
316 restoreDefaults(); // cleans data. evalOutput() should not be called again w/o assigning new
317 // data.
318 return true;
319}
320
321// NOLINTNEXTLINE(readability-convert-member-functions-to-static): Appears static without Gecode
322void Solns2Out::checkSolution(std::ostream& oss) {
323#ifdef HAS_GECODE
324
325 std::ostringstream checker;
326 checker << _checkerModel;
327 {
328 GCLock lock;
329 for (auto& i : *getModel()) {
330 if (auto* vdi = i->dynamicCast<VarDeclI>()) {
331 if (vdi->e()->ann().contains(constants().ann.mzn_check_var)) {
332 checker << vdi->e()->id()->str() << " = ";
333 Expression* e = eval_par(getEnv()->envi(), vdi->e()->e());
334 auto* al = e->dynamicCast<ArrayLit>();
335 std::vector<Id*> enumids;
336 if (Call* cev = vdi->e()->ann().getCall(constants().ann.mzn_check_enum_var)) {
337 auto* enumIdsAl = cev->arg(0)->cast<ArrayLit>();
338 for (int j = 0; j < enumIdsAl->size(); j++) {
339 enumids.push_back((*enumIdsAl)[j]->dynamicCast<Id>());
340 }
341 }
342
343 if (al != nullptr) {
344 checker << "array" << al->dims() << "d(";
345 for (int i = 0; i < al->dims(); i++) {
346 if (!enumids.empty() && enumids[i] != nullptr) {
347 checker << "to_enum(" << *enumids[i] << ",";
348 }
349 checker << al->min(i) << ".." << al->max(i);
350 if (!enumids.empty() && enumids[i] != nullptr) {
351 checker << ")";
352 }
353 checker << ",";
354 }
355 }
356 if (!enumids.empty() && enumids.back() != nullptr) {
357 checker << "to_enum(" << *enumids.back() << "," << *e << ")";
358 } else {
359 checker << *e;
360 }
361 if (al != nullptr) {
362 checker << ")";
363 }
364 checker << ";\n";
365 }
366 }
367 }
368 }
369
370 MznSolver slv(oss, oss);
371 slv.s2out.opt.solutionSeparator = "";
372 try {
373 std::vector<std::string> args({"--solver", "org.minizinc.gecode_presolver"});
374 slv.run(args, checker.str(), "minizinc", "checker.mzc");
375 } catch (const LocationException& e) {
376 oss << e.loc() << ":" << std::endl;
377 oss << e.what() << ": " << e.msg() << std::endl;
378 } catch (const Exception& e) {
379 std::string what = e.what();
380 oss << what << (what.empty() ? "" : ": ") << e.msg() << std::endl;
381 } catch (const exception& e) {
382 oss << e.what() << std::endl;
383 } catch (...) {
384 oss << " UNKNOWN EXCEPTION." << std::endl;
385 }
386
387#else
388 oss << "% solution checking not supported (need built-in Gecode)" << std::endl;
389#endif
390}
391
392// NOLINTNEXTLINE(readability-convert-member-functions-to-static): Appears static without Gecode
393void Solns2Out::checkStatistics(std::ostream& oss) {
394#ifdef HAS_GECODE
395
396 std::ostringstream checker;
397 checker << _statisticsCheckerModel;
398 checker << "mzn_stats_failures = " << stats.nFails << ";\n";
399 checker << "mzn_stats_solutions = " << stats.nSolns << ";\n";
400 checker << "mzn_stats_nodes = " << stats.nNodes << ";\n";
401 checker << "mzn_stats_time = " << _starttime.ms() << ";\n";
402
403 MznSolver slv(oss, oss);
404 slv.s2out.opt.solutionSeparator = "";
405 try {
406 std::vector<std::string> args({"--solver", "org.minizinc.gecode_presolver"});
407 slv.run(args, checker.str(), "minizinc", "checker.mzc");
408 } catch (const LocationException& e) {
409 oss << e.loc() << ":" << std::endl;
410 oss << e.what() << ": " << e.msg() << std::endl;
411 } catch (const Exception& e) {
412 std::string what = e.what();
413 oss << what << (what.empty() ? "" : ": ") << e.msg() << std::endl;
414 } catch (const exception& e) {
415 oss << e.what() << std::endl;
416 } catch (...) {
417 oss << " UNKNOWN EXCEPTION." << std::endl;
418 }
419
420#else
421 oss << "% statistics checking not supported (need built-in Gecode)" << std::endl;
422#endif
423}
424
425bool Solns2Out::evalOutputInternal(ostream& fout) {
426 if (nullptr != _outputExpr) {
427 _env->envi().evalOutput(fout, _log);
428 }
429 return true;
430}
431
432bool Solns2Out::evalStatus(SolverInstance::Status status) {
433 if (opt.flagCanonicalize) {
434 evalOutputFinalInternal(opt.flagOutputFlush);
435 }
436 evalStatusMsg(status);
437 fStatusPrinted = true;
438 return true;
439}
440
441bool Solns2Out::evalOutputFinalInternal(bool /*b*/) {
442 /// Print the canonical list
443 for (const auto& sol : _sSolsCanon) {
444 if ((!opt.solutionComma.empty()) && &sol != &*_sSolsCanon.begin()) {
445 getOutput() << opt.solutionComma << '\n';
446 }
447 getOutput() << sol;
448 if (!opt.solutionSeparator.empty()) {
449 getOutput() << opt.solutionSeparator << '\n';
450 }
451 }
452 return true;
453}
454
455bool Solns2Out::evalStatusMsg(SolverInstance::Status status) {
456 std::map<SolverInstance::Status, string> stat2msg;
457 stat2msg[SolverInstance::OPT] = opt.searchCompleteMsg;
458 stat2msg[SolverInstance::UNSAT] = opt.unsatisfiableMsg;
459 stat2msg[SolverInstance::UNBND] = opt.unboundedMsg;
460 stat2msg[SolverInstance::UNSATorUNBND] = opt.unsatorunbndMsg;
461 stat2msg[SolverInstance::UNKNOWN] = opt.unknownMsg;
462 stat2msg[SolverInstance::ERROR] = opt.errorMsg;
463 stat2msg[SolverInstance::NONE] = "";
464 auto it = stat2msg.find(status);
465 if (stat2msg.end() != it) {
466 getOutput() << comments;
467 if (!it->second.empty()) {
468 getOutput() << it->second << '\n';
469 }
470 if (opt.flagOutputTime) {
471 getOutput() << "% time elapsed: " << _starttime.stoptime() << "\n";
472 }
473 if (opt.flagOutputFlush) {
474 getOutput().flush();
475 }
476 Solns2Out::status = status;
477 } else {
478 getOutput() << comments;
479 if (opt.flagOutputFlush) {
480 getOutput().flush();
481 }
482 MZN_ASSERT_HARD_MSG(SolverInstance::SAT == status, // which is ignored
483 "solns2out_base: undefined solution status code " << status);
484 Solns2Out::status = SolverInstance::SAT;
485 }
486 comments = "";
487 return true;
488}
489
490void Solns2Out::init() {
491 _declmap.clear();
492 for (auto& i : *getModel()) {
493 if (auto* oi = i->dynamicCast<OutputI>()) {
494 _outputExpr = oi->e();
495 } else if (auto* vdi = i->dynamicCast<VarDeclI>()) {
496 if (vdi->e()->id()->idn() == -1 && vdi->e()->id()->v() == "_mzn_solution_checker") {
497 _checkerModel = eval_string(getEnv()->envi(), vdi->e()->e());
498 if (!_checkerModel.empty() && _checkerModel[0] == '@') {
499 _checkerModel = FileUtils::decode_base64(_checkerModel);
500 FileUtils::inflate_string(_checkerModel);
501 }
502 } else if (vdi->e()->id()->idn() == -1 && vdi->e()->id()->v() == "_mzn_stats_checker") {
503 _statisticsCheckerModel = eval_string(getEnv()->envi(), vdi->e()->e());
504 if (!_statisticsCheckerModel.empty() && _statisticsCheckerModel[0] == '@') {
505 _statisticsCheckerModel = FileUtils::decode_base64(_statisticsCheckerModel);
506 FileUtils::inflate_string(_statisticsCheckerModel);
507 }
508 } else {
509 GCLock lock;
510 _declmap.insert(make_pair(vdi->e()->id()->str(), DE(vdi->e(), vdi->e()->e())));
511 }
512 }
513 }
514
515 /// Main output file
516 if (nullptr == _outStream) {
517 if (!opt.flagOutputFile.empty()) {
518 _outStream.reset(new ofstream(FILE_PATH(opt.flagOutputFile)));
519 MZN_ASSERT_HARD_MSG(_outStream.get(),
520 "solns2out_base: could not allocate stream object for file output into "
521 << opt.flagOutputFile);
522 check_io_status(_outStream->good(), opt.flagOutputFile);
523 }
524 }
525 /// Non-canonical output
526 if (opt.flagCanonicalize && (!opt.flagOutputNoncanonical.empty())) {
527 _outStreamNonCanon.reset(new ofstream(FILE_PATH(opt.flagOutputNoncanonical)));
528 MZN_ASSERT_HARD_MSG(_outStreamNonCanon.get(),
529 "solns2out_base: could not allocate stream object for non-canon output");
530 check_io_status(_outStreamNonCanon->good(), opt.flagOutputNoncanonical, false);
531 }
532 /// Raw output
533 if (!opt.flagOutputRaw.empty()) {
534 _outStreamRaw.reset(new ofstream(FILE_PATH(opt.flagOutputRaw)));
535 MZN_ASSERT_HARD_MSG(_outStreamRaw.get(),
536 "solns2out_base: could not allocate stream object for raw output");
537 check_io_status(_outStreamRaw->good(), opt.flagOutputRaw, false);
538 }
539 /// Assume all options are set before
540 nLinesIgnore = opt.flagIgnoreLines;
541}
542
543Solns2Out::Solns2Out(std::ostream& os0, std::ostream& log0, std::string stdlibDir0)
544 : _os(os0), _log(log0), _stdlibDir(std::move(stdlibDir0)) {}
545
546Solns2Out::~Solns2Out() {
547 getOutput() << comments;
548 if (opt.flagOutputFlush) {
549 getOutput() << flush;
550 }
551}
552
553ostream& Solns2Out::getOutput() {
554 return (((_outStream != nullptr) && _outStream->good()) ? *_outStream : _os);
555}
556
557ostream& Solns2Out::getLog() { return _log; }
558
559bool Solns2Out::feedRawDataChunk(const char* data) {
560 istringstream solstream(data);
561 while (solstream.good()) {
562 string line;
563 getline(solstream, line);
564 if (!_linePart.empty()) {
565 line = _linePart + line;
566 _linePart.clear();
567 }
568 if (solstream.eof()) { // wait next chunk
569 _linePart = line;
570 break; // to get to raw output
571 }
572 if (!line.empty()) {
573 if ('\r' == line.back()) {
574 line.pop_back(); // For WIN files
575 }
576 }
577 if (nLinesIgnore > 0) {
578 --nLinesIgnore;
579 continue;
580 }
581 if (_mapInputStatus.empty()) {
582 createInputMap();
583 }
584 auto it = _mapInputStatus.find(line);
585 if (_mapInputStatus.end() != it) {
586 if (SolverInstance::SAT == it->second) {
587 parseAssignments(solution);
588 evalOutput();
589 } else {
590 evalStatus(it->second);
591 }
592 } else {
593 solution += line + '\n';
594 if (opt.flagOutputComments) {
595 std::istringstream iss(line);
596 char c = '_';
597 iss >> skipws >> c;
598 if (iss.good() && '%' == c) {
599 // Feed comments directly
600 getOutput() << line << '\n';
601 if (opt.flagOutputFlush) {
602 getOutput().flush();
603 }
604 if (_outStreamNonCanon != nullptr) {
605 if (_outStreamNonCanon->good()) {
606 (*_outStreamNonCanon) << line << '\n';
607 }
608 }
609 if (line.substr(0, 13) == "%%%mzn-stat: " && line.size() > 13) {
610 if (line.substr(13, 6) == "nodes=") {
611 std::istringstream iss(line.substr(19));
612 int n_nodes;
613 iss >> n_nodes;
614 stats.nNodes = n_nodes;
615 } else if (line.substr(13, 9) == "failures=") {
616 std::istringstream iss(line.substr(22));
617 int n_failures;
618 iss >> n_failures;
619 stats.nFails = n_failures;
620 }
621 }
622 }
623 }
624 }
625 }
626 if (_outStreamRaw != nullptr) {
627 *_outStreamRaw << data;
628 if (opt.flagOutputFlush) {
629 _outStreamRaw->flush();
630 }
631 }
632 return true;
633}
634
635void Solns2Out::createInputMap() {
636 _mapInputStatus[opt.searchCompleteMsgDef] = SolverInstance::OPT;
637 _mapInputStatus[opt.solutionSeparatorDef] = SolverInstance::SAT;
638 _mapInputStatus[opt.unsatisfiableMsgDef] = SolverInstance::UNSAT;
639 _mapInputStatus[opt.unboundedMsgDef] = SolverInstance::UNBND;
640 _mapInputStatus[opt.unsatorunbndMsgDef] = SolverInstance::UNSATorUNBND;
641 _mapInputStatus[opt.unknownMsgDef] = SolverInstance::UNKNOWN;
642 _mapInputStatus[opt.errorMsg] = SolverInstance::ERROR;
643}
644
645void Solns2Out::printStatistics(ostream& os) {
646 os << "%%%mzn-stat: nSolutions=" << stats.nSolns << "\n";
647 if (!_statisticsCheckerModel.empty()) {
648 std::ostringstream oss;
649 checkStatistics(oss);
650 os << "%%%mzn-stat: statisticsCheck=\"" << Printer::escapeStringLit(oss.str()) << "\"\n";
651 }
652 os << "%%%mzn-stat-end\n";
653}