Lattice Land Parsing Library
Loading...
Searching...
No Matches
flatzinc_parser.hpp
Go to the documentation of this file.
1// Copyright 2022 Pierre Talbot
2
3#ifndef LALA_PARSING_FLATZINC_PARSER_HPP
4#define LALA_PARSING_FLATZINC_PARSER_HPP
5
6#include "peglib.h"
7#include <cassert>
8#include <cstdlib>
9#include <string>
10#include <istream>
11#include <fstream>
12#include <streambuf>
13#include <iostream>
14#include <cfenv>
15#include <set>
16#include <cinttypes>
17#include "battery/shared_ptr.hpp"
18#include "lala/logic/ast.hpp"
19#include "solver_output.hpp"
20
21namespace lala {
22
23namespace impl {
24
25/** Unfortunately, I'm really not sure this function works in all cases due to compiler bugs with rounding modes... */
26inline logic_real string_to_real(const std::string& s) {
27 #if !defined(__GNUC__) && !defined(_MSC_VER)
28 #pragma STDC FENV_ACCESS ON
29 #endif
30 int old = std::fegetround();
31 int r = std::fesetround(FE_DOWNWARD);
32 assert(r == 0);
33 double lb = std::strtod(s.c_str(), nullptr);
34 r = std::fesetround(FE_UPWARD);
35 assert(r == 0);
36 double ub = std::strtod(s.c_str(), nullptr);
37 std::fesetround(old);
38 return battery::make_tuple(lb, ub);
39}
40
41template <class Allocator>
42class FlatZincParser {
43 using allocator_type = Allocator;
44 using F = TFormula<allocator_type>;
45 using SV = peg::SemanticValues;
46 using Set = logic_set<F>;
47 using So = Sort<allocator_type>;
48 using bstring = battery::string<Allocator>;
49 using FSeq = typename F::Sequence;
50
51 std::map<std::string, F> params; // Name and value of the parameters occuring in the model.
52 std::map<std::string, int> arrays; // Size of all named arrays (parameters and variables).
53 bool error; // If an error was found during parsing.
54 bool silent; // If we do not want to output error messages.
55 SolverOutput<Allocator>& output;
56
57 // Contains all the annotations ignored.
58 // It is used to avoid printing an error message more than once per annotation.
59 std::set<std::string> ignored_annotations;
60
61 enum class TableKind {
62 PLAIN,
63 SHORT,
64 COMPRESSED,
65 BASIC
66 };
67
68public:
69 FlatZincParser(SolverOutput<Allocator>& output): error(false), silent(false), output(output) {}
70
71 battery::shared_ptr<F, allocator_type> parse(const std::string& input) {
72 peg::parser parser(R"(
73 Statements <- (PredicateDecl / VariableDecl / VarArrayDecl / ParameterDecl / ConstraintDecl / SolveItem / Comment)+
74
75 Literal <- Boolean / Real / Integer / ArrayAccess / VariableLit / Set
76 RangeLiteral <- SetRange / Literal
77 InnerRangeLiteral <- InnerSetRange / Literal
78
79 VariableLit <- Identifier
80 Identifier <- < [a-zA-Z_][a-zA-Z0-9_]* >
81 Boolean <- < 'true' / 'false' >
82 Real <- < (
83 'inf'
84 / '-inf'
85 / [+-]? [0-9]+ (('.' (&'..' / !'.') [0-9]*) / ([Ee][+-]?[0-9]+)) ) >
86 Integer <- < [+-]? [0-9]+ >
87 Set <- '{' '}' / '{' InnerRangeLiteral (',' InnerRangeLiteral)* '}'
88 InnerSetRange <- Literal '..' Literal
89 SetRange <- InnerSetRange
90 ArrayAccess <- Identifier '[' (VariableLit / Integer) ']'
91
92 VariableDecl <- 'var' ValueType ':' Identifier Annotations ('=' Literal)? ';'
93 VarArrayDecl <- 'array' '[' IndexSet ']' 'of' 'var' ValueType ':' Identifier Annotations ('=' LiteralArray)? ';'
94
95 SetValue <- 'set' 'of' (SetRange / Set)
96
97 ValueType <- Type
98 / SetValue
99 / SetRange
100 / Set
101
102 IntType <- 'int'
103 RealType <- 'float' / 'real'
104 BoolType <- 'bool'
105 SetType <- 'set' 'of' Type
106 Type <- IntType / RealType / BoolType / SetType
107
108 Annotation <- Identifier ('(' Parameter (',' Parameter)* ')')?
109 Annotations <- ('::' Annotation)*
110
111 ConstraintDecl <- 'constraint' (PredicateCall / Boolean) Annotations ';'
112
113 LiteralInExpression <- RangeLiteral !'('
114 FunctionCall <- Identifier '(' Parameter (',' Parameter )* ')'
115 Parameter <- LiteralInExpression / FunctionCall / LiteralArray
116 PredicateCall <- Identifier '(' Parameter (',' Parameter)* ')'
117
118 PredicateDecl <- 'predicate' Identifier '(' (!')' .)* ')' ';'
119
120 MinimizeItem <- 'minimize' RangeLiteral
121 MaximizeItem <- 'maximize' RangeLiteral
122 SatisfyItem <- 'satisfy'
123 SolveItem <- 'solve' SearchAnnotations (MinimizeItem / MaximizeItem / SatisfyItem) ';'
124
125 SearchAnnotations <- ('::' SearchAnnotation)*
126 SearchAnnotation <- SeqSearch / BaseSearch
127 SeqSearch <- 'seq_search' '(' '[' SearchAnnotation (',' SearchAnnotation)* ']' ')'
128 BaseSearch <- ('int_search' / 'bool_search' / 'set_search') '(' (VariableLit / LiteralArray) ',' Identifier ',' Identifier ',' Identifier ')'
129
130 LiteralArray <- '[]' / '[' RangeLiteral (',' RangeLiteral)* ']'
131 ParameterExpr <- RangeLiteral / LiteralArray
132 IndexSet <- '1' '..' Integer
133 ArrayType <- 'array' '[' IndexSet ']' 'of' Type
134 ParameterType <- Type / ArrayType
135 ParameterDecl <- ParameterType ':' Identifier '=' ParameterExpr ';'
136
137 ~Comment <- '%' [^\n\r]* [ \n\r\t]*
138 %whitespace <- [ \n\r\t]*
139 )");
140
141 assert(static_cast<bool>(parser) == true);
142
143 parser["Integer"] = [](const SV &sv) { return F::make_z(sv.token_to_number<logic_int>()); };
144 parser["Real"] = [](const SV &sv) { return F::make_real(string_to_real(sv.token_to_string())); };
145 parser["Boolean"] = [](const SV &sv) { return sv.token_to_string() == "true" ? F::make_true() : F::make_false(); };
146 parser["Identifier"] = [](const SV &sv) { return sv.token_to_string(); };
147 parser["Set"] = [this](const SV &sv) { return make_set_literal(sv); };
148 parser["InnerSetRange"] = [this](const SV &sv) { return battery::make_tuple(f(sv[0]), f(sv[1])); };
149 parser["SetRange"] = [this](const SV &sv) { return F::make_set(Set({itv(sv[0])})); };
150 parser["ArrayAccess"] = [this](const SV &sv) { return make_access_literal(sv); };
151 parser["LiteralArray"] = [](const SV &sv) { return sv; };
152 parser["ParameterDecl"] = [this] (const SV &sv) { return make_parameter_decl(sv); };
153 parser["PredicateDecl"] = [this] (const SV &sv) { return F(); };
154 parser["VariableLit"] = [](const SV &sv) { return F::make_lvar(UNTYPED, LVar<Allocator>(std::any_cast<std::string>(sv[0]))); };
155 parser["IntType"] = [](const SV &sv) { return So(So::Int); };
156 parser["RealType"] = [](const SV &sv) { return So(So::Real); };
157 parser["BoolType"] = [](const SV &sv) { return So(So::Bool); };
158 parser["SetType"] = [](const SV &sv) { return So(So::Set, std::any_cast<Sort<Allocator>>(sv[0])); };
159 parser["Annotations"] = [](const SV &sv) { return sv; };
160 parser["Annotation"] = [](const SV &sv) { return sv; };
161 // When we have `var set of 1..5: s;`, what it means is that `s in {}..{1..5}`, i.e., a set between {} and {1..5}.
162 parser["SetValue"] = [](const SV &sv) { return F::make_set(Set({battery::make_tuple(F::make_set(Set{}), f(sv[0]))})); };
163 parser["VariableDecl"] = [this](const SV &sv) { return make_variable_init_decl(sv); };
164 parser["VarArrayDecl"] = [this](const SV &sv) { return make_variable_array_decl(sv); };
165 parser["ConstraintDecl"] = [this](const SV &sv) { return update_with_annotations(sv, f(sv[0]), std::any_cast<SV>(sv[1])); };
166 parser["FunctionCall"] = [this](const SV &sv) { return function_call(sv); };
167 parser["PredicateCall"] = [this](const SV &sv) { return predicate_call(sv); };
168 parser["Statements"] = [this](const SV &sv) { return make_statements(sv); };
169 parser["MinimizeItem"] = [](const SV &sv) { return F::make_unary(MINIMIZE, f(sv[0])); };
170 parser["MaximizeItem"] = [](const SV &sv) { return F::make_unary(MAXIMIZE, f(sv[0])); };
171 parser["SatisfyItem"] = [](const SV &sv) { return F(); };
172 parser["SolveItem"] = [this](const SV &sv) { return make_solve_item(sv);};
173 parser["SearchAnnotations"] = [this](const SV &sv) { return make_search_annotations(sv);};
174 parser["BaseSearch"] = [this](const SV &sv) { return make_base_search(sv);};
175 parser["SeqSearch"] = [this](const SV &sv) { return make_seq_search(sv);};
176 parser.set_logger([](size_t line, size_t col, const std::string& msg, const std::string &rule) {
177 std::cerr << line << ":" << col << ": " << msg << "\n";
178 });
179
180 F f;
181 if(parser.parse(input.c_str(), f) && !error) {
182 return battery::make_shared<TFormula<Allocator>, Allocator>(std::move(f));
183 }
184 else {
185 return nullptr;
186 }
187 }
188
189 private:
190 static F f(const std::any& any) {
191 return std::any_cast<F>(any);
192 }
193
194 static battery::tuple<F, F> itv(const std::any& any) {
195 return std::any_cast<battery::tuple<F, F>>(any);
196 }
197
198 F make_error(const SV& sv, const std::string& msg) {
199 if(!silent) {
200 std::cerr << sv.line_info().first << ":" << sv.line_info().second << ":" << msg << std::endl;
201 }
202 error = true;
203 return F::make_false();
204 }
205
206 F make_arity_error(const SV& sv, Sig sig, int expected, int obtained) {
207 return make_error(sv, "The symbol `" + std::string(string_of_sig(sig)) +
208 "` expects `" + std::to_string(expected) + "` parameters" +
209 ", but we got `" + std::to_string(obtained) + "` parameters.");
210 }
211
212 F make_set_literal(const SV& sv) {
213 logic_set<F> set;
214 for(int i = 0; i < sv.size(); ++i) {
215 try {
216 auto range = std::any_cast<battery::tuple<F,F>>(sv[i]);
217 set.push_back(range);
218 }
219 catch(std::bad_any_cast) {
220 bool element_added = false;
221 auto element = f(sv[i]);
222 if(element.is(F::Z) && set.size() > 0) {
223 auto& ub = battery::get<1>(set.back());
224 if(!ub.is(F::Z)) {
225 return make_error(sv, "Elements in a set are expected to be all of the same type.");
226 }
227 else if(ub.z() == element.z() - 1) {
228 ub.z() = element.z();
229 element_added = true;
230 }
231 }
232 else if(element.is(F::LV)) {
233 std::string name(element.lv().data());
234 if(params.contains(name)) {
235 set.push_back(battery::make_tuple(params[name], params[name]));
236 element_added = true;
237 }
238 else {
239 return make_error(sv, "Undeclared parameter `" + name + "`.");
240 }
241 }
242 if(!element_added) {
243 set.push_back(battery::make_tuple(element, element));
244 }
245 }
246 }
247 return F::make_set(set);
248 }
249
250 F make_access_literal(const SV& sv) {
251 auto name = std::any_cast<std::string>(sv[0]);
252 auto index = f(sv[1]);
253 int idx = -1;
254 if(index.is(F::Z)) {
255 idx = static_cast<int>(index.z());
256 }
257 else if(index.is(F::LV)) {
258 if(params.contains(index.lv().data())) {
259 auto pindex = params[index.lv().data()];
260 if(pindex.is(F::Z)) {
261 idx = static_cast<int>(pindex.z());
262 }
263 }
264 }
265 if(idx == -1) {
266 return make_error(sv, "Given `a[b]`, `b` must be an integer or an integer parameter.");
267 }
268 auto access_var = make_array_access(name, idx-1);
269 if(params.contains(access_var)) {
270 return params[access_var];
271 }
272 else {
273 return F::make_lvar(UNTYPED, access_var);
274 }
275 }
276
277 F make_parameter_decl(const SV& sv) {
278 std::string identifier(std::any_cast<std::string>(sv[1]));
279 try {
280 if(params.contains(identifier)) {
281 return make_error(sv, ("Parameter `" + identifier + "` already declared.").c_str());
282 }
283 else {
284 params[identifier] = f(sv[2]);
285 }
286 } catch(std::bad_any_cast) {
287 auto array = std::any_cast<SV>(sv[2]);
288 arrays[identifier] = static_cast<int>(array.size());
289 for(int i = 0; i < static_cast<int>(array.size()); ++i) {
290 auto id = make_array_access(identifier, i);
291 params[id] = f(array[i]);
292 }
293 }
294 return F::make_true();
295 }
296
297 F make_variable_array_decl(const SV& sv) {
298 int arraySize = static_cast<int>(f(sv[0]).z());
299 auto name = std::any_cast<std::string>(sv[2]);
300 arrays[name] = arraySize;
301 battery::vector<F, Allocator> decl;
302 for(int i = 0; i < arraySize; ++i) {
303 decl.push_back(make_variable_decl(sv, make_array_access(name, i), sv[1], sv[3]));
304 }
305 if(sv.size() == 5) {
306 auto array = resolve_array(sv, sv[4]);
307 if(!array.is(F::Seq)) {
308 return array;
309 }
310 for(int i = 0; i < array.seq().size(); ++i) {
311 decl.push_back(F::make_binary(
312 F::make_lvar(UNTYPED, LVar<Allocator>(make_array_access(name, i))),
313 EQ,
314 array.seq(i)));
315 }
316 }
317 return F::make_nary(AND, std::move(decl));
318 }
319
320 F update_with_annotations(const SV& sv, F formula, const SV& annots) {
321 for(int i = 0; i < annots.size(); ++i) {
322 auto annot = std::any_cast<SV>(annots[i]);
323 auto name = std::any_cast<std::string>(annot[0]);
324 if(name == "abstract") {
325 AType ty = f(annot[1]).z();
326 formula.type_as(ty);
327 }
328 else if(name == "is_defined_var") {}
329 else if(name == "defines_var") {}
330 else if(name == "var_is_introduced") {}
331 else if(name == "output_var" && formula.is(F::E)) {
332 output.add_var(battery::get<0>(formula.exists()));
333 }
334 else if(name == "output_array" && formula.is(F::E)) {
335 auto array_name = std::any_cast<std::string>(sv[2]);
336 auto dims = std::any_cast<SV>(annot[1]);
337 output.add_array_var(array_name, battery::get<0>(formula.exists()), dims);
338 }
339 else {
340 if(!ignored_annotations.contains(name)) {
341 ignored_annotations.insert(name);
342 std::cerr << "% WARNING: Annotation " + name + " is unknown and was ignored." << std::endl;
343 }
344 }
345 }
346 return std::move(formula);
347 }
348
349 F make_binary(Sig sig, const SV &sv) {
350 if(sv.size() != 3) {
351 return make_arity_error(sv, sig, 2, static_cast<int>(sv.size()/*size_t*/) - 1);
352 }
353 return F::make_binary(f(sv[1]), sig, f(sv[2]));
354 }
355
356 F make_unary_fun_eq(Sig sig, const SV &sv, Sig eq_kind = EQ) {
357 if(sv.size() != 3) {
358 return make_arity_error(sv, sig, 1, static_cast<int>(sv.size()) - 2);
359 }
360 auto fun = F::make_unary(sig, f(sv[1]));
361 return F::make_binary(fun, eq_kind, f(sv[2]));
362 }
363
364 F make_unary_fun(Sig sig, const SV &sv) {
365 if(sv.size() != 2) {
366 return make_arity_error(sv, sig, 1, static_cast<int>(sv.size()) - 1);
367 }
368 return F::make_unary(sig, f(sv[1]));
369 }
370
371 F make_binary_fun_eq(Sig sig, const SV &sv, Sig eq_kind = EQ) {
372 if(sv.size() != 4) {
373 return make_arity_error(sv, sig, 2, static_cast<int>(sv.size()) - 2);
374 }
375 auto left = F::make_binary(f(sv[1]), sig, f(sv[2]));
376 auto right = f(sv[3]);
377 if(eq_kind == EQUIV && right.is_true()) {
378 return left;
379 }
380 return F::make_binary(left, eq_kind, right);
381 }
382
383 F make_binary_fun(Sig sig, const SV& sv) {
384 if(sv.size() != 3) {
385 return make_arity_error(sv, sig, 2, static_cast<int>(sv.size()) - 1);
386 }
387 return F::make_binary(f(sv[1]), sig, f(sv[2]));
388 }
389
390 F make_nary_fun(Sig sig, const SV &sv) {
391 FSeq seq;
392 for(int i = 1; i < sv.size(); ++i) {
393 seq.push_back(f(sv[i]));
394 }
395 return F::make_nary(sig, std::move(seq));
396 }
397
398 F make_float_in(const SV &sv) {
399 return F::make_binary(
400 F::make_binary(f(sv[1]), GEQ, f(sv[2])),
401 AND,
402 F::make_binary(f(sv[1]), LEQ, f(sv[3])));
403 }
404
405 F make_log(int base, const SV &sv) {
406 return F::make_binary(f(sv[1]), LOG, F::make_z(base));
407 }
408
409 F make_log_eq(int base, const SV &sv) {
410 return F::make_binary(make_log(base, sv), EQ, f(sv[2]));
411 }
412
413 F predicate_call(const SV &sv) {
414 auto name = std::any_cast<std::string>(sv[0]);
415 if (name == "int_le") { return make_binary(LEQ, sv); }
416 if (name == "int_lt") { return make_binary(LT, sv); }
417 if (name == "int_ge") { return make_binary(GEQ, sv); }
418 if (name == "int_gt") { return make_binary(GT, sv); }
419 if (name == "int_eq") { return make_binary(EQ, sv); }
420 if (name == "int_ne") { return make_binary(NEQ, sv); }
421 if (name == "int_abs") { return make_unary_fun_eq(ABS, sv); }
422 if (name == "int_neg") { return make_unary_fun_eq(NEG, sv); }
423 if (name == "int_div") { return make_binary_fun_eq(TDIV, sv); }
424 if (name == "int_ediv") { return make_binary_fun_eq(EDIV, sv); }
425 if (name == "int_tdiv") { return make_binary_fun_eq(TDIV, sv); }
426 if (name == "int_cdiv") { return make_binary_fun_eq(CDIV, sv); }
427 if (name == "int_fdiv") { return make_binary_fun_eq(FDIV, sv); }
428 if (name == "int_mod") { return make_binary_fun_eq(EMOD, sv); }
429 if (name == "int_plus") { return make_binary_fun_eq(ADD, sv); }
430 if (name == "int_minus") { return make_binary_fun_eq(SUB, sv); }
431 if (name == "int_pow") { return make_binary_fun_eq(POW, sv); }
432 if (name == "int_times") { return make_binary_fun_eq(MUL, sv); }
433 if (name == "int_max") { return make_binary_fun_eq(MAX, sv); }
434 if (name == "int_min") { return make_binary_fun_eq(MIN, sv); }
435 if (name == "int_eq_reif") { return make_binary_fun_eq(EQ, sv, EQUIV); }
436 if (name == "int_le_reif") { return make_binary_fun_eq(LEQ, sv, EQUIV); }
437 if (name == "int_lt_reif") { return make_binary_fun_eq(LT, sv, EQUIV); }
438 if (name == "int_ne_reif") { return make_binary_fun_eq(NEQ, sv, EQUIV); }
439 if (name == "bool2int") { return make_binary(EQ, sv); }
440 if (name == "bool_eq") { return make_binary(EQ, sv); }
441 if (name == "bool_le") { return make_binary(LEQ, sv); }
442 if (name == "bool_lt") { return make_binary(LT, sv); }
443 if (name == "bool_imply") { return make_binary(IMPLY, sv); }
444 if (name == "bool_eq_reif") { return make_binary_fun_eq(EQ, sv, EQUIV); }
445 if (name == "bool_le_reif") { return make_binary_fun_eq(LEQ, sv, EQUIV); }
446 if (name == "bool_lt_reif") { return make_binary_fun_eq(LT, sv, EQUIV); }
447 if (name == "bool_and") { return make_binary_fun_eq(AND, sv, EQUIV); }
448 if (name == "bool_not") {
449 if(sv.size() == 3) { return make_binary(XOR, sv); }
450 else { return make_unary_fun(NOT, sv); }
451 }
452 if (name == "bool_or") { return make_binary_fun_eq(OR, sv, EQUIV); }
453 if (name == "nbool_and") { return make_nary_fun(AND, sv); }
454 if (name == "nbool_or") { return make_nary_fun(OR, sv); }
455 if (name == "nbool_equiv") { return make_nary_fun(EQUIV, sv); }
456 if (name == "bool_xor") {
457 if(sv.size() == 3) { return make_binary(XOR, sv); }
458 else { return make_binary_fun_eq(XOR, sv, EQUIV); }
459 }
460 if (name == "set_card") { return make_unary_fun_eq(CARD, sv); }
461 if (name == "set_diff") { return make_binary_fun_eq(DIFFERENCE, sv); }
462 if (name == "set_eq") { return make_binary(EQ, sv); }
463 if (name == "set_eq_reif") { return make_binary_fun_eq(EQ, sv, EQUIV); }
464 if (name == "set_in") { return make_binary(IN, sv); }
465 if (name == "set_in_reif") { return make_binary_fun_eq(IN, sv, EQUIV); }
466 if (name == "set_intersect") { return make_binary_fun_eq(INTERSECTION, sv, EQUIV); }
467 if (name == "set_union") { return make_binary_fun_eq(UNION, sv, EQUIV); }
468 if (name == "set_ne") { return make_binary(NEQ, sv); }
469 if (name == "set_ne_reif") { return make_binary_fun_eq(NEQ, sv, EQUIV); }
470 if (name == "set_subset") { return make_binary(SUBSETEQ, sv); }
471 if (name == "set_subset_reif") { return make_binary_fun_eq(SUBSETEQ, sv, EQUIV); }
472 if (name == "set_superset") { return make_binary(SUPSETEQ, sv); }
473 if (name == "set_symdiff") { return make_binary_fun_eq(SYMMETRIC_DIFFERENCE, sv, EQUIV); }
474 if (name == "set_le") { return make_binary(LEQ, sv); }
475 if (name == "set_le_reif") { return make_binary_fun_eq(LEQ, sv, EQUIV); }
476 if (name == "set_lt") { return make_binary(LT, sv); }
477 if (name == "set_lt_reif") { return make_binary_fun_eq(LT, sv, EQUIV); }
478 if (name == "float_abs") { return make_binary_fun_eq(ABS, sv); }
479 if (name == "float_neg") { return make_binary_fun_eq(NEG, sv); }
480 if (name == "float_plus") { return make_binary_fun_eq(ADD, sv); }
481 if (name == "float_minus") { return make_binary_fun_eq(SUB, sv); }
482 if (name == "float_times") { return make_binary_fun_eq(MUL, sv); }
483 if (name == "float_acos") { return make_unary_fun_eq(ACOS, sv); }
484 if (name == "float_acosh") { return make_unary_fun_eq(ACOSH, sv); }
485 if (name == "float_asin") { return make_unary_fun_eq(ASIN, sv); }
486 if (name == "float_asinh") { return make_unary_fun_eq(ASINH, sv); }
487 if (name == "float_atan") { return make_unary_fun_eq(ATAN, sv); }
488 if (name == "float_atanh") { return make_unary_fun_eq(ATANH, sv); }
489 if (name == "float_cos") { return make_unary_fun_eq(COS, sv); }
490 if (name == "float_cosh") { return make_unary_fun_eq(COSH, sv); }
491 if (name == "float_sin") { return make_unary_fun_eq(SIN, sv); }
492 if (name == "float_sinh") { return make_unary_fun_eq(SINH, sv); }
493 if (name == "float_tan") { return make_unary_fun_eq(TAN, sv); }
494 if (name == "float_tanh") { return make_unary_fun_eq(TANH, sv); }
495 if (name == "float_div") { return make_binary(DIV, sv); }
496 if (name == "float_eq") { return make_binary(EQ, sv); }
497 if (name == "float_eq_reif") { return make_binary_fun_eq(EQ, sv, EQUIV); }
498 if (name == "float_le") { return make_binary(LEQ, sv); }
499 if (name == "float_le_reif") { return make_binary_fun_eq(LEQ, sv, EQUIV); }
500 if (name == "float_ne") { return make_binary(NEQ, sv); }
501 if (name == "float_ne_reif") { return make_binary_fun_eq(NEQ, sv, EQUIV); }
502 if (name == "float_lt") { return make_binary(LT, sv); }
503 if (name == "float_lt_reif") { return make_binary_fun_eq(LT, sv, EQUIV); }
504 if (name == "float_in") { return make_float_in(sv); }
505 if (name == "float_in_reif") {
506 return F::make_binary(make_float_in(sv), EQUIV, f(sv[4]));
507 }
508 if (name == "float_log10") { return make_log_eq(10, sv); }
509 if (name == "float_log2") { return make_log_eq(2, sv); }
510 if (name == "float_min") { return make_binary_fun_eq(MIN, sv); }
511 if (name == "float_max") { return make_binary_fun_eq(MAX, sv); }
512 if (name == "float_exp") { return make_unary_fun_eq(EXP, sv); }
513 if (name == "float_ln") { return make_unary_fun_eq(LN, sv); }
514 if (name == "float_pow") { return make_binary_fun_eq(POW, sv); }
515 if (name == "float_sqrt") { return make_unary_fun_eq(SQRT, sv); }
516 if (name == "int2float") { return make_binary(EQ, sv); }
517 if (name == "array_int_element" || name == "array_var_int_element"
518 || name == "array_bool_element" || name == "array_var_bool_element"
519 || name == "array_set_element" || name == "array_var_set_element"
520 || name == "array_float_element" || name == "array_var_float_element")
521 {
522 return make_element_constraint(name, sv);
523 }
524 if (name == "int_lin_eq" || name == "bool_lin_eq" || name == "float_lin_eq" ||
525 name == "int_lin_eq_reif" || name == "bool_lin_eq_reif" || name == "float_lin_eq_reif")
526 {
527 return make_linear_constraint(name, EQ, sv);
528 }
529 if (name == "int_lin_le" || name == "bool_lin_le" || name == "float_lin_le" ||
530 name == "int_lin_le_reif" || name == "bool_lin_le_reif" || name == "float_lin_le_reif")
531 {
532 return make_linear_constraint(name, LEQ, sv);
533 }
534 if (name == "int_lin_ne" || name == "bool_lin_ne" || name == "float_lin_ne" ||
535 name == "int_lin_ne_reif" || name == "bool_lin_ne_reif" || name == "float_lin_ne_reif")
536 {
537 return make_linear_constraint(name, NEQ, sv);
538 }
539 if (name == "array_bool_and") { return make_boolean_constraint(name, AND, sv); }
540 if (name == "array_bool_or") { return make_boolean_constraint(name, OR, sv); }
541 if (name == "array_bool_xor") { return make_boolean_constraint(name, XOR, sv); }
542 if (name == "bool_clause" || name == "bool_clause_reif") {
543 return make_boolean_clause(name, sv);
544 }
545 if(name == "turbo_fzn_table_bool" || name == "turbo_fzn_table_int") {
546 return make_table_constraint(name, sv, TableKind::PLAIN);
547 }
548 if(name == "turbo_fzn_short_table_int" || name == "turbo_fzn_short_table_set_of_int") {
549 return make_table_constraint(name, sv, TableKind::SHORT);
550 }
551 if(name == "turbo_fzn_basic_table_int" || name == "turbo_fzn_basic_table_set_of_int") {
552 return make_table_constraint(name, sv, TableKind::BASIC);
553 }
554 if(name == "turbo_fzn_compressed_table_int") {
555 return make_table_constraint(name, sv, TableKind::COMPRESSED);
556 }
557 return make_error(sv, "Unknown predicate `" + name + "`");
558 }
559
560 F function_call(const SV &sv) {
561 auto name = std::any_cast<std::string>(sv[0]);
562 silent = true;
563 bool err = error;
564 error = false;
565 auto p = predicate_call(sv);
566 silent = false;
567 if(!error) {
568 return f(p);
569 }
570 else {
571 error = err;
572 if(name == "int_abs") { return make_unary_fun(ABS, sv); }
573 if (name == "int_neg") { return make_unary_fun(NEG, sv); }
574 if (name == "int_div") { return make_binary_fun(TDIV, sv); }
575 if (name == "int_ediv") { return make_binary_fun(EDIV, sv); }
576 if (name == "int_fdiv") { return make_binary_fun(FDIV, sv); }
577 if (name == "int_cdiv") { return make_binary_fun(CDIV, sv); }
578 if (name == "int_tdiv") { return make_binary_fun(TDIV, sv); }
579 if (name == "int_mod") { return make_binary_fun(EMOD, sv); }
580 if (name == "int_plus") { return make_binary_fun(ADD, sv); }
581 if (name == "int_minus") { return make_binary_fun(SUB, sv); }
582 if (name == "int_pow") { return make_binary_fun(POW, sv); }
583 if (name == "int_times") { return make_binary_fun(MUL, sv); }
584 if (name == "int_max") { return make_binary_fun(MAX, sv); }
585 if (name == "int_min") { return make_binary_fun(MIN, sv); }
586 if (name == "bool_and") { return make_binary_fun(AND, sv); }
587 if (name == "bool_not") { return make_unary_fun(NOT, sv); }
588 if (name == "bool_or") { return make_binary_fun(OR, sv); }
589 if (name == "bool_xor") { return make_binary_fun(XOR, sv); }
590 if (name == "set_card") { return make_unary_fun(CARD, sv); }
591 if (name == "set_diff") { return make_binary_fun(DIFFERENCE, sv); }
592 if (name == "set_intersect") { return make_binary_fun(INTERSECTION, sv); }
593 if (name == "set_union") { return make_binary_fun(UNION, sv); }
594 if (name == "set_symdiff") { return make_binary_fun(SYMMETRIC_DIFFERENCE, sv); }
595 if (name == "float_abs") { return make_binary_fun(ABS, sv); }
596 if (name == "float_neg") { return make_binary_fun(NEG, sv); }
597 if (name == "float_plus") { return make_binary_fun(ADD, sv); }
598 if (name == "float_minus") { return make_binary_fun(SUB, sv); }
599 if (name == "float_times") { return make_binary_fun(MUL, sv); }
600 if (name == "float_acos") { return make_unary_fun(ACOS, sv); }
601 if (name == "float_acosh") { return make_unary_fun(ACOSH, sv); }
602 if (name == "float_asin") { return make_unary_fun(ASIN, sv); }
603 if (name == "float_asinh") { return make_unary_fun(ASINH, sv); }
604 if (name == "float_atan") { return make_unary_fun(ATAN, sv); }
605 if (name == "float_atanh") { return make_unary_fun(ATANH, sv); }
606 if (name == "float_cos") { return make_unary_fun(COS, sv); }
607 if (name == "float_cosh") { return make_unary_fun(COSH, sv); }
608 if (name == "float_sin") { return make_unary_fun(SIN, sv); }
609 if (name == "float_sinh") { return make_unary_fun(SINH, sv); }
610 if (name == "float_tan") { return make_unary_fun(TAN, sv); }
611 if (name == "float_tanh") { return make_unary_fun(TANH, sv); }
612 if (name == "float_div") { return make_binary_fun(DIV, sv); }
613 if (name == "float_log10") { return make_log(10, sv); }
614 if (name == "float_log2") { return make_log(2, sv); }
615 if (name == "float_min") { return make_binary_fun(MIN, sv); }
616 if (name == "float_max") { return make_binary_fun(MAX, sv); }
617 if (name == "float_exp") { return make_unary_fun(EXP, sv); }
618 if (name == "float_ln") { return make_unary_fun(LN, sv); }
619 if (name == "float_pow") { return make_binary_fun(POW, sv); }
620 if (name == "float_sqrt") { return make_unary_fun(SQRT, sv); }
621 return make_error(sv, "Unknown function or predicate symbol `" + name + "`");
622 }
623 }
624
625 F make_statements(const SV& sv) {
626 if(sv.size() == 1) {
627 return f(sv[0]);
628 }
629 else {
630 FSeq children;
631 for(int i = 0; i < sv.size(); ++i) {
632 F formula = f(sv[i]);
633 if(!formula.is_true()) {
634 children.push_back(formula);
635 }
636 }
637 return F::make_nary(AND, std::move(children));
638 }
639 }
640
641 F make_existential(const SV& sv, const So& ty, const std::string& name, const std::any& sv_annots) {
642 auto f = F::make_exists(UNTYPED,
643 LVar<allocator_type>(name.data()),
644 ty);
645 auto annots = std::any_cast<SV>(sv_annots);
646 return update_with_annotations(sv, f, annots);
647 }
648
649 template<class S>
650 std::string make_array_access(const S& name, int i) {
651 return std::string(name.data()) + "[" + std::to_string(i+1) + "]"; // FlatZinc array starts at 1.
652 }
653
654 F make_variable_init_decl(const SV& sv) {
655 auto name = std::any_cast<std::string>(sv[1]);
656 auto var_decl = make_variable_decl(sv, name, sv[0], sv[2]);
657 if(sv.size() == 4) {
658 return F::make_binary(std::move(var_decl), AND,
659 F::make_binary(
660 F::make_lvar(UNTYPED, LVar<allocator_type>(name.data())),
661 EQ,
662 f(sv[3])));
663 }
664 else {
665 return std::move(var_decl);
666 }
667 }
668
669 F make_variable_decl(const SV& sv, const std::string& name, const std::any& typeVar, const std::any& annots) {
670 try {
671 auto ty = std::any_cast<So>(typeVar);
672 return make_existential(sv, ty, name, annots);
673 }
674 catch(std::bad_any_cast) {
675 auto typeValue = f(typeVar);
676 auto inConstraint = F::make_binary(F::make_lvar(UNTYPED, LVar<allocator_type>(name.data())), IN, typeValue);
677 auto sort = typeValue.sort();
678 if(!sort.has_value() || !sort->is_set()) {
679 return make_error(sv, "We only allow type-value of variables to be of type Set.");
680 }
681 auto exists = make_existential(sv, *(sort->sub), name, annots);
682 return F::make_binary(std::move(exists), AND, std::move(inConstraint));
683 }
684 }
685
686 F make_element_constraint(const std::string& name, const SV& sv) {
687 if(sv.size() < 4) {
688 return make_error(sv, "`" + name + "` expects 3 parameters, but we got `" + std::to_string(sv.size()-1) + "` parameters");
689 }
690 auto index = f(sv[1]);
691 auto array = resolve_array(sv, sv[2]);
692 if(!array.is(F::Seq)) {
693 return array;
694 }
695 auto value = f(sv[3]);
696 FSeq seq;
697 for(int i = 0; i < array.seq().size(); ++i) {
698 // index = (i+1) ==> varName = value
699 seq.push_back(F::make_binary(
700 F::make_binary(index, EQ, F::make_z(i+1)),
701 IMPLY,
702 F::make_binary(array.seq(i), EQ, value)));
703 }
704 return F::make_nary(AND, std::move(seq));
705 }
706
707 F resolve_bool(const SV& sv, const std::any& any) {
708 try {
709 auto boolParam = f(any);
710 if(boolParam.is(F::LV)) {
711 std::string paramName(boolParam.lv().data());
712 if(params.contains(paramName)) {
713 boolParam = params[paramName];
714 }
715 else {
716 return make_error(sv, "Undeclared parameter `" + paramName + "`.");
717 }
718 }
719 if(boolParam.is(F::B)) {
720 return boolParam;
721 }
722 else {
723 return make_error(sv, "Expects a Boolean parameter.");
724 }
725 }
726 catch(std::bad_any_cast) {
727 return make_error(sv, "Expects a Boolean parameter.");
728 }
729 }
730
731 // We return the elements inside the array in the form `arr[1] /\ arr[2] /\ ... /\ arr[N]`.
732 // The array can either be a literal array directly, or the name of an array.
733 F resolve_array(const SV& sv, const std::any& any) {
734 FSeq seq;
735 try {
736 auto arrayVar = f(any);
737 if(arrayVar.is(F::LV)) {
738 std::string arrayName(arrayVar.lv().data());
739 if(arrays.contains(arrayName)) {
740 int size = arrays[arrayName];
741 for(int i = 0; i < size; ++i) {
742 auto varName = make_array_access(arrayName, i);
743 if(params.contains(varName)) {
744 seq.push_back(params[varName]);
745 }
746 else {
747 seq.push_back(F::make_lvar(UNTYPED, LVar<allocator_type>(varName.data())));
748 }
749 }
750 }
751 else {
752 return make_error(sv, "Unknown array parameter `" + arrayName + "`");
753 }
754 }
755 else {
756 return make_error(sv, "Expects an array or the name of an array.");
757 }
758 }
759 catch(std::bad_any_cast) {
760 try {
761 auto array = std::any_cast<SV>(any);
762 for(int i = 0; i < array.size(); ++i) {
763 seq.push_back(f(array[i]));
764 }
765 }
766 catch(std::bad_any_cast) {
767 return make_error(sv, "Expects an array of valid elements.");
768 }
769 }
770 return F::make_nary(AND, std::move(seq));
771 }
772
773 F make_linear_constraint(const std::string& name, Sig sig, const SV& sv) {
774 if(sv.size() != 4 && sv.size() != 5) {
775 return make_error(sv, "`" + name + "` expects 3 (or 4 if reified) parameters, but we got `" + std::to_string(sv.size() - 1) + "` parameters");
776 }
777 auto as = resolve_array(sv, sv[1]);
778 if(!as.is(F::Seq)) { return as; }
779 auto bs = resolve_array(sv, sv[2]);
780 if(!bs.is(F::Seq)) { return bs; }
781 auto c = f(sv[3]);
782 if(as.seq().size() != bs.seq().size()) {
783 return make_error(sv, "`" + name + "` expects arrays of the same size.");
784 }
785 FSeq sum;
786 for(int i = 0; i < as.seq().size(); ++i) {
787 sum.push_back(F::make_binary(as.seq(i), MUL, bs.seq(i)));
788 }
789 F linearCons =
790 sum.size() == 1
791 ? F::make_binary(std::move(sum[0]), sig, c)
792 : F::make_binary(F::make_nary(ADD, std::move(sum)), sig, c);
793 if(sv.size() == 5) { // reified version.
794 return F::make_binary(f(sv[4]), EQUIV, std::move(linearCons));
795 }
796 else {
797 return std::move(linearCons);
798 }
799 }
800
801 F make_boolean_constraint(const std::string& name, Sig sig, const SV& sv) {
802 if(sv.size() != 2 && sv.size() != 3) {
803 return make_error(sv, "`" + name + "` expects 1 (or 2 if reified) parameters, but we got `" + std::to_string(sv.size() - 1) + "` parameters");
804 }
805 auto array = resolve_array(sv, sv[1]);
806 if(!array.is(F::Seq)) { return array; }
807 if(sv.size() == 3) { // reified
808 return F::make_binary(f(sv[2]), EQUIV, F::make_nary(sig, array.seq()));
809 }
810 else {
811 return F::make_nary(sig, array.seq());
812 }
813 }
814
815 F make_boolean_clause(const std::string& name, const SV& sv) {
816 if(sv.size() != 3 && sv.size() != 4) {
817 return make_error(sv, "`" + name + "` expects 2 (or 3 if reified) parameters, but we got `" + std::to_string(sv.size() - 1) + "` parameters");
818 }
819 auto as = resolve_array(sv, sv[1]);
820 if(!as.is(F::Seq)) { return as; }
821 auto bs = resolve_array(sv, sv[2]);
822 if(!bs.is(F::Seq)) { return bs; }
823 FSeq negs;
824 for(int i = 0; i < bs.seq().size(); ++i) {
825 negs.push_back(F::make_unary(NOT, bs.seq(i)));
826 }
827 F clause = F::make_binary(F::make_nary(OR, as.seq()), OR, F::make_nary(OR, negs));
828 if(sv.size() == 4) {
829 return F::make_binary(f(sv[3]), EQUIV, std::move(clause));
830 }
831 else {
832 return std::move(clause);
833 }
834 }
835
836 /** Given a cell `f` in the context of a table constraint, and `sort` the type of the variable.
837 * If `f` represents the values taken by an integer variable, then 2147483647 and {} are the wildcards.
838 * If `f` represents the values taken by a set of integer variable, then {2147483647} is the wildcard.
839 */
840 bool is_wildcard(const F& f, So sort) {
841 if(sort.is_int()) {
842 return (f.is(F::Z) && f.z() == 2147483647)
843 || (f.is(F::S) && f.s().size() == 0);
844 }
845 else if(sort.is_set() && f.is(F::S) && f.s().size() == 1) {
846 auto l = battery::get<0>(f.s()[0]);
847 auto u = battery::get<1>(f.s()[0]);
848 return l.is(F::Z) && u.is(F::Z) && l.z() == 2147483647 && u.z() == 2147483647;
849 }
850 return false;
851 }
852
853 So sort_of_table_constraint(const std::string& name) {
854 if(name == "turbo_fzn_table_bool") { return So(So::Bool); }
855 else if(name == "turbo_fzn_table_int") { return So(So::Int); }
856 else if(name == "turbo_fzn_short_table_int") { return So(So::Int); }
857 else if(name == "turbo_fzn_short_table_set_of_int") { return So(So::Set, So(So::Int)); }
858 else if(name == "turbo_fzn_basic_table_int") { return So(So::Int); }
859 else if(name == "turbo_fzn_basic_table_set_of_int") { return So(So::Set, So(So::Int)); }
860 else if(name == "turbo_fzn_compressed_table_int") { return So(So::Int); }
861 else { printf("missing table constraint."); assert(false); return So(So::Bool); }
862 }
863
864 F make_table_constraint(const std::string& name, const SV& sv, TableKind kind) {
865 bool positive = true;
866 int header_idx = 1;
867 int table_idx = 2;
868 if(sv.size() != 3 && (name == "turbo_fzn_table_bool" || name == "turbo_fzn_table_bool")) {
869 return make_error(sv, "`" + name + "` expects 2 parameters, but we got `" + std::to_string(sv.size() - 1) + "` parameters");
870 }
871 else {
872 if(sv.size() != 4) {
873 return make_error(sv, "`" + name + "` expects 3 parameters, but we got `" + std::to_string(sv.size() - 1) + "` parameters");
874 }
875 auto boolParam = resolve_bool(sv, sv[1]);
876 if(!boolParam.is(F::B)) { return boolParam; }
877 positive = boolParam.b();
878 ++header_idx;
879 ++table_idx;
880 }
881 auto header = resolve_array(sv, sv[header_idx]);
882 if(!header.is(F::Seq)) { return header; }
883 auto table = resolve_array(sv, sv[table_idx]);
884 if(!table.is(F::Seq)) { return table; }
885 size_t num_t_cols = (kind == TableKind::BASIC) ? header.seq().size() * 2 : header.seq().size();
886 if(table.seq().size() % num_t_cols != 0) {
887 return make_error(sv, "`" + name + "` expects the number of variables is equal to the number of columns of the table (or twice for basic tables).");
888 }
889 size_t num_cols = header.seq().size();
890 size_t num_rows = table.seq().size() / header.seq().size();
891 So sort = sort_of_table_constraint(name);
892 FSeq disjuncts;
893 for(int i = 0; i < num_rows; ++i) {
894 FSeq conjuncts;
895 for(int z = 0; z < num_cols; ++z) {
896 int j = z * (kind == TableKind::BASIC ? 2 : 1);
897 auto cell = table.seq(i*num_t_cols + j);
898 auto var = header.seq(z);
899 switch(kind) {
900 case TableKind::SHORT: {
901 if(is_wildcard(cell, sort)) { continue; }
902 }
903 case TableKind::PLAIN: { // x[j] == t[i][j]
904 if(!cell.is(F::S) && !cell.is(F::Z) && !cell.is(F::B)) {
905 return make_error(sv, "`" + name + "` expects each cell to be an integer, a set or a Boolean.");
906 }
907 conjuncts.push_back(F::make_binary(var, EQ, cell));
908 break;
909 }
910 case TableKind::COMPRESSED: {
911 if(!cell.is(F::S)) {
912 return make_error(sv, "`" + name + "` expects each cell to be a set.");
913 }
914 if(is_wildcard(cell, sort)) { continue; }
915 conjuncts.push_back(F::make_binary(var, IN, cell));
916 break;
917 }
918 case TableKind::BASIC: {
919 auto l = cell;
920 auto u = table.seq(i*num_t_cols + j + 1);
921 if(!l.is(F::S) && !l.is(F::Z) && !u.is(F::S) && !u.is(F::Z)) {
922 return make_error(sv, "`" + name + "` expects each cell to be an integer or a set.");
923 }
924 if(!is_wildcard(l, sort)) {
925 if(l.is(F::Z)) {
926 conjuncts.push_back(F::make_binary(var, GEQ, l));
927 }
928 else {
929 conjuncts.push_back(F::make_binary(var, SUPSETEQ, l));
930 }
931 }
932 if(!is_wildcard(u, sort)) {
933 if(u.is(F::Z)) {
934 conjuncts.push_back(F::make_binary(var, LEQ, u));
935 }
936 else {
937 conjuncts.push_back(F::make_binary(var, SUBSETEQ, u));
938 }
939 }
940 break;
941 }
942 }
943 }
944 if(conjuncts.size() == 0) {
945 return F::make_true();
946 }
947 else if(conjuncts.size() == 1) {
948 disjuncts.push_back(std::move(conjuncts[0]));
949 }
950 else {
951 disjuncts.push_back(F::make_nary(AND, std::move(conjuncts)));
952 }
953 }
954 if(disjuncts.size() == 0) {
955 return F::make_false();
956 }
957 else if(disjuncts.size() == 1) {
958 return std::move(disjuncts[0]);
959 }
960 else {
961 return F::make_nary(OR, std::move(disjuncts));
962 }
963 }
964
965 F make_solve_item(const SV& sv) {
966 if(sv.size() == 1) {
967 return f(sv[0]);
968 }
969 else {
970 if(f(sv[1]).is_true()) {
971 return f(sv[0]);
972 }
973 else {
974 return F::make_binary(f(sv[0]), AND, f(sv[1]));
975 }
976 }
977 }
978
979 void make_seq_search(const SV& sv, FSeq& seq) {
980 for(int i = 0; i < sv.size(); ++i) {
981 const auto& sub_search = f(sv[i]);
982 if(sub_search.is(F::Seq) && sub_search.sig() == AND) {
983 for(int j = 0; j < sub_search.seq().size(); ++j) {
984 seq.push_back(sub_search.seq(j));
985 }
986 }
987 else {
988 seq.push_back(sub_search);
989 }
990 }
991 }
992
993 F make_seq_search(const SV& sv) {
994 FSeq seq;
995 make_seq_search(sv, seq);
996 return F::make_nary(AND, seq);
997 }
998
999 F make_base_search(const SV& sv) {
1000 FSeq seq;
1001 seq.push_back(F::make_nary(bstring(std::any_cast<std::string>(sv[1]).data()), FSeq{}));
1002 seq.push_back(F::make_nary(bstring(std::any_cast<std::string>(sv[2]).data()), FSeq{}));
1003 auto array = resolve_array(sv, sv[0]);
1004 for(int i = 0; i < array.seq().size(); ++i) {
1005 if(array.seq(i).is_variable()) {
1006 seq.push_back(array.seq(i));
1007 }
1008 }
1009 return F::make_nary("search", seq);
1010 }
1011
1012 F make_search_annotations(const SV& sv) {
1013 if(sv.size() == 1) {
1014 return f(sv[0]);
1015 }
1016 else {
1017 return make_seq_search(sv);
1018 }
1019 }
1020 };
1021}
1022
1023 /** We parse the constraint language FlatZinc as described in the documentation: https://www.minizinc.org/doc-2.4.1/en/fzn-spec.html#specification-of-flatzinc.
1024 * We also extend FlatZinc conservatively for the purposes of our framework:
1025
1026 - Add the type alias `real` (same as `float`).
1027 - Add the predicates `int_ge`, `int_gt` mainly to simplify testing in lala_core.
1028 - Add the functions `int_minus`, `float_minus`, `int_neg`, `float_neg`.
1029 - Add the ability to have `true` and `false` in the `constraint` statement.
1030 - Parameters of predicates are not required to be flat, every constraint comes with a functional flavor, e.g., `int_le(int_plus(a,b), 5)` stands for `a+b <= 5`.
1031 - Several solve items are allowed, which is useful for multi-objectives optimization.
1032 */
1033 template<class Allocator>
1034 battery::shared_ptr<TFormula<Allocator>, Allocator> parse_flatzinc_str(const std::string& input, SolverOutput<Allocator>& output) {
1035 impl::FlatZincParser<Allocator> parser(output);
1036 return parser.parse(input);
1037 }
1038
1039 template<class Allocator>
1040 battery::shared_ptr<TFormula<Allocator>, Allocator> parse_flatzinc(const std::string& filename, SolverOutput<Allocator>& output) {
1041 std::ifstream t(filename);
1042 if(t.is_open()) {
1043 std::string input((std::istreambuf_iterator<char>(t)), std::istreambuf_iterator<char>());
1044 return parse_flatzinc_str<Allocator>(input, output);
1045 }
1046 else {
1047 std::cerr << "File `" << filename << "` does not exists:." << std::endl;
1048 }
1049 return nullptr;
1050 }
1051
1052 template<class Allocator>
1053 battery::shared_ptr<TFormula<Allocator>, Allocator> parse_flatzinc_str(const std::string& input, const Allocator& allocator = Allocator()) {
1054 SolverOutput<Allocator> output(allocator);
1055 return parse_flatzinc_str(input, output);
1056 }
1057
1058 template<class Allocator>
1059 battery::shared_ptr<TFormula<Allocator>, Allocator> parse_flatzinc(const std::string& filename, const Allocator& allocator = Allocator()) {
1060 SolverOutput<Allocator> output(allocator);
1061 return parse_flatzinc(filename, output);
1062 }
1063}
1064
1065#endif
lala::SolverOutput
Definition solver_output.hpp:18
lala::SolverOutput::add_var
void add_var(const bstring &var_name)
Definition solver_output.hpp:96
lala::SolverOutput::add_array_var
void add_array_var(const std::string &name, const bstring &var_name, const peg::SemanticValues &sv)
Definition solver_output.hpp:72
lala
Definition flatzinc_parser.hpp:21
lala::parse_flatzinc
battery::shared_ptr< TFormula< Allocator >, Allocator > parse_flatzinc(const std::string &filename, SolverOutput< Allocator > &output)
Definition flatzinc_parser.hpp:1040
lala::parse_flatzinc_str
battery::shared_ptr< TFormula< Allocator >, Allocator > parse_flatzinc_str(const std::string &input, SolverOutput< Allocator > &output)
Definition flatzinc_parser.hpp:1034
solver_output.hpp