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(EDIV, sv); }
424 if (name == "int_mod") { return make_binary_fun_eq(EMOD, sv); }
425 if (name == "int_plus") { return make_binary_fun_eq(ADD, sv); }
426 if (name == "int_minus") { return make_binary_fun_eq(SUB, sv); }
427 if (name == "int_pow") { return make_binary_fun_eq(POW, sv); }
428 if (name == "int_times") { return make_binary_fun_eq(MUL, sv); }
429 if (name == "int_max") { return make_binary_fun_eq(MAX, sv); }
430 if (name == "int_min") { return make_binary_fun_eq(MIN, sv); }
431 if (name == "int_eq_reif") { return make_binary_fun_eq(EQ, sv, EQUIV); }
432 if (name == "int_le_reif") { return make_binary_fun_eq(LEQ, sv, EQUIV); }
433 if (name == "int_lt_reif") { return make_binary_fun_eq(LT, sv, EQUIV); }
434 if (name == "int_ne_reif") { return make_binary_fun_eq(NEQ, sv, EQUIV); }
435 if (name == "bool2int") { return make_binary(EQ, sv); }
436 if (name == "bool_eq") { return make_binary(EQ, sv); }
437 if (name == "bool_le") { return make_binary(LEQ, sv); }
438 if (name == "bool_lt") { return make_binary(LT, sv); }
439 if (name == "bool_eq_reif") { return make_binary_fun_eq(EQ, sv, EQUIV); }
440 if (name == "bool_le_reif") { return make_binary_fun_eq(LEQ, sv, EQUIV); }
441 if (name == "bool_lt_reif") { return make_binary_fun_eq(LT, sv, EQUIV); }
442 if (name == "bool_and") { return make_binary_fun_eq(AND, sv, EQUIV); }
443 if (name == "bool_not") {
444 if(sv.size() == 3) { return make_binary(XOR, sv); }
445 else { return make_unary_fun(NOT, sv); }
446 }
447 if (name == "bool_or") { return make_binary_fun_eq(OR, sv, EQUIV); }
448 if (name == "nbool_and") { return make_nary_fun(AND, sv); }
449 if (name == "nbool_or") { return make_nary_fun(OR, sv); }
450 if (name == "nbool_equiv") { return make_nary_fun(EQUIV, sv); }
451 if (name == "bool_xor") {
452 if(sv.size() == 3) { return make_binary(XOR, sv); }
453 else { return make_binary_fun_eq(XOR, sv, EQUIV); }
454 }
455 if (name == "set_card") { return make_unary_fun_eq(CARD, sv); }
456 if (name == "set_diff") { return make_binary_fun_eq(DIFFERENCE, sv); }
457 if (name == "set_eq") { return make_binary(EQ, sv); }
458 if (name == "set_eq_reif") { return make_binary_fun_eq(EQ, sv, EQUIV); }
459 if (name == "set_in") { return make_binary(IN, sv); }
460 if (name == "set_in_reif") { return make_binary_fun_eq(IN, sv, EQUIV); }
461 if (name == "set_intersect") { return make_binary_fun_eq(INTERSECTION, sv, EQUIV); }
462 if (name == "set_union") { return make_binary_fun_eq(UNION, sv, EQUIV); }
463 if (name == "set_ne") { return make_binary(NEQ, sv); }
464 if (name == "set_ne_reif") { return make_binary_fun_eq(NEQ, sv, EQUIV); }
465 if (name == "set_subset") { return make_binary(SUBSETEQ, sv); }
466 if (name == "set_subset_reif") { return make_binary_fun_eq(SUBSETEQ, sv, EQUIV); }
467 if (name == "set_superset") { return make_binary(SUPSETEQ, sv); }
468 if (name == "set_symdiff") { return make_binary_fun_eq(SYMMETRIC_DIFFERENCE, sv, EQUIV); }
469 if (name == "set_le") { return make_binary(LEQ, sv); }
470 if (name == "set_le_reif") { return make_binary_fun_eq(LEQ, sv, EQUIV); }
471 if (name == "set_lt") { return make_binary(LT, sv); }
472 if (name == "set_lt_reif") { return make_binary_fun_eq(LT, sv, EQUIV); }
473 if (name == "float_abs") { return make_binary_fun_eq(ABS, sv); }
474 if (name == "float_neg") { return make_binary_fun_eq(NEG, sv); }
475 if (name == "float_plus") { return make_binary_fun_eq(ADD, sv); }
476 if (name == "float_minus") { return make_binary_fun_eq(SUB, sv); }
477 if (name == "float_times") { return make_binary_fun_eq(MUL, sv); }
478 if (name == "float_acos") { return make_unary_fun_eq(ACOS, sv); }
479 if (name == "float_acosh") { return make_unary_fun_eq(ACOSH, sv); }
480 if (name == "float_asin") { return make_unary_fun_eq(ASIN, sv); }
481 if (name == "float_asinh") { return make_unary_fun_eq(ASINH, sv); }
482 if (name == "float_atan") { return make_unary_fun_eq(ATAN, sv); }
483 if (name == "float_atanh") { return make_unary_fun_eq(ATANH, sv); }
484 if (name == "float_cos") { return make_unary_fun_eq(COS, sv); }
485 if (name == "float_cosh") { return make_unary_fun_eq(COSH, sv); }
486 if (name == "float_sin") { return make_unary_fun_eq(SIN, sv); }
487 if (name == "float_sinh") { return make_unary_fun_eq(SINH, sv); }
488 if (name == "float_tan") { return make_unary_fun_eq(TAN, sv); }
489 if (name == "float_tanh") { return make_unary_fun_eq(TANH, sv); }
490 if (name == "float_div") { return make_binary(DIV, sv); }
491 if (name == "float_eq") { return make_binary(EQ, sv); }
492 if (name == "float_eq_reif") { return make_binary_fun_eq(EQ, sv, EQUIV); }
493 if (name == "float_le") { return make_binary(LEQ, sv); }
494 if (name == "float_le_reif") { return make_binary_fun_eq(LEQ, sv, EQUIV); }
495 if (name == "float_ne") { return make_binary(NEQ, sv); }
496 if (name == "float_ne_reif") { return make_binary_fun_eq(NEQ, sv, EQUIV); }
497 if (name == "float_lt") { return make_binary(LT, sv); }
498 if (name == "float_lt_reif") { return make_binary_fun_eq(LT, sv, EQUIV); }
499 if (name == "float_in") { return make_float_in(sv); }
500 if (name == "float_in_reif") {
501 return F::make_binary(make_float_in(sv), EQUIV, f(sv[4]));
502 }
503 if (name == "float_log10") { return make_log_eq(10, sv); }
504 if (name == "float_log2") { return make_log_eq(2, sv); }
505 if (name == "float_min") { return make_binary_fun_eq(MIN, sv); }
506 if (name == "float_max") { return make_binary_fun_eq(MAX, sv); }
507 if (name == "float_exp") { return make_unary_fun_eq(EXP, sv); }
508 if (name == "float_ln") { return make_unary_fun_eq(LN, sv); }
509 if (name == "float_pow") { return make_binary_fun_eq(POW, sv); }
510 if (name == "float_sqrt") { return make_unary_fun_eq(SQRT, sv); }
511 if (name == "int2float") { return make_binary(EQ, sv); }
512 if (name == "array_int_element" || name == "array_var_int_element"
513 || name == "array_bool_element" || name == "array_var_bool_element"
514 || name == "array_set_element" || name == "array_var_set_element"
515 || name == "array_float_element" || name == "array_var_float_element")
516 {
517 return make_element_constraint(name, sv);
518 }
519 if (name == "int_lin_eq" || name == "bool_lin_eq" || name == "float_lin_eq" ||
520 name == "int_lin_eq_reif" || name == "bool_lin_eq_reif" || name == "float_lin_eq_reif")
521 {
522 return make_linear_constraint(name, EQ, sv);
523 }
524 if (name == "int_lin_le" || name == "bool_lin_le" || name == "float_lin_le" ||
525 name == "int_lin_le_reif" || name == "bool_lin_le_reif" || name == "float_lin_le_reif")
526 {
527 return make_linear_constraint(name, LEQ, sv);
528 }
529 if (name == "int_lin_ne" || name == "bool_lin_ne" || name == "float_lin_ne" ||
530 name == "int_lin_ne_reif" || name == "bool_lin_ne_reif" || name == "float_lin_ne_reif")
531 {
532 return make_linear_constraint(name, NEQ, sv);
533 }
534 if (name == "array_bool_and") { return make_boolean_constraint(name, AND, sv); }
535 if (name == "array_bool_or") { return make_boolean_constraint(name, OR, sv); }
536 if (name == "array_bool_xor") { return make_boolean_constraint(name, XOR, sv); }
537 if (name == "bool_clause" || name == "bool_clause_reif") {
538 return make_boolean_clause(name, sv);
539 }
540 if(name == "turbo_fzn_table_bool" || name == "turbo_fzn_table_int") {
541 return make_table_constraint(name, sv, TableKind::PLAIN);
542 }
543 if(name == "turbo_fzn_short_table_int" || name == "turbo_fzn_short_table_set_of_int") {
544 return make_table_constraint(name, sv, TableKind::SHORT);
545 }
546 if(name == "turbo_fzn_basic_table_int" || name == "turbo_fzn_basic_table_set_of_int") {
547 return make_table_constraint(name, sv, TableKind::BASIC);
548 }
549 if(name == "turbo_fzn_compressed_table_int") {
550 return make_table_constraint(name, sv, TableKind::COMPRESSED);
551 }
552 return make_error(sv, "Unknown predicate `" + name + "`");
553 }
554
555 F function_call(const SV &sv) {
556 auto name = std::any_cast<std::string>(sv[0]);
557 silent = true;
558 bool err = error;
559 error = false;
560 auto p = predicate_call(sv);
561 silent = false;
562 if(!error) {
563 return f(p);
564 }
565 else {
566 error = err;
567 if(name == "int_abs") { return make_unary_fun(ABS, sv); }
568 if (name == "int_neg") { return make_unary_fun(NEG, sv); }
569 if (name == "int_div") { return make_binary_fun(EDIV, sv); }
570 if (name == "int_mod") { return make_binary_fun(EMOD, sv); }
571 if (name == "int_plus") { return make_binary_fun(ADD, sv); }
572 if (name == "int_minus") { return make_binary_fun(SUB, sv); }
573 if (name == "int_pow") { return make_binary_fun(POW, sv); }
574 if (name == "int_times") { return make_binary_fun(MUL, sv); }
575 if (name == "int_max") { return make_binary_fun(MAX, sv); }
576 if (name == "int_min") { return make_binary_fun(MIN, sv); }
577 if (name == "bool_and") { return make_binary_fun(AND, sv); }
578 if (name == "bool_not") { return make_unary_fun(NOT, sv); }
579 if (name == "bool_or") { return make_binary_fun(OR, sv); }
580 if (name == "bool_xor") { return make_binary_fun(XOR, sv); }
581 if (name == "set_card") { return make_unary_fun(CARD, sv); }
582 if (name == "set_diff") { return make_binary_fun(DIFFERENCE, sv); }
583 if (name == "set_intersect") { return make_binary_fun(INTERSECTION, sv); }
584 if (name == "set_union") { return make_binary_fun(UNION, sv); }
585 if (name == "set_symdiff") { return make_binary_fun(SYMMETRIC_DIFFERENCE, sv); }
586 if (name == "float_abs") { return make_binary_fun(ABS, sv); }
587 if (name == "float_neg") { return make_binary_fun(NEG, sv); }
588 if (name == "float_plus") { return make_binary_fun(ADD, sv); }
589 if (name == "float_minus") { return make_binary_fun(SUB, sv); }
590 if (name == "float_times") { return make_binary_fun(MUL, sv); }
591 if (name == "float_acos") { return make_unary_fun(ACOS, sv); }
592 if (name == "float_acosh") { return make_unary_fun(ACOSH, sv); }
593 if (name == "float_asin") { return make_unary_fun(ASIN, sv); }
594 if (name == "float_asinh") { return make_unary_fun(ASINH, sv); }
595 if (name == "float_atan") { return make_unary_fun(ATAN, sv); }
596 if (name == "float_atanh") { return make_unary_fun(ATANH, sv); }
597 if (name == "float_cos") { return make_unary_fun(COS, sv); }
598 if (name == "float_cosh") { return make_unary_fun(COSH, sv); }
599 if (name == "float_sin") { return make_unary_fun(SIN, sv); }
600 if (name == "float_sinh") { return make_unary_fun(SINH, sv); }
601 if (name == "float_tan") { return make_unary_fun(TAN, sv); }
602 if (name == "float_tanh") { return make_unary_fun(TANH, sv); }
603 if (name == "float_div") { return make_binary_fun(DIV, sv); }
604 if (name == "float_log10") { return make_log(10, sv); }
605 if (name == "float_log2") { return make_log(2, sv); }
606 if (name == "float_min") { return make_binary_fun(MIN, sv); }
607 if (name == "float_max") { return make_binary_fun(MAX, sv); }
608 if (name == "float_exp") { return make_unary_fun(EXP, sv); }
609 if (name == "float_ln") { return make_unary_fun(LN, sv); }
610 if (name == "float_pow") { return make_binary_fun(POW, sv); }
611 if (name == "float_sqrt") { return make_unary_fun(SQRT, sv); }
612 return make_error(sv, "Unknown function or predicate symbol `" + name + "`");
613 }
614 }
615
616 F make_statements(const SV& sv) {
617 if(sv.size() == 1) {
618 return f(sv[0]);
619 }
620 else {
621 FSeq children;
622 for(int i = 0; i < sv.size(); ++i) {
623 F formula = f(sv[i]);
624 if(!formula.is_true()) {
625 children.push_back(formula);
626 }
627 }
628 return F::make_nary(AND, std::move(children));
629 }
630 }
631
632 F make_existential(const SV& sv, const So& ty, const std::string& name, const std::any& sv_annots) {
633 auto f = F::make_exists(UNTYPED,
634 LVar<allocator_type>(name.data()),
635 ty);
636 auto annots = std::any_cast<SV>(sv_annots);
637 return update_with_annotations(sv, f, annots);
638 }
639
640 template<class S>
641 std::string make_array_access(const S& name, int i) {
642 return std::string(name.data()) + "[" + std::to_string(i+1) + "]"; // FlatZinc array starts at 1.
643 }
644
645 F make_variable_init_decl(const SV& sv) {
646 auto name = std::any_cast<std::string>(sv[1]);
647 auto var_decl = make_variable_decl(sv, name, sv[0], sv[2]);
648 if(sv.size() == 4) {
649 return F::make_binary(std::move(var_decl), AND,
650 F::make_binary(
651 F::make_lvar(UNTYPED, LVar<allocator_type>(name.data())),
652 EQ,
653 f(sv[3])));
654 }
655 else {
656 return std::move(var_decl);
657 }
658 }
659
660 F make_variable_decl(const SV& sv, const std::string& name, const std::any& typeVar, const std::any& annots) {
661 try {
662 auto ty = std::any_cast<So>(typeVar);
663 return make_existential(sv, ty, name, annots);
664 }
665 catch(std::bad_any_cast) {
666 auto typeValue = f(typeVar);
667 auto inConstraint = F::make_binary(F::make_lvar(UNTYPED, LVar<allocator_type>(name.data())), IN, typeValue);
668 auto sort = typeValue.sort();
669 if(!sort.has_value() || !sort->is_set()) {
670 return make_error(sv, "We only allow type-value of variables to be of type Set.");
671 }
672 auto exists = make_existential(sv, *(sort->sub), name, annots);
673 return F::make_binary(std::move(exists), AND, std::move(inConstraint));
674 }
675 }
676
677 F make_element_constraint(const std::string& name, const SV& sv) {
678 if(sv.size() < 4) {
679 return make_error(sv, "`" + name + "` expects 3 parameters, but we got `" + std::to_string(sv.size()-1) + "` parameters");
680 }
681 auto index = f(sv[1]);
682 auto array = resolve_array(sv, sv[2]);
683 if(!array.is(F::Seq)) {
684 return array;
685 }
686 auto value = f(sv[3]);
687 FSeq seq;
688 for(int i = 0; i < array.seq().size(); ++i) {
689 // index = (i+1) ==> varName = value
690 seq.push_back(F::make_binary(
691 F::make_binary(index, EQ, F::make_z(i+1)),
692 IMPLY,
693 F::make_binary(array.seq(i), EQ, value)));
694 }
695 return F::make_nary(AND, std::move(seq));
696 }
697
698 F resolve_bool(const SV& sv, const std::any& any) {
699 try {
700 auto boolParam = f(any);
701 if(boolParam.is(F::LV)) {
702 std::string paramName(boolParam.lv().data());
703 if(params.contains(paramName)) {
704 boolParam = params[paramName];
705 }
706 else {
707 return make_error(sv, "Undeclared parameter `" + paramName + "`.");
708 }
709 }
710 if(boolParam.is(F::B)) {
711 return boolParam;
712 }
713 else {
714 return make_error(sv, "Expects a Boolean parameter.");
715 }
716 }
717 catch(std::bad_any_cast) {
718 return make_error(sv, "Expects a Boolean parameter.");
719 }
720 }
721
722 // We return the elements inside the array in the form `arr[1] /\ arr[2] /\ ... /\ arr[N]`.
723 // The array can either be a literal array directly, or the name of an array.
724 F resolve_array(const SV& sv, const std::any& any) {
725 FSeq seq;
726 try {
727 auto arrayVar = f(any);
728 if(arrayVar.is(F::LV)) {
729 std::string arrayName(arrayVar.lv().data());
730 if(arrays.contains(arrayName)) {
731 int size = arrays[arrayName];
732 for(int i = 0; i < size; ++i) {
733 auto varName = make_array_access(arrayName, i);
734 if(params.contains(varName)) {
735 seq.push_back(params[varName]);
736 }
737 else {
738 seq.push_back(F::make_lvar(UNTYPED, LVar<allocator_type>(varName.data())));
739 }
740 }
741 }
742 else {
743 return make_error(sv, "Unknown array parameter `" + arrayName + "`");
744 }
745 }
746 else {
747 return make_error(sv, "Expects an array or the name of an array.");
748 }
749 }
750 catch(std::bad_any_cast) {
751 try {
752 auto array = std::any_cast<SV>(any);
753 for(int i = 0; i < array.size(); ++i) {
754 seq.push_back(f(array[i]));
755 }
756 }
757 catch(std::bad_any_cast) {
758 return make_error(sv, "Expects an array of valid elements.");
759 }
760 }
761 return F::make_nary(AND, std::move(seq));
762 }
763
764 F make_linear_constraint(const std::string& name, Sig sig, const SV& sv) {
765 if(sv.size() != 4 && sv.size() != 5) {
766 return make_error(sv, "`" + name + "` expects 3 (or 4 if reified) parameters, but we got `" + std::to_string(sv.size() - 1) + "` parameters");
767 }
768 auto as = resolve_array(sv, sv[1]);
769 if(!as.is(F::Seq)) { return as; }
770 auto bs = resolve_array(sv, sv[2]);
771 if(!bs.is(F::Seq)) { return bs; }
772 auto c = f(sv[3]);
773 if(as.seq().size() != bs.seq().size()) {
774 return make_error(sv, "`" + name + "` expects arrays of the same size.");
775 }
776 FSeq sum;
777 for(int i = 0; i < as.seq().size(); ++i) {
778 sum.push_back(F::make_binary(as.seq(i), MUL, bs.seq(i)));
779 }
780 F linearCons =
781 sum.size() == 1
782 ? F::make_binary(std::move(sum[0]), sig, c)
783 : F::make_binary(F::make_nary(ADD, std::move(sum)), sig, c);
784 if(sv.size() == 5) { // reified version.
785 return F::make_binary(f(sv[4]), EQUIV, std::move(linearCons));
786 }
787 else {
788 return std::move(linearCons);
789 }
790 }
791
792 F make_boolean_constraint(const std::string& name, Sig sig, const SV& sv) {
793 if(sv.size() != 2 && sv.size() != 3) {
794 return make_error(sv, "`" + name + "` expects 1 (or 2 if reified) parameters, but we got `" + std::to_string(sv.size() - 1) + "` parameters");
795 }
796 auto array = resolve_array(sv, sv[1]);
797 if(!array.is(F::Seq)) { return array; }
798 if(sv.size() == 3) { // reified
799 return F::make_binary(f(sv[2]), EQUIV, F::make_nary(sig, array.seq()));
800 }
801 else {
802 return F::make_nary(sig, array.seq());
803 }
804 }
805
806 F make_boolean_clause(const std::string& name, const SV& sv) {
807 if(sv.size() != 3 && sv.size() != 4) {
808 return make_error(sv, "`" + name + "` expects 2 (or 3 if reified) parameters, but we got `" + std::to_string(sv.size() - 1) + "` parameters");
809 }
810 auto as = resolve_array(sv, sv[1]);
811 if(!as.is(F::Seq)) { return as; }
812 auto bs = resolve_array(sv, sv[2]);
813 if(!bs.is(F::Seq)) { return bs; }
814 FSeq negs;
815 for(int i = 0; i < bs.seq().size(); ++i) {
816 negs.push_back(F::make_unary(NOT, bs.seq(i)));
817 }
818 F clause = F::make_binary(F::make_nary(OR, as.seq()), OR, F::make_nary(OR, negs));
819 if(sv.size() == 4) {
820 return F::make_binary(f(sv[3]), EQUIV, std::move(clause));
821 }
822 else {
823 return std::move(clause);
824 }
825 }
826
827 /** Given a cell `f` in the context of a table constraint, and `sort` the type of the variable.
828 * If `f` represents the values taken by an integer variable, then 2147483647 and {} are the wildcards.
829 * If `f` represents the values taken by a set of integer variable, then {2147483647} is the wildcard.
830 */
831 bool is_wildcard(const F& f, So sort) {
832 if(sort.is_int()) {
833 return (f.is(F::Z) && f.z() == 2147483647)
834 || (f.is(F::S) && f.s().size() == 0);
835 }
836 else if(sort.is_set() && f.is(F::S) && f.s().size() == 1) {
837 auto l = battery::get<0>(f.s()[0]);
838 auto u = battery::get<1>(f.s()[0]);
839 return l.is(F::Z) && u.is(F::Z) && l.z() == 2147483647 && u.z() == 2147483647;
840 }
841 return false;
842 }
843
844 So sort_of_table_constraint(const std::string& name) {
845 if(name == "turbo_fzn_table_bool") { return So(So::Bool); }
846 else if(name == "turbo_fzn_table_int") { return So(So::Int); }
847 else if(name == "turbo_fzn_short_table_int") { return So(So::Int); }
848 else if(name == "turbo_fzn_short_table_set_of_int") { return So(So::Set, So(So::Int)); }
849 else if(name == "turbo_fzn_basic_table_int") { return So(So::Int); }
850 else if(name == "turbo_fzn_basic_table_set_of_int") { return So(So::Set, So(So::Int)); }
851 else if(name == "turbo_fzn_compressed_table_int") { return So(So::Int); }
852 else { printf("missing table constraint."); assert(false); return So(So::Bool); }
853 }
854
855 F make_table_constraint(const std::string& name, const SV& sv, TableKind kind) {
856 bool positive = true;
857 int header_idx = 1;
858 int table_idx = 2;
859 if(sv.size() != 3 && (name == "turbo_fzn_table_bool" || name == "turbo_fzn_table_bool")) {
860 return make_error(sv, "`" + name + "` expects 2 parameters, but we got `" + std::to_string(sv.size() - 1) + "` parameters");
861 }
862 else {
863 if(sv.size() != 4) {
864 return make_error(sv, "`" + name + "` expects 3 parameters, but we got `" + std::to_string(sv.size() - 1) + "` parameters");
865 }
866 auto boolParam = resolve_bool(sv, sv[1]);
867 if(!boolParam.is(F::B)) { return boolParam; }
868 positive = boolParam.b();
869 ++header_idx;
870 ++table_idx;
871 }
872 auto header = resolve_array(sv, sv[header_idx]);
873 if(!header.is(F::Seq)) { return header; }
874 auto table = resolve_array(sv, sv[table_idx]);
875 if(!table.is(F::Seq)) { return table; }
876 size_t num_t_cols = (kind == TableKind::BASIC) ? header.seq().size() * 2 : header.seq().size();
877 if(table.seq().size() % num_t_cols != 0) {
878 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).");
879 }
880 size_t num_cols = header.seq().size();
881 size_t num_rows = table.seq().size() / header.seq().size();
882 So sort = sort_of_table_constraint(name);
883 FSeq disjuncts;
884 for(int i = 0; i < num_rows; ++i) {
885 FSeq conjuncts;
886 for(int z = 0; z < num_cols; ++z) {
887 int j = z * (kind == TableKind::BASIC ? 2 : 1);
888 auto cell = table.seq(i*num_t_cols + j);
889 auto var = header.seq(z);
890 switch(kind) {
891 case TableKind::SHORT: {
892 if(is_wildcard(cell, sort)) { continue; }
893 }
894 case TableKind::PLAIN: { // x[j] == t[i][j]
895 if(!cell.is(F::S) && !cell.is(F::Z) && !cell.is(F::B)) {
896 return make_error(sv, "`" + name + "` expects each cell to be an integer, a set or a Boolean.");
897 }
898 conjuncts.push_back(F::make_binary(var, EQ, cell));
899 break;
900 }
901 case TableKind::COMPRESSED: {
902 if(!cell.is(F::S)) {
903 return make_error(sv, "`" + name + "` expects each cell to be a set.");
904 }
905 if(is_wildcard(cell, sort)) { continue; }
906 conjuncts.push_back(F::make_binary(var, IN, cell));
907 break;
908 }
909 case TableKind::BASIC: {
910 auto l = cell;
911 auto u = table.seq(i*num_t_cols + j + 1);
912 if(!l.is(F::S) && !l.is(F::Z) && !u.is(F::S) && !u.is(F::Z)) {
913 return make_error(sv, "`" + name + "` expects each cell to be an integer or a set.");
914 }
915 if(!is_wildcard(l, sort)) {
916 if(l.is(F::Z)) {
917 conjuncts.push_back(F::make_binary(var, GEQ, l));
918 }
919 else {
920 conjuncts.push_back(F::make_binary(var, SUPSETEQ, l));
921 }
922 }
923 if(!is_wildcard(u, sort)) {
924 if(u.is(F::Z)) {
925 conjuncts.push_back(F::make_binary(var, LEQ, u));
926 }
927 else {
928 conjuncts.push_back(F::make_binary(var, SUBSETEQ, u));
929 }
930 }
931 break;
932 }
933 }
934 }
935 if(conjuncts.size() == 0) {
936 return F::make_true();
937 }
938 else if(conjuncts.size() == 1) {
939 disjuncts.push_back(std::move(conjuncts[0]));
940 }
941 else {
942 disjuncts.push_back(F::make_nary(AND, std::move(conjuncts)));
943 }
944 }
945 if(disjuncts.size() == 0) {
946 return F::make_false();
947 }
948 else if(disjuncts.size() == 1) {
949 return std::move(disjuncts[0]);
950 }
951 else {
952 return F::make_nary(OR, std::move(disjuncts));
953 }
954 }
955
956 F make_solve_item(const SV& sv) {
957 if(sv.size() == 1) {
958 return f(sv[0]);
959 }
960 else {
961 if(f(sv[1]).is_true()) {
962 return f(sv[0]);
963 }
964 else {
965 return F::make_binary(f(sv[0]), AND, f(sv[1]));
966 }
967 }
968 }
969
970 void make_seq_search(const SV& sv, FSeq& seq) {
971 for(int i = 0; i < sv.size(); ++i) {
972 const auto& sub_search = f(sv[i]);
973 if(sub_search.is(F::Seq) && sub_search.sig() == AND) {
974 for(int j = 0; j < sub_search.seq().size(); ++j) {
975 seq.push_back(sub_search.seq(j));
976 }
977 }
978 else {
979 seq.push_back(sub_search);
980 }
981 }
982 }
983
984 F make_seq_search(const SV& sv) {
985 FSeq seq;
986 make_seq_search(sv, seq);
987 return F::make_nary(AND, seq);
988 }
989
990 F make_base_search(const SV& sv) {
991 FSeq seq;
992 seq.push_back(F::make_nary(bstring(std::any_cast<std::string>(sv[1]).data()), FSeq{}));
993 seq.push_back(F::make_nary(bstring(std::any_cast<std::string>(sv[2]).data()), FSeq{}));
994 auto array = resolve_array(sv, sv[0]);
995 for(int i = 0; i < array.seq().size(); ++i) {
996 if(array.seq(i).is_variable()) {
997 seq.push_back(array.seq(i));
998 }
999 }
1000 return F::make_nary("search", seq);
1001 }
1002
1003 F make_search_annotations(const SV& sv) {
1004 if(sv.size() == 1) {
1005 return f(sv[0]);
1006 }
1007 else {
1008 return make_seq_search(sv);
1009 }
1010 }
1011 };
1012}
1013
1014 /** 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.
1015 * We also extend FlatZinc conservatively for the purposes of our framework:
1016
1017 - Add the type alias `real` (same as `float`).
1018 - Add the predicates `int_ge`, `int_gt` mainly to simplify testing in lala_core.
1019 - Add the functions `int_minus`, `float_minus`, `int_neg`, `float_neg`.
1020 - Add the ability to have `true` and `false` in the `constraint` statement.
1021 - 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`.
1022 - Several solve items are allowed, which is useful for multi-objectives optimization.
1023 */
1024 template<class Allocator>
1025 battery::shared_ptr<TFormula<Allocator>, Allocator> parse_flatzinc_str(const std::string& input, SolverOutput<Allocator>& output) {
1026 impl::FlatZincParser<Allocator> parser(output);
1027 return parser.parse(input);
1028 }
1029
1030 template<class Allocator>
1031 battery::shared_ptr<TFormula<Allocator>, Allocator> parse_flatzinc(const std::string& filename, SolverOutput<Allocator>& output) {
1032 std::ifstream t(filename);
1033 if(t.is_open()) {
1034 std::string input((std::istreambuf_iterator<char>(t)), std::istreambuf_iterator<char>());
1035 return parse_flatzinc_str<Allocator>(input, output);
1036 }
1037 else {
1038 std::cerr << "File `" << filename << "` does not exists:." << std::endl;
1039 }
1040 return nullptr;
1041 }
1042
1043 template<class Allocator>
1044 battery::shared_ptr<TFormula<Allocator>, Allocator> parse_flatzinc_str(const std::string& input, const Allocator& allocator = Allocator()) {
1045 SolverOutput<Allocator> output(allocator);
1046 return parse_flatzinc_str(input, output);
1047 }
1048
1049 template<class Allocator>
1050 battery::shared_ptr<TFormula<Allocator>, Allocator> parse_flatzinc(const std::string& filename, const Allocator& allocator = Allocator()) {
1051 SolverOutput<Allocator> output(allocator);
1052 return parse_flatzinc(filename, output);
1053 }
1054}
1055
1056#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:1031
lala::parse_flatzinc_str
battery::shared_ptr< TFormula< Allocator >, Allocator > parse_flatzinc_str(const std::string &input, SolverOutput< Allocator > &output)
Definition flatzinc_parser.hpp:1025
solver_output.hpp