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 <minizinc/param_config.hh>
27#include <minizinc/solver.hh>
28
29#include <chrono>
30#include <cstdlib>
31#include <ctime>
32#include <fstream>
33#include <iomanip>
34#include <iostream>
35#include <ratio>
36
37#ifdef HAS_GUROBI
38#include <minizinc/solvers/MIP/MIP_gurobi_solverfactory.hh>
39#endif
40#ifdef HAS_CPLEX
41#include <minizinc/solvers/MIP/MIP_cplex_solverfactory.hh>
42#endif
43#ifdef HAS_OSICBC
44#include <minizinc/solvers/MIP/MIP_osicbc_solverfactory.hh>
45#endif
46#ifdef HAS_XPRESS
47#include <minizinc/solvers/MIP/MIP_xpress_solverfactory.hh>
48#endif
49#ifdef HAS_GECODE
50#include <minizinc/solvers/gecode_solverfactory.hh>
51#endif
52#ifdef HAS_GEAS
53#include <minizinc/solvers/geas_solverfactory.hh>
54#endif
55#ifdef HAS_SCIP
56#include <minizinc/solvers/MIP/MIP_scip_solverfactory.hh>
57#endif
58#include <minizinc/solvers/fzn_solverfactory.hh>
59#include <minizinc/solvers/fzn_solverinstance.hh>
60#include <minizinc/solvers/mzn_solverfactory.hh>
61#include <minizinc/solvers/mzn_solverinstance.hh>
62#include <minizinc/solvers/nl/nl_solverfactory.hh>
63#include <minizinc/solvers/nl/nl_solverinstance.hh>
64
65using namespace std;
66using namespace MiniZinc;
67
68SolverInitialiser::SolverInitialiser() {
69#ifdef HAS_GUROBI
70 GurobiSolverFactoryInitialiser _gurobi_init;
71#endif
72#ifdef HAS_CPLEX
73 static CplexSolverFactoryInitialiser _cplex_init;
74#endif
75#ifdef HAS_OSICBC
76 static OSICBCSolverFactoryInitialiser _osicbc_init;
77#endif
78#ifdef HAS_XPRESS
79 static XpressSolverFactoryInitialiser _xpress_init;
80#endif
81#ifdef HAS_GECODE
82 static GecodeSolverFactoryInitialiser _gecode_init;
83#endif
84#ifdef HAS_GEAS
85 static GeasSolverFactoryInitialiser _geas_init;
86#endif
87#ifdef HAS_SCIP
88 static SCIPSolverFactoryInitialiser _scip_init;
89#endif
90 static FZNSolverFactoryInitialiser _fzn_init;
91 static MZNSolverFactoryInitialiser _mzn_init;
92 static NLSolverFactoryInitialiser _nl_init;
93}
94
95MZNFZNSolverFlag MZNFZNSolverFlag::std(const std::string& n0) {
96 const std::string argFlags("-I -n -p -r -n-o");
97 if (argFlags.find(n0) != std::string::npos) {
98 return MZNFZNSolverFlag(FT_ARG, n0);
99 }
100 return MZNFZNSolverFlag(FT_NOARG, n0);
101}
102
103MZNFZNSolverFlag MZNFZNSolverFlag::extra(const SolverConfig::ExtraFlag& ef) {
104 return MZNFZNSolverFlag(
105 ef.flagType == SolverConfig::ExtraFlag::FlagType::T_BOOL && ef.range.empty() ? FT_NOARG
106 : FT_ARG,
107 ef.flag);
108}
109
110// ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
111SolverRegistry* MiniZinc::get_global_solver_registry() {
112 static SolverRegistry sr;
113 return &sr;
114}
115
116void SolverRegistry::addSolverFactory(SolverFactory* pSF) {
117 assert(pSF);
118 _sfstorage.push_back(pSF);
119}
120
121void SolverRegistry::removeSolverFactory(SolverFactory* pSF) {
122 auto it = find(_sfstorage.begin(), _sfstorage.end(), pSF);
123 assert(pSF);
124 _sfstorage.erase(it);
125}
126
127void SolverRegistry::addFactoryFlag(const std::string& flag, SolverFactory* sf) {
128 assert(sf);
129 _factoryFlagStorage.push_back(std::make_pair(flag, sf));
130}
131
132void SolverRegistry::removeFactoryFlag(const std::string& flag, SolverFactory* sf) {
133 assert(sf);
134 auto it = find(_factoryFlagStorage.begin(), _factoryFlagStorage.end(), std::make_pair(flag, sf));
135 _factoryFlagStorage.erase(it);
136}
137
138/// Function createSI also adds each SI to the local storage
139SolverInstanceBase* SolverFactory::createSI(Env& env, std::ostream& log,
140 SolverInstanceBase::Options* opt) {
141 SolverInstanceBase* pSI = doCreateSI(env, log, opt);
142 if (pSI == nullptr) {
143 throw InternalError("SolverFactory: failed to initialize solver " + getDescription());
144 }
145 _sistorage.resize(_sistorage.size() + 1);
146 _sistorage.back().reset(pSI);
147 return pSI;
148}
149
150/// also providing a destroy function for a DLL or just special allocator etc.
151void SolverFactory::destroySI(SolverInstanceBase* pSI) {
152 auto it = _sistorage.begin();
153 for (; it != _sistorage.end(); ++it) {
154 if (it->get() == pSI) {
155 break;
156 }
157 }
158 if (_sistorage.end() == it) {
159 cerr << " SolverFactory: failed to remove solver at " << pSI << endl;
160 throw InternalError(" SolverFactory: failed to remove solver");
161 }
162 _sistorage.erase(it);
163}
164
165MznSolver::MznSolver(std::ostream& os0, std::ostream& log0)
166 : _solverConfigs(log0),
167 _flt(os0, log0, _solverConfigs.mznlibDir()),
168 _executableName("<executable>"),
169 _os(os0),
170 _log(log0),
171 s2out(os0, log0, _solverConfigs.mznlibDir()) {}
172
173MznSolver::~MznSolver() {
174 // if (si) // first the solver
175 // CleanupSolverInterface(si);
176 // TODO cleanup the used solver interfaces
177 _si = nullptr;
178 _siOpt = nullptr;
179 GC::trigger();
180}
181
182bool MznSolver::ifMzn2Fzn() const { return _isMzn2fzn; }
183
184bool MznSolver::ifSolns2out() const { return s2out.opt.flagStandaloneSolns2Out; }
185
186void MznSolver::addSolverInterface(SolverFactory* sf) {
187 _si = sf->createSI(*_flt.getEnv(), _log, _siOpt);
188 assert(_si);
189 if (s2out.getEnv() == nullptr) {
190 s2out.initFromEnv(_flt.getEnv());
191 }
192 _si->setSolns2Out(&s2out);
193 if (flagCompilerVerbose) {
194 _log
195 // << " ---------------------------------------------------------------------------\n"
196 << " % SOLVING PHASE\n"
197 << sf->getDescription(_siOpt) << endl;
198 }
199}
200
201void MznSolver::addSolverInterface() {
202 GCLock lock;
203 if (_sf == nullptr) {
204 if (get_global_solver_registry()->getSolverFactories().empty()) {
205 _log << " MznSolver: NO SOLVER FACTORIES LINKED." << endl;
206 assert(0);
207 }
208 _sf = get_global_solver_registry()->getSolverFactories().back();
209 }
210 addSolverInterface(_sf);
211}
212
213void MznSolver::printUsage() {
214 _os << _executableName << ": ";
215 if (ifMzn2Fzn()) {
216 _os << "MiniZinc to FlatZinc converter.\n"
217 << "Usage: " << _executableName
218 << " [<options>] [-I <include path>] <model>.mzn [<data>.dzn ...]" << std::endl;
219 } else if (ifSolns2out()) {
220 _os << "Solutions to output translator.\n"
221 << "Usage: " << _executableName << " [<options>] <model>.ozn" << std::endl;
222 } else {
223 _os << "MiniZinc driver.\n"
224 << "Usage: " << _executableName
225 << " [<options>] [-I <include path>] <model>.mzn [<data>.dzn ...] or just <flat>.fzn"
226 << std::endl;
227 }
228}
229
230void MznSolver::printHelp(const std::string& selectedSolver) {
231 printUsage();
232 _os << "General options:" << std::endl
233 << " --help, -h\n Print this help message." << std::endl
234 << " --version\n Print version information." << std::endl
235 << " --solvers\n Print list of available solvers." << std::endl
236 << " --time-limit <ms>\n Stop after <ms> milliseconds (includes compilation and solving)."
237 << std::endl
238 << " --solver <solver id>, --solver <solver config file>.msc\n Select solver to use."
239 << std::endl
240 << " --help <solver id>\n Print help for a particular solver." << std::endl
241 << " -v, -l, --verbose\n Print progress/log statements. Note that some solvers may log "
242 "to "
243 "stdout."
244 << std::endl
245 << " --verbose-compilation\n Print progress/log statements for compilation." << std::endl
246 << " -s, --statistics\n Print statistics." << std::endl
247 << " --compiler-statistics\n Print statistics for compilation." << std::endl
248 << " -c, --compile\n Compile only (do not run solver)." << std::endl
249 << " --config-dirs\n Output configuration directories." << std::endl
250 << " --param-file <file>\n Load parameters from the given JSON file." << std::endl;
251
252 if (selectedSolver.empty()) {
253 _flt.printHelp(_os);
254 _os << endl;
255 if (!ifMzn2Fzn()) {
256 Solns2Out::printHelp(_os);
257 _os << endl;
258 }
259 _os << "Available solvers (get help using --help <solver id>):" << endl;
260 std::vector<std::string> solvers = _solverConfigs.solvers();
261 if (solvers.empty()) {
262 cout << " none.\n";
263 }
264 for (auto& solver : solvers) {
265 cout << " " << solver << endl;
266 }
267 } else {
268 const SolverConfig& sc = _solverConfigs.config(selectedSolver);
269 string solverId = sc.executable().empty() ? sc.id()
270 : (sc.supportsMzn() ? string("org.minizinc.mzn-mzn")
271 : string("org.minizinc.mzn-fzn"));
272 bool found = false;
273 for (auto it = get_global_solver_registry()->getSolverFactories().rbegin();
274 it != get_global_solver_registry()->getSolverFactories().rend(); ++it) {
275 if ((*it)->getId() == solverId) {
276 _os << endl;
277 (*it)->printHelp(_os);
278 if (!sc.executable().empty() && !sc.extraFlags().empty()) {
279 _os << "Extra solver flags (use with ";
280 _os << (sc.supportsMzn() ? "--mzn-flags" : "--fzn-flags") << ")" << endl;
281 for (const SolverConfig::ExtraFlag& ef : sc.extraFlags()) {
282 _os << " " << ef.flag << endl << " " << ef.description << endl;
283 }
284 }
285 found = true;
286 }
287 }
288 if (!found) {
289 _os << "No help found for solver " << selectedSolver << endl;
290 }
291 }
292}
293
294void add_flags(const std::string& sep, const std::vector<std::string>& in_args,
295 std::vector<std::string>& out_args) {
296 for (const std::string& arg : in_args) {
297 out_args.push_back(sep);
298 out_args.push_back(arg);
299 }
300}
301
302MznSolver::OptionStatus MznSolver::processOptions(std::vector<std::string>& argv) {
303 _executableName = argv[0];
304 _executableName = _executableName.substr(_executableName.find_last_of("/\\") + 1);
305 size_t lastdot = _executableName.find_last_of('.');
306 if (lastdot != std::string::npos) {
307 _executableName = _executableName.substr(0, lastdot);
308 }
309 string solver;
310 bool load_params = false;
311 bool mzn2fzn_exe = (_executableName == "mzn2fzn");
312 if (mzn2fzn_exe) {
313 _isMzn2fzn = true;
314 } else if (_executableName == "solns2out") {
315 s2out.opt.flagStandaloneSolns2Out = true;
316 flagIsSolns2out = true;
317 }
318 bool compileSolutionChecker = false;
319 int i = 1;
320 int j = 1;
321 int argc = static_cast<int>(argv.size());
322 std::vector<std::string> workingDirs = {""};
323 if (argc < 2) {
324 return OPTION_ERROR;
325 }
326
327 // Add params from a file if necessary
328 std::vector<std::string> paramFiles;
329 for (i = 1; i < argc; ++i) {
330 string paramFile;
331 bool usedFlag = false;
332 bool pushWorkingDir = true;
333
334 if (argv[i] == "--param-file") {
335 usedFlag = true;
336 ++i;
337 if (i == argc) {
338 _log << "Argument required for --param-file" << endl;
339 return OPTION_ERROR;
340 }
341 paramFile = argv[i];
342 } else if (argv[i] == "--param-file-no-push") {
343 usedFlag = true;
344 pushWorkingDir = false;
345 ++i;
346 if (i == argc) {
347 _log << "Argument required for --param-file-no-push" << endl;
348 return OPTION_ERROR;
349 }
350 paramFile = argv[i];
351 } else if (argv[i] == "--push-working-directory") {
352 ++i;
353 workingDirs.push_back(argv[i]);
354 } else if (argv[i] == "--pop-working-directory") {
355 workingDirs.pop_back();
356 } else {
357 size_t last_dot = argv[i].find_last_of('.');
358 if (last_dot != string::npos && argv[i].substr(last_dot, string::npos) == ".mpc") {
359 paramFile = argv[i];
360 }
361 }
362
363 if (!paramFile.empty()) {
364 try {
365 auto paramFilePath = FileUtils::file_path(paramFile, workingDirs.back());
366 if (std::find(paramFiles.begin(), paramFiles.end(), paramFilePath) != paramFiles.end()) {
367 throw ParamException("Cyclic parameter configuration file");
368 }
369 // add parameter file arguments
370 ParamConfig pc;
371 pc.blacklist(
372 {"--solvers", "--solvers-json", "--solver-json", "--help", "-h", "--config-dirs"});
373 pc.negatedFlag("-i", "-n-i");
374 pc.negatedFlag("--intermediate", "--no-intermediate");
375 pc.negatedFlag("--intermediate-solutions", "--no-intermediate-solutions");
376 pc.negatedFlag("--all-satisfaction", "--disable-all-satisfaction");
377 pc.load(paramFilePath);
378
379 // Insert the new options
380 auto toInsert = pc.argv();
381 auto remove = argv.begin() + (usedFlag ? i - 1 : i);
382 auto position = argv.erase(remove, argv.begin() + i + 1);
383 if (pushWorkingDir) {
384 position =
385 argv.insert(position, {"--push-working-directory",
386 FileUtils::file_path(FileUtils::dir_name(paramFilePath))}) +
387 2;
388 }
389 position = argv.insert(position, toInsert.begin(), toInsert.end()) + toInsert.size();
390 if (pushWorkingDir) {
391 position = argv.insert(position, "--pop-working-directory") + 1;
392 }
393 paramFiles.push_back(paramFilePath);
394 argc = argv.size();
395
396 // Have to process the newly added options
397 if (usedFlag) {
398 i -= 2;
399 } else {
400 i--;
401 }
402 } catch (ParamException& e) {
403 _log << "Solver parameter exception: " << e.msg() << endl;
404 return OPTION_ERROR;
405 }
406 }
407 }
408
409 // Process any registered factory flags
410 const auto& factoryFlags = get_global_solver_registry()->getFactoryFlags();
411 std::unordered_map<std::string, std::vector<std::string>> reducedSolverDefaults;
412 if (!factoryFlags.empty()) {
413 // Process solver default factory flags
414 for (const auto& factoryFlag : factoryFlags) {
415 auto factoryId = factoryFlag.second->getId();
416 if (reducedSolverDefaults.count(factoryId) == 0) {
417 reducedSolverDefaults.insert({factoryId, _solverConfigs.defaultOptions(factoryId)});
418 }
419 auto& defaultArgs = reducedSolverDefaults.find(factoryId)->second;
420 std::vector<std::string> keep;
421 for (i = 0; i < defaultArgs.size(); i++) {
422 if (defaultArgs[i] != factoryFlag.first ||
423 !factoryFlag.second->processFactoryOption(i, defaultArgs)) {
424 keep.push_back(defaultArgs[i]);
425 }
426 }
427 defaultArgs = keep;
428 }
429 // Process command line factory flags
430 std::vector<std::string> remaining = {argv[0]};
431 for (i = 1; i < argc; i++) {
432 bool ok = false;
433 if (argv[i] == "--push-working-directory") {
434 remaining.push_back(argv[i]);
435 i++;
436 workingDirs.push_back(argv[i]);
437 } else if (argv[i] == "--pop-working-directory") {
438 workingDirs.pop_back();
439 } else {
440 for (const auto& factoryFlag : factoryFlags) {
441 if (argv[i] == factoryFlag.first &&
442 factoryFlag.second->processFactoryOption(i, argv, workingDirs.back())) {
443 ok = true;
444 break;
445 }
446 }
447 }
448 if (!ok) {
449 remaining.push_back(argv[i]);
450 }
451 }
452 argv = remaining;
453 argc = remaining.size();
454 }
455 for (auto* sf : get_global_solver_registry()->getSolverFactories()) {
456 // Notify solver factories that factory flags are done
457 sf->factoryOptionsFinished();
458 }
459
460 // After this point all solver configurations must be available
461 _solverConfigs.populate(_log);
462
463 for (i = 1; i < argc; ++i) {
464 if (argv[i] == "-h" || argv[i] == "--help") {
465 if (argc > i + 1) {
466 printHelp(argv[i + 1]);
467 } else {
468 printHelp();
469 }
470 return OPTION_FINISH;
471 }
472 if (argv[i] == "--version") {
473 Flattener::printVersion(cout);
474 return OPTION_FINISH;
475 }
476 if (argv[i] == "--solvers") {
477 cout << "MiniZinc driver.\nAvailable solver configurations:\n";
478 std::vector<std::string> solvers = _solverConfigs.solvers();
479 if (solvers.empty()) {
480 cout << " none.\n";
481 }
482 for (auto& solver : solvers) {
483 cout << " " << solver << endl;
484 }
485 cout << "Search path for solver configurations:\n";
486 for (const string& p : _solverConfigs.solverConfigsPath()) {
487 cout << " " << p << endl;
488 }
489 return OPTION_FINISH;
490 }
491 if (argv[i] == "--solvers-json") {
492 cout << _solverConfigs.solverConfigsJSON();
493 return OPTION_FINISH;
494 }
495 if (argv[i] == "--solver-json") {
496 ++i;
497 if (i == argc) {
498 _log << "Argument required for --solver-json" << endl;
499 return OPTION_ERROR;
500 }
501 if (!solver.empty() && solver != argv[i]) {
502 _log << "Only one --solver-json option allowed" << endl;
503 return OPTION_ERROR;
504 }
505 solver = argv[i];
506 const SolverConfig& sc = _solverConfigs.config(solver);
507 cout << sc.toJSON(_solverConfigs);
508 return OPTION_FINISH;
509 }
510 if (argv[i] == "--config-dirs") {
511 GCLock lock;
512 cout << "{\n";
513 cout << " \"globalConfigFile\" : \""
514 << Printer::escapeStringLit(FileUtils::global_config_file()) << "\",\n";
515 cout << " \"userConfigFile\" : \"" << Printer::escapeStringLit(FileUtils::user_config_file())
516 << "\",\n";
517 cout << " \"userSolverConfigDir\" : \""
518 << Printer::escapeStringLit(FileUtils::user_config_dir()) << "/solvers\",\n";
519 cout << " \"mznStdlibDir\" : \"" << Printer::escapeStringLit(_solverConfigs.mznlibDir())
520 << "\"\n";
521 cout << "}\n";
522 return OPTION_FINISH;
523 }
524 if (argv[i] == "--time-limit") {
525 ++i;
526 if (i == argc) {
527 _log << "Argument required for --time-limit" << endl;
528 return OPTION_ERROR;
529 }
530 flagOverallTimeLimit = atoi(argv[i].c_str());
531 } else if (argv[i] == "--solver") {
532 ++i;
533 if (i == argc) {
534 _log << "Argument required for --solver" << endl;
535 return OPTION_ERROR;
536 }
537 if (!solver.empty() && solver != argv[i]) {
538 _log << "Only one --solver option allowed" << endl;
539 return OPTION_ERROR;
540 }
541 solver = argv[i];
542 } else if (argv[i] == "-c" || argv[i] == "--compile") {
543 _isMzn2fzn = true;
544 } else if (argv[i] == "-v" || argv[i] == "--verbose" || argv[i] == "-l") {
545 flagVerbose = true;
546 flagCompilerVerbose = true;
547 } else if (argv[i] == "--verbose-compilation") {
548 flagCompilerVerbose = true;
549 } else if (argv[i] == "-s" || argv[i] == "--statistics") {
550 flagStatistics = true;
551 flagCompilerStatistics = true;
552 } else if (argv[i] == "--compiler-statistics") {
553 flagCompilerStatistics = true;
554 } else {
555 if ((argv[i] == "--fzn-cmd" || argv[i] == "--flatzinc-cmd") && solver.empty()) {
556 solver = "org.minizinc.mzn-fzn";
557 }
558 if (argv[i] == "--compile-solution-checker") {
559 compileSolutionChecker = true;
560 }
561 if (argv[i] == "--ozn-file") {
562 flagIsSolns2out = true;
563 }
564 argv[j++] = argv[i];
565 }
566 }
567 argv.resize(j);
568 argc = j;
569
570 if ((mzn2fzn_exe || compileSolutionChecker) && solver.empty()) {
571 solver = "org.minizinc.mzn-fzn";
572 }
573
574 if (flagVerbose) {
575 argv.emplace_back("--verbose-solving");
576 argc++;
577 }
578 if (flagStatistics) {
579 argv.emplace_back("--solver-statistics");
580 argc++;
581 }
582
583 _flt.setFlagOutputByDefault(ifMzn2Fzn());
584
585 bool isMznMzn = false;
586
587 if (!flagIsSolns2out) {
588 try {
589 const SolverConfig& sc = _solverConfigs.config(solver);
590 string solverId;
591 if (sc.executable().empty()) {
592 solverId = sc.id();
593 } else if (sc.supportsMzn()) {
594 solverId = "org.minizinc.mzn-mzn";
595 } else if (sc.supportsFzn()) {
596 solverId = "org.minizinc.mzn-fzn";
597 } else if (sc.supportsNL()) {
598 solverId = "org.minizinc.mzn-nl";
599 } else {
600 _log << "Selected solver does not support MiniZinc, FlatZinc or NL input." << endl;
601 return OPTION_ERROR;
602 }
603
604 // Check support of -a and -i
605 for (const auto& flag : sc.stdFlags()) {
606 if (flag == "-a") {
607 _supportsA = true;
608 } else if (flag == "-i") {
609 _supportsI = true;
610 }
611 }
612
613 for (auto* it : get_global_solver_registry()->getSolverFactories()) {
614 if (it->getId() ==
615 solverId) { /// TODO: also check version (currently assumes all ids are unique)
616 _sf = it;
617 delete _siOpt;
618 _siOpt = _sf->createOptions();
619 if (!sc.executable().empty() || solverId == "org.minizinc.mzn-fzn" ||
620 solverId == "org.minizinc.mzn-nl") {
621 std::vector<MZNFZNSolverFlag> acceptedFlags;
622 for (const auto& sf : sc.stdFlags()) {
623 acceptedFlags.push_back(MZNFZNSolverFlag::std(sf));
624 }
625 for (const auto& ef : sc.extraFlags()) {
626 acceptedFlags.push_back(MZNFZNSolverFlag::extra(ef));
627 }
628
629 // Collect arguments required for underlying exe
630 vector<string> fzn_mzn_flags;
631 if (sc.needsStdlibDir()) {
632 fzn_mzn_flags.emplace_back("--stdlib-dir");
633 fzn_mzn_flags.push_back(FileUtils::share_directory());
634 }
635 if (sc.needsMznExecutable()) {
636 fzn_mzn_flags.emplace_back("--minizinc-exe");
637 fzn_mzn_flags.push_back(FileUtils::progpath() + "/" + _executableName);
638 }
639
640 if (sc.supportsMzn()) {
641 isMznMzn = true;
642 MZNSolverFactory::setAcceptedFlags(_siOpt, acceptedFlags);
643 std::vector<std::string> additionalArgs_s;
644 additionalArgs_s.emplace_back("-m");
645 if (!sc.executableResolved().empty()) {
646 additionalArgs_s.push_back(sc.executableResolved());
647 } else {
648 additionalArgs_s.push_back(sc.executable());
649 }
650
651 if (!fzn_mzn_flags.empty()) {
652 add_flags("--mzn-flag", fzn_mzn_flags, additionalArgs_s);
653 }
654
655 // This should maybe be moved to fill in fzn_mzn_flags when
656 // --find-muses is implemented (these arguments will be passed
657 // through to the subsolver of findMUS)
658 if (!sc.mznlib().empty()) {
659 if (sc.mznlib().substr(0, 2) == "-G") {
660 additionalArgs_s.emplace_back("--mzn-flag");
661 additionalArgs_s.push_back(sc.mznlib());
662 } else {
663 additionalArgs_s.emplace_back("--mzn-flag");
664 additionalArgs_s.emplace_back("-I");
665 additionalArgs_s.emplace_back("--mzn-flag");
666 std::string _mznlib;
667 if (!sc.mznlibResolved().empty()) {
668 _mznlib = sc.mznlibResolved();
669 } else {
670 _mznlib = sc.mznlib();
671 }
672 additionalArgs_s.push_back(_mznlib);
673 }
674 }
675
676 for (i = 0; i < additionalArgs_s.size(); ++i) {
677 bool success = _sf->processOption(_siOpt, i, additionalArgs_s);
678 if (!success) {
679 _log << "Solver backend " << solverId << " does not recognise option "
680 << additionalArgs_s[i] << "." << endl;
681 return OPTION_ERROR;
682 }
683 }
684 } else {
685 // supports fzn or nl
686 std::vector<std::string> additionalArgs;
687 if (sc.supportsFzn()) {
688 FZNSolverFactory::setAcceptedFlags(_siOpt, acceptedFlags);
689 additionalArgs.emplace_back("--fzn-cmd");
690 } else {
691 // supports nl
692 additionalArgs.emplace_back("--nl-cmd");
693 }
694 if (!sc.executableResolved().empty()) {
695 additionalArgs.push_back(sc.executableResolved());
696 } else {
697 additionalArgs.push_back(sc.executable());
698 }
699 if (!fzn_mzn_flags.empty()) {
700 if (sc.supportsFzn()) {
701 add_flags("--fzn-flag", fzn_mzn_flags, additionalArgs);
702 } else {
703 add_flags("--nl-flag", fzn_mzn_flags, additionalArgs);
704 }
705 }
706 if (sc.needsPathsFile()) {
707 // Instruct flattener to hold onto paths
708 int i = 0;
709 vector<string> args{"--keep-paths"};
710 _flt.processOption(i, args);
711
712 // Instruct FznSolverInstance to write a path file
713 // and pass it to the executable with --paths arg
714 additionalArgs.emplace_back("--fzn-needs-paths");
715 }
716 if (!sc.needsSolns2Out()) {
717 additionalArgs.emplace_back("--fzn-output-passthrough");
718 }
719 int i = 0;
720 for (i = 0; i < additionalArgs.size(); ++i) {
721 bool success = _sf->processOption(_siOpt, i, additionalArgs);
722 if (!success) {
723 _log << "Solver backend " << solverId << " does not recognise option "
724 << additionalArgs[i] << "." << endl;
725 return OPTION_ERROR;
726 }
727 }
728 }
729 }
730 if (!sc.mznlib().empty()) {
731 if (sc.mznlib().substr(0, 2) == "-G") {
732 std::vector<std::string> additionalArgs({sc.mznlib()});
733 int i = 0;
734 if (!_flt.processOption(i, additionalArgs)) {
735 _log << "Flattener does not recognise option " << sc.mznlib() << endl;
736 return OPTION_ERROR;
737 }
738 } else {
739 std::vector<std::string> additionalArgs(2);
740 additionalArgs[0] = "-I";
741 if (!sc.mznlibResolved().empty()) {
742 additionalArgs[1] = sc.mznlibResolved();
743 } else {
744 additionalArgs[1] = sc.mznlib();
745 }
746 int i = 0;
747 if (!_flt.processOption(i, additionalArgs)) {
748 _log << "Flattener does not recognise option -I." << endl;
749 return OPTION_ERROR;
750 }
751 }
752 }
753 auto reducedDefaultFlags = reducedSolverDefaults.find(sc.id());
754 const auto& defaultFlags = reducedDefaultFlags == reducedSolverDefaults.end()
755 ? sc.defaultFlags()
756 : reducedDefaultFlags->second;
757 if (!defaultFlags.empty()) {
758 std::vector<std::string> addedArgs;
759 addedArgs.push_back(argv[0]); // excutable name
760 for (const auto& df : defaultFlags) {
761 addedArgs.push_back(df);
762 }
763 for (int i = 1; i < argv.size(); i++) {
764 addedArgs.push_back(argv[i]);
765 }
766 argv = addedArgs;
767 argc = addedArgs.size();
768 }
769 break;
770 }
771 }
772
773 } catch (ConfigException& e) {
774 _log << "Config exception: " << e.msg() << endl;
775 return OPTION_ERROR;
776 }
777
778 if (_sf == nullptr) {
779 _log << "Solver " << solver << " not found." << endl;
780 return OPTION_ERROR;
781 }
782
783 CLOParser cop(i, argv); // For special handling of -a, -i and -n-i
784 for (i = 1; i < argc; ++i) {
785 if (argv[i] == "--push-working-directory") {
786 i++;
787 workingDirs.push_back(argv[i]);
788 } else if (argv[i] == "--pop-working-directory") {
789 workingDirs.pop_back();
790 } else if (!ifMzn2Fzn() ? s2out.processOption(i, argv, workingDirs.back())
791 : false) { // NOLINT: Allow repeated empty if
792 // Processed by Solns2Out
793 } else if ((!isMznMzn || _isMzn2fzn) &&
794 _flt.processOption(i, argv,
795 workingDirs.back())) { // NOLINT: Allow repeated empty if
796 // Processed by Flattener
797 } else if ((_supportsA || _supportsI) && cop.get("-a --all --all-solns --all-solutions")) {
798 _flagAllSatisfaction = true;
799 _flagIntermediate = true;
800 } else if ((_supportsA || _supportsI) &&
801 cop.get("-i --intermediate --intermediate-solutions")) {
802 _flagIntermediate = true;
803 } else if (cop.getOption("-n-i --no-intermediate --no-intermediate-solutions")) {
804 _flagIntermediate = false;
805 } else if (_supportsA && cop.get("--all-satisfaction")) {
806 _flagAllSatisfaction = true;
807 } else if (cop.get("--disable-all-satisfaction")) {
808 _flagAllSatisfaction = false;
809 } else if (_sf != nullptr &&
810 _sf->processOption(_siOpt, i, argv)) { // NOLINT: Allow repeated empty if
811 // Processed by Solver Factory
812 } else {
813 std::string executable_name(argv[0]);
814 executable_name = executable_name.substr(executable_name.find_last_of("/\\") + 1);
815 _log << executable_name << ": Unrecognized option or bad format `" << argv[i] << "'"
816 << endl;
817 return OPTION_ERROR;
818 }
819 }
820 return OPTION_OK;
821 }
822 for (i = 1; i < argc; ++i) {
823 if (argv[i] == "--push-working-directory") {
824 i++;
825 workingDirs.push_back(argv[i]);
826 } else if (argv[i] == "--pop-working-directory") {
827 workingDirs.pop_back();
828 } else if (s2out.processOption(i, argv, workingDirs.back())) {
829 // Processed by Solns2Out
830 } else {
831 std::string executable_name(argv[0]);
832 executable_name = executable_name.substr(executable_name.find_last_of("/\\") + 1);
833 _log << executable_name << ": Unrecognized option or bad format `" << argv[i] << "'" << endl;
834 return OPTION_ERROR;
835 }
836 }
837 return OPTION_OK;
838}
839
840void MznSolver::flatten(const std::string& modelString, const std::string& modelName) {
841 _flt.setFlagVerbose(flagCompilerVerbose);
842 _flt.setFlagStatistics(flagCompilerStatistics);
843 _flt.setFlagTimelimit(flagOverallTimeLimit);
844 _flt.flatten(modelString, modelName);
845}
846
847SolverInstance::Status MznSolver::solve() {
848 { // To be able to clean up flatzinc after PrcessFlt()
849 GCLock lock;
850 getSI()->processFlatZinc();
851 }
852 SolverInstance::Status status = getSI()->solve();
853 GCLock lock;
854 if (!getSI()->getSolns2Out()->fStatusPrinted) {
855 getSI()->getSolns2Out()->evalStatus(status);
856 }
857 if (_siOpt->printStatistics) {
858 getSI()->printStatistics();
859 }
860 if (flagStatistics) {
861 getSI()->getSolns2Out()->printStatistics(_os);
862 }
863 return status;
864}
865
866SolverInstance::Status MznSolver::run(const std::vector<std::string>& args0,
867 const std::string& model, const std::string& exeName,
868 const std::string& modelName) {
869 using namespace std::chrono;
870 steady_clock::time_point startTime = steady_clock::now();
871 std::vector<std::string> args = {exeName};
872 for (const auto& a : args0) {
873 args.push_back(a);
874 }
875 switch (processOptions(args)) {
876 case OPTION_FINISH:
877 return SolverInstance::NONE;
878 case OPTION_ERROR:
879 printUsage();
880 _os << "More info with \"" << exeName << " --help\"\n";
881 return SolverInstance::ERROR;
882 case OPTION_OK:
883 break;
884 }
885 if (flagIsSolns2out &&
886 (ifMzn2Fzn() || _sf == nullptr || _sf->getId() != "org.minizinc.mzn-mzn") &&
887 !_flt.hasInputFiles() && model.empty()) {
888 // We are in solns2out mode
889 while (std::cin.good()) {
890 string line;
891 getline(std::cin, line);
892 line += '\n'; // need eols as in t=raw stream
893 s2out.feedRawDataChunk(line.c_str());
894 }
895 return SolverInstance::NONE;
896 }
897
898 if (!ifMzn2Fzn() && _sf->getId() == "org.minizinc.mzn-mzn") {
899 Env env;
900 _si = _sf->createSI(env, _log, _siOpt);
901 _si->setSolns2Out(&s2out);
902 { // To be able to clean up flatzinc after PrcessFlt()
903 GCLock lock;
904 _si->options()->verbose = getFlagVerbose();
905 _si->options()->printStatistics = getFlagStatistics();
906 }
907 _si->solve();
908 return SolverInstance::NONE;
909 }
910
911 try {
912 flatten(model, modelName);
913 } catch (Timeout&) {
914 s2out.evalStatus(SolverInstance::UNKNOWN);
915 return SolverInstance::UNKNOWN;
916 }
917
918 if (!ifMzn2Fzn() && flagOverallTimeLimit != 0) {
919 steady_clock::time_point afterFlattening = steady_clock::now();
920 milliseconds passed = duration_cast<milliseconds>(afterFlattening - startTime);
921 milliseconds time_limit(flagOverallTimeLimit);
922 if (passed > time_limit) {
923 s2out.evalStatus(getFltStatus());
924 return SolverInstance::UNKNOWN;
925 }
926 int time_left = (time_limit - passed).count();
927 std::vector<std::string> timeoutArgs(2);
928 timeoutArgs[0] = "--solver-time-limit";
929 std::ostringstream oss;
930 oss << time_left;
931 timeoutArgs[1] = oss.str();
932 int i = 0;
933 _sf->processOption(_siOpt, i, timeoutArgs);
934 }
935
936 if (SolverInstance::UNKNOWN == getFltStatus()) {
937 if (!ifMzn2Fzn()) { // only then
938 // Special handling of basic stdFlags
939 auto* solve_item = _flt.getEnv()->model()->solveItem();
940 bool is_sat_problem =
941 solve_item != nullptr ? solve_item->st() == SolveI::SolveType::ST_SAT : true;
942 if (is_sat_problem && _flagAllSatisfaction) {
943 if (_supportsA) {
944 std::vector<std::string> a_flag = {"-a"};
945 int i = 0;
946 _sf->processOption(_siOpt, i, a_flag);
947 } else {
948 // Solver does not support -a
949 _log << "WARNING: Solver does not support all solutions for satisfaction problems."
950 << endl;
951 }
952 }
953 if (!is_sat_problem && _flagIntermediate) {
954 std::vector<std::string> i_flag(1);
955 i_flag[0] = _supportsI ? "-i" : "-a"; // Fallback to -a if -i is not supported
956 int i = 0;
957 _sf->processOption(_siOpt, i, i_flag);
958 }
959
960 // GCLock lock; // better locally, to enable cleanup after ProcessFlt()
961 addSolverInterface();
962 return solve();
963 }
964 return SolverInstance::NONE;
965 }
966 if (!ifMzn2Fzn()) {
967 s2out.evalStatus(getFltStatus());
968 }
969 return getFltStatus();
970 // Add evalOutput() here? TODO
971}