1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
|
/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
/*
* Main authors:
* Guido Tack <guido.tack@monash.edu>
*/
/* This Source Code Form is subject to the terms of the Mozilla Public
* License, v. 2.0. If a copy of the MPL was not distributed with this
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
#ifdef _MSC_VER
#define _CRT_SECURE_NO_WARNINGS
#endif
#include <iostream>
#include <fstream>
#include <iomanip>
#include <minizinc/model.hh>
#include <minizinc/parser.hh>
#include <minizinc/prettyprinter.hh>
#include <minizinc/typecheck.hh>
#include <minizinc/astexception.hh>
#include <minizinc/hash.hh>
#include <minizinc/eval_par.hh>
#include <minizinc/builtins.hh>
#include <minizinc/file_utils.hh>
#include <minizinc/timer.hh>
using namespace MiniZinc;
using namespace std;
std::string stoptime(Timer& timer) {
std::ostringstream oss;
oss << std::setprecision(0) << std::fixed << timer.ms() << " ms";
return oss.str();
}
int main(int argc, char** argv) {
Timer starttime;
string filename;
string flag_output_file;
bool flag_output_comments = true;
bool flag_output_flush = true;
bool flag_output_time = false;
string solfile;
int flag_ignore_lines = 0;
istream& solstream = cin;
string solution_separator = "----------";
string solution_comma = "";
string unsatisfiable_msg = "=====UNSATISFIABLE=====";
string unbounded_msg = "=====UNBOUNDED=====";
string unknown_msg = "=====UNKNOWN=====";
string search_complete_msg= "==========";
vector<string> includePaths;
string std_lib_dir;
if (char* MZNSTDLIBDIR = getenv("MZN_STDLIB_DIR")) {
std_lib_dir = string(MZNSTDLIBDIR);
}
if (argc < 2)
goto error;
for (int i=1; i<argc; i++) {
if (string(argv[i])==string("--version")) {
std::cout << "NICTA MiniZinc solution printing tool, version "
<< MZN_VERSION_MAJOR << "." << MZN_VERSION_MINOR << "." << MZN_VERSION_PATCH << std::endl;
std::cout << "Copyright (C) 2014, 2015 Monash University and NICTA" << std::endl;
std::exit(EXIT_SUCCESS);
}
if (string(argv[i])==string("-h") || string(argv[i])==string("--help")) {
goto error;
} else if (string(argv[i])=="-o" || string(argv[i])=="--output-to-file") {
i++;
if (i==argc)
goto error;
flag_output_file = argv[i];
} else if (string(argv[i])=="--stdlib-dir") {
i++;
if (i==argc)
goto error;
std_lib_dir = argv[i];
} else if (string(argv[i])=="--no-flush-output") {
flag_output_flush = false;
} else if (string(argv[i])=="--no-output-comments") {
flag_output_comments = false;
} else if (string(argv[i])=="-i" ||
string(argv[i])=="--ignore-lines" ||
string(argv[i])=="--ignore-leading-lines") {
++i;
if (i==argc)
goto error;
flag_ignore_lines = atoi(argv[i]);
} else if (string(argv[i])=="--soln-sep" ||
string(argv[i])=="--soln-separator" ||
string(argv[i])=="--solution-separator") {
++i;
if (i==argc)
goto error;
solution_separator = string(argv[i]);
} else if (string(argv[i])=="--soln-comma" ||
string(argv[i])=="--solution-comma") {
++i;
if (i==argc)
goto error;
solution_comma = string(argv[i]);
} else if (string(argv[i])=="--unsat-msg" ||
string(argv[i])=="--unsatisfiable-msg") {
++i;
if (i==argc)
goto error;
unsatisfiable_msg = string(argv[i]);
} else if (string(argv[i])=="--unbounded-msg") {
++i;
if (i==argc)
goto error;
unbounded_msg = string(argv[i]);
} else if (string(argv[i])=="--unknown-msg") {
++i;
if (i==argc)
goto error;
unknown_msg = string(argv[i]);
} else if (string(argv[i])=="--search-complete-msg") {
++i;
if (i==argc)
goto error;
search_complete_msg = string(argv[i]);
} else if (string(argv[i])=="--output-time") {
flag_output_time = true;
} else {
filename = argv[i++];
if (filename.length()<=4 ||
filename.substr(filename.length()-4,string::npos) != ".ozn") {
std::cerr << "Invalid .ozn file " << filename << "." << std::endl;
goto error;
}
}
}
if (std_lib_dir=="") {
std::string mypath = FileUtils::progpath();
if (!mypath.empty()) {
if (FileUtils::file_exists(mypath+"/share/minizinc/std/builtins.mzn")) {
std_lib_dir = mypath+"/share/minizinc";
} else if (FileUtils::file_exists(mypath+"/../share/minizinc/std/builtins.mzn")) {
std_lib_dir = mypath+"/../share/minizinc";
} else if (FileUtils::file_exists(mypath+"/../../share/minizinc/std/builtins.mzn")) {
std_lib_dir = mypath+"/../../share/minizinc";
}
}
}
if (std_lib_dir=="") {
std::cerr << "Error: unknown minizinc standard library directory.\n"
<< "Specify --stdlib-dir on the command line or set the\n"
<< "MZN_STDLIB_DIR environment variable.\n";
std::exit(EXIT_FAILURE);
}
includePaths.push_back(std_lib_dir+"/std/");
{
if (Model* outputm = parse(filename, std::vector<std::string>(), includePaths, false, false, false,
std::cerr)) {
try {
std::vector<TypeError> typeErrors;
Env env(outputm);
MiniZinc::typecheck(env,outputm,typeErrors);
MiniZinc::registerBuiltins(env,outputm);
typedef pair<VarDecl*,Expression*> DE;
ASTStringMap<DE>::t declmap;
Expression* outputExpr = NULL;
for (unsigned int i=0; i<outputm->size(); i++) {
if (VarDeclI* vdi = (*outputm)[i]->dyn_cast<VarDeclI>()) {
declmap.insert(pair<ASTString,DE>(vdi->e()->id()->v(),DE(vdi->e(),vdi->e()->e())));
} else if (OutputI* oi = (*outputm)[i]->dyn_cast<OutputI>()) {
outputExpr = oi->e();
}
}
//ostream& fout(flag_output_file.empty() ? std::cout : new fstream(flag_output_file));
fstream file_ostream;
if (!flag_output_file.empty())
file_ostream.open(flag_output_file.c_str(), std::fstream::out);
ostream& fout = flag_output_file.empty() ? std::cout : file_ostream;
int solutions_found = 0;
string solution;
string comments;
for (;;) {
if (solstream.good()) {
string line;
getline(solstream, line);
if (flag_ignore_lines > 0) {
flag_ignore_lines--;
continue;
}
if (line=="----------") {
++solutions_found;
if (flag_output_time)
fout << "% time elapsed: " << stoptime(starttime) << "\n";
// Put the "solution comma" before the solution itself,
// but only for solutions after the first one.
if (solutions_found > 1 && !solution_comma.empty())
fout << solution_comma << std::endl;
if (outputExpr != NULL) {
for (unsigned int i=0; i<outputm->size(); i++) {
if (VarDeclI* vdi = (*outputm)[i]->dyn_cast<VarDeclI>()) {
ASTStringMap<DE>::t::iterator it = declmap.find(vdi->e()->id()->v());
vdi->e()->e(it->second.second);
vdi->e()->evaluated(false);
}
}
Model* sm = parseFromString(solution, "solution received from solver", includePaths, true, false, false, cerr);
if (!sm) {
exit(EXIT_FAILURE);
}
for (unsigned int i=0; i<sm->size(); i++) {
if (AssignI* ai = (*sm)[i]->dyn_cast<AssignI>()) {
ASTStringMap<DE>::t::iterator it = declmap.find(ai->id());
if (it==declmap.end()) {
cerr << "Error: unexpected identifier " << ai->id() << " in output\n";
exit(EXIT_FAILURE);
}
ai->e()->type(it->second.first->type());
ai->decl(it->second.first);
typecheck(env,outputm, ai);
if (Call* c = ai->e()->dyn_cast<Call>()) {
// This is an arrayXd call, make sure we get the right builtin
assert(c->args()[c->args().size()-1]->isa<ArrayLit>());
for (unsigned int i=0; i<c->args().size(); i++)
c->args()[i]->type(Type::parsetint());
c->args()[c->args().size()-1]->type(it->second.first->type());
c->decl(outputm->matchFn(env.envi(),c));
}
it->second.first->e(ai->e());
}
}
delete sm;
GCLock lock;
ArrayLit* al = eval_array_lit(env.envi(),outputExpr);
std::string os;
for (unsigned int i=0; i<al->v().size(); i++) {
std::string s = eval_string(env.envi(),al->v()[i]);
if (!s.empty()) {
os = s;
fout << os;
if (flag_output_flush)
fout.flush();
}
}
if (!os.empty() && os[os.size()-1] != '\n')
fout << std::endl;
if (flag_output_flush)
fout.flush();
}
fout << comments;
fout << solution_separator << std::endl;
if (flag_output_flush)
fout.flush();
solution = "";
comments = "";
} else if (line=="==========") {
if (flag_output_time)
fout << "% time elapsed: " << stoptime(starttime) << "\n";
fout << search_complete_msg << std::endl;
if (flag_output_flush)
fout.flush();
} else if(line=="=====UNSATISFIABLE=====") {
if (flag_output_time)
fout << "% time elapsed: " << stoptime(starttime) << "\n";
fout << unsatisfiable_msg << std::endl;
if (flag_output_flush)
fout.flush();
} else if(line=="=====UNBOUNDED=====") {
if (flag_output_time)
fout << "% time elapsed: " << stoptime(starttime) << "\n";
fout << unbounded_msg << std::endl;
if (flag_output_flush)
fout.flush();
} else if(line=="=====UNKNOWN=====") {
if (flag_output_time)
fout << "% time elapsed: " << stoptime(starttime) << "\n";
fout << unknown_msg << std::endl;
if (flag_output_flush)
fout.flush();
} else {
solution += line+"\n";
size_t comment_pos = line.find('%');
if (comment_pos != string::npos) {
comments += line.substr(comment_pos);
comments += "\n";
}
}
} else {
break;
}
}
fout << comments;
if (flag_output_flush)
fout.flush();
} catch (LocationException& e) {
std::cerr << e.what() << ": " << e.msg() << std::endl;
std::cerr << e.loc() << std::endl;
exit(EXIT_FAILURE);
} catch (Exception& e) {
std::cerr << e.what() << ": " << e.msg() << std::endl;
exit(EXIT_FAILURE);
}
delete outputm;
}
}
return 0;
error:
std::cerr << "Usage: "<< argv[0]
<< " [<options>] <model>.ozn" << std::endl
<< std::endl
<< "Options:" << std::endl
<< " --help, -h\n Print this help message." << std::endl
<< " --version\n Print version information." << std::endl
<< " -o <file>, --output-to-file <file>\n Filename for generated output." << std::endl
<< " --stdlib-dir <dir>\n Path to MiniZinc standard library directory." << std::endl
<< " --no-output-comments\n Do not print comments in the FlatZinc solution stream." << std::endl
<< " --output-time\n Print timing information in the FlatZinc solution stream." << std::endl
<< " --no-flush-output\n Don't flush output stream after every line." << std::endl
<< " -i <n>, --ignore-lines <n>, --ignore-leading-lines <n>\n Ignore the first <n> lines in the FlatZinc solution stream." << std::endl
<< " --soln-sep <s>, --soln-separator <s>, --solution-separator <s>\n Specify the string printed after each solution.\n The default is to use the same as FlatZinc,\n \"----------\"." << std::endl
<< " --soln-comma <s>, --solution-comma <s>\n Specify the string used to separate solutions.\n The default is the empty string." << std::endl
<< " --unsat-msg <msg>, --unsatisfiable-msg <msg>\n Specify the message to print if the model instance is\n unsatisfiable.\n The default is to print \"=====UNSATISFIABLE=====\"." << std::endl
<< " --unbounded-msg <msg>\n Specify the message to print if the objective of the\n model instance is unbounded.\n The default is to print \"=====UNBOUNDED=====\"." << std::endl
<< " --unknown-msg <msg>\n Specify the message to print if search terminates without\n the entire search space having been explored and no\n solution has been found.\n The default is to print \"=====UNKNOWN=====\"." << std::endl
<< " --search-complete-msg <msg>\n Specify the message to print if search terminates having\n explored the entire search space.\n The default is to print \"==========\"." << std::endl
;
exit(EXIT_FAILURE);
}
|
