this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2
3/*
4 * Main authors:
5 * Guido Tack <guido.tack@monash.edu>
6 */
7
8/* This Source Code Form is subject to the terms of the Mozilla Public
9 * License, v. 2.0. If a copy of the MPL was not distributed with this
10 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
11
12#ifdef _MSC_VER
13#define _CRT_SECURE_NO_WARNINGS
14#endif
15
16#include <minizinc/builtins.hh>
17#include <minizinc/eval_par.hh>
18#include <minizinc/parser.hh>
19#include <minizinc/pathfileprinter.hh>
20#include <minizinc/prettyprinter.hh>
21#include <minizinc/process.hh>
22#include <minizinc/solvers/fzn_solverinstance.hh>
23#include <minizinc/timer.hh>
24#include <minizinc/typecheck.hh>
25
26#include <cstdio>
27#include <fstream>
28
29using namespace std;
30
31namespace MiniZinc {
32
33FZNSolverFactory::FZNSolverFactory() {
34 SolverConfig sc("org.minizinc.mzn-fzn",
35 MZN_VERSION_MAJOR "." MZN_VERSION_MINOR "." MZN_VERSION_PATCH);
36 sc.name("Generic FlatZinc driver");
37 sc.mznlibVersion(1);
38 sc.description("MiniZinc generic FlatZinc solver plugin");
39 sc.requiredFlags({"--fzn-cmd"});
40 sc.stdFlags({"-a", "-n", "-f", "-p", "-s", "-r", "-v"});
41 sc.tags({"__internal__"});
42 SolverConfigs::registerBuiltinSolver(sc);
43}
44
45string FZNSolverFactory::getDescription(SolverInstanceBase::Options* /*opt*/) {
46 string v = "FZN solver plugin, compiled " __DATE__ " " __TIME__;
47 return v;
48}
49
50string FZNSolverFactory::getVersion(SolverInstanceBase::Options* /*opt*/) {
51 return MZN_VERSION_MAJOR;
52}
53
54string FZNSolverFactory::getId() { return "org.minizinc.mzn-fzn"; }
55
56void FZNSolverFactory::printHelp(ostream& os) {
57 os << "MZN-FZN plugin options:" << std::endl
58 << " --fzn-cmd , --flatzinc-cmd <exe>\n the backend solver filename.\n"
59 << " -b, --backend, --solver-backend <be>\n the backend codename. Currently passed to "
60 "the solver.\n"
61 << " --fzn-flags <options>, --flatzinc-flags <options> --backend-flags <options>\n"
62 " Specify option to be passed to the FlatZinc interpreter.\n"
63 << " --fzn-flag <option>, --flatzinc-flag <option>, --backend-flag\n"
64 " As above, but for a single option string that need to be quoted in a shell.\n"
65 << " -t <ms>, --solver-time-limit <ms>, --fzn-time-limit <ms>\n Set time limit (in "
66 "milliseconds) for solving.\n"
67 << " --fzn-sigint\n Send SIGINT instead of SIGTERM.\n"
68 << " -n <n>, --num-solutions <n>\n"
69 << " An upper bound on the number of solutions to output for satisfaction problems. The "
70 "default should be 1.\n"
71 << " -a, --all, --all-solns, --all-solutions\n Print all solutions for satisfaction "
72 "problems and intermediate solutions for optimization problems.\n"
73 << " -i, --intermediate --intermediate-solutions\n Print intermediate solutions for "
74 "optimisation problems.\n"
75 << " -n-i, --no-intermediate --no-intermediate-solutions\n Don't print intermediate "
76 "solutions for optimisation problems.\n"
77 << " --all-satisfaction\n Print all solutions for satisfaction problems.\n"
78 << " --disable-all-satisfaction\n Don't print all solutions for satisfaction problems.\n"
79 << " -n-o <n>, --num-opt-solutions <n>\n"
80 << " An upper bound on the number of optimal solutions to output for optimisation "
81 "problems. The default should be 1.\n"
82 << " -a-o, --all-opt, --all-optimal\n Print all optimal solutions for optimisation "
83 "problems.\n"
84 << " -p <n>, --parallel <n>\n Use <n> threads during search. The default is "
85 "solver-dependent.\n"
86 << " -k, --keep-files\n For compatibility only: to produce .ozn and .fzn, use mzn2fzn\n"
87 " or <this_exe> --fzn ..., --ozn ...\n"
88 << " -r <n>, --seed <n>, --random-seed <n>\n For compatibility only: use solver flags "
89 "instead.\n"
90 << " --cp-profiler <id>,<port>\n Send search to cp-profiler with given execution ID and "
91 "port.\n";
92}
93
94SolverInstanceBase::Options* FZNSolverFactory::createOptions() { return new FZNSolverOptions; }
95
96SolverInstanceBase* FZNSolverFactory::doCreateSI(Env& env, std::ostream& log,
97 SolverInstanceBase::Options* opt) {
98 return new FZNSolverInstance(env, log, opt);
99}
100
101bool FZNSolverFactory::processOption(SolverInstanceBase::Options* opt, int& i,
102 std::vector<std::string>& argv,
103 const std::string& workingDir) {
104 auto& _opt = static_cast<FZNSolverOptions&>(*opt);
105 CLOParser cop(i, argv);
106 string buffer;
107 int nn = -1;
108
109 if (cop.getOption("--fzn-cmd --flatzinc-cmd", &buffer)) {
110 _opt.fznSolver = buffer;
111 } else if (cop.getOption("-b --backend --solver-backend", &buffer)) {
112 _opt.backend = buffer;
113 } else if (cop.getOption("--fzn-flags --flatzinc-flags --backend-flags", &buffer)) {
114 std::vector<std::string> cmdLine = FileUtils::parse_cmd_line(buffer);
115 for (auto& s : cmdLine) {
116 _opt.fznFlags.push_back(s);
117 }
118 } else if (cop.getOption("-t --solver-time-limit --fzn-time-limit", &nn)) {
119 _opt.fznTimeLimitMilliseconds = nn;
120 if (_opt.supportsT) {
121 _opt.solverTimeLimitMilliseconds = nn;
122 _opt.fznTimeLimitMilliseconds += 1000; // kill 1 second after solver should have stopped
123 }
124 } else if (cop.getOption("--fzn-sigint")) {
125 _opt.fznSigint = true;
126 } else if (cop.getOption("--fzn-needs-paths")) {
127 _opt.fznNeedsPaths = true;
128 } else if (cop.getOption("--fzn-output-passthrough")) {
129 _opt.fznOutputPassthrough = true;
130 } else if (cop.getOption("--fzn-flag --flatzinc-flag --backend-flag", &buffer)) {
131 _opt.fznFlags.push_back(buffer);
132 } else if (_opt.supportsN && cop.getOption("-n --num-solutions", &nn)) {
133 _opt.numSols = nn;
134 } else if (cop.getOption("-a")) {
135 _opt.fznFlags.emplace_back("-a");
136 } else if (cop.getOption("-i")) {
137 _opt.fznFlags.emplace_back("-i");
138 } else if (_opt.supportsNO && cop.getOption("-n-o --num-optimal", &nn)) {
139 _opt.numOptimal = (nn != 0);
140 } else if (_opt.supportsAO && cop.getOption("-a-o --all-opt --all-optimal")) {
141 _opt.allOptimal = true;
142 } else if (cop.getOption("-p --parallel", &nn)) {
143 if (_opt.supportsP) {
144 _opt.parallel = to_string(nn);
145 }
146 } else if (cop.getOption("-k --keep-files")) {
147 // Deprecated option! Does nothing.
148 } else if (cop.getOption("-r --seed --random-seed", &buffer)) {
149 if (_opt.supportsR) {
150 _opt.fznFlags.emplace_back("-r");
151 _opt.fznFlags.push_back(buffer);
152 }
153 } else if (cop.getOption("-s --solver-statistics")) {
154 if (_opt.supportsS) {
155 _opt.printStatistics = true;
156 }
157 } else if (cop.getOption("-v --verbose-solving")) {
158 _opt.verbose = true;
159 } else if (cop.getOption("-f --free-search")) {
160 if (_opt.supportsF) {
161 _opt.fznFlags.emplace_back("-f");
162 }
163 } else if (_opt.supportsCpprofiler && cop.getOption("--cp-profiler", &buffer)) {
164 _opt.fznFlags.emplace_back("--cp-profiler");
165 _opt.fznFlags.push_back(buffer);
166 } else {
167 for (auto& fznf : _opt.fznSolverFlags) {
168 if (fznf.t == MZNFZNSolverFlag::FT_ARG && cop.getOption(fznf.n.c_str(), &buffer)) {
169 _opt.fznFlags.push_back(fznf.n);
170 _opt.fznFlags.push_back(buffer);
171 return true;
172 }
173 if (fznf.t == MZNFZNSolverFlag::FT_NOARG && cop.getOption(fznf.n.c_str())) {
174 _opt.fznFlags.push_back(fznf.n);
175 return true;
176 }
177 }
178
179 return false;
180 }
181 return true;
182}
183
184void FZNSolverFactory::setAcceptedFlags(SolverInstanceBase::Options* opt,
185 const std::vector<MZNFZNSolverFlag>& flags) {
186 auto& _opt = static_cast<FZNSolverOptions&>(*opt);
187 _opt.fznSolverFlags.clear();
188 for (const auto& f : flags) {
189 if (f.n == "-a") {
190 _opt.supportsA = true;
191 } else if (f.n == "-n") {
192 _opt.supportsN = true;
193 } else if (f.n == "-f") {
194 _opt.supportsF = true;
195 } else if (f.n == "-p") {
196 _opt.supportsP = true;
197 } else if (f.n == "-s") {
198 _opt.supportsS = true;
199 } else if (f.n == "-r") {
200 _opt.supportsR = true;
201 } else if (f.n == "-v") {
202 _opt.supportsV = true;
203 } else if (f.n == "-t") {
204 _opt.supportsT = true;
205 } else if (f.n == "-i") {
206 _opt.supportsI = true;
207 } else if (f.n == "-n-o") {
208 _opt.supportsNO = true;
209 } else if (f.n == "-a-o") {
210 _opt.supportsAO = true;
211 } else if (f.n == "--cp-profiler") {
212 _opt.supportsCpprofiler = true;
213 } else {
214 _opt.fznSolverFlags.push_back(f);
215 }
216 }
217}
218
219FZNSolverInstance::FZNSolverInstance(Env& env, std::ostream& log,
220 SolverInstanceBase::Options* options)
221 : SolverInstanceBase(env, log, options), _fzn(env.flat()), _ozn(env.output()) {}
222
223FZNSolverInstance::~FZNSolverInstance() {}
224
225SolverInstance::Status FZNSolverInstance::solve() {
226 auto& opt = static_cast<FZNSolverOptions&>(*_options);
227 if (opt.fznSolver.empty()) {
228 throw InternalError("No FlatZinc solver specified");
229 }
230 /// Passing options to solver
231 vector<string> cmd_line;
232 cmd_line.push_back(opt.fznSolver);
233 string sBE = opt.backend;
234 bool is_sat = _fzn->solveItem()->st() == SolveI::SolveType::ST_SAT;
235 if (!sBE.empty()) {
236 cmd_line.emplace_back("-b");
237 cmd_line.push_back(sBE);
238 }
239 for (auto& f : opt.fznFlags) {
240 cmd_line.push_back(f);
241 }
242 if (opt.allOptimal && !is_sat) {
243 cmd_line.emplace_back("-a-o");
244 }
245 if (static_cast<int>(opt.numOptimal) != 1 && !is_sat) {
246 cmd_line.emplace_back("-n-o");
247 ostringstream oss;
248 oss << opt.numOptimal;
249 cmd_line.push_back(oss.str());
250 }
251 if (opt.numSols != 1 && is_sat) {
252 cmd_line.emplace_back("-n");
253 ostringstream oss;
254 oss << opt.numSols;
255 cmd_line.push_back(oss.str());
256 }
257 if (!opt.parallel.empty()) {
258 cmd_line.emplace_back("-p");
259 ostringstream oss;
260 oss << opt.parallel;
261 cmd_line.push_back(oss.str());
262 }
263 if (opt.printStatistics) {
264 cmd_line.emplace_back("-s");
265 }
266 if (opt.solverTimeLimitMilliseconds != 0) {
267 cmd_line.emplace_back("-t");
268 std::ostringstream oss;
269 oss << opt.solverTimeLimitMilliseconds;
270 cmd_line.push_back(oss.str());
271 }
272 if (opt.verbose) {
273 if (opt.supportsV) {
274 cmd_line.emplace_back("-v");
275 }
276 std::cerr << "Using FZN solver " << cmd_line[0] << " for solving, parameters: ";
277 for (int i = 1; i < cmd_line.size(); ++i) {
278 cerr << "" << cmd_line[i] << " ";
279 }
280 cerr << std::endl;
281 }
282 int timelimit = opt.fznTimeLimitMilliseconds;
283 bool sigint = opt.fznSigint;
284
285 FileUtils::TmpFile fznFile(".fzn");
286 std::ofstream os(FILE_PATH(fznFile.name()));
287 Printer p(os, 0, true);
288 for (FunctionIterator it = _fzn->functions().begin(); it != _fzn->functions().end(); ++it) {
289 if (!it->removed()) {
290 Item& item = *it;
291 p.print(&item);
292 }
293 }
294 for (VarDeclIterator it = _fzn->vardecls().begin(); it != _fzn->vardecls().end(); ++it) {
295 if (!it->removed()) {
296 Item& item = *it;
297 p.print(&item);
298 }
299 }
300 for (ConstraintIterator it = _fzn->constraints().begin(); it != _fzn->constraints().end(); ++it) {
301 if (!it->removed()) {
302 Item& item = *it;
303 p.print(&item);
304 }
305 }
306 p.print(_fzn->solveItem());
307 cmd_line.push_back(fznFile.name());
308
309 FileUtils::TmpFile* pathsFile = nullptr;
310 if (opt.fznNeedsPaths) {
311 pathsFile = new FileUtils::TmpFile(".paths");
312 std::ofstream ofs(FILE_PATH(pathsFile->name()));
313 PathFilePrinter pfp(ofs, _env.envi());
314 pfp.print(_fzn);
315
316 cmd_line.emplace_back("--paths");
317 cmd_line.push_back(pathsFile->name());
318 }
319
320 if (!opt.fznOutputPassthrough) {
321 Process<Solns2Out> proc(cmd_line, getSolns2Out(), timelimit, sigint);
322 int exitStatus = proc.run();
323 delete pathsFile;
324 return exitStatus == 0 ? getSolns2Out()->status : SolverInstance::ERROR;
325 }
326 Solns2Log s2l(getSolns2Out()->getOutput(), _log);
327 Process<Solns2Log> proc(cmd_line, &s2l, timelimit, sigint);
328 int exitStatus = proc.run();
329 delete pathsFile;
330 return exitStatus == 0 ? SolverInstance::NONE : SolverInstance::ERROR;
331}
332
333void FZNSolverInstance::processFlatZinc() {}
334
335void FZNSolverInstance::resetSolver() {}
336
337Expression* FZNSolverInstance::getSolutionValue(Id* id) {
338 assert(false);
339 return nullptr;
340}
341} // namespace MiniZinc