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#endif
27
28using namespace std;
29using namespace MiniZinc;
30
31void Flattener::printVersion(ostream& os) {
32 os << "MiniZinc to FlatZinc converter, version " << MZN_VERSION_MAJOR << "." << MZN_VERSION_MINOR
33 << "." << MZN_VERSION_PATCH;
34 if (!std::string(MZN_BUILD_REF).empty()) {
35 os << ", build " << MZN_BUILD_REF;
36 }
37 os << std::endl;
38 os << "Copyright (C) 2014-" << string(__DATE__).substr(7, 4)
39 << " Monash University, NICTA, Data61" << std::endl;
40}
41
42void Flattener::printHelp(ostream& os) {
43 os << std::endl
44 << "Flattener input options:" << std::endl
45 << " --ignore-stdlib\n Ignore the standard libraries stdlib.mzn and builtins.mzn"
46 << std::endl
47 << " --instance-check-only\n Check the model instance (including data) for errors, but do "
48 "not\n convert to FlatZinc."
49 << std::endl
50 << " -e, --model-check-only\n Check the model (without requiring data) for errors, but do "
51 "not\n convert to FlatZinc."
52 << std::endl
53 << " --model-interface-only\n Only extract parameters and output variables." << std::endl
54 << " --model-types-only\n Only output variable (enum) type information." << std::endl
55 << " --no-optimize\n Do not optimize the FlatZinc" << std::endl
56 << " --no-chain-compression\n Do not simplify chains of implication constraints."
57 << std::endl
58 << " -d <file>, --data <file>\n File named <file> contains data used by the model."
59 << std::endl
60 << " -D <data>, --cmdline-data <data>\n Include the given data assignment in the model."
61 << std::endl
62 << " --stdlib-dir <dir>\n Path to MiniZinc standard library directory" << std::endl
63 << " -G <dir>, --globals-dir <dir>, --mzn-globals-dir <dir>\n Search for included globals "
64 "in <stdlib>/<dir>."
65 << std::endl
66 << " -, --input-from-stdin\n Read problem from standard input" << std::endl
67 << " -I <dir>, --search-dir <dir>\n Additionally search for included files in <dir>."
68 << std::endl
69 << " -D \"fMIPdomains=true\"\n Switch on MIPDomain Unification" << std::endl
70 << " --MIPDMaxIntvEE <n>\n MIPD: max integer domain subinterval length to enforce "
71 "equality encoding, default "
72 << opt_MIPDmaxIntvEE << std::endl
73 << " --MIPDMaxDensEE <n>\n MIPD: max domain cardinality to N subintervals ratio\n to "
74 "enforce equality encoding, default "
75 << opt_MIPDmaxDensEE << ", either condition triggers" << std::endl
76 << " --only-range-domains\n When no MIPdomains: all domains contiguous, holes replaced by "
77 "inequalities"
78 << std::endl
79 << " --allow-multiple-assignments\n Allow multiple assignments to the same variable (e.g. "
80 "in dzn)"
81 << std::endl
82 << " --no-half-reifications\n Only use fully reified constraints, even when a half "
83 "reified constraint is defined."
84 << std::endl
85 << " --compile-solution-checker <file>.mzc.mzn\n Compile solution checker model"
86 << std::endl
87 << std::endl
88 << "Flattener two-pass options:" << std::endl
89 << " --two-pass\n Flatten twice to make better flattening decisions for the target"
90 << std::endl
91#ifdef HAS_GECODE
92 << " --use-gecode\n Perform root-node-propagation with Gecode (adds --two-pass)"
93 << std::endl
94 << " --shave\n Probe bounds of all variables at the root node (adds --use-gecode)"
95 << std::endl
96 << " --sac\n Probe values of all variables at the root node (adds --use-gecode)"
97 << std::endl
98 << " --pre-passes <n>\n Number of times to apply shave/sac pass (0 = fixed-point, 1 = "
99 "default)"
100 << std::endl
101#endif
102 << " -O<n>\n Two-pass optimisation levels:" << std::endl
103 << " -O0: Disable optimize (--no-optimize) -O1: Single pass (default)" << std::endl
104 << " -O2: Same as: --two-pass"
105#ifdef HAS_GECODE
106 << " -O3: Same as: --use-gecode" << std::endl
107 << " -O4: Same as: --shave -O5: Same as: --sac" << std::endl
108#else
109 << "\n -O3,4,5: Disabled [Requires MiniZinc with built-in Gecode support]" << std::endl
110#endif
111 << " -g\n Debug mode: Forces -O0 and records all domain changes as constraints instead of "
112 "applying them"
113 << std::endl
114 << std::endl;
115 os << "Flattener output options:" << std::endl
116 << " --no-output-ozn, -O-\n Do not output ozn file" << std::endl
117 << " --output-base <name>\n Base name for output files" << std::endl
118 << (fOutputByDefault
119 ? " -o <file>, --fzn <file>, --output-to-file <file>, --output-fzn-to-file <file>\n"
120 : " --fzn <file>, --output-fzn-to-file <file>\n")
121 << " Filename for generated FlatZinc output" << std::endl
122 << " -O, --ozn, --output-ozn-to-file <file>\n Filename for model output specification "
123 "(-O- for none)"
124 << std::endl
125 << " --keep-paths\n Don't remove path annotations from FlatZinc" << std::endl
126 << " --output-paths\n Output a symbol table (.paths file)" << std::endl
127 << " --output-paths-to-file <file>\n Output a symbol table (.paths file) to <file>"
128 << std::endl
129 << " --output-to-stdout, --output-fzn-to-stdout\n Print generated FlatZinc to standard "
130 "output"
131 << std::endl
132 << " --output-ozn-to-stdout\n Print model output specification to standard output"
133 << std::endl
134 << " --output-paths-to-stdout\n Output symbol table to standard output" << std::endl
135 << " --output-mode <item|dzn|json>\n Create output according to output item (default), or "
136 "output compatible\n with dzn or json format"
137 << std::endl
138 << " --output-objective\n Print value of objective function in dzn or json output"
139 << std::endl
140 << " --output-output-item\n Print the output item as a string in the dzn or json output"
141 << std::endl
142 << " -Werror\n Turn warnings into errors" << std::endl;
143}
144
145bool Flattener::processOption(int& i, std::vector<std::string>& argv) {
146 CLOParser cop(i, argv);
147 string buffer;
148
149 if (cop.getOption("-I --search-dir", &buffer)) {
150 includePaths.push_back(buffer + string("/"));
151 } else if (cop.getOption("--ignore-stdlib")) {
152 flag_ignoreStdlib = true;
153 } else if (cop.getOption("--no-typecheck")) {
154 flag_typecheck = false;
155 } else if (cop.getOption("--instance-check-only")) {
156 flag_instance_check_only = true;
157 } else if (cop.getOption("-e --model-check-only")) {
158 flag_model_check_only = true;
159 } else if (cop.getOption("--model-interface-only")) {
160 flag_model_interface_only = true;
161 } else if (cop.getOption("--model-types-only")) {
162 flag_model_types_only = true;
163 } else if (cop.getOption("-v --verbose")) {
164 flag_verbose = true;
165 } else if (string(argv[i]) == string("--newfzn")) {
166 flag_newfzn = true;
167 } else if (cop.getOption("--no-optimize --no-optimise")) {
168 flag_optimize = false;
169 } else if (cop.getOption("--no-chain-compression")) {
170 flag_chain_compression = false;
171 } else if (cop.getOption("--no-output-ozn -O-")) {
172 flag_no_output_ozn = true;
173 } else if (cop.getOption("--output-base", &flag_output_base)) {
174 } else if (cop.getOption(fOutputByDefault ? "-o --fzn --output-to-file --output-fzn-to-file"
175 : "--fzn --output-fzn-to-file",
176 &flag_output_fzn)) {
177 } else if (cop.getOption("--output-paths-to-file", &flag_output_paths)) {
178 fopts.collect_mzn_paths = true;
179 } else if (cop.getOption("--output-paths")) {
180 fopts.collect_mzn_paths = true;
181 } else if (cop.getOption("--output-to-stdout --output-fzn-to-stdout")) {
182 flag_output_fzn_stdout = true;
183 } else if (cop.getOption("--output-ozn-to-stdout")) {
184 flag_output_ozn_stdout = true;
185 } else if (cop.getOption("--output-paths-to-stdout")) {
186 fopts.collect_mzn_paths = true;
187 flag_output_paths_stdout = true;
188 } else if (cop.getOption("--output-mode", &buffer)) {
189 if (buffer == "dzn") {
190 flag_output_mode = FlatteningOptions::OUTPUT_DZN;
191 } else if (buffer == "json") {
192 flag_output_mode = FlatteningOptions::OUTPUT_JSON;
193 } else if (buffer == "item") {
194 flag_output_mode = FlatteningOptions::OUTPUT_ITEM;
195 } else {
196 return false;
197 }
198 } else if (cop.getOption("--output-objective")) {
199 flag_output_objective = true;
200 } else if (cop.getOption("--output-output-item")) {
201 flag_output_output_item = true;
202 } else if (cop.getOption("- --input-from-stdin")) {
203 flag_stdinInput = true;
204 } else if (cop.getOption("-d --data", &buffer)) {
205 if (buffer.length() <= 4 || buffer.substr(buffer.length() - 4, string::npos) != ".dzn")
206 return false;
207 datafiles.push_back(buffer);
208 } else if (cop.getOption("--stdlib-dir", &std_lib_dir)) {
209 } else if (cop.getOption("-G --globals-dir --mzn-globals-dir", &globals_dir)) {
210 } else if (cop.getOption("-D --cmdline-data", &buffer)) {
211 datafiles.push_back("cmd:/" + buffer);
212 } else if (cop.getOption("--allow-unbounded-vars")) {
213 flag_allow_unbounded_vars = true;
214 } else if (cop.getOption("--only-range-domains")) {
215 flag_only_range_domains = true;
216 } else if (cop.getOption("--no-MIPdomains")) { // internal
217 flag_noMIPdomains = true;
218 } else if (cop.getOption("--MIPDMaxIntvEE", &opt_MIPDmaxIntvEE)) {
219 } else if (cop.getOption("--MIPDMaxDensEE", &opt_MIPDmaxDensEE)) {
220 } else if (cop.getOption("-Werror")) {
221 flag_werror = true;
222 } else if (string(argv[i]) == "--use-gecode") {
223#ifdef HAS_GECODE
224 flag_two_pass = true;
225 flag_gecode = true;
226#else
227 log << "warning: Gecode not available. Ignoring '--use-gecode'\n";
228#endif
229 } else if (string(argv[i]) == "--sac") {
230#ifdef HAS_GECODE
231 flag_two_pass = true;
232 flag_gecode = true;
233 flag_sac = true;
234#else
235 log << "warning: Gecode not available. Ignoring '--sac'\n";
236#endif
237
238 } else if (string(argv[i]) == "--shave") {
239#ifdef HAS_GECODE
240 flag_two_pass = true;
241 flag_gecode = true;
242 flag_shave = true;
243#else
244 log << "warning: Gecode not available. Ignoring '--shave'\n";
245#endif
246 } else if (string(argv[i]) == "--two-pass") {
247 flag_two_pass = true;
248 } else if (string(argv[i]) == "--npass") {
249 i++;
250 if (i == argv.size()) return false;
251 log << "warning: --npass option is deprecated --two-pass\n";
252 int passes = atoi(argv[i].c_str());
253 if (passes == 1)
254 flag_two_pass = false;
255 else if (passes == 2)
256 flag_two_pass = true;
257 } else if (string(argv[i]) == "--pre-passes") {
258 i++;
259 if (i == argv.size()) return false;
260 int passes = atoi(argv[i].c_str());
261 if (passes >= 0) {
262 flag_pre_passes = static_cast<unsigned int>(passes);
263 }
264 } else if (string(argv[i]) == "-O0") {
265 flag_optimize = false;
266 } else if (string(argv[i]) == "-O1") {
267 // Default settings
268 } else if (string(argv[i]) == "-O2") {
269 flag_two_pass = true;
270#ifdef HAS_GECODE
271 } else if (string(argv[i]) == "-O3") {
272 flag_two_pass = true;
273 flag_gecode = true;
274 } else if (string(argv[i]) == "-O4") {
275 flag_two_pass = true;
276 flag_gecode = true;
277 flag_shave = true;
278 } else if (string(argv[i]) == "-O5") {
279 flag_two_pass = true;
280 flag_gecode = true;
281 flag_sac = true;
282#else
283 } else if (string(argv[i]) == "-O3" || string(argv[i]) == "-O4" || string(argv[i]) == "-O5") {
284 log << "% Warning: This compiler does not have Gecode builtin, cannot process -O3,-O4,-O5.\n";
285 return false;
286#endif
287 // ozn options must be after the -O<n> optimisation options
288 } else if (cop.getOption("-O --ozn --output-ozn-to-file", &flag_output_ozn)) {
289 } else if (string(argv[i]) == "-g") {
290 flag_optimize = false;
291 flag_two_pass = false;
292 flag_gecode = false;
293 flag_shave = false;
294 flag_sac = false;
295 fopts.record_domain_changes = true;
296 } else if (string(argv[i]) == "--keep-paths") {
297 flag_keep_mzn_paths = true;
298 fopts.collect_mzn_paths = true;
299 } else if (string(argv[i]) == "--only-toplevel-presolve") {
300 fopts.only_toplevel_paths = true;
301 } else if (cop.getOption("--allow-multiple-assignments")) {
302 flag_allow_multi_assign = true;
303 } else if (cop.getOption("--no-half-reifications")) {
304 fopts.enable_imp = false;
305 } else if (string(argv[i]) == "--input-is-flatzinc") {
306 is_flatzinc = true;
307 } else if (cop.getOption("--compile-solution-checker", &buffer)) {
308 if (buffer.length() >= 8 && buffer.substr(buffer.length() - 8, string::npos) == ".mzc.mzn") {
309 flag_compile_solution_check_model = true;
310 flag_model_check_only = true;
311 filenames.push_back(buffer);
312 } else {
313 log << "Error: solution checker model must have extension .mzc.mzn" << std::endl;
314 return false;
315 }
316 } else {
317 std::string input_file(argv[i]);
318 if (input_file.length() <= 4) {
319 return false;
320 }
321 size_t last_dot = input_file.find_last_of('.');
322 if (last_dot == string::npos) {
323 return false;
324 }
325 std::string extension = input_file.substr(last_dot, string::npos);
326 if (extension == ".mzc" ||
327 (input_file.length() >= 8 &&
328 input_file.substr(input_file.length() - 8, string::npos) == ".mzc.mzn")) {
329 flag_solution_check_model = input_file;
330 } else if (extension == ".mzn" || extension == ".fzn") {
331 if (extension == ".fzn") {
332 is_flatzinc = true;
333 if (fOutputByDefault) // mzn2fzn mode
334 return false;
335 }
336 filenames.push_back(input_file);
337 } else if (extension == ".dzn" || extension == ".json") {
338 datafiles.push_back(input_file);
339 } else {
340 if (fOutputByDefault)
341 log << "Error: cannot handle file extension " << extension << "." << std::endl;
342 return false;
343 }
344 }
345 return true;
346}
347
348Flattener::Flattener(std::ostream& os_, std::ostream& log_, const std::string& stdlibDir)
349 : os(os_), log(log_), std_lib_dir(stdlibDir) {}
350
351Flattener::~Flattener() {
352 if (pEnv.get()) { // ??? TODO
353 if (is_flatzinc) {
354 pEnv->swap();
355 }
356 }
357}
358
359Env* Flattener::multiPassFlatten(const vector<unique_ptr<Pass> >& passes) {
360 Env& e = *getEnv();
361
362 Env* pre_env = &e;
363 size_t npasses = passes.size();
364 pre_env->envi().final_pass_no = static_cast<unsigned int>(npasses);
365 Timer starttime;
366 bool verbose = false;
367 for (unsigned int i = 0; i < passes.size(); i++) {
368 pre_env->envi().current_pass_no = i;
369 if (verbose) log << "Start pass " << i << ":\n";
370
371 Env* out_env = passes[i]->run(pre_env, log);
372 if (out_env == nullptr) return nullptr;
373 if (pre_env != &e && pre_env != out_env) {
374 delete pre_env;
375 }
376 pre_env = out_env;
377
378 if (verbose) log << "Finish pass " << i << ": " << starttime.stoptime() << "\n";
379 }
380
381 return pre_env;
382}
383
384class FlattenTimeout {
385public:
386 FlattenTimeout(unsigned long long int t) { GC::setTimeout(t); }
387 ~FlattenTimeout(void) { GC::setTimeout(0); }
388};
389
390void Flattener::flatten(const std::string& modelString, const std::string& modelName) {
391 FlattenTimeout flatten_timeout(fopts.timeout);
392 Timer flatten_time;
393 starttime.reset();
394
395 if (flag_verbose) printVersion(log);
396
397 if (filenames.empty() && !flag_solution_check_model.empty()) {
398 // Compile solution check model as if it were a normal model
399 filenames.push_back(flag_solution_check_model);
400 flag_solution_check_model = "";
401 }
402
403 if (filenames.empty() && !flag_stdinInput && modelString.empty()) {
404 throw Error("Error: no model file given.");
405 }
406
407 if (std_lib_dir == "") {
408 throw Error(
409 "Error: unknown minizinc standard library directory.\n"
410 "Specify --stdlib-dir on the command line or set the\n"
411 "MZN_STDLIB_DIR environment variable.");
412 }
413
414 if (globals_dir != "") {
415 includePaths.insert(includePaths.begin(), std_lib_dir + "/" + globals_dir + "/");
416 }
417 includePaths.push_back(std_lib_dir + "/std/");
418
419 for (unsigned int i = 0; i < includePaths.size(); i++) {
420 if (!FileUtils::directory_exists(includePaths[i])) {
421 throw Error("Cannot access include directory " + includePaths[i]);
422 }
423 }
424
425 if (flag_output_base == "") {
426 if (filenames.empty()) {
427 flag_output_base = "mznout";
428 } else {
429 flag_output_base = filenames[0].substr(0, filenames[0].length() - 4);
430 }
431 }
432
433 if (filenames.end() != find(filenames.begin(), filenames.end(), flag_output_fzn) ||
434 datafiles.end() != find(datafiles.begin(), datafiles.end(), flag_output_fzn)) {
435 log << " WARNING: fzn filename '" << flag_output_fzn << "' matches an input file, ignoring."
436 << endl;
437 flag_output_fzn = "";
438 }
439 if (filenames.end() != find(filenames.begin(), filenames.end(), flag_output_ozn) ||
440 datafiles.end() != find(datafiles.begin(), datafiles.end(), flag_output_ozn)) {
441 log << " WARNING: ozn filename '" << flag_output_ozn << "' matches an input file, ignoring."
442 << endl;
443 flag_output_ozn = "";
444 }
445
446 if (fOutputByDefault) {
447 if (flag_output_fzn == "") {
448 flag_output_fzn = flag_output_base + ".fzn";
449 }
450 if (flag_output_paths == "" && fopts.collect_mzn_paths) {
451 flag_output_paths = flag_output_base + ".paths";
452 }
453 if (flag_output_ozn == "" && !flag_no_output_ozn) {
454 flag_output_ozn = flag_output_base + ".ozn";
455 }
456 }
457
458 {
459 std::stringstream errstream;
460
461 Model* m;
462 pEnv.reset(new Env(NULL, os, log));
463 Env* env = getEnv();
464
465 if (!flag_compile_solution_check_model && !flag_solution_check_model.empty()) {
466 // Extract variables to check from solution check model
467 if (flag_verbose)
468 log << "Parsing solution checker model " << flag_solution_check_model << " ..." << endl;
469 bool isCompressedChecker =
470 flag_solution_check_model.size() >= 4 &&
471 flag_solution_check_model.substr(flag_solution_check_model.size() - 4) == ".mzc";
472 std::vector<std::string> smm_model({flag_solution_check_model});
473 Model* smm = parse(*env, smm_model, datafiles, "", "", includePaths, flag_ignoreStdlib, false,
474 flag_verbose, errstream);
475 if (flag_verbose) log << " done parsing (" << starttime.stoptime() << ")" << std::endl;
476 if (smm) {
477 log << errstream.str();
478 errstream.str("");
479 std::ostringstream smm_oss;
480 Printer p(smm_oss, 0, false);
481 p.print(smm);
482 Env smm_env(smm);
483 GCLock lock;
484 vector<TypeError> typeErrors;
485 try {
486 MiniZinc::typecheck(smm_env, smm, typeErrors, true, false, true);
487 if (typeErrors.size() > 0) {
488 if (!isCompressedChecker) {
489 for (unsigned int i = 0; i < typeErrors.size(); i++) {
490 if (flag_verbose) log << std::endl;
491 log << typeErrors[i].loc() << ":" << std::endl;
492 log << typeErrors[i].what() << ": " << typeErrors[i].msg() << std::endl;
493 }
494 }
495 throw Error("multiple type errors");
496 }
497 for (unsigned int i = 0; i < smm->size(); i++) {
498 if (VarDeclI* vdi = (*smm)[i]->dyn_cast<VarDeclI>()) {
499 if (vdi->e()->e() == NULL) env->envi().checkVars.push_back(vdi->e());
500 }
501 }
502 smm->compact();
503 std::string smm_compressed =
504 FileUtils::encodeBase64(FileUtils::deflateString(smm_oss.str()));
505 TypeInst* ti = new TypeInst(Location().introduce(), Type::parstring(), NULL);
506 VarDecl* checkString =
507 new VarDecl(Location().introduce(), ti, ASTString("_mzn_solution_checker"),
508 new StringLit(Location().introduce(), smm_compressed));
509 VarDeclI* checkStringI = new VarDeclI(Location().introduce(), checkString);
510 env->output()->addItem(checkStringI);
511 } catch (TypeError& e) {
512 if (isCompressedChecker) {
513 log << "Warning: type error in solution checker model\n";
514 } else {
515 throw;
516 }
517 }
518 } else {
519 if (isCompressedChecker) {
520 log << "Warning: syntax error in solution checker model\n";
521 } else {
522 log << errstream.str();
523 throw Error("parse error");
524 }
525 }
526 }
527
528 if (flag_compile_solution_check_model) {
529 if (!modelString.empty()) {
530 throw Error("Cannot compile solution checker model with additional model inputs.");
531 }
532 if (flag_stdinInput) {
533 throw Error(
534 "Cannot compile solution checker model with additional model from standard input.");
535 }
536 if (filenames.size() != 1) {
537 throw Error("Cannot compile solution checker model with more than one model given.");
538 }
539 }
540
541 if (!flag_solution_check_model.empty() && filenames.size() == 0) {
542 throw Error("Cannot run solution checker without model.");
543 }
544
545 std::string modelText = modelString;
546 if (flag_stdinInput) {
547 std::string input =
548 std::string(istreambuf_iterator<char>(std::cin), istreambuf_iterator<char>());
549 modelText += input;
550 }
551
552 if (flag_verbose) {
553 log << "Parsing file(s) ";
554 for (int i = 0; i < filenames.size(); ++i)
555 log << (i == 0 ? "" : ", '") << filenames[i] << '\'';
556 for (const auto& sFln : datafiles) log << ", '" << sFln << '\'';
557 log << " ..." << std::endl;
558 }
559 errstream.str("");
560 m = parse(*env, filenames, datafiles, modelText, modelName.empty() ? "stdin" : modelName,
561 includePaths, flag_ignoreStdlib, false, flag_verbose, errstream);
562 if (globals_dir != "") {
563 includePaths.erase(includePaths.begin());
564 }
565 if (m == NULL) throw Error(errstream.str());
566 log << errstream.str();
567 env->model(m);
568 if (flag_typecheck) {
569 if (flag_verbose) log << " done parsing (" << starttime.stoptime() << ")" << std::endl;
570
571 if (flag_instance_check_only || flag_model_check_only || flag_model_interface_only ||
572 flag_model_types_only) {
573 std::ostringstream compiledSolutionCheckModel;
574 if (flag_compile_solution_check_model) {
575 Printer p(compiledSolutionCheckModel, 0);
576 p.print(m);
577 }
578 GCLock lock;
579 vector<TypeError> typeErrors;
580 MiniZinc::typecheck(
581 *env, m, typeErrors,
582 flag_model_types_only || flag_model_interface_only || flag_model_check_only,
583 flag_allow_multi_assign);
584 if (typeErrors.size() > 0) {
585 for (unsigned int i = 0; i < typeErrors.size(); i++) {
586 if (flag_verbose) log << std::endl;
587 log << typeErrors[i].loc() << ":" << std::endl;
588 log << typeErrors[i].what() << ": " << typeErrors[i].msg() << std::endl;
589 }
590 throw Error("multiple type errors");
591 }
592 if (flag_model_interface_only) {
593 MiniZinc::output_model_interface(*env, m, os);
594 }
595 if (flag_model_types_only) {
596 MiniZinc::output_model_variable_types(*env, m, os);
597 }
598 if (flag_compile_solution_check_model) {
599 std::string mzc(FileUtils::deflateString(compiledSolutionCheckModel.str()));
600 mzc = FileUtils::encodeBase64(mzc);
601 std::string mzc_filename = filenames[0].substr(0, filenames[0].size() - 4);
602 if (flag_verbose) log << "Write solution checker to " << mzc_filename << "\n";
603 std::ofstream mzc_f(mzc_filename);
604 mzc_f << mzc;
605 mzc_f.close();
606 }
607 status = SolverInstance::NONE;
608 } else {
609 if (is_flatzinc) {
610 GCLock lock;
611 vector<TypeError> typeErrors;
612 MiniZinc::typecheck(*env, m, typeErrors,
613 flag_model_check_only || flag_model_interface_only,
614 flag_allow_multi_assign, true);
615 if (typeErrors.size() > 0) {
616 for (unsigned int i = 0; i < typeErrors.size(); i++) {
617 if (flag_verbose) log << std::endl;
618 log << typeErrors[i].loc() << ":" << std::endl;
619 log << typeErrors[i].what() << ": " << typeErrors[i].msg() << std::endl;
620 }
621 throw Error("multiple type errors");
622 }
623 MiniZinc::registerBuiltins(*env);
624 env->swap();
625 populateOutput(*env);
626 } else {
627 if (flag_verbose) log << "Flattening ...";
628
629 fopts.onlyRangeDomains = flag_only_range_domains;
630 fopts.verbose = flag_verbose;
631 fopts.outputMode = flag_output_mode;
632 fopts.outputObjective = flag_output_objective;
633 fopts.outputOutputItem = flag_output_output_item;
634#ifdef HAS_GECODE
635 GecodeOptions gopts;
636 gopts.only_range_domains = flag_only_range_domains;
637 gopts.sac = flag_sac;
638 gopts.allow_unbounded_vars = flag_allow_unbounded_vars;
639 gopts.shave = flag_shave;
640 gopts.printStatistics = flag_statistics;
641 gopts.pre_passes = flag_pre_passes;
642#endif
643 FlatteningOptions pass_opts = fopts;
644 CompilePassFlags cfs;
645 cfs.noMIPdomains = flag_noMIPdomains;
646 cfs.verbose = flag_verbose;
647 cfs.statistics = flag_statistics;
648 cfs.optimize = flag_optimize;
649 cfs.chain_compression = flag_chain_compression;
650 cfs.newfzn = flag_newfzn;
651 cfs.werror = flag_werror;
652 cfs.model_check_only = flag_model_check_only;
653 cfs.model_interface_only = flag_model_interface_only;
654 cfs.allow_multi_assign = flag_allow_multi_assign;
655
656 std::vector<unique_ptr<Pass> > managed_passes;
657
658 if (flag_two_pass) {
659 std::string library = std_lib_dir + (flag_gecode ? "/gecode_presolver/" : "/std/");
660 bool differentLibrary = (library != std_lib_dir + "/" + globals_dir + "/");
661 managed_passes.emplace_back(new CompilePass(env, pass_opts, cfs, library, includePaths,
662 true, differentLibrary));
663#ifdef HAS_GECODE
664 if (flag_gecode) managed_passes.emplace_back(new GecodePass(&gopts));
665#endif
666 }
667 managed_passes.emplace_back(new CompilePass(env, fopts, cfs,
668 std_lib_dir + "/" + globals_dir + "/",
669 includePaths, flag_two_pass, false));
670
671 Env* out_env = multiPassFlatten(managed_passes);
672 if (out_env == nullptr) exit(EXIT_FAILURE);
673
674 if (out_env != env) {
675 pEnv.reset(out_env);
676 }
677 env = out_env;
678 if (flag_verbose)
679 log << " done (" << starttime.stoptime() << "),"
680 << " max stack depth " << env->maxCallStack() << std::endl;
681 }
682
683 if (flag_statistics) {
684 FlatModelStatistics stats = statistics(env->flat());
685 os << "% Generated FlatZinc statistics:\n";
686
687 os << "%%%mzn-stat: paths=" << env->envi().getPathMap().size() << endl;
688
689 if (stats.n_bool_vars) {
690 os << "%%%mzn-stat: flatBoolVars=" << stats.n_bool_vars << endl;
691 }
692 if (stats.n_int_vars) {
693 os << "%%%mzn-stat: flatIntVars=" << stats.n_int_vars << endl;
694 }
695 if (stats.n_float_vars) {
696 os << "%%%mzn-stat: flatFloatVars=" << stats.n_float_vars << endl;
697 }
698 if (stats.n_set_vars) {
699 os << "%%%mzn-stat: flatSetVars=" << stats.n_set_vars << endl;
700 }
701
702 if (stats.n_bool_ct) {
703 os << "%%%mzn-stat: flatBoolConstraints=" << stats.n_bool_ct << endl;
704 }
705 if (stats.n_int_ct) {
706 os << "%%%mzn-stat: flatIntConstraints=" << stats.n_int_ct << endl;
707 }
708 if (stats.n_float_ct) {
709 os << "%%%mzn-stat: flatFloatConstraints=" << stats.n_float_ct << endl;
710 }
711 if (stats.n_set_ct) {
712 os << "%%%mzn-stat: flatSetConstraints=" << stats.n_set_ct << endl;
713 }
714
715 if (stats.n_reif_ct) {
716 os << "%%%mzn-stat: evaluatedReifiedConstraints=" << stats.n_reif_ct << endl;
717 }
718 if (stats.n_imp_ct) {
719 os << "%%%mzn-stat: evaluatedHalfReifiedConstraints=" << stats.n_imp_ct << endl;
720 }
721
722 if (stats.n_imp_del) {
723 os << "%%%mzn-stat: eliminatedImplications=" << stats.n_imp_del << endl;
724 }
725 if (stats.n_lin_del) {
726 os << "%%%mzn-stat: eliminatedLinearConstraints=" << stats.n_lin_del << endl;
727 }
728
729 /// Objective / SAT. These messages are used by mzn-test.py.
730 SolveI* solveItem = env->flat()->solveItem();
731 if (solveItem->st() != SolveI::SolveType::ST_SAT) {
732 if (solveItem->st() == SolveI::SolveType::ST_MAX) {
733 os << "%%%mzn-stat: method=\"maximize\"" << endl;
734 } else {
735 os << "%%%mzn-stat: method=\"minimize\"" << endl;
736 }
737 } else {
738 os << "%%%mzn-stat: method=\"satisfy\"" << endl;
739 }
740
741 os << "%%%mzn-stat: flatTime=" << flatten_time.s() << endl;
742 os << "%%%mzn-stat-end" << endl << endl;
743 }
744
745 if (flag_output_paths_stdout) {
746 if (flag_verbose) log << "Printing Paths to stdout ..." << std::endl;
747 PathFilePrinter pfp(os, env->envi());
748 pfp.print(env->flat());
749 if (flag_verbose) log << " done (" << starttime.stoptime() << ")" << std::endl;
750 } else if (flag_output_paths != "") {
751 if (flag_verbose)
752 log << "Printing Paths to '" << flag_output_paths << "' ..." << std::flush;
753 std::ofstream ofs;
754 ofs.open(flag_output_paths.c_str(), ios::out);
755 checkIOStatus(ofs.good(), " I/O error: cannot open fzn output file. ");
756 PathFilePrinter pfp(ofs, env->envi());
757 pfp.print(env->flat());
758 checkIOStatus(ofs.good(), " I/O error: cannot write fzn output file. ");
759 ofs.close();
760 if (flag_verbose) log << " done (" << starttime.stoptime() << ")" << std::endl;
761 }
762
763 if ((fopts.collect_mzn_paths || flag_two_pass) && !flag_keep_mzn_paths) {
764 class RemovePathAnnotations : public ItemVisitor {
765 public:
766 void removePath(Annotation& a) const { a.removeCall(constants().ann.mzn_path); }
767 void vVarDeclI(VarDeclI* vdi) const { removePath(vdi->e()->ann()); }
768 void vConstraintI(ConstraintI* ci) const { removePath(ci->e()->ann()); }
769 void vSolveI(SolveI* si) const {
770 removePath(si->ann());
771 if (Expression* e = si->e()) removePath(e->ann());
772 }
773 } removePaths;
774 iterItems<RemovePathAnnotations>(removePaths, env->flat());
775 }
776
777 if (flag_output_fzn_stdout) {
778 if (flag_verbose) log << "Printing FlatZinc to stdout ..." << std::endl;
779 Printer p(os, 0);
780 p.print(env->flat());
781 if (flag_verbose) log << " done (" << starttime.stoptime() << ")" << std::endl;
782 } else if (flag_output_fzn != "") {
783 if (flag_verbose)
784 log << "Printing FlatZinc to '" << flag_output_fzn << "' ..." << std::flush;
785 std::ofstream ofs;
786 ofs.open(flag_output_fzn.c_str(), ios::out);
787 checkIOStatus(ofs.good(), " I/O error: cannot open fzn output file. ");
788 Printer p(ofs, 0);
789 p.print(env->flat());
790 checkIOStatus(ofs.good(), " I/O error: cannot write fzn output file. ");
791 ofs.close();
792 if (flag_verbose) log << " done (" << starttime.stoptime() << ")" << std::endl;
793 }
794 if (!flag_no_output_ozn) {
795 if (flag_output_ozn_stdout) {
796 if (flag_verbose) log << "Printing .ozn to stdout ..." << std::endl;
797 Printer p(os, 0);
798 p.print(env->output());
799 if (flag_verbose) log << " done (" << starttime.stoptime() << ")" << std::endl;
800 } else if (flag_output_ozn != "") {
801 if (flag_verbose)
802 log << "Printing .ozn to '" << flag_output_ozn << "' ..." << std::flush;
803 std::ofstream ofs;
804 ofs.open(flag_output_ozn.c_str(), std::ios::out);
805 checkIOStatus(ofs.good(), " I/O error: cannot open ozn output file. ");
806 Printer p(ofs, 0);
807 p.print(env->output());
808 checkIOStatus(ofs.good(), " I/O error: cannot write ozn output file. ");
809 ofs.close();
810 if (flag_verbose) log << " done (" << starttime.stoptime() << ")" << std::endl;
811 }
812 }
813 }
814 } else { // !flag_typecheck
815 Printer p(os);
816 p.print(m);
817 }
818 }
819
820 if (getEnv()->envi().failed()) {
821 status = SolverInstance::UNSAT;
822 }
823
824 if (flag_verbose) {
825 size_t mem = GC::maxMem();
826 if (mem < 1024)
827 log << "Maximum memory " << mem << " bytes";
828 else if (mem < 1024 * 1024)
829 log << "Maximum memory " << mem / 1024 << " Kbytes";
830 else
831 log << "Maximum memory " << mem / (1024 * 1024) << " Mbytes";
832 log << "." << std::endl;
833 }
834}
835
836void Flattener::printStatistics(ostream&) {}