this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2
3/*
4 * Main authors:
5 * Guido Tack <guido.tack@monash.edu>
6 * Gleb Belov <gleb.belov@monash.edu>
7 */
8
9/* This Source Code Form is subject to the terms of the Mozilla Public
10 * License, v. 2.0. If a copy of the MPL was not distributed with this
11 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
12
13/* This (main) file coordinates flattening and solving.
14 * The corresponding modules are flexibly plugged in
15 * as derived classes, prospectively from DLLs.
16 * A flattening module should provide MinZinc::GetFlattener()
17 * A solving module should provide an object of a class derived from SolverFactory.
18 * Need to get more flexible for multi-pass & multi-solving stuff TODO
19 */
20
21#ifdef _MSC_VER
22#define _CRT_SECURE_NO_WARNINGS
23#endif
24
25#include <chrono>
26#include <cstdlib>
27#include <ctime>
28#include <fstream>
29#include <iomanip>
30#include <iostream>
31#include <ratio>
32
33using namespace std;
34
35#include <minizinc/flat_exp.hh>
36#include <minizinc/solver.hh>
37#include <minizinc/support/mza_parser.hh>
38
39using namespace MiniZinc;
40
41#ifdef HAS_GUROBI
42#include <minizinc/solvers/MIP/MIP_gurobi_solverfactory.hh>
43#endif
44#ifdef HAS_CPLEX
45#include <minizinc/solvers/MIP/MIP_cplex_solverfactory.hh>
46#endif
47#ifdef HAS_OSICBC
48#include <minizinc/solvers/MIP/MIP_osicbc_solverfactory.hh>
49#endif
50#ifdef HAS_XPRESS
51#include <minizinc/solvers/MIP/MIP_xpress_solverfactory.hh>
52#endif
53#ifdef HAS_GECODE
54#include <minizinc/solvers/gecode_solverfactory.hh>
55#endif
56#ifdef HAS_GEAS
57#include <minizinc/solvers/geas_solverfactory.hh>
58#endif
59#ifdef HAS_SCIP
60#include <minizinc/solvers/MIP/MIP_scip_solverfactory.hh>
61#endif
62#include <minizinc/solvers/fzn_solverfactory.hh>
63#include <minizinc/solvers/fzn_solverinstance.hh>
64#include <minizinc/solvers/mzn_solverfactory.hh>
65#include <minizinc/solvers/mzn_solverinstance.hh>
66#include <minizinc/solvers/nl/nl_solverfactory.hh>
67#include <minizinc/solvers/nl/nl_solverinstance.hh>
68
69SolverInitialiser::SolverInitialiser(void) {
70#ifdef HAS_GUROBI
71 Gurobi_SolverFactoryInitialiser _gurobi_init;
72#endif
73#ifdef HAS_CPLEX
74 static Cplex_SolverFactoryInitialiser _cplex_init;
75#endif
76#ifdef HAS_OSICBC
77 static OSICBC_SolverFactoryInitialiser _osicbc_init;
78#endif
79#ifdef HAS_XPRESS
80 static Xpress_SolverFactoryInitialiser _xpress_init;
81#endif
82#ifdef HAS_GECODE
83 static Gecode_SolverFactoryInitialiser _gecode_init;
84#endif
85#ifdef HAS_GEAS
86 static Geas_SolverFactoryInitialiser _geas_init;
87#endif
88#ifdef HAS_SCIP
89 static SCIP_SolverFactoryInitialiser _scip_init;
90#endif
91 static FZN_SolverFactoryInitialiser _fzn_init;
92 static MZN_SolverFactoryInitialiser _mzn_init;
93 static NL_SolverFactoryInitialiser _nl_init;
94}
95
96MZNFZNSolverFlag MZNFZNSolverFlag::std(const std::string& n0) {
97 const std::string argFlags("-I -n -p -r");
98 if (argFlags.find(n0) != std::string::npos) return MZNFZNSolverFlag(FT_ARG, n0);
99 return MZNFZNSolverFlag(FT_NOARG, n0);
100}
101
102MZNFZNSolverFlag MZNFZNSolverFlag::extra(const std::string& n0, const std::string& t0) {
103 return MZNFZNSolverFlag(t0 == "bool" ? FT_NOARG : FT_ARG, n0);
104}
105
106// ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
107SolverRegistry* MiniZinc::getGlobalSolverRegistry() {
108 static SolverRegistry sr;
109 return &sr;
110}
111
112void SolverRegistry::addSolverFactory(SolverFactory* pSF) {
113 assert(pSF);
114 sfstorage.push_back(pSF);
115}
116
117void SolverRegistry::removeSolverFactory(SolverFactory* pSF) {
118 auto it = find(sfstorage.begin(), sfstorage.end(), pSF);
119 assert(pSF);
120 sfstorage.erase(it);
121}
122
123/// Function createSI also adds each SI to the local storage
124SolverInstanceBase* SolverFactory::createSI(std::ostream& log, SolverInstanceBase::Options* opt) {
125 SolverInstanceBase* pSI = doCreateSI(log, opt);
126 if (!pSI) {
127 throw InternalError("SolverFactory: failed to initialize solver " + getDescription());
128 }
129 sistorage.resize(sistorage.size() + 1);
130 sistorage.back().reset(pSI);
131 return pSI;
132}
133
134/// also providing a destroy function for a DLL or just special allocator etc.
135void SolverFactory::destroySI(SolverInstanceBase* pSI) {
136 auto it = sistorage.begin();
137 for (; it != sistorage.end(); ++it)
138 if (it->get() == pSI) break;
139 if (sistorage.end() == it) {
140 cerr << " SolverFactory: failed to remove solver at " << pSI << endl;
141 throw InternalError(" SolverFactory: failed to remove solver");
142 }
143 sistorage.erase(it);
144}
145
146MznSolver::MznSolver(std::vector<std::string> args0)
147 : solver_configs(std::cerr),
148 executable_name("minizinc"),
149 os(std::cout),
150 log(std::cerr),
151 s2out(std::cout, std::cerr, solver_configs.mznlibDir()) {
152 std::vector<std::string> args = {executable_name};
153 args.insert(args.end(), args0.begin(), args0.end());
154 switch (processOptions(args)) {
155 case OPTION_FINISH:
156 return;
157 case OPTION_ERROR:
158 printUsage();
159 os << "More info with \"" << executable_name << " --help\"\n";
160 return;
161 case OPTION_OK:
162 break;
163 }
164
165 flatten(file, file);
166 // Definition* head = interpreter->_agg[0].def_stack;
167 // def_ptr = head;
168}
169
170MznSolver::~MznSolver() {
171 // if (si) // first the solver
172 // CleanupSolverInterface(si);
173 // TODO cleanup the used solver interfaces
174 delete interpreter;
175 si = 0;
176 si_opt = nullptr;
177 GC::trigger();
178}
179
180bool MznSolver::ifMzn2Fzn() { return is_mzn2fzn; }
181
182bool MznSolver::ifSolns2out() { return s2out._opt.flag_standaloneSolns2Out; }
183
184void MznSolver::addSolverInterface(SolverFactory* sf) {
185 si = sf->createSI(log, si_opt);
186 assert(si);
187 Model* m = in_out_defs.model();
188 if (m) {
189 for (FunctionIterator it = m->begin_functions(); it != m->end_functions(); ++it) {
190 if (!it->removed()) {
191 FunctionI& fi = *it;
192 if (fi.from_stdlib() || fi.ti()->type().isann() || fi.e()) {
193 continue;
194 }
195 si->addFunction(&fi);
196 }
197 }
198 }
199 si->setSolns2Out(new Solns2Out(os, log, ""));
200 // if (s2out.getEnv()==NULL)
201 // s2out.initFromEnv( flt.getEnv() );
202 // si->setSolns2Out( &s2out );
203 if (flag_compiler_verbose)
204 log
205 // << " ---------------------------------------------------------------------------\n"
206 << " % SOLVING PHASE\n"
207 << sf->getDescription(si_opt) << endl;
208}
209
210void MznSolver::addSolverInterface() {
211 GCLock lock;
212 if (sf == NULL) {
213 if (getGlobalSolverRegistry()->getSolverFactories().empty()) {
214 log << " MznSolver: NO SOLVER FACTORIES LINKED." << endl;
215 assert(0);
216 }
217 sf = getGlobalSolverRegistry()->getSolverFactories().back();
218 }
219 addSolverInterface(sf);
220}
221
222void MznSolver::printUsage() {
223 os << executable_name << ": ";
224 if (ifMzn2Fzn()) {
225 os << "MiniZinc to FlatZinc converter.\n"
226 << "Usage: " << executable_name
227 << " [<options>] [-I <include path>] <model>.mzn [<data>.dzn ...]" << std::endl;
228 } else if (ifSolns2out()) {
229 os << "Solutions to output translator.\n"
230 << "Usage: " << executable_name << " [<options>] <model>.ozn" << std::endl;
231 } else {
232 os << "MiniZinc driver.\n"
233 << "Usage: " << executable_name
234 << " [<options>] [-I <include path>] <model>.mzn [<data>.dzn ...] or just <flat>.fzn"
235 << std::endl;
236 }
237}
238
239void MznSolver::printHelp(const std::string& selectedSolver) {
240 printUsage();
241 os << "General options:" << std::endl
242 << " --help, -h\n Print this help message." << std::endl
243 << " --version\n Print version information." << std::endl
244 << " --solvers\n Print list of available solvers." << std::endl
245 << " --time-limit <ms>\n Stop after <ms> milliseconds (includes compilation and solving)."
246 << std::endl
247 << " --solver <solver id>, --solver <solver config file>.msc\n Select solver to use."
248 << std::endl
249 << " --help <solver id>\n Print help for a particular solver." << std::endl
250 << " -v, -l, --verbose\n Print progress/log statements. Note that some solvers may log to "
251 "stdout."
252 << std::endl
253 << " --verbose-compilation\n Print progress/log statements for compilation." << std::endl
254 << " -s, --statistics\n Print statistics." << std::endl
255 << " --compiler-statistics\n Print statistics for compilation." << std::endl
256 << " -c, --compile\n Compile only (do not run solver)." << std::endl
257 << " --config-dirs\n Output configuration directories." << std::endl;
258
259 if (selectedSolver.empty()) {
260 // flt.printHelp(os);
261 os << endl;
262 if (!ifMzn2Fzn()) {
263 s2out.printHelp(os);
264 os << endl;
265 }
266 os << "Available solvers (get help using --help <solver id>):" << endl;
267 std::vector<std::string> solvers = solver_configs.solvers();
268 if (solvers.size() == 0) cout << " none.\n";
269 for (unsigned int i = 0; i < solvers.size(); i++) {
270 cout << " " << solvers[i] << endl;
271 }
272 } else {
273 const SolverConfig& sc = solver_configs.config(selectedSolver);
274 string solverId = sc.executable().empty() ? sc.id()
275 : (sc.supportsMzn() ? string("org.minizinc.mzn-mzn")
276 : string("org.minizinc.mzn-fzn"));
277 bool found = false;
278 for (auto it = getGlobalSolverRegistry()->getSolverFactories().rbegin();
279 it != getGlobalSolverRegistry()->getSolverFactories().rend(); ++it) {
280 if ((*it)->getId() == solverId) {
281 os << endl;
282 (*it)->printHelp(os);
283 if (!sc.executable().empty() && !sc.extraFlags().empty()) {
284 os << "Extra solver flags (use with ";
285 os << (sc.supportsMzn() ? "--mzn-flags" : "--fzn-flags") << ")" << endl;
286 for (const SolverConfig::ExtraFlag& ef : sc.extraFlags()) {
287 os << " " << ef.flag << endl << " " << ef.description << endl;
288 }
289 }
290 found = true;
291 }
292 }
293 if (!found) {
294 os << "No help found for solver " << selectedSolver << endl;
295 }
296 }
297}
298
299void addFlags(const std::string& sep, const std::vector<std::string>& in_args,
300 std::vector<std::string>& out_args) {
301 for (const std::string& arg : in_args) {
302 out_args.push_back(sep);
303 out_args.push_back(arg);
304 }
305}
306
307MznSolver::OptionStatus MznSolver::processOptions(std::vector<std::string>& argv) {
308 executable_name = argv[0];
309 executable_name = executable_name.substr(executable_name.find_last_of("/\\") + 1);
310 size_t lastdot = executable_name.find_last_of('.');
311 if (lastdot != std::string::npos) {
312 executable_name = executable_name.substr(0, lastdot);
313 }
314 string solver;
315 bool mzn2fzn_exe = (executable_name == "mzn2fzn");
316 if (mzn2fzn_exe) {
317 is_mzn2fzn = true;
318 } else if (executable_name == "solns2out") {
319 s2out._opt.flag_standaloneSolns2Out = true;
320 flag_is_solns2out = true;
321 }
322 bool compileSolutionChecker = false;
323 int i = 1, j = 1;
324 int argc = static_cast<int>(argv.size());
325 if (argc < 2) return OPTION_ERROR;
326 for (i = 1; i < argc; ++i) {
327 if (argv[i] == "-h" || argv[i] == "--help") {
328 if (argc > i + 1) {
329 printHelp(argv[i + 1]);
330 } else {
331 printHelp();
332 }
333 return OPTION_FINISH;
334 }
335 if (argv[i] == "--version") {
336 // flt.printVersion(cout);
337 return OPTION_FINISH;
338 }
339 if (argv[i] == "--solvers") {
340 cout << "MiniZinc driver.\nAvailable solver configurations:\n";
341 std::vector<std::string> solvers = solver_configs.solvers();
342 if (solvers.size() == 0) cout << " none.\n";
343 for (unsigned int i = 0; i < solvers.size(); i++) {
344 cout << " " << solvers[i] << endl;
345 }
346 cout << "Search path for solver configurations:\n";
347 for (const string& p : solver_configs.solverConfigsPath()) {
348 cout << " " << p << endl;
349 }
350 return OPTION_FINISH;
351 }
352 if (argv[i] == "--solvers-json") {
353 cout << solver_configs.solverConfigsJSON();
354 return OPTION_FINISH;
355 }
356 if (argv[i] == "--config-dirs") {
357 GCLock lock;
358 cout << "{\n";
359 cout << " \"globalConfigFile\" : \""
360 << Printer::escapeStringLit(FileUtils::global_config_file()) << "\",\n";
361 cout << " \"userConfigFile\" : \"" << Printer::escapeStringLit(FileUtils::user_config_file())
362 << "\",\n";
363 cout << " \"userSolverConfigDir\" : \""
364 << Printer::escapeStringLit(FileUtils::user_config_dir()) << "/solvers\",\n";
365 cout << " \"mznStdlibDir\" : \"" << Printer::escapeStringLit(solver_configs.mznlibDir())
366 << "\"\n";
367 cout << "}\n";
368 return OPTION_FINISH;
369 }
370 if (argv[i] == "--time-limit") {
371 ++i;
372 if (i == argc) {
373 log << "Argument required for --time-limit" << endl;
374 return OPTION_ERROR;
375 }
376 flag_overall_time_limit = atoi(argv[i].c_str());
377 } else if (argv[i] == "--solver") {
378 ++i;
379 if (i == argc) {
380 log << "Argument required for --solver" << endl;
381 return OPTION_ERROR;
382 }
383 if (solver.size() > 0 && solver != argv[i]) {
384 log << "Only one --solver option allowed" << endl;
385 return OPTION_ERROR;
386 }
387 solver = argv[i];
388 } else if (argv[i] == "--output-dict") {
389 output_dict = true;
390 } else if (argv[i] == "-c" || argv[i] == "--compile") {
391 is_mzn2fzn = true;
392 } else if (argv[i] == "-v" || argv[i] == "--verbose" || argv[i] == "-l") {
393 flag_verbose = true;
394 flag_compiler_verbose = true;
395 } else if (argv[i] == "--verbose-compilation") {
396 flag_compiler_verbose = true;
397 } else if (argv[i] == "-s" || argv[i] == "--statistics") {
398 flag_statistics = true;
399 flag_compiler_statistics = true;
400 } else if (argv[i] == "--compiler-statistics") {
401 flag_compiler_statistics = true;
402 } else {
403 if ((argv[i] == "--fzn-cmd" || argv[i] == "--flatzinc-cmd") && solver.empty()) {
404 solver = "org.minizinc.mzn-fzn";
405 }
406 if (argv[i] == "--compile-solution-checker") {
407 compileSolutionChecker = true;
408 }
409 if (argv[i] == "--ozn-file") {
410 flag_is_solns2out = true;
411 }
412 argv[j++] = argv[i];
413 }
414 }
415 argv.resize(j);
416 argc = j;
417
418 if ((mzn2fzn_exe || compileSolutionChecker) && solver.empty()) {
419 solver = "org.minizinc.mzn-fzn";
420 }
421
422 // if (flag_verbose) {
423 // argv.push_back("--verbose-solving");
424 // argc++;
425 // }
426 if (flag_statistics) {
427 argv.push_back("--solver-statistics");
428 argc++;
429 }
430
431 // flt.set_flag_output_by_default(ifMzn2Fzn());
432
433 bool isMznMzn = false;
434
435 if (!flag_is_solns2out) {
436 try {
437 const SolverConfig& sc = solver_configs.config(solver);
438 string solverId;
439 if (sc.executable().empty()) {
440 if (is_mzn2fzn) {
441 solverId = "org.minizinc.mzn-fzn";
442 } else {
443 solverId = sc.id();
444 }
445 } else if (sc.supportsMzn()) {
446 solverId = "org.minizinc.mzn-mzn";
447 } else if (sc.supportsFzn()) {
448 solverId = "org.minizinc.mzn-fzn";
449 } else if (sc.supportsNL()) {
450 solverId = "org.minizinc.mzn-nl";
451 } else {
452 log << "Selected solver does not support MiniZinc, FlatZinc or NL input." << endl;
453 return OPTION_ERROR;
454 }
455 for (auto it = getGlobalSolverRegistry()->getSolverFactories().begin();
456 it != getGlobalSolverRegistry()->getSolverFactories().end(); ++it) {
457 if ((*it)->getId() ==
458 solverId) { /// TODO: also check version (currently assumes all ids are unique)
459 sf = *it;
460 if (si_opt) {
461 delete si_opt;
462 }
463 si_opt = sf->createOptions();
464 if (!sc.executable().empty() || solverId == "org.minizinc.mzn-fzn" ||
465 solverId == "org.minizinc.mzn-nl") {
466 std::vector<MZNFZNSolverFlag> acceptedFlags;
467 for (auto& sf : sc.stdFlags()) acceptedFlags.push_back(MZNFZNSolverFlag::std(sf));
468 for (auto& ef : sc.extraFlags())
469 acceptedFlags.push_back(MZNFZNSolverFlag::extra(ef.flag, ef.flag_type));
470
471 // Collect arguments required for underlying exe
472 vector<string> fzn_mzn_flags;
473 if (sc.needsStdlibDir()) {
474 fzn_mzn_flags.push_back("--stdlib-dir");
475 fzn_mzn_flags.push_back(FileUtils::share_directory());
476 }
477 if (sc.needsMznExecutable()) {
478 fzn_mzn_flags.push_back("--minizinc-exe");
479 fzn_mzn_flags.push_back(FileUtils::progpath() + "/" + executable_name);
480 }
481
482 if (sc.supportsMzn()) {
483 isMznMzn = true;
484 static_cast<MZN_SolverFactory*>(sf)->setAcceptedFlags(si_opt, acceptedFlags);
485 std::vector<std::string> additionalArgs_s;
486 additionalArgs_s.push_back("-m");
487 if (sc.executable_resolved().size()) {
488 additionalArgs_s.push_back(sc.executable_resolved());
489 } else {
490 additionalArgs_s.push_back(sc.executable());
491 }
492
493 if (!fzn_mzn_flags.empty()) {
494 addFlags("--mzn-flag", fzn_mzn_flags, additionalArgs_s);
495 }
496
497 // This should maybe be moved to fill in fzn_mzn_flags when
498 // --find-muses is implemented (these arguments will be passed
499 // through to the subsolver of findMUS)
500 if (!sc.mznlib().empty()) {
501 if (sc.mznlib().substr(0, 2) == "-G") {
502 additionalArgs_s.push_back("--mzn-flag");
503 additionalArgs_s.push_back(sc.mznlib());
504 } else {
505 additionalArgs_s.push_back("--mzn-flag");
506 additionalArgs_s.push_back("-I");
507 additionalArgs_s.push_back("--mzn-flag");
508 std::string _mznlib;
509 if (sc.mznlib_resolved().size()) {
510 _mznlib = sc.mznlib_resolved();
511 } else {
512 _mznlib = sc.mznlib();
513 }
514 additionalArgs_s.push_back(_mznlib);
515 }
516 }
517
518 for (i = 0; i < additionalArgs_s.size(); ++i) {
519 bool success = sf->processOption(si_opt, i, additionalArgs_s);
520 if (!success) {
521 log << "Solver backend " << solverId << " does not recognise option "
522 << additionalArgs_s[i] << "." << endl;
523 return OPTION_ERROR;
524 }
525 }
526 } else {
527 // supports fzn or nl
528 std::vector<std::string> additionalArgs;
529 if (sc.supportsFzn()) {
530 static_cast<FZN_SolverFactory*>(sf)->setAcceptedFlags(si_opt, acceptedFlags);
531 additionalArgs.push_back("--fzn-cmd");
532 } else {
533 // supports nl
534 additionalArgs.push_back("--nl-cmd");
535 }
536 if (sc.executable_resolved().size()) {
537 additionalArgs.push_back(sc.executable_resolved());
538 } else {
539 additionalArgs.push_back(sc.executable());
540 }
541 if (!fzn_mzn_flags.empty()) {
542 if (sc.supportsFzn()) {
543 addFlags("--fzn-flag", fzn_mzn_flags, additionalArgs);
544 } else {
545 addFlags("--nl-flag", fzn_mzn_flags, additionalArgs);
546 }
547 }
548 if (sc.needsPathsFile()) {
549 // Instruct flattener to hold onto paths
550 int i = 0;
551 vector<string> args{"--keep-paths"};
552 // flt.processOption(i, args);
553
554 // Instruct FznSolverInstance to write a path file
555 // and pass it to the executable with --paths arg
556 additionalArgs.push_back("--fzn-needs-paths");
557 }
558 if (!sc.needsSolns2Out()) {
559 additionalArgs.push_back("--fzn-output-passthrough");
560 }
561 int i = 0;
562 for (i = 0; i < additionalArgs.size(); ++i) {
563 bool success = sf->processOption(si_opt, i, additionalArgs);
564 if (!success) {
565 log << "Solver backend " << solverId << " does not recognise option "
566 << additionalArgs[i] << "." << endl;
567 return OPTION_ERROR;
568 }
569 }
570 }
571 }
572 if (!sc.mznlib().empty()) {
573 if (sc.mznlib().substr(0, 2) == "-G") {
574 std::vector<std::string> additionalArgs({sc.mznlib()});
575 int i = 0;
576 // if (!flt.processOption(i, additionalArgs)) {
577 // log << "Flattener does not recognise option " << sc.mznlib() << endl;
578 // return OPTION_ERROR;
579 // }
580 } else {
581 std::vector<std::string> additionalArgs(2);
582 additionalArgs[0] = "-I";
583 if (sc.mznlib_resolved().size()) {
584 additionalArgs[1] = sc.mznlib_resolved();
585 } else {
586 additionalArgs[1] = sc.mznlib();
587 }
588 int i = 0;
589 // if (!flt.processOption(i, additionalArgs)) {
590 // log << "Flattener does not recognise option -I." << endl;
591 // return OPTION_ERROR;
592 // }
593 }
594 }
595 if (!sc.defaultFlags().empty()) {
596 std::vector<std::string> addedArgs;
597 addedArgs.push_back(argv[0]); // excutable name
598 for (auto& df : sc.defaultFlags()) {
599 addedArgs.push_back(df);
600 }
601 for (int i = 1; i < argv.size(); i++) {
602 addedArgs.push_back(argv[i]);
603 }
604 argv = addedArgs;
605 argc = addedArgs.size();
606 }
607 break;
608 }
609 }
610
611 } catch (ConfigException& e) {
612 log << "Config exception: " << e.msg() << endl;
613 return OPTION_ERROR;
614 }
615
616 if (sf == NULL) {
617 log << "Solver " << solver << " not found." << endl;
618 return OPTION_ERROR;
619 }
620
621 for (i = 1; i < argc; ++i) {
622 if (!ifMzn2Fzn() ? s2out.processOption(i, argv) : false) {
623 // } else if ((!isMznMzn || is_mzn2fzn) && flt.processOption(i, argv)) {
624 } else if (sf != NULL && sf->processOption(si_opt, i, argv)) {
625 } else {
626 size_t last_dot = argv[i].find_last_of('.');
627 if (last_dot != string::npos) {
628 std::string extension = argv[i].substr(last_dot, string::npos);
629 if (extension == ".uzn" || extension == ".mza") {
630 assert(file == "");
631 file = argv[i];
632 } else if (extension == ".dzn") {
633 data_files.push_back(argv[i]);
634 }
635 } else {
636 std::string executable_name(argv[0]);
637 executable_name = executable_name.substr(executable_name.find_last_of("/\\") + 1);
638 log << executable_name << ": Unrecognized option or bad format `" << argv[i] << "'"
639 << endl;
640 return OPTION_ERROR;
641 }
642 }
643 }
644 return OPTION_OK;
645
646 } else {
647 for (i = 1; i < argc; ++i) {
648 if (s2out.processOption(i, argv)) {
649 } else {
650 std::string executable_name(argv[0]);
651 executable_name = executable_name.substr(executable_name.find_last_of("/\\") + 1);
652 log << executable_name << ": Unrecognized option or bad format `" << argv[i] << "'" << endl;
653 return OPTION_ERROR;
654 }
655 }
656 return OPTION_OK;
657 }
658}
659
660Val MznSolver::eval_val(EnvI& env, Expression* e) {
661 if (e->type().dim() > 0) {
662 ArrayLit* al = eval_array_lit(env, e);
663 std:
664 vector<Val> content(al->size());
665 for (size_t i = 0; i < al->size(); ++i) {
666 content[i] = eval_val(env, (*al)[i]);
667 }
668 Val ret = Val(Vec::a(interpreter, interpreter->newIdent(), content));
669
670 if (al->dims() > 1 || al->min(0) != 1) {
671 std::vector<Val> idxs(al->dims() * 2);
672 for (size_t i = 0; i < al->dims(); ++i) {
673 idxs[i * 2] = Val(al->min(i));
674 idxs[i * 2 + 1] = Val(al->max(i));
675 }
676 Vec* ranges = Vec::a(interpreter, interpreter->newIdent(), idxs);
677 ret = Val(Vec::a(interpreter, interpreter->newIdent(), {ret, Val(ranges)}, true));
678 }
679
680 return ret;
681 }
682 if (e->type().is_set()) {
683 // TODO: Might not be int
684 IntSetVal* sl = eval_intset(env, e);
685 std::vector<Val> vranges(sl->size() * 2);
686 for (size_t i = 0; i < sl->size(); ++i) {
687 vranges[i * 2] = Val::fromIntVal(sl->min(i));
688 vranges[i * 2 + 1] = Val::fromIntVal(sl->max(i));
689 }
690 return Val(Vec::a(interpreter, interpreter->newIdent(), vranges));
691 }
692 if (e->type().isbool()) {
693 bool b(eval_bool(env, e));
694 return Val(b);
695 }
696 if (e->type().isfloat()) {
697 throw InternalError("Unsupported Type");
698 }
699 IntVal iv(eval_int(env, e));
700 return Val::fromIntVal(iv);
701}
702
703void MznSolver::flatten(const std::string& filename, const std::string& modelName) {
704 if (!FileUtils::file_exists(filename)) {
705 std::cerr << "Error: cannot open assembly file '" << filename << "'." << std::endl;
706 return;
707 }
708 bool verbose = flag_compiler_verbose;
709 std::ifstream t(filename, std::ifstream::in);
710 std::string line;
711 std::string mzn_defs;
712 while (std::getline(t, line)) {
713 if (line == "@@@@@@@@@@") {
714 break;
715 }
716 mzn_defs += line + "\n";
717 }
718 std::string assembly;
719 while (std::getline(t, line)) {
720 assembly += line + "\n";
721 }
722 if (assembly.empty()) {
723 std::swap(mzn_defs, assembly);
724 }
725 // Parse assembly file
726 int max_glob;
727 std::tie(max_glob, bs) = parse_mza(assembly);
728 if (verbose) {
729 std::cerr << "Disassembled code:\n";
730 int b_count = 0;
731 for (auto& b : bs) {
732 for (int i = 0; i < BytecodeProc::MAX_MODE; i++) {
733 if (b.mode[i].size() > 0) {
734 std::cerr << ":" << b.name << ":" << BytecodeProc::mode_to_string[i] << " %% " << b_count
735 << "\n";
736 std::cerr << b.mode[i].toString(bs);
737 }
738 }
739 b_count++;
740 }
741 std::cerr << "\n";
742 }
743 for (size_t i = 0; i < bs.size(); i++) {
744 resolve_call.insert({bs[i].name, {i, bs[i].nargs}});
745 }
746 // The main procedure is the last one in the file
747 BytecodeFrame frame(bs.back().mode[BytecodeProc::ROOT], bs.size() - 1, BytecodeProc::ROOT);
748 interpreter = new Interpreter(bs, frame, max_glob);
749 // Parse and add data
750 if (!mzn_defs.empty()) {
751 GCLock lock;
752 std::vector<SyntaxError> syntaxErrors;
753 Model* m = parse(in_out_defs, {}, data_files, mzn_defs, file,
754 {solver_configs.mznlibDir() + "/std"}, false, false, verbose, std::cerr);
755 if (!m) {
756 throw Error("Unable to parse MiniZinc Declarations");
757 }
758 assert(!in_out_defs.model());
759 in_out_defs.model(m);
760 long long int idn = 0;
761 std::vector<TypeError> typeErrors;
762 typecheck(in_out_defs, in_out_defs.model(), typeErrors, false, true, false);
763 registerBuiltins(in_out_defs);
764 if (typeErrors.size() > 0) {
765 for (unsigned int i = 0; i < typeErrors.size(); i++) {
766 if (flag_verbose) log << std::endl;
767 log << typeErrors[i].loc() << ":" << std::endl;
768 log << typeErrors[i].what() << ": " << typeErrors[i].msg() << std::endl;
769 }
770 throw Error("multiple type errors");
771 }
772 if (verbose) {
773 std::cerr << "Input Data:\n";
774 }
775 for (VarDeclIterator it = in_out_defs.model()->begin_vardecls();
776 it != in_out_defs.model()->end_vardecls(); ++it) {
777 if (it->removed()) {
778 continue;
779 }
780 GCLock lock;
781 Env& env = in_out_defs;
782 Model* m = in_out_defs.model();
783
784 VarDecl* vd = it->e();
785 if (vd->type().isann()) {
786 continue;
787 }
788 assert(vd->e());
789 Call* global_ann = vd->ann().getCall(constants().ann.global_register);
790 if (!global_ann) {
791 throw TypeError(env.envi(), vd->loc(), "Unkown global " + vd->id()->str().str());
792 }
793 IntVal global = eval_int(env.envi(), global_ann->arg(0));
794
795 if (vd->type().dim() > 0) {
796 ArrayLit* al = eval_array_lit(env.envi(), vd->e());
797 checkIndexSets(env.envi(), vd, al);
798 }
799 Val v = eval_val(env.envi(), vd->e());
800
801 interpreter->globals.assign(interpreter, global.toInt(), v);
802 if (verbose) {
803 std::cerr << " - R" << global << "(" << vd->id()->str() << ") = " << v.toString()
804 << std::endl;
805 }
806 }
807 }
808 // Start interpreter
809 Timer tm01;
810 if (verbose) {
811 std::cerr << "Run:\n";
812 }
813 bool delayed = true;
814 interpreter->run();
815 while (interpreter->status() == Interpreter::ROGER && delayed) {
816 delayed = interpreter->runDelayed();
817 }
818 flatten_time = tm01.s();
819 // FIXME: Global registers should not be removed, merely hidden
820 // interpreter->clear_globals();
821 if (verbose) {
822 std::cerr << "Status: " << Interpreter::status_to_string[interpreter->status()] << std::endl;
823 if (interpreter->status() == Interpreter::ROGER) {
824 interpreter->dumpState(std::cerr);
825 }
826 std::cerr << "----------------" << std::endl;
827 }
828 switch (interpreter->status()) {
829 case Interpreter::ROGER:
830 interpreter_status = SolverInstance::UNKNOWN;
831 break;
832 case Interpreter::ERROR:
833 case Interpreter::ABORTED:
834 interpreter_status = SolverInstance::ERROR;
835 break;
836 case Interpreter::INCONSISTENT:
837 interpreter_status = SolverInstance::UNSAT;
838 break;
839 }
840}
841
842std::pair<SolverInstance::Status, std::string> MznSolver::solve() {
843 SolverInstance::Status status = getSI()->solve();
844 std::string sol = printSolution(status);
845 if (si_opt->printStatistics) getSI()->printStatistics();
846 /* if (flag_statistics) */
847 /* getSI()->getSolns2Out()->printStatistics(log); */
848 return {status, sol};
849}
850
851void MznSolver::printStatistics() { // from flattener too? TODO
852 if (si) getSI()->printStatistics();
853}
854
855std::string MznSolver::printSolution(SolverInstance::Status s) {
856 std::stringstream ss;
857 switch (s) {
858 case SolverInstance::SAT:
859 case SolverInstance::OPT: {
860 if (output) {
861 Val vec = output->arg(0);
862 ss << (output_dict ? '{' : '[');
863 for (int i = 0; i < vec.size(); ++i) {
864 Val v = vec[i];
865 if (i > 0) {
866 ss << ", ";
867 }
868 if (v.isVar()) {
869 if (output_dict) {
870 ss << "\"" << v.timestamp() << "\""
871 << ": ";
872 }
873 v = Val::follow_alias(v);
874 if (v.isVar()) {
875 ss << si->getSolutionValue(v.toVar()).toString();
876 } else {
877 ss << v.toString();
878 }
879 } else {
880 assert(!output_dict);
881 ss << v.toString();
882 }
883 }
884 ss << (output_dict ? '}' : ']') << std::endl;
885
886 // Set output for sol() builtin
887 interpreter->solutions.clear();
888 for (int i = 0; i < vec.size(); ++i) {
889 Val v = Val::follow_alias(vec[i]);
890 if (v.isVar()) {
891 interpreter->solutions.emplace(v.timestamp(), si->getSolutionValue(v.toVar()));
892 }
893 }
894 } else {
895 interpreter->solutions.clear();
896 bool first = true;
897 ss << "{" << std::endl;
898 for (Variable* v = interpreter->root()->next(); v != interpreter->root(); v = v->next()) {
899 Val va = Val::follow_alias(Val(v));
900 if (va.isVar()) {
901 int timestamp = va.timestamp();
902 if (timestamp >= 0) {
903 /// TODO: all timestamps >= 0 ?
904 if (!first) {
905 ss << "," << std::endl;
906 }
907 ss << " \"" << timestamp << "\""
908 << ": ";
909 Val sv = si->getSolutionValue(va.toVar());
910 ss << sv.toString();
911 first = false;
912 // Set output for sol() builtin
913 interpreter->solutions.emplace(timestamp, sv);
914 }
915 }
916 }
917 ss << std::endl << "}" << std::endl;
918 }
919 } break;
920 case SolverInstance::UNSAT:
921 ss << "=====UNSATISFIABLE=====" << std::endl;
922 break;
923 case SolverInstance::UNKNOWN:
924 ss << "=====UNKNOWN=====" << std::endl;
925 break;
926 case SolverInstance::ERROR:
927 default:
928 ss << "=====ERROR=====" << std::endl;
929 break;
930 }
931 return ss.str();
932}
933
934std::pair<SolverInstance::Status, std::string> MznSolver::run() {
935 using namespace std::chrono;
936 steady_clock::time_point startTime = steady_clock::now();
937
938 if (!ifMzn2Fzn() && flag_overall_time_limit != 0) {
939 steady_clock::time_point afterFlattening = steady_clock::now();
940 milliseconds passed = duration_cast<milliseconds>(afterFlattening - startTime);
941 milliseconds time_limit(flag_overall_time_limit);
942 if (passed > time_limit) {
943 s2out.evalStatus(getFltStatus());
944 return {SolverInstance::UNKNOWN, ""};
945 }
946 int time_left = (time_limit - passed).count();
947 std::vector<std::string> timeoutArgs(2);
948 timeoutArgs[0] = "--solver-time-limit";
949 std::ostringstream oss;
950 oss << time_left;
951 timeoutArgs[1] = oss.str();
952 int i = 0;
953 sf->processOption(si_opt, i, timeoutArgs);
954 }
955
956 if (flag_statistics) {
957 os << "%%%mzn-stat: flatTime=" << flatten_time << endl;
958 }
959
960 if (getFltStatus() != SolverInstance::UNKNOWN) {
961 if (ifMzn2Fzn()) {
962 GCLock lock;
963 std::ofstream os(file.substr(0, file.size() - 4) + std::string(".fzn"));
964 Printer p(os, 0, true);
965 auto c = new Call(Location().introduce(), constants().ids.bool_eq,
966 {constants().lit_true, constants().lit_false});
967 auto ci = new ConstraintI(Location().introduce(), c);
968 p.print(ci);
969 p.print(SolveI::sat(Location().introduce()));
970 }
971 return {getFltStatus(), printSolution(getFltStatus())};
972 }
973
974 if (!si) { // only then
975 // GCLock lock; // better locally, to enable cleanup after ProcessFlt()
976 addSolverInterface();
977 }
978 addDefinitions();
979 if (ifMzn2Fzn()) {
980 assert(dynamic_cast<FZNSolverInstance*>(si));
981 // Print flatzinc to file
982 static_cast<FZNSolverInstance*>(si)->printFlatZincToFile(file.substr(0, file.size() - 4) +
983 std::string(".fzn"));
984 static_cast<FZNSolverInstance*>(si)->printOutputToFile(file.substr(0, file.size() - 4) +
985 std::string(".ozn"));
986
987 if (flag_statistics) {
988 si->printStatistics();
989 }
990 return {SolverInstance::UNKNOWN, ""};
991 }
992 return solve();
993}
994
995void MznSolver::addDefinitions() {
996 /// TODO: currently this will always add all variables and constraints
997 Variable* v_start;
998 size_t c_start;
999 std::tie(v_start, c_start) = def_stack.back();
1000 std::set<int> output_vars;
1001 Variable* root = interpreter->root();
1002
1003 auto fzn = dynamic_cast<FZNSolverInstance*>(si);
1004 if (v_start == nullptr) {
1005 v_start = root;
1006 for (Constraint* c : v_start->definitions()) {
1007 if (interpreter->_procs[c->pred()].name == "output_this") {
1008 assert(c->size() == 1);
1009 output = c;
1010 Val arg = c->arg(0);
1011 assert(arg.isVec());
1012 for (int i = 0; i < arg.size(); ++i) {
1013 Val real = Val::follow_alias(Val(arg[i]));
1014 if (real.isVar()) {
1015 output_vars.insert(real.toVar()->timestamp());
1016 }
1017 }
1018 break;
1019 }
1020 }
1021 }
1022
1023 // Add all new variables
1024 for (Variable* v = v_start->next(); v != interpreter->root(); v = v->next()) {
1025 // Only add variables that are not aliased
1026 if (Val(v) == Val::follow_alias(Val(v))) {
1027 si->addVariable(v,
1028 output != nullptr || output_vars.find(v->timestamp()) != output_vars.end());
1029 }
1030 }
1031 // Add defining constraints
1032 for (Variable* v = v_start->next(); v != interpreter->root(); v = v->next()) {
1033 for (Constraint* c : v->definitions()) {
1034 si->addConstraint(interpreter->_procs, c);
1035 }
1036 }
1037 // Add new root level constraints
1038 for (size_t i = c_start; i < root->definitions().size(); ++i) {
1039 Constraint* c = root->definitions()[i];
1040 if (interpreter->_procs[c->pred()].name == "output_this") {
1041 if (fzn) {
1042 assert(c->size() == 1);
1043 fzn->outputArray(c->arg(0).toVec());
1044 }
1045 continue;
1046 } else {
1047 si->addConstraint(interpreter->_procs, c);
1048 }
1049 }
1050 // Force output statement
1051 if (output == nullptr && fzn != nullptr) {
1052 fzn->outputDict(interpreter->root());
1053 }
1054 // TODO: Domain Changes
1055 def_stack[def_stack.size() - 1] = {root->prev(), root->definitions().size()};
1056}
1057
1058void MznSolver::pushToSolver() {
1059 assert(interpreter->trail.len() > 0);
1060
1061 if (auto tsi = dynamic_cast<TrailableSolverInstance*>(si)) {
1062 assert(interpreter->trail.len() == tsi->states() + 1);
1063 tsi->restart();
1064 addDefinitions();
1065 def_stack.push_back(def_stack.back());
1066 tsi->pushState();
1067 } else {
1068 assert(false);
1069 }
1070}
1071
1072void MznSolver::popFromSolver() {
1073 if (auto tsi = dynamic_cast<TrailableSolverInstance*>(si)) {
1074 assert(interpreter->trail.len() == tsi->states() - 1);
1075 tsi->restart();
1076 tsi->popState();
1077 def_stack.pop_back();
1078 } else {
1079 assert(false);
1080 delete si;
1081 si = nullptr;
1082 // TODO: do we need to reconstruct the model here or can we trust there is a push before
1083 // solving
1084 }
1085}