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#ifdef _WIN32
17#define NOMINMAX // Need this before all (implicit) include's of Windows.h
18#endif
19
20#include <minizinc/builtins.hh>
21#include <minizinc/eval_par.hh>
22#include <minizinc/parser.hh>
23#include <minizinc/pathfileprinter.hh>
24#include <minizinc/prettyprinter.hh>
25#include <minizinc/process.hh>
26#include <minizinc/solvers/fzn_solverinstance.hh>
27#include <minizinc/timer.hh>
28#include <minizinc/typecheck.hh>
29
30#include <cstdio>
31#include <fstream>
32
33#ifdef _WIN32
34#undef ERROR
35#endif
36
37using namespace std;
38
39namespace MiniZinc {
40
41FZN_SolverFactory::FZN_SolverFactory(void) {
42 SolverConfig sc("org.minizinc.mzn-fzn",
43 MZN_VERSION_MAJOR "." MZN_VERSION_MINOR "." MZN_VERSION_PATCH);
44 sc.name("Generic FlatZinc driver");
45 sc.mznlibVersion(1);
46 sc.description("MiniZinc generic FlatZinc solver plugin");
47 sc.requiredFlags({"--fzn-cmd"});
48 sc.stdFlags({"-a", "-n", "-f", "-p", "-s", "-r", "-v"});
49 sc.tags({"__internal__"});
50 SolverConfigs::registerBuiltinSolver(sc);
51}
52
53string FZN_SolverFactory::getDescription(SolverInstanceBase::Options*) {
54 string v = "FZN solver plugin, compiled " __DATE__ " " __TIME__;
55 return v;
56}
57
58string FZN_SolverFactory::getVersion(SolverInstanceBase::Options*) { return MZN_VERSION_MAJOR; }
59
60string FZN_SolverFactory::getId() { return "org.minizinc.mzn-fzn"; }
61
62void FZN_SolverFactory::printHelp(ostream& os) {
63 os << "MZN-FZN plugin options:" << std::endl
64 << " --fzn-cmd , --flatzinc-cmd <exe>\n the backend solver filename.\n"
65 << " -b, --backend, --solver-backend <be>\n the backend codename. Currently passed to "
66 "the solver.\n"
67 << " --fzn-flags <options>, --flatzinc-flags <options>\n Specify option to be passed to "
68 "the FlatZinc interpreter.\n"
69 << " --fzn-flag <option>, --flatzinc-flag <option>\n As above, but for a single option "
70 "string that need to be quoted in a shell.\n"
71 << " -n <n>, --num-solutions <n>\n An upper bound on the number of solutions to output. "
72 "The default should be 1.\n"
73 << " -t <ms>, --solver-time-limit <ms>, --fzn-time-limit <ms>\n Set time limit (in "
74 "milliseconds) for solving.\n"
75 << " --fzn-sigint\n Send SIGINT instead of SIGTERM.\n"
76 << " -a, --all, --all-solns, --all-solutions\n Print all solutions.\n"
77 << " -p <n>, --parallel <n>\n Use <n> threads during search. The default is "
78 "solver-dependent.\n"
79 << " -k, --keep-files\n For compatibility only: to produce .ozn and .fzn, use mzn2fzn\n"
80 " or <this_exe> --fzn ..., --ozn ...\n"
81 << " -r <n>, --seed <n>, --random-seed <n>\n For compatibility only: use solver flags "
82 "instead.\n";
83}
84
85SolverInstanceBase::Options* FZN_SolverFactory::createOptions(void) { return new FZNSolverOptions; }
86
87SolverInstanceBase* FZN_SolverFactory::doCreateSI(std::ostream& log,
88 SolverInstanceBase::Options* opt) {
89 return new FZNSolverInstance(log, opt);
90}
91
92bool FZN_SolverFactory::processOption(SolverInstanceBase::Options* opt, int& i,
93 std::vector<std::string>& argv) {
94 FZNSolverOptions& _opt = static_cast<FZNSolverOptions&>(*opt);
95 CLOParser cop(i, argv);
96 string buffer;
97 int nn = -1;
98
99 if (cop.getOption("--fzn-cmd --flatzinc-cmd", &buffer)) {
100 _opt.fzn_solver = buffer;
101 } else if (cop.getOption("-b --backend --solver-backend", &buffer)) {
102 _opt.backend = buffer;
103 } else if (cop.getOption("--fzn-flags --flatzinc-flags", &buffer)) {
104 std::vector<std::string> cmdLine = FileUtils::parseCmdLine(buffer);
105 for (auto& s : cmdLine) {
106 _opt.fzn_flags.push_back(s);
107 }
108 } else if (cop.getOption("-t --solver-time-limit --fzn-time-limit", &nn)) {
109 _opt.fzn_time_limit_ms = nn;
110 if (_opt.supports_t) {
111 _opt.solver_time_limit_ms = nn;
112 _opt.fzn_time_limit_ms += 1000; // kill 1 second after solver should have stopped
113 }
114 } else if (cop.getOption("--fzn-sigint")) {
115 _opt.fzn_sigint = true;
116 } else if (cop.getOption("--fzn-needs-paths")) {
117 _opt.fzn_needs_paths = true;
118 } else if (cop.getOption("--fzn-output-passthrough")) {
119 _opt.fzn_output_passthrough = true;
120 } else if (cop.getOption("--fzn-flag --flatzinc-flag", &buffer)) {
121 _opt.fzn_flags.push_back(buffer);
122 } else if (_opt.supports_n && cop.getOption("-n --num-solutions", &nn)) {
123 _opt.numSols = nn;
124 } else if (_opt.supports_a && cop.getOption("-a --all --all-solns --all-solutions")) {
125 _opt.allSols = true;
126 } else if (cop.getOption("-p --parallel", &nn)) {
127 if (_opt.supports_p) _opt.parallel = to_string(nn);
128 } else if (cop.getOption("-k --keep-files")) {
129 } else if (cop.getOption("-r --seed --random-seed", &buffer)) {
130 if (_opt.supports_r) {
131 _opt.fzn_flags.push_back("-r");
132 _opt.fzn_flags.push_back(buffer);
133 }
134 } else if (cop.getOption("-s --solver-statistics")) {
135 if (_opt.supports_s) {
136 _opt.printStatistics = true;
137 }
138 } else if (cop.getOption("-v --verbose-solving")) {
139 _opt.verbose = true;
140 } else if (cop.getOption("-f --free-search")) {
141 if (_opt.supports_f) _opt.fzn_flags.push_back("-f");
142 } else {
143 for (auto& fznf : _opt.fzn_solver_flags) {
144 if (fznf.t == MZNFZNSolverFlag::FT_ARG && cop.getOption(fznf.n.c_str(), &buffer)) {
145 _opt.fzn_flags.push_back(fznf.n);
146 _opt.fzn_flags.push_back(buffer);
147 return true;
148 } else if (fznf.t == MZNFZNSolverFlag::FT_NOARG && cop.getOption(fznf.n.c_str())) {
149 _opt.fzn_flags.push_back(fznf.n);
150 return true;
151 }
152 }
153
154 return false;
155 }
156 return true;
157}
158
159void FZN_SolverFactory::setAcceptedFlags(SolverInstanceBase::Options* opt,
160 const std::vector<MZNFZNSolverFlag>& flags) {
161 FZNSolverOptions& _opt = static_cast<FZNSolverOptions&>(*opt);
162 _opt.fzn_solver_flags.clear();
163 for (auto& f : flags) {
164 if (f.n == "-a") {
165 _opt.supports_a = true;
166 } else if (f.n == "-n") {
167 _opt.supports_n = true;
168 } else if (f.n == "-f") {
169 _opt.supports_f = true;
170 } else if (f.n == "-p") {
171 _opt.supports_p = true;
172 } else if (f.n == "-s") {
173 _opt.supports_s = true;
174 } else if (f.n == "-r") {
175 _opt.supports_r = true;
176 } else if (f.n == "-v") {
177 _opt.supports_v = true;
178 } else if (f.n == "-t") {
179 _opt.supports_t = true;
180 } else {
181 _opt.fzn_solver_flags.push_back(f);
182 }
183 }
184}
185
186FZNSolverInstance::FZNSolverInstance(std::ostream& log, SolverInstanceBase::Options* options)
187 : SolverInstanceBase(log, options), _model(new Model()), env(_model) {}
188
189FZNSolverInstance::~FZNSolverInstance(void) {}
190
191void FZNSolverInstance::addFunction(FunctionI* fi) {
192 _model->addItem(fi);
193 _model->registerFn(env.envi(), fi);
194}
195
196VarDecl* FZNSolverInstance::add_var_to_model(int ident, TypeInst* ti, bool view, bool isOutput) {
197 VarDecl* vd;
198 if (!view) {
199 vd = new VarDecl(Location().introduce(), ti, ident);
200
201 if (isOutput) {
202 vd->addAnnotation(constants().ann.output_var);
203 bool is_bool = ti->type().isbool();
204 auto output_ti =
205 new TypeInst(Location().introduce(), is_bool ? Type::parbool() : Type::parint(), nullptr);
206 auto output_vd = new VarDecl(Location().introduce(), output_ti, ident);
207 env.output()->addItem(new VarDeclI(Location().introduce(), output_vd));
208 }
209 } else {
210 vd = new VarDecl(Location().introduce(), ti, "view_" + std::to_string(ident));
211 }
212 auto vdi = new VarDeclI(Location().introduce(), vd);
213 _model->addItem(vdi);
214 return vd;
215}
216
217Expression* FZNSolverInstance::val_to_expr(Type ty, Val v) {
218 v = Val::follow_alias(v);
219 if (v.isInt()) {
220 if (ty.isbool()) {
221 return v == 0 ? constants().lit_false : constants().lit_true;
222 }
223 return IntLit::a(v.toIntVal());
224 } else if (v.isVar()) {
225 auto it = vdmap.find(v.timestamp());
226 assert(it != vdmap.end());
227 VarStore& vs = it->second;
228 if (ty.isbool()) {
229 if (vs.used_bool) {
230 return vs.bool_var()->cast<VarDecl>()->id();
231 }
232 vs.used_bool = true;
233
234 auto ti = new TypeInst(Location().introduce(), Type::varbool());
235 VarDecl* vd = add_var_to_model(v.timestamp(), ti, vs.used_int);
236 vs.bool_var = KeepAlive(vd);
237
238 if (vs.used_int) {
239 _model->addItem(new ConstraintI(
240 Location().introduce(),
241 new Call(Location().introduce(), constants().ids.bool2int,
242 {vs.bool_var()->cast<VarDecl>()->id(), vs.int_var()->cast<VarDecl>()->id()})));
243 } else {
244 uninitialised_vars.erase(v.timestamp());
245 }
246 return vs.bool_var()->cast<VarDecl>()->id();
247 }
248 if (vs.used_int) {
249 return vs.int_var()->cast<VarDecl>()->id();
250 }
251 vs.used_int = true;
252
253 SetLit* dom_set = new SetLit(Location().introduce(), IntSetVal::a(0, 1));
254 auto ti = new TypeInst(Location().introduce(), Type::varint(), dom_set);
255 VarDecl* vd = add_var_to_model(v.timestamp(), ti, vs.used_bool);
256 vs.int_var = KeepAlive(vd);
257
258 if (vs.used_bool) {
259 _model->addItem(new ConstraintI(
260 Location().introduce(),
261 new Call(Location().introduce(), constants().ids.bool2int,
262 {vs.bool_var()->cast<VarDecl>()->id(), vs.int_var()->cast<VarDecl>()->id()})));
263 } else {
264 uninitialised_vars.erase(v.timestamp());
265 }
266
267 return vs.int_var()->cast<VarDecl>()->id();
268 } else {
269 assert(v.isVec());
270 if (ty.is_set()) {
271 std::vector<IntSetVal::Range> ranges;
272 Vec* vec = v.toVec();
273 for (int i = 0; i < vec->size(); i += 2) {
274 ranges.push_back(IntSetVal::Range((*vec)[i].toIntVal(), (*vec)[i + 1].toIntVal()));
275 }
276 auto sl = new SetLit(Location().introduce(), IntSetVal::a(ranges));
277 return sl;
278 } else {
279 // this is an array
280 Val vec = v.toVec()->raw_data();
281 std::vector<Expression*> evec(vec.size());
282 bool par = true;
283 for (int i = 0; i < vec.size(); ++i) {
284 assert(!vec[i].isVec());
285 Type nty = ty;
286 nty.dim(0);
287 evec[i] = val_to_expr(nty, vec[i]);
288 par = par && evec[i]->type().ispar();
289 }
290 auto al = new ArrayLit(Location().introduce(), evec);
291 al->type(par ? Type::parint(1) : Type::varint(1));
292 return al;
293 }
294 }
295}
296
297void FZNSolverInstance::addConstraint(const std::vector<BytecodeProc>& bs, Constraint* c) {
298 GCLock lock;
299 const BytecodeProc& proc = bs[c->pred()];
300 const std::string& name = proc.name;
301 if (name == "solve_this") {
302 IntVal solve_mode = c->arg(0).toIntVal();
303 Val obj = c->arg(1);
304 SolveI* si;
305 if (solve_mode == 0) {
306 si = SolveI::sat(Location().introduce());
307 } else if (solve_mode == 1) {
308 si = SolveI::min(Location().introduce(), val_to_expr(Type::varint(), obj));
309 } else {
310 assert(solve_mode == 2);
311 si = SolveI::max(Location().introduce(), val_to_expr(Type::varint(), obj));
312 }
313 if (c->size() == 5) {
314 Val search_a = c->arg(2);
315 IntVal var_sel = c->arg(3).toIntVal();
316 IntVal val_sel = c->arg(4).toIntVal();
317 if (search_a.isVec() && search_a.size() > 0 && var_sel > 0 && val_sel > 0) {
318 Expression* search_vars = val_to_expr(Type::varint(1), search_a);
319 ASTString var_sel_s(var_sel == 1 ? "input_order" : "first_fail");
320 ASTString val_sel_s(val_sel == 1 ? "indomain_min" : "indomain_max");
321 Id* var_sel_id = new Id(Location().introduce(), var_sel_s, nullptr);
322 Id* val_sel_id = new Id(Location().introduce(), val_sel_s, nullptr);
323 Id* complete_id = new Id(Location().introduce(), "complete", nullptr);
324 si->ann().add(new Call(Location().introduce(), ASTString("int_search"),
325 {search_vars, var_sel_id, val_sel_id, complete_id}));
326 }
327 }
328 _model->addItem(si);
329 return;
330 }
331 auto fnit = _model->fnmap.find(ASTString(name));
332 assert(fnit != _model->fnmap.end());
333 assert(fnit->second.size() == 1);
334 std::vector<Type>& tys = fnit->second[0].t;
335 assert(tys.size() == c->size());
336 std::vector<Expression*> args(proc.nargs);
337 for (int i = 0; i < proc.nargs; ++i) {
338 args[i] = val_to_expr(tys[i], c->arg(i));
339 }
340 auto call = new Call(Location().introduce(), name, args);
341 auto ci = new ConstraintI(Location().introduce(), call);
342 _model->addItem(ci);
343};
344
345void FZNSolverInstance::addVariable(Variable* var, bool isOutput) {
346 GCLock lock;
347 Vec* dom = var->domain();
348 assert(dom->size() >= 2 && dom->size() % 2 == 0);
349
350 if (!isOutput && dom->size() == 2 && (*dom)[0] == 0 && (*dom)[1] == 1) {
351 vdmap.emplace(std::piecewise_construct, std::forward_as_tuple(var->timestamp()),
352 std::forward_as_tuple(nullptr, nullptr, false, false));
353 uninitialised_vars.insert(var->timestamp());
354 return;
355 }
356
357 std::vector<IntSetVal::Range> ranges;
358 for (int i = 0; i < dom->size(); i += 2) {
359 ranges.emplace_back((*dom)[i].toIntVal(), (*dom)[i + 1].toIntVal());
360 }
361 SetLit* dom_set = new SetLit(Location().introduce(), IntSetVal::a(ranges));
362 auto ti = new TypeInst(Location().introduce(), Type::varint(), dom_set);
363 VarDecl* vd = add_var_to_model(var->timestamp(), ti, false, isOutput);
364 vdmap.emplace(std::piecewise_construct, std::forward_as_tuple(var->timestamp()),
365 std::forward_as_tuple(vd, nullptr, true, false));
366}
367
368Val FZNSolverInstance::getSolutionValue(Variable* var) {
369 GCLock lock;
370 Id ident(Location().introduce(), var->timestamp(), nullptr);
371 auto de = getSolns2Out()->findOutputVar(ident.str());
372 assert(de.first->e()); // A solution must have been assigned
373 return Val::fromIntVal(eval_int(env.envi(), de.first->e()));
374};
375
376void FZNSolverInstance::pushState() { stack.emplace_back(_model->size()); }
377
378void FZNSolverInstance::popState() {
379 for (auto i = stack.back(); i < _model->size(); ++i) {
380 Item* it = (*_model)[i];
381 if (!it->isa<FunctionI>()) {
382 it->remove();
383 }
384 }
385 _model->compact();
386 stack.pop_back();
387}
388
389void FZNSolverInstance::printStatistics(bool fLegend) {
390 FlatModelStatistics stats = statistics(_model);
391 auto& out = getSolns2Out()->getOutput();
392
393 if (stats.n_bool_vars) {
394 out << "%%%mzn-stat: flatBoolVars=" << stats.n_bool_vars << endl;
395 }
396 if (stats.n_int_vars) {
397 out << "%%%mzn-stat: flatIntVars=" << stats.n_int_vars << endl;
398 }
399 if (stats.n_float_vars) {
400 out << "%%%mzn-stat: flatFloatVars=" << stats.n_float_vars << endl;
401 }
402 if (stats.n_set_vars) {
403 out << "%%%mzn-stat: flatSetVars=" << stats.n_set_vars << endl;
404 }
405
406 if (stats.n_bool_ct) {
407 out << "%%%mzn-stat: flatBoolConstraints=" << stats.n_bool_ct << endl;
408 }
409 if (stats.n_int_ct) {
410 out << "%%%mzn-stat: flatIntConstraints=" << stats.n_int_ct << endl;
411 }
412 if (stats.n_float_ct) {
413 out << "%%%mzn-stat: flatFloatConstraints=" << stats.n_float_ct << endl;
414 }
415 if (stats.n_set_ct) {
416 out << "%%%mzn-stat: flatSetConstraints=" << stats.n_set_ct << endl;
417 }
418
419 if (stats.n_reif_ct) {
420 out << "%%%mzn-stat: evaluatedReifiedConstraints=" << stats.n_reif_ct << endl;
421 }
422 if (stats.n_imp_ct) {
423 out << "%%%mzn-stat: evaluatedHalfReifiedConstraints=" << stats.n_imp_ct << endl;
424 }
425
426 if (stats.n_imp_del) {
427 out << "%%%mzn-stat: eliminatedImplications=" << stats.n_imp_del << endl;
428 }
429 if (stats.n_lin_del) {
430 out << "%%%mzn-stat: eliminatedLinearConstraints=" << stats.n_lin_del << endl;
431 }
432
433 /// Objective / SAT. These messages are used by mzn-test.py.
434 SolveI* solveItem = _model->solveItem();
435 if (solveItem && solveItem->st() != SolveI::SolveType::ST_SAT) {
436 if (solveItem->st() == SolveI::SolveType::ST_MAX) {
437 out << "%%%mzn-stat: method=\"maximize\"" << endl;
438 } else {
439 out << "%%%mzn-stat: method=\"minimize\"" << endl;
440 }
441 } else {
442 out << "%%%mzn-stat: method=\"satisfy\"" << endl;
443 }
444 out << "%%%mzn-stat-end" << endl << endl;
445}
446void FZNSolverInstance::printFlatZincToFile(std::string filename) {
447 std::ofstream os(filename);
448 Printer p(os, 0, true);
449 for (FunctionIterator it = _model->begin_functions(); it != _model->end_functions(); ++it) {
450 if (!it->removed()) {
451 Item& item = *it;
452 p.print(&item);
453 }
454 }
455 for (VarDeclIterator it = _model->begin_vardecls(); it != _model->end_vardecls(); ++it) {
456 if (!it->removed()) {
457 Item& item = *it;
458 p.print(&item);
459 }
460 }
461 for (ConstraintIterator it = _model->begin_constraints(); it != _model->end_constraints(); ++it) {
462 if (!it->removed()) {
463 Item& item = *it;
464 p.print(&item);
465 }
466 }
467 if (_model->solveItem()) {
468 p.print(_model->solveItem());
469 } else {
470 GCLock lock;
471 auto si = SolveI::sat(Location().introduce());
472 p.print(si);
473 }
474}
475void FZNSolverInstance::printOutputToFile(std::string filename) {
476 Model* output = env.output();
477 std::ofstream os(filename);
478 Printer p(os, 0, true);
479 p.print(output);
480}
481void FZNSolverInstance::outputArray(Vec* arr) {
482 GCLock lock;
483 std::vector<Expression*> content;
484 for (int i = 0; i < arr->size(); ++i) {
485 Val real = Val::follow_alias((*arr)[i]);
486 content.push_back(val_to_expr(Type::parint(), real));
487 }
488 auto* al = new ArrayLit(Location().introduce(), content);
489 std::vector<Expression*> sarg = {new Call(Location().introduce(), constants().ids.show, {al})};
490 auto* sal = new ArrayLit(Location().introduce(), sarg);
491 env.output()->addItem(new OutputI(Location().introduce(), sal));
492}
493void FZNSolverInstance::outputDict(Variable* start) {
494 GCLock lock;
495 std::vector<Expression*> content;
496 auto* open = new StringLit(Location().introduce(), "{");
497 auto* close = new StringLit(Location().introduce(), "}");
498 auto* comma = new StringLit(Location().introduce(), ",");
499 auto* quote = new StringLit(Location().introduce(), "\"");
500 auto* quote_colon = new StringLit(Location().introduce(), "\":");
501 auto* var_start = new StringLit(Location().introduce(), "X_INTRODUCED_");
502
503 content.push_back(open);
504 Variable* v = start->next(); // Skip root node
505 bool first = true;
506 while (v != start) {
507 if (!first) {
508 content.push_back(comma);
509 }
510 Val real = Val::follow_alias(Val(v));
511 content.push_back(quote);
512 content.push_back(var_start);
513 content.push_back(new StringLit(Location().introduce(), std::to_string(v->timestamp())));
514 content.push_back(quote_colon);
515 content.push_back(new Call(Location().introduce(), constants().ids.show,
516 {val_to_expr(Type::parint(), real)}));
517 v = v->next();
518 first = false;
519 };
520 content.push_back(close);
521 auto* al = new ArrayLit(Location().introduce(), content);
522 env.output()->addItem(new OutputI(Location().introduce(), al));
523}
524
525SolverInstance::Status FZNSolverInstance::solve(void) {
526 {
527 // Add all remaining variables to the model
528 GCLock lock;
529 auto ti = new TypeInst(Location().introduce(), Type::varbool());
530 for (int var : uninitialised_vars) {
531 add_var_to_model(var, ti);
532 }
533 }
534
535 FZNSolverOptions& opt = static_cast<FZNSolverOptions&>(*_options);
536 if (opt.fzn_solver.empty()) {
537 throw InternalError("No FlatZinc solver specified");
538 }
539 /// Passing options to solver
540 vector<string> cmd_line;
541 cmd_line.push_back(opt.fzn_solver);
542 string sBE = opt.backend;
543 if (sBE.size()) {
544 cmd_line.push_back("-b");
545 cmd_line.push_back(sBE);
546 }
547 for (auto& f : opt.fzn_flags) {
548 cmd_line.push_back(f);
549 }
550 if (opt.numSols != 1) {
551 cmd_line.push_back("-n");
552 ostringstream oss;
553 oss << opt.numSols;
554 cmd_line.push_back(oss.str());
555 }
556 if (opt.allSols) {
557 cmd_line.push_back("-a");
558 }
559 if (opt.parallel.size()) {
560 cmd_line.push_back("-p");
561 ostringstream oss;
562 oss << opt.parallel;
563 cmd_line.push_back(oss.str());
564 }
565 if (opt.printStatistics) {
566 cmd_line.push_back("-s");
567 }
568 if (opt.solver_time_limit_ms != 0) {
569 cmd_line.push_back("-t");
570 std::ostringstream oss;
571 oss << opt.solver_time_limit_ms;
572 cmd_line.push_back(oss.str());
573 }
574 if (opt.verbose) {
575 if (opt.supports_v) cmd_line.push_back("-v");
576 std::cerr << "Using FZN solver " << cmd_line[0] << " for solving, parameters: ";
577 for (int i = 1; i < cmd_line.size(); ++i) cerr << "" << cmd_line[i] << " ";
578 cerr << std::endl;
579 }
580 int timelimit = opt.fzn_time_limit_ms;
581 bool sigint = opt.fzn_sigint;
582
583 FileUtils::TmpFile fznFile(".fzn");
584 printFlatZincToFile(fznFile.name());
585 cmd_line.push_back(fznFile.name());
586
587 FileUtils::TmpFile* pathsFile = NULL;
588 // if(opt.fzn_needs_paths) {
589 // pathsFile = new FileUtils::TmpFile(".paths");
590 // std::ofstream ofs(pathsFile->name());
591 // PathFilePrinter pfp(ofs, _env.envi());
592 // pfp.print(_fzn);
593
594 // cmd_line.push_back("--paths");
595 // cmd_line.push_back(pathsFile->name());
596 // }
597 getSolns2Out()->initFromEnv(&env);
598
599 if (!opt.fzn_output_passthrough) {
600 Process<Solns2Out> proc(cmd_line, getSolns2Out(), timelimit, sigint);
601 int exitStatus = proc.run();
602 delete pathsFile;
603 return exitStatus == 0 ? getSolns2Out()->status : SolverInstance::ERROR;
604 } else {
605 Solns2Log s2l(getSolns2Out()->getOutput(), _log);
606 Process<Solns2Log> proc(cmd_line, &s2l, timelimit, sigint);
607 int exitStatus = proc.run();
608 delete pathsFile;
609 return exitStatus == 0 ? SolverInstance::NONE : SolverInstance::ERROR;
610 }
611}
612
613void FZNSolverInstance::processFlatZinc(void) {}
614
615void FZNSolverInstance::resetSolver(void) {}
616
617Expression* FZNSolverInstance::getSolutionValue(Id* id) {
618 assert(false);
619 return NULL;
620}
621} // namespace MiniZinc