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 ! distributed with this
10 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
11
12/* A basic mzn2fzn wrapper, can be used as a plugin
13 */
14
15#ifdef _MSC_VER
16#define _CRT_SECURE_NO_WARNINGS
17#endif
18
19#include <minizinc/flattener.hh>
20#include <minizinc/pathfileprinter.hh>
21
22#include <fstream>
23
24#ifdef HAS_GECODE
25#include <minizinc/solvers/gecode_solverinstance.hh>
26
27#include <utility>
28#endif
29
30using namespace std;
31using namespace MiniZinc;
32
33void Flattener::printVersion(ostream& os) {
34 os << "MiniZinc to FlatZinc converter, version " << MZN_VERSION_MAJOR << "." << MZN_VERSION_MINOR
35 << "." << MZN_VERSION_PATCH;
36 if (!std::string(MZN_BUILD_REF).empty()) {
37 os << ", build " << MZN_BUILD_REF;
38 }
39 os << std::endl;
40 os << "Copyright (C) 2014-" << string(__DATE__).substr(7, 4)
41 << " Monash University, NICTA, Data61" << std::endl;
42}
43
44void Flattener::printHelp(ostream& os) const {
45 os << std::endl
46 << "Flattener input options:" << std::endl
47 << " --instance-check-only\n Check the model instance (including data) for errors, but "
48 "do "
49 "not\n convert to FlatZinc."
50 << std::endl
51 << " -e, --model-check-only\n Check the model (without requiring data) for errors, but "
52 "do "
53 "not\n convert to FlatZinc."
54 << std::endl
55 << " --model-interface-only\n Only extract parameters and output variables." << std::endl
56 << " --model-types-only\n Only output variable (enum) type information." << std::endl
57 << " --no-optimize\n Do not optimize the FlatZinc" << std::endl
58 << " --no-chain-compression\n Do not simplify chains of implication constraints."
59 << std::endl
60 << " -m <file>, --model <file>\n File named <file> is the model." << std::endl
61 << " -d <file>, --data <file>\n File named <file> contains data used by the model."
62 << std::endl
63 << " -D <data>, --cmdline-data <data>\n Include the given data assignment in the model."
64 << std::endl
65 << " --stdlib-dir <dir>\n Path to MiniZinc standard library directory" << std::endl
66 << " -G <dir>, --globals-dir <dir>, --mzn-globals-dir <dir>\n Search for included "
67 "globals "
68 "in <stdlib>/<dir>."
69 << std::endl
70 << " -, --input-from-stdin\n Read problem from standard input" << std::endl
71 << " -I <dir>, --search-dir <dir>\n Additionally search for included files in <dir>."
72 << std::endl
73 << " -D \"fMIPdomains=true\"\n Switch on MIPDomain Unification" << std::endl
74 << " --MIPDMaxIntvEE <n>\n MIPD: max integer domain subinterval length to enforce "
75 "equality encoding, default "
76 << _optMIPDmaxIntvEE << std::endl
77 << " --MIPDMaxDensEE <n>\n MIPD: max domain cardinality to N subintervals ratio\n to "
78 "enforce equality encoding, default "
79 << _optMIPDmaxDensEE << ", either condition triggers" << std::endl
80 << " --only-range-domains\n When no MIPdomains: all domains contiguous, holes replaced "
81 "by "
82 "inequalities"
83 << std::endl
84 << " --allow-multiple-assignments\n Allow multiple assignments to the same variable "
85 "(e.g. "
86 "in dzn)"
87 << std::endl
88 << " --no-half-reifications\n Only use fully reified constraints, even when a half "
89 "reified constraint is defined."
90 << std::endl
91 << " --compile-solution-checker <file>.mzc.mzn\n Compile solution checker model"
92 << std::endl
93 << std::endl
94 << "Flattener two-pass options:" << std::endl
95 << " --two-pass\n Flatten twice to make better flattening decisions for the target"
96 << std::endl
97#ifdef HAS_GECODE
98 << " --use-gecode\n Perform root-node-propagation with Gecode (adds --two-pass)"
99 << std::endl
100 << " --shave\n Probe bounds of all variables at the root node (adds --use-gecode)"
101 << std::endl
102 << " --sac\n Probe values of all variables at the root node (adds --use-gecode)"
103 << std::endl
104 << " --pre-passes <n>\n Number of times to apply shave/sac pass (0 = fixed-point, 1 = "
105 "default)"
106 << std::endl
107#endif
108 << " -O<n>\n Two-pass optimisation levels:" << std::endl
109 << " -O0: Disable optimize (--no-optimize) -O1: Single pass (default)" << std::endl
110 << " -O2: Same as: --two-pass"
111#ifdef HAS_GECODE
112 << " -O3: Same as: --use-gecode" << std::endl
113 << " -O4: Same as: --shave -O5: Same as: --sac" << std::endl
114#else
115 << "\n -O3,4,5: Disabled [Requires MiniZinc with built-in Gecode support]" << std::endl
116#endif
117 << " -g\n Debug mode: Forces -O0 and records all domain changes as constraints instead "
118 "of "
119 "applying them"
120 << std::endl
121 << std::endl;
122 os << "Flattener output options:" << std::endl
123 << " --no-output-ozn, -O-\n Do not output ozn file" << std::endl
124 << " --output-base <name>\n Base name for output files" << std::endl
125 << (_fOutputByDefault
126 ? " -o <file>, --fzn <file>, --output-to-file <file>, --output-fzn-to-file <file>\n"
127 : " --fzn <file>, --output-fzn-to-file <file>\n")
128 << " Filename for generated FlatZinc output" << std::endl
129 << " --ozn, --output-ozn-to-file <file>\n Filename for model output specification "
130 "(--ozn- "
131 "for none)"
132 << std::endl
133 << " --keep-paths\n Don't remove path annotations from FlatZinc" << std::endl
134 << " --output-paths\n Output a symbol table (.paths file)" << std::endl
135 << " --output-paths-to-file <file>\n Output a symbol table (.paths file) to <file>"
136 << std::endl
137 << " --output-detailed-timing\n Output detailed profiling information of compilation time"
138 << std::endl
139 << " --output-to-stdout, --output-fzn-to-stdout\n Print generated FlatZinc to standard "
140 "output"
141 << std::endl
142 << " --output-ozn-to-stdout\n Print model output specification to standard output"
143 << std::endl
144 << " --output-paths-to-stdout\n Output symbol table to standard output" << std::endl
145 << " --output-mode <item|dzn|json|checker>\n Create output according to output item "
146 "(default), or output compatible\n with dzn or json format, or for solution checking"
147 << std::endl
148 << " --output-objective\n Print value of objective function in dzn or json output"
149 << std::endl
150 << " --output-output-item\n Print the output item as a string in the dzn or json output"
151 << std::endl
152 << " -Werror\n Turn warnings into errors" << std::endl;
153}
154
155bool Flattener::processOption(int& i, std::vector<std::string>& argv,
156 const std::string& workingDir) {
157 CLOParser cop(i, argv);
158 string buffer;
159 int intBuffer;
160
161 if (cop.getOption("-I --search-dir", &buffer)) {
162 _includePaths.push_back(FileUtils::file_path(buffer + "/", workingDir));
163 } else if (cop.getOption("--no-typecheck")) {
164 _flags.typecheck = false;
165 } else if (cop.getOption("--instance-check-only")) {
166 _flags.instanceCheckOnly = true;
167 } else if (cop.getOption("-e --model-check-only")) {
168 _flags.modelCheckOnly = true;
169 } else if (cop.getOption("--model-interface-only")) {
170 _flags.modelInterfaceOnly = true;
171 } else if (cop.getOption("--model-types-only")) {
172 _flags.modelTypesOnly = true;
173 } else if (cop.getOption("-v --verbose")) {
174 _flags.verbose = true;
175 } else if (cop.getOption("--newfzn")) {
176 _flags.newfzn = true;
177 } else if (cop.getOption("--no-optimize --no-optimise")) {
178 _flags.optimize = false;
179 } else if (cop.getOption("--no-chain-compression")) {
180 _flags.chainCompression = false;
181 } else if (cop.getOption("--no-output-ozn -O-")) {
182 _flags.noOutputOzn = true;
183 } else if (cop.getOption("--output-base", &_flagOutputBase)) { // NOLINT: Allow repeated empty if
184 // Parsed by reference
185 } else if (cop.getOption(_fOutputByDefault ? "-o --fzn --output-to-file --output-fzn-to-file"
186 : "--fzn --output-fzn-to-file",
187 &buffer)) {
188 _flagOutputFzn = FileUtils::file_path(buffer, workingDir);
189 } else if (cop.getOption("--output-paths")) {
190 _fopts.collectMznPaths = true;
191 } else if (cop.getOption("--output-paths-to-file", &buffer)) {
192 _flagOutputPaths = FileUtils::file_path(buffer, workingDir);
193 _fopts.collectMznPaths = true;
194 } else if (cop.getOption("--output-to-stdout --output-fzn-to-stdout")) {
195 _flags.outputFznStdout = true;
196 } else if (cop.getOption("--output-ozn-to-stdout")) {
197 _flags.outputOznStdout = true;
198 } else if (cop.getOption("--output-paths-to-stdout")) {
199 _fopts.collectMznPaths = true;
200 _flags.outputPathsStdout = true;
201 } else if (cop.getOption("--output-detailed-timing")) {
202 _fopts.detailedTiming = true;
203 } else if (cop.getOption("--output-mode", &buffer)) {
204 if (buffer == "dzn") {
205 _flagOutputMode = FlatteningOptions::OUTPUT_DZN;
206 } else if (buffer == "json") {
207 _flagOutputMode = FlatteningOptions::OUTPUT_JSON;
208 } else if (buffer == "item") {
209 _flagOutputMode = FlatteningOptions::OUTPUT_ITEM;
210 } else if (buffer == "checker") {
211 _flagOutputMode = FlatteningOptions::OUTPUT_CHECKER;
212 } else {
213 return false;
214 }
215 } else if (cop.getOption("--output-objective")) {
216 _flags.outputObjective = true;
217 } else if (cop.getOption("--output-output-item")) {
218 _flags.outputOutputItem = true;
219 } else if (cop.getOption("- --input-from-stdin")) {
220 _flags.stdinInput = true;
221 } else if (cop.getOption("-d --data", &buffer)) {
222 auto last_dot = buffer.find_last_of('.');
223 if (last_dot == string::npos) {
224 return false;
225 }
226 auto extension = buffer.substr(last_dot, string::npos);
227 if (extension != ".dzn" && extension != ".json") {
228 return false;
229 }
230 _datafiles.push_back(FileUtils::file_path(buffer, workingDir));
231 } else if (cop.getOption("--stdlib-dir", &buffer)) {
232 _stdLibDir = FileUtils::file_path(buffer, workingDir);
233 } else if (cop.getOption("-G --globals-dir --mzn-globals-dir",
234 &_globalsDir)) { // NOLINT: Allow repeated empty if
235 // Parsed by reference
236 } else if (cop.getOption("-D --cmdline-data", &buffer)) {
237 _datafiles.push_back("cmd:/" + buffer);
238 } else if (cop.getOption("--allow-unbounded-vars")) {
239 _flags.allowUnboundedVars = true;
240 } else if (cop.getOption("--only-range-domains")) {
241 _flags.onlyRangeDomains = true;
242 } else if (cop.getOption("--no-MIPdomains")) { // internal
243 _flags.noMIPdomains = true;
244 } else if (cop.getOption("--MIPDMaxIntvEE",
245 &_optMIPDmaxIntvEE)) { // NOLINT: Allow repeated empty if
246 // Parsed by reference
247 } else if (cop.getOption("--MIPDMaxDensEE",
248 &_optMIPDmaxDensEE)) { // NOLINT: Allow repeated empty if
249 // Parsed by reference
250 } else if (cop.getOption("-Werror")) {
251 _flags.werror = true;
252 } else if (cop.getOption("--use-gecode")) {
253#ifdef HAS_GECODE
254 _flags.twoPass = true;
255 _flags.gecode = true;
256#else
257 _log << "warning: Gecode not available. Ignoring '--use-gecode'\n";
258#endif
259 } else if (cop.getOption("--sac")) {
260#ifdef HAS_GECODE
261 _flags.twoPass = true;
262 _flags.gecode = true;
263 _flags.sac = true;
264#else
265 _log << "warning: Gecode not available. Ignoring '--sac'\n";
266#endif
267
268 } else if (cop.getOption("--shave")) {
269#ifdef HAS_GECODE
270 _flags.twoPass = true;
271 _flags.gecode = true;
272 _flags.shave = true;
273#else
274 _log << "warning: Gecode not available. Ignoring '--shave'\n";
275#endif
276 } else if (cop.getOption("--two-pass")) {
277 _flags.twoPass = true;
278 } else if (cop.getOption("--pre-passes", &intBuffer)) {
279 if (intBuffer >= 0) {
280 _flagPrePasses = static_cast<unsigned int>(intBuffer);
281 }
282 } else if (cop.getOption("-O", &intBuffer)) {
283 switch (intBuffer) {
284 case 0: {
285 _flags.optimize = false;
286 break;
287 }
288 case 1: {
289 // Default settings
290 break;
291 }
292 case 2: {
293 _flags.twoPass = true;
294 break;
295 }
296 case 3: {
297 _flags.twoPass = true;
298 _flags.gecode = true;
299 break;
300 }
301 case 4: {
302 _flags.twoPass = true;
303 _flags.gecode = true;
304 _flags.shave = true;
305 break;
306 }
307 case 5: {
308 _flags.twoPass = true;
309 _flags.gecode = true;
310 _flags.sac = true;
311 break;
312 }
313 default: {
314 _log << "% Error: Unsupported optimisation level, cannot process -O" << intBuffer << "."
315 << std::endl;
316 return false;
317 }
318 }
319 // ozn options must be after the -O<n> optimisation options
320 } else if (cop.getOption("--ozn --output-ozn-to-file", &buffer)) {
321 _flagOutputOzn = FileUtils::file_path(buffer, workingDir);
322 } else if (cop.getOption("-g")) {
323 _flags.optimize = false;
324 _flags.twoPass = false;
325 _flags.gecode = false;
326 _flags.shave = false;
327 _flags.sac = false;
328 _fopts.recordDomainChanges = true;
329 } else if (string(argv[i]) == "--keep-paths") {
330 _flags.keepMznPaths = true;
331 _fopts.collectMznPaths = true;
332 } else if (string(argv[i]) == "--only-toplevel-presolve") {
333 _fopts.onlyToplevelPaths = true;
334 } else if (cop.getOption("--allow-multiple-assignments")) {
335 _flags.allowMultiAssign = true;
336 } else if (cop.getOption("--no-half-reifications")) {
337 _fopts.enableHalfReification = false;
338 } else if (string(argv[i]) == "--input-is-flatzinc") {
339 _isFlatzinc = true;
340 } else if (cop.getOption("--compile-solution-checker", &buffer)) {
341 if (buffer.length() >= 8 && buffer.substr(buffer.length() - 8, string::npos) == ".mzc.mzn") {
342 _flags.compileSolutionCheckModel = true;
343 _flags.modelCheckOnly = true;
344 _filenames.push_back(FileUtils::file_path(buffer, workingDir));
345 } else {
346 _log << "Error: solution checker model must have extension .mzc.mzn" << std::endl;
347 return false;
348 }
349 } else if (cop.getOption("-m --model", &buffer)) {
350 if (buffer.length() <= 4) {
351 return false;
352 }
353 auto extension = buffer.substr(buffer.length() - 4, string::npos);
354 auto isChecker =
355 buffer.length() > 8 && buffer.substr(buffer.length() - 8, string::npos) == ".mzc.mzn";
356 if ((extension == ".mzn" && !isChecker) || extension == ".fzn") {
357 if (extension == ".fzn") {
358 _isFlatzinc = true;
359 if (_fOutputByDefault) { // mzn2fzn mode
360 return false;
361 }
362 }
363 _filenames.push_back(FileUtils::file_path(buffer, workingDir));
364 return true;
365 }
366 _log << "Error: model must have extension .mzn (or .fzn)" << std::endl;
367 return false;
368 } else {
369 std::string input_file(argv[i]);
370 if (input_file.length() <= 4) {
371 return false;
372 }
373 size_t last_dot = input_file.find_last_of('.');
374 if (last_dot == string::npos) {
375 return false;
376 }
377 std::string extension = input_file.substr(last_dot, string::npos);
378 if (extension == ".mzc" ||
379 (input_file.length() >= 8 &&
380 input_file.substr(input_file.length() - 8, string::npos) == ".mzc.mzn")) {
381 _flagSolutionCheckModel = input_file;
382 } else if (extension == ".mzn" || extension == ".fzn") {
383 if (extension == ".fzn") {
384 _isFlatzinc = true;
385 if (_fOutputByDefault) { // mzn2fzn mode
386 return false;
387 }
388 }
389 _filenames.push_back(input_file);
390 } else if (extension == ".dzn" || extension == ".json") {
391 _datafiles.push_back(input_file);
392 } else {
393 if (_fOutputByDefault) {
394 _log << "Error: cannot handle file extension " << extension << "." << std::endl;
395 }
396 return false;
397 }
398 }
399 return true;
400}
401
402Flattener::Flattener(std::ostream& os, std::ostream& log, std::string stdlibDir)
403 : _os(os), _log(log), _stdLibDir(std::move(stdlibDir)) {}
404
405Flattener::~Flattener() {
406 if (_pEnv != nullptr) { // ??? TODO
407 if (_isFlatzinc) {
408 _pEnv->swap();
409 }
410 }
411}
412
413Env* Flattener::multiPassFlatten(const vector<unique_ptr<Pass> >& passes) {
414 Env& e = *getEnv();
415
416 Env* pre_env = &e;
417 size_t npasses = passes.size();
418 pre_env->envi().finalPassNumber = static_cast<unsigned int>(npasses);
419 Timer starttime;
420 bool verbose = false;
421 for (unsigned int i = 0; i < passes.size(); i++) {
422 pre_env->envi().currentPassNumber = i;
423 if (verbose) {
424 _log << "Start pass " << i << ":\n";
425 }
426
427 Env* out_env = passes[i]->run(pre_env, _log);
428 if (out_env == nullptr) {
429 return nullptr;
430 }
431 if (pre_env != &e && pre_env != out_env) {
432 delete pre_env;
433 }
434 pre_env = out_env;
435
436 if (verbose) {
437 _log << "Finish pass " << i << ": " << starttime.stoptime() << "\n";
438 }
439 }
440
441 return pre_env;
442}
443
444class FlattenTimeout {
445public:
446 FlattenTimeout(unsigned long long int t) { GC::setTimeout(t); }
447 ~FlattenTimeout() { GC::setTimeout(0); }
448};
449
450void Flattener::flatten(const std::string& modelString, const std::string& modelName) {
451 FlattenTimeout flatten_timeout(_fopts.timeout);
452 Timer flatten_time;
453 _starttime.reset();
454
455 if (_flags.verbose) {
456 printVersion(_log);
457 }
458
459 if (_filenames.empty() && !_flagSolutionCheckModel.empty()) {
460 // Compile solution check model as if it were a normal model
461 _filenames.push_back(_flagSolutionCheckModel);
462 _flagSolutionCheckModel = "";
463 }
464
465 if (_filenames.empty() && !_flags.stdinInput && modelString.empty()) {
466 throw Error("Error: no model file given.");
467 }
468
469 if (_stdLibDir.empty()) {
470 throw Error(
471 "Error: unknown minizinc standard library directory.\n"
472 "Specify --stdlib-dir on the command line or set the\n"
473 "MZN_STDLIB_DIR environment variable.");
474 }
475
476 if (!_globalsDir.empty()) {
477 _includePaths.insert(_includePaths.begin(), _stdLibDir + "/" + _globalsDir + "/");
478 }
479 _includePaths.push_back(_stdLibDir + "/std/");
480
481 for (auto& includePath : _includePaths) {
482 if (!FileUtils::directory_exists(includePath)) {
483 throw Error("Cannot access include directory " + includePath);
484 }
485 }
486
487 if (_flagOutputBase.empty()) {
488 if (_filenames.empty()) {
489 _flagOutputBase = "mznout";
490 } else {
491 _flagOutputBase = _filenames[0].substr(0, _filenames[0].length() - 4);
492 }
493 }
494
495 if (_filenames.end() != find(_filenames.begin(), _filenames.end(), _flagOutputFzn) ||
496 _datafiles.end() != find(_datafiles.begin(), _datafiles.end(), _flagOutputFzn)) {
497 _log << " WARNING: fzn filename '" << _flagOutputFzn << "' matches an input file, ignoring."
498 << endl;
499 _flagOutputFzn = "";
500 }
501 if (_filenames.end() != find(_filenames.begin(), _filenames.end(), _flagOutputOzn) ||
502 _datafiles.end() != find(_datafiles.begin(), _datafiles.end(), _flagOutputOzn)) {
503 _log << " WARNING: ozn filename '" << _flagOutputOzn << "' matches an input file, ignoring."
504 << endl;
505 _flagOutputOzn = "";
506 }
507
508 if (_fOutputByDefault) {
509 if (_flagOutputFzn.empty()) {
510 _flagOutputFzn = _flagOutputBase + ".fzn";
511 }
512 if (_flagOutputPaths.empty() && _fopts.collectMznPaths) {
513 _flagOutputPaths = _flagOutputBase + ".paths";
514 }
515 if (_flagOutputOzn.empty() && !_flags.noOutputOzn) {
516 _flagOutputOzn = _flagOutputBase + ".ozn";
517 }
518 }
519
520 {
521 std::stringstream errstream;
522
523 Model* m;
524 _pEnv.reset(new Env(nullptr, _os, _log));
525 Env* env = getEnv();
526
527 if (!_flags.compileSolutionCheckModel && !_flagSolutionCheckModel.empty()) {
528 // Extract variables to check from solution check model
529 if (_flags.verbose) {
530 _log << "Parsing solution checker model " << _flagSolutionCheckModel << " ..." << endl;
531 }
532 bool isCompressedChecker =
533 _flagSolutionCheckModel.size() >= 4 &&
534 _flagSolutionCheckModel.substr(_flagSolutionCheckModel.size() - 4) == ".mzc";
535 std::vector<std::string> smm_model({_flagSolutionCheckModel});
536 Model* smm = parse(*env, smm_model, _datafiles, "", "", _includePaths, _isFlatzinc, false,
537 false, _flags.verbose, errstream);
538 if (_flags.verbose) {
539 _log << " done parsing (" << _starttime.stoptime() << ")" << std::endl;
540 }
541 if (smm != nullptr) {
542 _log << errstream.str();
543 errstream.str("");
544 std::ostringstream smm_oss;
545 std::ostringstream smm_stats_oss;
546 Printer p(smm_oss, 0, false);
547 p.print(smm);
548 Env smm_env(smm);
549 GCLock lock;
550 vector<TypeError> typeErrors;
551 try {
552 MiniZinc::typecheck(smm_env, smm, typeErrors, true, false, true);
553 if (!typeErrors.empty()) {
554 if (!isCompressedChecker) {
555 for (auto& typeError : typeErrors) {
556 if (_flags.verbose) {
557 _log << std::endl;
558 }
559 _log << typeError.loc() << ":" << std::endl;
560 _log << typeError.what() << ": " << typeError.msg() << std::endl;
561 }
562 }
563 throw Error("multiple type errors");
564 }
565 for (auto& i : *smm) {
566 if (auto* vdi = i->dynamicCast<VarDeclI>()) {
567 if (vdi->e()->e() == nullptr) {
568 env->envi().checkVars.emplace_back(vdi->e());
569 } else if (vdi->e()->ann().contains(constants().ann.rhs_from_assignment)) {
570 smm_stats_oss << *vdi;
571 }
572 }
573 }
574 smm->compact();
575 std::string smm_compressed =
576 FileUtils::encode_base64(FileUtils::deflate_string(smm_oss.str()));
577 auto* ti = new TypeInst(Location().introduce(), Type::parstring(), nullptr);
578 auto* checkString =
579 new VarDecl(Location().introduce(), ti, ASTString("_mzn_solution_checker"),
580 new StringLit(Location().introduce(), smm_compressed));
581 auto* checkStringI = new VarDeclI(Location().introduce(), checkString);
582 env->output()->addItem(checkStringI);
583
584 for (FunctionIterator it = smm->functions().begin(); it != smm->functions().end(); ++it) {
585 if (it->id() == "checkStatistics") {
586 smm_stats_oss << *it;
587 smm_stats_oss << "int: mzn_stats_failures;\n";
588 smm_stats_oss << "int: mzn_stats_solutions;\n";
589 smm_stats_oss << "int: mzn_stats_nodes;\n";
590 smm_stats_oss << "int: mzn_stats_time;\n";
591 smm_stats_oss << "output "
592 "[checkStatistics(mzn_stats_failures,mzn_stats_solutions,mzn_stats_"
593 "nodes,mzn_stats_time)];\n";
594 std::string smm_stats_compressed =
595 FileUtils::encode_base64(FileUtils::deflate_string(smm_stats_oss.str()));
596 auto* ti = new TypeInst(Location().introduce(), Type::parstring(), nullptr);
597 auto* checkStatsString =
598 new VarDecl(Location().introduce(), ti, ASTString("_mzn_stats_checker"),
599 new StringLit(Location().introduce(), smm_stats_compressed));
600 auto* checkStatsStringI = new VarDeclI(Location().introduce(), checkStatsString);
601 env->output()->addItem(checkStatsStringI);
602 }
603 }
604 } catch (TypeError& e) {
605 if (isCompressedChecker) {
606 _log << "Warning: type error in solution checker model\n";
607 } else {
608 throw;
609 }
610 }
611 } else {
612 if (isCompressedChecker) {
613 _log << "Warning: syntax error in solution checker model\n";
614 } else {
615 _log << errstream.str();
616 throw Error("parse error");
617 }
618 }
619 }
620
621 if (_flags.compileSolutionCheckModel) {
622 if (!modelString.empty()) {
623 throw Error("Cannot compile solution checker model with additional model inputs.");
624 }
625 if (_flags.stdinInput) {
626 throw Error(
627 "Cannot compile solution checker model with additional model from standard input.");
628 }
629 if (_filenames.size() != 1) {
630 throw Error("Cannot compile solution checker model with more than one model given.");
631 }
632 }
633
634 if (!_flagSolutionCheckModel.empty() && _filenames.empty()) {
635 throw Error("Cannot run solution checker without model.");
636 }
637
638 std::string modelText = modelString;
639 if (_flags.stdinInput) {
640 std::string input =
641 std::string(istreambuf_iterator<char>(std::cin), istreambuf_iterator<char>());
642 modelText += input;
643 }
644
645 if (_flags.verbose) {
646 _log << "Parsing file(s) ";
647 for (int i = 0; i < _filenames.size(); ++i) {
648 _log << (i == 0 ? "" : ", '") << _filenames[i] << '\'';
649 }
650 for (const auto& sFln : _datafiles) {
651 _log << ", '" << sFln << '\'';
652 }
653 _log << " ..." << std::endl;
654 }
655 errstream.str("");
656 m = parse(*env, _filenames, _datafiles, modelText, modelName.empty() ? "stdin" : modelName,
657 _includePaths, _isFlatzinc, false, false, _flags.verbose, errstream);
658 if (!_globalsDir.empty()) {
659 _includePaths.erase(_includePaths.begin());
660 }
661 if (m == nullptr) {
662 throw Error(errstream.str());
663 }
664 _log << errstream.str();
665 env->model(m);
666 if (_flags.typecheck) {
667 if (_flags.verbose) {
668 _log << " done parsing (" << _starttime.stoptime() << ")" << std::endl;
669 }
670
671 if (_flags.instanceCheckOnly || _flags.modelCheckOnly || _flags.modelInterfaceOnly ||
672 _flags.modelTypesOnly) {
673 std::ostringstream compiledSolutionCheckModel;
674 if (_flags.compileSolutionCheckModel) {
675 Printer p(compiledSolutionCheckModel, 0);
676 p.print(m);
677 }
678 GCLock lock;
679 vector<TypeError> typeErrors;
680 MiniZinc::typecheck(
681 *env, m, typeErrors,
682 _flags.modelTypesOnly || _flags.modelInterfaceOnly || _flags.modelCheckOnly,
683 _flags.allowMultiAssign);
684 if (!typeErrors.empty()) {
685 for (auto& typeError : typeErrors) {
686 if (_flags.verbose) {
687 _log << std::endl;
688 }
689 _log << typeError.loc() << ":" << std::endl;
690 _log << typeError.what() << ": " << typeError.msg() << std::endl;
691 }
692 throw Error("multiple type errors");
693 }
694 if (_flags.modelInterfaceOnly) {
695 MiniZinc::output_model_interface(*env, m, _os, _includePaths);
696 }
697 if (_flags.modelTypesOnly) {
698 MiniZinc::output_model_variable_types(*env, m, _os, _includePaths);
699 }
700 if (_flags.compileSolutionCheckModel) {
701 std::string mzc(FileUtils::deflate_string(compiledSolutionCheckModel.str()));
702 mzc = FileUtils::encode_base64(mzc);
703 std::string mzc_filename = _filenames[0].substr(0, _filenames[0].size() - 4);
704 if (_flags.verbose) {
705 _log << "Write solution checker to " << mzc_filename << "\n";
706 }
707 std::ofstream mzc_f(FILE_PATH(mzc_filename));
708 mzc_f << mzc;
709 mzc_f.close();
710 }
711 status = SolverInstance::NONE;
712 } else {
713 if (_isFlatzinc) {
714 GCLock lock;
715 vector<TypeError> typeErrors;
716 MiniZinc::typecheck(*env, m, typeErrors,
717 _flags.modelCheckOnly || _flags.modelInterfaceOnly,
718 _flags.allowMultiAssign, true);
719 if (!typeErrors.empty()) {
720 for (auto& typeError : typeErrors) {
721 if (_flags.verbose) {
722 _log << std::endl;
723 }
724 _log << typeError.loc() << ":" << std::endl;
725 _log << typeError.what() << ": " << typeError.msg() << std::endl;
726 }
727 throw Error("multiple type errors");
728 }
729 MiniZinc::register_builtins(*env);
730 env->swap();
731 populate_output(*env);
732 } else {
733 if (_flags.verbose) {
734 _log << "Flattening ...";
735 }
736
737 _fopts.onlyRangeDomains = _flags.onlyRangeDomains;
738 _fopts.verbose = _flags.verbose;
739 _fopts.outputMode = _flagOutputMode;
740 _fopts.outputObjective = _flags.outputObjective;
741 _fopts.outputOutputItem = _flags.outputOutputItem;
742 _fopts.hasChecker = !_flagSolutionCheckModel.empty();
743#ifdef HAS_GECODE
744 GecodeOptions gopts;
745 gopts.onlyRangeDomains = _flags.onlyRangeDomains;
746 gopts.sac = _flags.sac;
747 gopts.allowUnboundedVars = _flags.allowUnboundedVars;
748 gopts.shave = _flags.shave;
749 gopts.printStatistics = _flags.statistics;
750 gopts.prePasses = _flagPrePasses;
751#endif
752 FlatteningOptions pass_opts = _fopts;
753 CompilePassFlags cfs;
754 cfs.noMIPdomains = _flags.noMIPdomains;
755 cfs.verbose = _flags.verbose;
756 cfs.statistics = _flags.statistics;
757 cfs.optimize = _flags.optimize;
758 cfs.chainCompression = _flags.chainCompression;
759 cfs.newfzn = _flags.newfzn;
760 cfs.werror = _flags.werror;
761 cfs.modelCheckOnly = _flags.modelCheckOnly;
762 cfs.modelInterfaceOnly = _flags.modelInterfaceOnly;
763 cfs.allowMultiAssign = _flags.allowMultiAssign;
764
765 std::vector<unique_ptr<Pass> > managed_passes;
766
767 if (_flags.twoPass) {
768 std::string library = _stdLibDir + (_flags.gecode ? "/gecode_presolver/" : "/std/");
769 bool differentLibrary = (library != _stdLibDir + "/" + _globalsDir + "/");
770 managed_passes.emplace_back(new CompilePass(env, pass_opts, cfs, library, _includePaths,
771 true, differentLibrary));
772#ifdef HAS_GECODE
773 if (_flags.gecode) {
774 managed_passes.emplace_back(new GecodePass(&gopts));
775 }
776#endif
777 }
778 managed_passes.emplace_back(new CompilePass(env, _fopts, cfs,
779 _stdLibDir + "/" + _globalsDir + "/",
780 _includePaths, _flags.twoPass, false));
781
782 Env* out_env = multiPassFlatten(managed_passes);
783 if (out_env == nullptr) {
784 exit(EXIT_FAILURE);
785 }
786
787 if (out_env != env) {
788 _pEnv.reset(out_env);
789 }
790 env = out_env;
791 if (_flags.verbose) {
792 _log << " done (" << _starttime.stoptime() << "),"
793 << " max stack depth " << env->maxCallStack() << std::endl;
794 }
795 }
796
797 if (_flags.statistics) {
798 FlatModelStatistics stats = statistics(*env);
799 _os << "% Generated FlatZinc statistics:\n";
800
801 _os << "%%%mzn-stat: paths=" << env->envi().getPathMap().size() << endl;
802
803 if (stats.n_bool_vars != 0) {
804 _os << "%%%mzn-stat: flatBoolVars=" << stats.n_bool_vars << endl;
805 }
806 if (stats.n_int_vars != 0) {
807 _os << "%%%mzn-stat: flatIntVars=" << stats.n_int_vars << endl;
808 }
809 if (stats.n_float_vars != 0) {
810 _os << "%%%mzn-stat: flatFloatVars=" << stats.n_float_vars << endl;
811 }
812 if (stats.n_set_vars != 0) {
813 _os << "%%%mzn-stat: flatSetVars=" << stats.n_set_vars << endl;
814 }
815
816 if (stats.n_bool_ct != 0) {
817 _os << "%%%mzn-stat: flatBoolConstraints=" << stats.n_bool_ct << endl;
818 }
819 if (stats.n_int_ct != 0) {
820 _os << "%%%mzn-stat: flatIntConstraints=" << stats.n_int_ct << endl;
821 }
822 if (stats.n_float_ct != 0) {
823 _os << "%%%mzn-stat: flatFloatConstraints=" << stats.n_float_ct << endl;
824 }
825 if (stats.n_set_ct != 0) {
826 _os << "%%%mzn-stat: flatSetConstraints=" << stats.n_set_ct << endl;
827 }
828
829 if (stats.n_reif_ct != 0) {
830 _os << "%%%mzn-stat: evaluatedReifiedConstraints=" << stats.n_reif_ct << endl;
831 }
832 if (stats.n_imp_ct != 0) {
833 _os << "%%%mzn-stat: evaluatedHalfReifiedConstraints=" << stats.n_imp_ct << endl;
834 }
835
836 if (stats.n_imp_del != 0) {
837 _os << "%%%mzn-stat: eliminatedImplications=" << stats.n_imp_del << endl;
838 }
839 if (stats.n_lin_del != 0) {
840 _os << "%%%mzn-stat: eliminatedLinearConstraints=" << stats.n_lin_del << endl;
841 }
842
843 /// Objective / SAT. These messages are used by mzn-test.py.
844 SolveI* solveItem = env->flat()->solveItem();
845 if (solveItem->st() != SolveI::SolveType::ST_SAT) {
846 if (solveItem->st() == SolveI::SolveType::ST_MAX) {
847 _os << "%%%mzn-stat: method=\"maximize\"" << endl;
848 } else {
849 _os << "%%%mzn-stat: method=\"minimize\"" << endl;
850 }
851 } else {
852 _os << "%%%mzn-stat: method=\"satisfy\"" << endl;
853 }
854
855 _os << "%%%mzn-stat: flatTime=" << flatten_time.s() << endl;
856 _os << "%%%mzn-stat-end" << endl << endl;
857 }
858
859 if (_flags.outputPathsStdout) {
860 if (_flags.verbose) {
861 _log << "Printing Paths to stdout ..." << std::endl;
862 }
863 PathFilePrinter pfp(_os, env->envi());
864 pfp.print(env->flat());
865 if (_flags.verbose) {
866 _log << " done (" << _starttime.stoptime() << ")" << std::endl;
867 }
868 } else if (!_flagOutputPaths.empty()) {
869 if (_flags.verbose) {
870 _log << "Printing Paths to '" << _flagOutputPaths << "' ..." << std::flush;
871 }
872 std::ofstream ofs(FILE_PATH(_flagOutputPaths), ios::out);
873 check_io_status(ofs.good(), " I/O error: cannot open fzn output file. ");
874 PathFilePrinter pfp(ofs, env->envi());
875 pfp.print(env->flat());
876 check_io_status(ofs.good(), " I/O error: cannot write fzn output file. ");
877 ofs.close();
878 if (_flags.verbose) {
879 _log << " done (" << _starttime.stoptime() << ")" << std::endl;
880 }
881 }
882
883 if ((_fopts.collectMznPaths || _flags.twoPass) && !_flags.keepMznPaths) {
884 class RemovePathAnnotations : public ItemVisitor {
885 public:
886 static void removePath(Annotation& a) { a.removeCall(constants().ann.mzn_path); }
887 static void vVarDeclI(VarDeclI* vdi) { removePath(vdi->e()->ann()); }
888 static void vConstraintI(ConstraintI* ci) { removePath(ci->e()->ann()); }
889 static void vSolveI(SolveI* si) {
890 removePath(si->ann());
891 if (Expression* e = si->e()) {
892 removePath(e->ann());
893 }
894 }
895 } removePaths;
896 iter_items<RemovePathAnnotations>(removePaths, env->flat());
897 }
898
899 if (_flags.outputFznStdout) {
900 if (_flags.verbose) {
901 _log << "Printing FlatZinc to stdout ..." << std::endl;
902 }
903 Printer p(_os, 0);
904 p.print(env->flat());
905 if (_flags.verbose) {
906 _log << " done (" << _starttime.stoptime() << ")" << std::endl;
907 }
908 } else if (!_flagOutputFzn.empty()) {
909 if (_flags.verbose) {
910 _log << "Printing FlatZinc to '" << _flagOutputFzn << "' ..." << std::flush;
911 }
912 std::ofstream ofs(FILE_PATH(_flagOutputFzn), ios::out);
913 check_io_status(ofs.good(), " I/O error: cannot open fzn output file. ");
914 Printer p(ofs, 0);
915 p.print(env->flat());
916 check_io_status(ofs.good(), " I/O error: cannot write fzn output file. ");
917 ofs.close();
918 if (_flags.verbose) {
919 _log << " done (" << _starttime.stoptime() << ")" << std::endl;
920 }
921 }
922 if (!_flags.noOutputOzn) {
923 if (_flags.outputOznStdout) {
924 if (_flags.verbose) {
925 _log << "Printing .ozn to stdout ..." << std::endl;
926 }
927 Printer p(_os, 0);
928 p.print(env->output());
929 if (_flags.verbose) {
930 _log << " done (" << _starttime.stoptime() << ")" << std::endl;
931 }
932 } else if (!_flagOutputOzn.empty()) {
933 if (_flags.verbose) {
934 _log << "Printing .ozn to '" << _flagOutputOzn << "' ..." << std::flush;
935 }
936 std::ofstream ofs(FILE_PATH(_flagOutputOzn), std::ios::out);
937 check_io_status(ofs.good(), " I/O error: cannot open ozn output file. ");
938 Printer p(ofs, 0);
939 p.print(env->output());
940 check_io_status(ofs.good(), " I/O error: cannot write ozn output file. ");
941 ofs.close();
942 if (_flags.verbose) {
943 _log << " done (" << _starttime.stoptime() << ")" << std::endl;
944 }
945 }
946 }
947 }
948 } else { // !flag_typecheck
949 Printer p(_os);
950 p.print(m);
951 }
952 }
953
954 if (getEnv()->envi().failed()) {
955 status = SolverInstance::UNSAT;
956 }
957
958 if (_flags.verbose) {
959 size_t mem = GC::maxMem();
960 if (mem < 1024) {
961 _log << "Maximum memory " << mem << " bytes";
962 } else if (mem < 1024 * 1024) {
963 _log << "Maximum memory " << mem / 1024 << " Kbytes";
964 } else {
965 _log << "Maximum memory " << mem / (1024 * 1024) << " Mbytes";
966 }
967 _log << "." << std::endl;
968 }
969}
970
971void Flattener::printStatistics(ostream& /*os*/) {}