this repo has no description
dekker.one
1
2/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
3
4/*
5 * Main authors:
6 * Guido Tack <guido.tack@monash.edu>
7 * Gleb Belov <gleb.belov@monash.edu>
8 */
9
10/* This Source Code Form is subject to the terms of the Mozilla Public
11 * License, v. 2.0. If a copy of the MPL was not distributed with this
12 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
13
14/* This (main) file coordinates flattening and solving.
15 * The corresponding modules are flexibly plugged in
16 * as derived classes, prospectively from DLLs.
17 * A flattening module should provide MinZinc::GetFlattener()
18 * A solving module should provide an object of a class derived from SolverFactory.
19 * Need to get more flexible for multi-pass & multi-solving stuff TODO
20 */
21
22#ifdef _MSC_VER
23#define _CRT_SECURE_NO_WARNINGS
24#endif
25
26#include <chrono>
27#include <cstdlib>
28#include <ctime>
29#include <fstream>
30#include <iomanip>
31#include <iostream>
32#include <ratio>
33
34using namespace std;
35
36#include <minizinc/file_utils.hh>
37#include <minizinc/model.hh>
38#include <minizinc/parser.hh>
39#include <minizinc/prettyprinter.hh>
40#include <minizinc/reader.hh>
41#include <minizinc/utils.hh>
42
43namespace MiniZinc {
44
45MznReader::MznReader(std::ostream& os0, std::ostream& log0)
46 : solver_configs(log0), /*flt(os0,log0,solver_configs.mznlibDir()), */ os(os0), log(log0) {}
47
48MznReader::~MznReader() { GC::trigger(); }
49
50void MznReader::printUsage() {
51 os << "TODO: print usage" << std::endl;
52 /*
53 os << executable_name << ": ";
54 if ( ifMzn2Fzn() ) {
55 os
56 << "MiniZinc to FlatZinc converter.\n"
57 << "Usage: " << executable_name
58 << " [<options>] [-I <include path>] <model>.mzn [<data>.dzn ...]" << std::endl;
59 } else if (ifSolns2out()) {
60 os
61 << "Solutions to output translator.\n"
62 << "Usage: " << executable_name
63 << " [<options>] <model>.ozn" << std::endl;
64 } else {
65 os
66 << "MiniZinc driver.\n"
67 << "Usage: " << executable_name
68 << " [<options>] [-I <include path>] <model>.mzn [<data>.dzn ...] or just <flat>.fzn" <<
69 std::endl;
70 }
71 */
72}
73
74void MznReader::printHelp(const std::string& selectedSolver) {
75 printUsage();
76 os << "TODO: print help" << std::endl;
77 /*
78 os
79 << "General options:" << std::endl
80 << " --help, -h\n Print this help message." << std::endl
81 << " --version\n Print version information." << std::endl
82 << " --solvers\n Print list of available solvers." << std::endl
83 << " --time-limit <ms>\n Stop after <ms> milliseconds (includes compilation and solving)."
84 << std::endl
85 << " --solver <solver id>, --solver <solver config file>.msc\n Select solver to use." <<
86 std::endl
87 << " --help <solver id>\n Print help for a particular solver." << std::endl
88 << " -v, -l, --verbose\n Print progress/log statements. Note that some solvers may log to
89 stdout." << std::endl
90 << " --verbose-compilation\n Print progress/log statements for compilation." << std::endl
91 << " -s, --statistics\n Print statistics." << std::endl
92 << " --compiler-statistics\n Print statistics for compilation." << std::endl
93 << " -c, --compile\n Compile only (do not run solver)." << std::endl
94 << " --config-dirs\n Output configuration directories." << std::endl;
95
96 if (selectedSolver.empty()) {
97 flt.printHelp(os);
98 os << endl;
99 if ( !ifMzn2Fzn() ) {
100 s2out.printHelp(os);
101 os << endl;
102 }
103 os << "Available solvers (get help using --help <solver id>):" << endl;
104 std::vector<std::string> solvers = solver_configs.solvers();
105 if (solvers.size()==0)
106 cout << " none.\n";
107 for (unsigned int i=0; i<solvers.size(); i++) {
108 cout << " " << solvers[i] << endl;
109 }
110 } else {
111 const SolverConfig& sc = solver_configs.config(selectedSolver);
112 string solverId = sc.executable().empty() ? sc.id() : (sc.supportsMzn() ?
113 string("org.minizinc.mzn-mzn") : string("org.minizinc.mzn-fzn")); bool found = false; for (auto it
114 = getGlobalSolverRegistry()->getSolverFactories().rbegin(); it !=
115 getGlobalSolverRegistry()->getSolverFactories().rend(); ++it) { if ((*it)->getId()==solverId) { os
116 << endl;
117 (*it)->printHelp(os);
118 if (!sc.executable().empty() && !sc.extraFlags().empty()) {
119 os << "Extra solver flags (use with ";
120 os << (sc.supportsMzn() ? "--mzn-flags" : "--fzn-flags") << ")" << endl;
121 for (const SolverConfig::ExtraFlag& ef: sc.extraFlags()) {
122 os << " " << ef.flag << endl << " " << ef.description << endl;
123 }
124 }
125 found = true;
126 }
127 }
128 if (!found) {
129 os << "No help found for solver " << selectedSolver << endl;
130 }
131 }
132 */
133}
134
135bool MznReader::processOption(int& i, std::vector<std::string>& argv) {
136 CLOParser cop(i, argv);
137 string buffer;
138
139 if (cop.getOption("-I --search-dir", &buffer)) {
140 includePaths.push_back(buffer + string("/"));
141 } else if (cop.getOption("--ignore-stdlib")) {
142 flag_ignoreStdlib = true;
143 /*
144 } else if ( cop.getOption( "--instance-check-only") ) {
145 flag_instance_check_only = true;
146 } else if ( cop.getOption( "-e --model-check-only") ) {
147 flag_model_check_only = true;
148 } else if ( cop.getOption( "--model-interface-only") ) {
149 flag_model_interface_only = true;
150 } else if ( cop.getOption( "--model-types-only") ) {
151 flag_model_types_only = true;
152 */
153 } else if (cop.getOption("-v --verbose")) {
154 flag_verbose = true;
155 /*
156 } else if ( cop.getOption( "--no-optimize --no-optimise") ) {
157 flag_optimize = false;
158 } else if ( cop.getOption( "--no-output-ozn -O-") ) {
159 flag_no_output_ozn = true;
160 } else if ( cop.getOption( "--output-base", &flag_output_base ) ) {
161 } else if ( cop.getOption(
162 fOutputByDefault ?
163 "-o --fzn --output-to-file --output-fzn-to-file"
164 : "--fzn --output-fzn-to-file", &flag_output_fzn) ) {
165 } else if ( cop.getOption( "--output-paths-to-file", &flag_output_paths) ) {
166 fopts.collect_mzn_paths = true;
167 } else if ( cop.getOption( "--output-paths") ) {
168 fopts.collect_mzn_paths = true;
169 */
170 /*
171 } else if ( cop.getOption( "--output-to-stdout --output-fzn-to-stdout" ) ) {
172 flag_output_fzn_stdout = true;
173 } else if ( cop.getOption( "--output-ozn-to-stdout" ) ) {
174 flag_output_ozn_stdout = true;
175 } else if ( cop.getOption( "--output-paths-to-stdout" ) ) {
176 fopts.collect_mzn_paths = true;
177 flag_output_paths_stdout = true;
178 } else if ( cop.getOption( "--output-mode", &buffer ) ) {
179 if (buffer == "dzn") {
180 flag_output_mode = FlatteningOptions::OUTPUT_DZN;
181 } else if (buffer == "json") {
182 flag_output_mode = FlatteningOptions::OUTPUT_JSON;
183 } else if (buffer == "item") {
184 flag_output_mode = FlatteningOptions::OUTPUT_ITEM;
185 } else {
186 return false;
187 }
188 } else if ( cop.getOption( "--output-objective" ) ) {
189 flag_output_objective = true;
190 } else if ( cop.getOption( "- --input-from-stdin" ) ) {
191 flag_stdinInput = true;
192 */
193 } else if (cop.getOption("-d --data", &buffer)) {
194 if (buffer.length() <= 4 || buffer.substr(buffer.length() - 4, string::npos) != ".dzn")
195 return false;
196 datafiles.push_back(buffer);
197 } else if (cop.getOption("--stdlib-dir", &std_lib_dir)) {
198 } else if (cop.getOption("-G --globals-dir --mzn-globals-dir", &globals_dir)) {
199 } else if (cop.getOption("-D --cmdline-data", &buffer)) {
200 datafiles.push_back("cmd:/" + buffer);
201 } else if (cop.getOption("--allow-unbounded-vars")) {
202 flag_allow_unbounded_vars = true;
203 } else if (cop.getOption("--only-range-domains")) {
204 flag_only_range_domains = true;
205 /*
206 } else if ( cop.getOption( "--no-MIPdomains" ) ) { // internal
207 flag_noMIPdomains = true;
208 } else if ( cop.getOption( "--MIPDMaxIntvEE", &opt_MIPDmaxIntvEE ) ) {
209 } else if ( cop.getOption( "--MIPDMaxDensEE", &opt_MIPDmaxDensEE ) ) {
210 */
211 } else if (cop.getOption("-Werror")) {
212 flag_werror = true;
213 /*
214 } else if (string(argv[i])=="--use-gecode") {
215#ifdef HAS_GECODE
216 flag_two_pass = true;
217 flag_gecode = true;
218#else
219 log << "warning: Gecode not available. Ignoring '--use-gecode'\n";
220#endif
221 } else if (string(argv[i])=="--sac") {
222#ifdef HAS_GECODE
223 flag_two_pass = true;
224 flag_gecode = true;
225 flag_sac = true;
226#else
227 log << "warning: Gecode not available. Ignoring '--sac'\n";
228#endif
229
230 } else if (string(argv[i])=="--shave") {
231#ifdef HAS_GECODE
232 flag_two_pass = true;
233 flag_gecode = true;
234 flag_shave = true;
235#else
236 log << "warning: Gecode not available. Ignoring '--shave'\n";
237#endif
238 } else if (string(argv[i])=="--two-pass") {
239 flag_two_pass = true;
240 } else if (string(argv[i])=="--npass") {
241 i++;
242 if (i==argv.size()) return false;
243 log << "warning: --npass option is deprecated --two-pass\n";
244 int passes = atoi(argv[i].c_str());
245 if(passes == 1) flag_two_pass = false;
246 else if(passes == 2) flag_two_pass = true;
247 } else if (string(argv[i])=="--pre-passes") {
248 i++;
249 if (i==argv.size()) return false;
250 int passes = atoi(argv[i].c_str());
251 if(passes >= 0) {
252 flag_pre_passes = static_cast<unsigned int>(passes);
253 }
254 } else if (string(argv[i])=="-O0") {
255 flag_optimize = false;
256 } else if (string(argv[i])=="-O1") {
257 // Default settings
258 } else if (string(argv[i])=="-O2") {
259 flag_two_pass = true;
260#ifdef HAS_GECODE
261 } else if (string(argv[i])=="-O3") {
262 flag_two_pass = true;
263 flag_gecode = true;
264 } else if (string(argv[i])=="-O4") {
265 flag_two_pass = true;
266 flag_gecode = true;
267 flag_shave = true;
268 } else if (string(argv[i])=="-O5") {
269 flag_two_pass = true;
270 flag_gecode = true;
271 flag_sac = true;
272#else
273 } else if (string(argv[i])=="-O3" || string(argv[i])=="-O4" || string(argv[i])=="-O5") {
274 log << "% Warning: This compiler does not have Gecode builtin, cannot process -O3,-O4,-O5.\n";
275 return false;
276#endif
277 */
278 // ozn options must be after the -O<n> optimisation options
279 /*
280 } else if ( cop.getOption( "-O --ozn --output-ozn-to-file", &flag_output_ozn) ) {
281 } else if (string(argv[i])=="--keep-paths") {
282 flag_keep_mzn_paths = true;
283 fopts.collect_mzn_paths = true;
284 } else if (string(argv[i])=="--only-toplevel-presolve") {
285 fopts.only_toplevel_paths = true;
286 } else if ( cop.getOption( "--allow-multiple-assignments" ) ) {
287 flag_allow_multi_assign = true;
288 } else if (string(argv[i])=="--input-is-flatzinc") {
289 is_flatzinc = true;
290 } else if ( cop.getOption( "--compile-solution-checker", &buffer) ) {
291 if (buffer.length()>=8 && buffer.substr(buffer.length()-8,string::npos) == ".mzc.mzn") {
292 flag_compile_solution_check_model = true;
293 flag_model_check_only = true;
294 filenames.push_back(buffer);
295 } else {
296 log << "Error: solution checker model must have extension .mzc.mzn" << std::endl;
297 return false;
298 }
299 */
300 } else {
301 std::string input_file(argv[i]);
302 if (input_file.length() <= 4) {
303 return false;
304 }
305 size_t last_dot = input_file.find_last_of('.');
306 if (last_dot == string::npos) {
307 return false;
308 }
309 std::string extension = input_file.substr(last_dot, string::npos);
310 /*
311 if ( extension == ".mzc" || (input_file.length()>=8 &&
312 input_file.substr(input_file.length()-8,string::npos) == ".mzc.mzn") ) {
313 flag_solution_check_model = input_file;
314 } else */
315 if (extension == ".mzn" || extension == ".fzn") {
316 /*
317 if ( extension == ".fzn" ) {
318 is_flatzinc = true;
319 if ( fOutputByDefault ) // mzn2fzn mode
320 return false;
321 }
322 */
323 filenames.push_back(input_file);
324 } else if (extension == ".dzn" || extension == ".json") {
325 datafiles.push_back(input_file);
326 } else {
327 // if ( fOutputByDefault )
328 log << "Error: cannot handle file extension " << extension << "." << std::endl;
329 return false;
330 }
331 }
332 return true;
333}
334
335MznReader::OptionStatus MznReader::processOptions(std::vector<std::string>& argv) {
336 std_lib_dir = solver_configs.mznlibDir();
337
338 int i(0);
339 int argc(argv.size());
340 for (; i < argv.size(); ++i) {
341 if (argv[i] == "-h" || argv[i] == "--help") {
342 if (argc > i + 1) {
343 printHelp(argv[i + 1]);
344 } else {
345 printHelp();
346 }
347 return OPTION_FINISH;
348 }
349 if (argv[i] == "--version") {
350 // flt.printVersion(cout);
351 cout << "MiniZinc model reader. Version EXTREMELY-ALPHA." << endl;
352 return OPTION_FINISH;
353 }
354 if (argv[i] == "--solvers") {
355 cout << "MiniZinc driver.\nAvailable solver configurations:\n";
356 std::vector<std::string> solvers = solver_configs.solvers();
357 if (solvers.size() == 0) cout << " none.\n";
358 for (unsigned int i = 0; i < solvers.size(); i++) {
359 cout << " " << solvers[i] << endl;
360 }
361 cout << "Search path for solver configurations:\n";
362 for (const string& p : solver_configs.solverConfigsPath()) {
363 cout << " " << p << endl;
364 }
365 return OPTION_FINISH;
366 }
367 /*
368 if (argv[i]=="--solvers-json") {
369 cout << solver_configs.solverConfigsJSON();
370 return OPTION_FINISH;
371 }
372 */
373 if (argv[i] == "--config-dirs") {
374 GCLock lock;
375 cout << "{\n";
376 cout << " \"globalConfigFile\" : \""
377 << Printer::escapeStringLit(FileUtils::global_config_file()) << "\",\n";
378 cout << " \"userConfigFile\" : \"" << Printer::escapeStringLit(FileUtils::user_config_file())
379 << "\",\n";
380 cout << " \"userSolverConfigDir\" : \""
381 << Printer::escapeStringLit(FileUtils::user_config_dir()) << "/solvers\",\n";
382 cout << " \"mznStdlibDir\" : \"" << Printer::escapeStringLit(solver_configs.mznlibDir())
383 << "\"\n";
384 cout << "}\n";
385 return OPTION_FINISH;
386 }
387 if (!processOption(i, argv)) return OPTION_ERROR;
388 }
389 return OPTION_OK;
390}
391
392Model* MznReader::read(const std::string& modelString, const std::string& modelName) {
393 Env env(NULL, os, log);
394
395 if (std_lib_dir == "") {
396 throw Error(
397 "Error: unknown minizinc standard library directory.\n"
398 "Specify --stdlib-dir on the command line or set the\n"
399 "MZN_STDLIB_DIR environment variable.");
400 }
401 if (globals_dir != "") {
402 includePaths.insert(includePaths.begin(), std_lib_dir + "/" + globals_dir + "/");
403 }
404 includePaths.push_back(std_lib_dir + "/std/");
405
406 for (unsigned int i = 0; i < includePaths.size(); i++) {
407 if (!FileUtils::directory_exists(includePaths[i])) {
408 throw Error("Cannot access include directory " + includePaths[i]);
409 }
410 }
411
412 Model* m(nullptr);
413
414 m = parse(env, filenames, datafiles, modelString, modelName.empty() ? "stdin" : modelName,
415 includePaths, flag_ignoreStdlib, false, flag_verbose, log);
416 return m;
417}
418
419#if 0
420void addFlags(const std::string& sep,
421 const std::vector<std::string>& in_args,
422 std::vector<std::string>& out_args) {
423 for(const std::string& arg : in_args) {
424 out_args.push_back(sep);
425 out_args.push_back(arg);
426 }
427}
428
429MznReader::OptionStatus MznReader::processOptions(std::vector<std::string>& argv)
430{
431 /*
432 executable_name = argv[0];
433 executable_name = executable_name.substr(executable_name.find_last_of("/\\") + 1);
434 size_t lastdot = executable_name.find_last_of('.');
435 if (lastdot != std::string::npos) {
436 executable_name = executable_name.substr(0, lastdot);
437 }
438 */
439 string solver;
440 /*
441 bool mzn2fzn_exe = (executable_name=="mzn2fzn");
442 if (mzn2fzn_exe) {
443 is_mzn2fzn=true;
444 } else if (executable_name=="solns2out") {
445 s2out._opt.flag_standaloneSolns2Out=true;
446 }
447 bool compileSolutionChecker = false;
448 */
449 int i=1, j=1;
450 int argc = static_cast<int>(argv.size());
451 if (argc < 2)
452 return OPTION_ERROR;
453 for (i=1; i<argc; ++i) {
454 if (argv[i]=="-h" || argv[i]=="--help") {
455 if (argc > i+1) {
456 printHelp(argv[i+1]);
457 } else {
458 printHelp();
459 }
460 return OPTION_FINISH;
461 }
462 if (argv[i]=="--version") {
463 flt.printVersion(cout);
464 return OPTION_FINISH;
465 }
466 if (argv[i]=="--solvers") {
467 cout << "MiniZinc driver.\nAvailable solver configurations:\n";
468 std::vector<std::string> solvers = solver_configs.solvers();
469 if (solvers.size()==0)
470 cout << " none.\n";
471 for (unsigned int i=0; i<solvers.size(); i++) {
472 cout << " " << solvers[i] << endl;
473 }
474 cout << "Search path for solver configurations:\n";
475 for (const string& p : solver_configs.solverConfigsPath()) {
476 cout << " " << p << endl;
477 }
478 return OPTION_FINISH;
479 }
480 if (argv[i]=="--solvers-json") {
481 cout << solver_configs.solverConfigsJSON();
482 return OPTION_FINISH;
483 }
484 if (argv[i]=="--config-dirs") {
485 GCLock lock;
486 cout << "{\n";
487 cout << " \"globalConfigFile\" : \"" << Printer::escapeStringLit(FileUtils::global_config_file()) << "\",\n";
488 cout << " \"userConfigFile\" : \"" << Printer::escapeStringLit(FileUtils::user_config_file()) << "\",\n";
489 cout << " \"userSolverConfigDir\" : \"" << Printer::escapeStringLit(FileUtils::user_config_dir()) << "/solvers\",\n";
490 cout << " \"mznStdlibDir\" : \"" << Printer::escapeStringLit(solver_configs.mznlibDir()) << "\"\n";
491 cout << "}\n";
492 return OPTION_FINISH;
493 }
494 if (argv[i]=="--time-limit") {
495 ++i;
496 if (i==argc) {
497 log << "Argument required for --time-limit" << endl;
498 return OPTION_ERROR;
499 }
500 flag_overall_time_limit = atoi(argv[i].c_str());
501 } else if (argv[i]=="--solver") {
502 ++i;
503 if (i==argc) {
504 log << "Argument required for --solver" << endl;
505 return OPTION_ERROR;
506 }
507 if (solver.size()>0 && solver != argv[i]) {
508 log << "Only one --solver option allowed" << endl;
509 return OPTION_ERROR;
510 }
511 solver = argv[i];
512 } else if (argv[i]=="-c" || argv[i]=="--compile") {
513 is_mzn2fzn = true;
514 } else if (argv[i]=="-v" || argv[i]=="--verbose" || argv[i]=="-l") {
515 flag_verbose = true;
516 flag_compiler_verbose = true;
517 } else if (argv[i]=="--verbose-compilation") {
518 flag_compiler_verbose = true;
519 } else if (argv[i]=="-s" || argv[i]=="--statistics") {
520 flag_statistics = true;
521 flag_compiler_statistics = true;
522 } else if (argv[i]=="--compiler-statistics") {
523 flag_compiler_statistics = true;
524 } else {
525 if ((argv[i]=="--fzn-cmd" || argv[i]=="--flatzinc-cmd") && solver.empty()) {
526 solver = "org.minizinc.mzn-fzn";
527 }
528 if (argv[i]=="--compile-solution-checker") {
529 compileSolutionChecker = true;
530 }
531 argv[j++] = argv[i];
532 }
533 }
534 argv.resize(j);
535 argc = j;
536
537 /*
538 if ( (mzn2fzn_exe || compileSolutionChecker) && solver.empty()) {
539 solver = "org.minizinc.mzn-fzn";
540 }
541 */
542
543 if (flag_verbose) {
544 argv.push_back("--verbose-solving");
545 argc++;
546 }
547 if (flag_statistics) {
548 argv.push_back("--solver-statistics");
549 argc++;
550 }
551
552 // flt.set_flag_output_by_default(ifMzn2Fzn());
553
554 // bool isMznMzn = false;
555
556 if (/*!ifSolns2out()*/ true) {
557 try {
558 const SolverConfig& sc = solver_configs.config(solver);
559 string solverId = sc.executable().empty() ? sc.id() : (sc.supportsMzn() ? string("org.minizinc.mzn-mzn") : string("org.minizinc.mzn-fzn"));
560 for (auto it = getGlobalSolverRegistry()->getSolverFactories().begin();
561 it != getGlobalSolverRegistry()->getSolverFactories().end(); ++it) {
562 if ((*it)->getId()==solverId) { /// TODO: also check version (currently assumes all ids are unique)
563 sf = *it;
564 si_opt = sf->createOptions();
565 if (!sc.executable().empty() || solverId=="org.minizinc.mzn-fzn") {
566 std::vector<MZNFZNSolverFlag> acceptedFlags;
567 for (auto& sf : sc.stdFlags())
568 acceptedFlags.push_back(MZNFZNSolverFlag::std(sf));
569 for (auto& ef : sc.extraFlags())
570 acceptedFlags.push_back(MZNFZNSolverFlag::extra(ef.flag,ef.flag_type));
571
572 // Collect arguments required for underlying exe
573 vector<string> fzn_mzn_flags;
574 if (sc.needsStdlibDir()) {
575 fzn_mzn_flags.push_back("--stdlib-dir");
576 fzn_mzn_flags.push_back(FileUtils::share_directory());
577 }
578 if (sc.needsMznExecutable()) {
579 fzn_mzn_flags.push_back("--minizinc-exe");
580 fzn_mzn_flags.push_back(FileUtils::progpath() + "/" + executable_name);
581 }
582
583 if (sc.supportsMzn()) {
584 isMznMzn = true;
585 static_cast<MZN_SolverFactory*>(sf)->setAcceptedFlags(si_opt, acceptedFlags);
586 std::vector<std::string> additionalArgs_s;
587 additionalArgs_s.push_back("-m");
588 if (sc.executable_resolved().size()) {
589 additionalArgs_s.push_back(sc.executable_resolved());
590 } else {
591 additionalArgs_s.push_back(sc.executable());
592 }
593
594 if(!fzn_mzn_flags.empty()) {
595 addFlags("--mzn-flag", fzn_mzn_flags, additionalArgs_s);
596 }
597
598 // This should maybe be moved to fill in fzn_mzn_flags when
599 // --find-muses is implemented (these arguments will be passed
600 // through to the subsolver of findMUS)
601 if (!sc.mznlib().empty()) {
602 if (sc.mznlib().substr(0,2)=="-G") {
603 additionalArgs_s.push_back("--mzn-flag");
604 additionalArgs_s.push_back(sc.mznlib());
605 } else {
606 additionalArgs_s.push_back("--mzn-flag");
607 additionalArgs_s.push_back("-I");
608 additionalArgs_s.push_back("--mzn-flag");
609 std::string _mznlib;
610 if (sc.mznlib_resolved().size()) {
611 _mznlib = sc.mznlib_resolved();
612 } else {
613 _mznlib = sc.mznlib();
614 }
615 additionalArgs_s.push_back(_mznlib);
616 }
617 }
618
619 for (i=0; i<additionalArgs_s.size(); ++i) {
620 bool success = sf->processOption(si_opt, i, additionalArgs_s);
621 if (!success) {
622 log << "Solver backend " << solverId << " does not recognise option " << additionalArgs_s[i] << "." << endl;
623 return OPTION_ERROR;
624 }
625 }
626 } else {
627 static_cast<FZN_SolverFactory*>(sf)->setAcceptedFlags(si_opt, acceptedFlags);
628 std::vector<std::string> additionalArgs;
629 additionalArgs.push_back("--fzn-cmd");
630 if (sc.executable_resolved().size()) {
631 additionalArgs.push_back(sc.executable_resolved());
632 } else {
633 additionalArgs.push_back(sc.executable());
634 }
635 if(!fzn_mzn_flags.empty()) {
636 addFlags("--fzn-flag", fzn_mzn_flags, additionalArgs);
637 }
638 if (sc.needsPathsFile()) {
639 // Instruct flattener to hold onto paths
640 int i=0;
641 vector<string> args {"--keep-paths"};
642 flt.processOption(i, args);
643
644 // Instruct FznSolverInstance to write a path file
645 // and pass it to the executable with --paths arg
646 additionalArgs.push_back("--fzn-needs-paths");
647 }
648 if (!sc.needsSolns2Out()) {
649 additionalArgs.push_back("--fzn-output-passthrough");
650 }
651 int i=0;
652 for (i=0; i<additionalArgs.size(); ++i) {
653 bool success = sf->processOption(si_opt, i, additionalArgs);
654 if (!success) {
655 log << "Solver backend " << solverId << " does not recognise option " << additionalArgs[i] << "." << endl;
656 return OPTION_ERROR;
657 }
658 }
659 }
660 }
661 if (!sc.mznlib().empty()) {
662 if (sc.mznlib().substr(0,2)=="-G") {
663 std::vector<std::string> additionalArgs({sc.mznlib()});
664 int i=0;
665 if (!flt.processOption(i, additionalArgs)) {
666 log << "Flattener does not recognise option " << sc.mznlib() << endl;
667 return OPTION_ERROR;
668 }
669 } else {
670 std::vector<std::string> additionalArgs(2);
671 additionalArgs[0] = "-I";
672 if (sc.mznlib_resolved().size()) {
673 additionalArgs[1] = sc.mznlib_resolved();
674 } else {
675 additionalArgs[1] = sc.mznlib();
676 }
677 int i=0;
678 if (!flt.processOption(i, additionalArgs)) {
679 log << "Flattener does not recognise option -I." << endl;
680 return OPTION_ERROR;
681 }
682 }
683 }
684 if (!sc.defaultFlags().empty()) {
685 std::vector<std::string> addedArgs;
686 addedArgs.push_back(argv[0]); // excutable name
687 for (auto& df : sc.defaultFlags()) {
688 addedArgs.push_back(df);
689 }
690 for (int i=1; i<argv.size(); i++) {
691 addedArgs.push_back(argv[i]);
692 }
693 argv = addedArgs;
694 argc = addedArgs.size();
695 }
696 break;
697 }
698 }
699
700 } catch (ConfigException& e) {
701 log << "Config exception: " << e.msg() << endl;
702 return OPTION_ERROR;
703 }
704
705 if (sf==NULL) {
706 log << "Solver " << solver << " not found." << endl;
707 return OPTION_ERROR;
708 }
709
710 for (i=1; i<argc; ++i) {
711 if ( !ifMzn2Fzn() ? s2out.processOption( i, argv ) : false ) {
712 } else if ((!isMznMzn || is_mzn2fzn) && flt.processOption(i, argv)) {
713 } else if (sf != NULL && sf->processOption(si_opt, i, argv)) {
714 } else {
715 std::string executable_name(argv[0]);
716 executable_name = executable_name.substr(executable_name.find_last_of("/\\") + 1);
717 log << executable_name << ": Unrecognized option or bad format `" << argv[i] << "'" << endl;
718 return OPTION_ERROR;
719 }
720 }
721 return OPTION_OK;
722
723 } else {
724 for (i=1; i<argc; ++i) {
725 if ( s2out.processOption( i, argv ) ) {
726 } else {
727 std::string executable_name(argv[0]);
728 executable_name = executable_name.substr(executable_name.find_last_of("/\\") + 1);
729 log << executable_name << ": Unrecognized option or bad format `" << argv[i] << "'" << endl;
730 return OPTION_ERROR;
731 }
732 }
733 return OPTION_OK;
734
735 }
736
737}
738
739/*
740void MznReader::flatten(const std::string& modelString, const std::string& modelName)
741{
742 flt.set_flag_verbose(flag_compiler_verbose);
743 flt.set_flag_statistics(flag_compiler_statistics);
744 Timer tm01;
745 flt.flatten(modelString, modelName);
746 /// The following message tells mzn-test.py that flattening succeeded.
747 if (flag_compiler_verbose)
748 log << " Flattening done, " << tm01.stoptime() << std::endl;
749}
750*/
751
752SolverInstance::Status MznSolver::solve()
753{
754 { // To be able to clean up flatzinc after PrcessFlt()
755 GCLock lock;
756 getSI()->processFlatZinc();
757 }
758 SolverInstance::Status status = getSI()->solve();
759 GCLock lock;
760 if (status==SolverInstance::SAT || status==SolverInstance::OPT) {
761 if ( !getSI()->getSolns2Out()->fStatusPrinted )
762 getSI()->getSolns2Out()->evalStatus( status );
763 }
764 else {
765 if ( !getSI()->getSolns2Out()->fStatusPrinted )
766 getSI()->getSolns2Out()->evalStatus( status );
767 }
768 if (si_opt->printStatistics)
769 printStatistics();
770 return status;
771}
772
773void MznSolver::printStatistics()
774{ // from flattener too? TODO
775 if (si)
776 getSI()->printStatistics();
777}
778
779SolverInstance::Status MznSolver::run(const std::vector<std::string>& args0, const std::string& model,
780 const std::string& exeName, const std::string& modelName) {
781 using namespace std::chrono;
782 steady_clock::time_point startTime = steady_clock::now();
783 std::vector<std::string> args = {exeName};
784 for (auto a : args0)
785 args.push_back(a);
786 switch (processOptions(args)) {
787 case OPTION_FINISH:
788 return SolverInstance::NONE;
789 case OPTION_ERROR:
790 printUsage();
791 os << "More info with \"" << exeName << " --help\"\n";
792 return SolverInstance::ERROR;
793 case OPTION_OK:
794 break;
795 }
796 if (!(!ifMzn2Fzn() && sf!=NULL && sf->getId() == "org.minizinc.mzn-mzn") && !flt.hasInputFiles() && model.empty()) {
797 // We are in solns2out mode
798 while ( std::cin.good() ) {
799 string line;
800 getline( std::cin, line );
801 line += '\n'; // need eols as in t=raw stream
802 s2out.feedRawDataChunk( line.c_str() );
803 }
804 return SolverInstance::NONE;
805 }
806
807 if (!ifMzn2Fzn() && sf->getId() == "org.minizinc.mzn-mzn") {
808 Env env;
809 si = sf->createSI(env, log, si_opt);
810 si->setSolns2Out( &s2out );
811 { // To be able to clean up flatzinc after PrcessFlt()
812 GCLock lock;
813 getSI()->_options->verbose = get_flag_verbose();
814 getSI()->_options->printStatistics = get_flag_statistics();
815 }
816 getSI()->solve();
817 return SolverInstance::NONE;
818 }
819
820 flatten(model,modelName);
821
822 if (!ifMzn2Fzn() && flag_overall_time_limit != 0) {
823 steady_clock::time_point afterFlattening = steady_clock::now();
824 milliseconds passed = duration_cast<milliseconds>(afterFlattening-startTime);
825 milliseconds time_limit(flag_overall_time_limit);
826 if (passed > time_limit) {
827 s2out.evalStatus( getFltStatus() );
828 return SolverInstance::UNKNOWN;
829 }
830 int time_left = (time_limit-passed).count();
831 std::vector<std::string> timeoutArgs(2);
832 timeoutArgs[0] = "--solver-time-limit";
833 std::ostringstream oss;
834 oss << time_left;
835 timeoutArgs[1] = oss.str();
836 int i=0;
837 sf->processOption(si_opt, i, timeoutArgs);
838 }
839
840 if (SolverInstance::UNKNOWN == getFltStatus())
841 {
842 if ( !ifMzn2Fzn() ) { // only then
843 // GCLock lock; // better locally, to enable cleanup after ProcessFlt()
844 addSolverInterface();
845 return solve();
846 }
847 return SolverInstance::NONE;
848 } else {
849 if ( !ifMzn2Fzn() )
850 s2out.evalStatus( getFltStatus() );
851 return getFltStatus();
852 } // Add evalOutput() here? TODO
853}
854#endif
855
856}; // namespace MiniZinc