1 // {{{ MIT License
2
3 // Copyright 2017 Roland Kaminski
4
5 // Permission is hereby granted, free of charge, to any person obtaining a copy
6 // of this software and associated documentation files (the "Software"), to
7 // deal in the Software without restriction, including without limitation the
8 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
9 // sell copies of the Software, and to permit persons to whom the Software is
10 // furnished to do so, subject to the following conditions:
11
12 // The above copyright notice and this permission notice shall be included in
13 // all copies or substantial portions of the Software.
14
15 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
20 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
21 // IN THE SOFTWARE.
22
23 // }}}
24
25 #include <clingo/astv2.hh>
26
27 namespace Gringo { namespace Input {
28
29 namespace {
30
31 template <class T>
get(AST & ast,clingo_ast_attribute_e name)32 T &get(AST &ast, clingo_ast_attribute_e name) {
33 return mpark::get<T>(ast.value(name));
34 }
35
36 template <class T>
get(AST const & ast,clingo_ast_attribute_e name)37 T const &get(AST const &ast, clingo_ast_attribute_e name) {
38 return mpark::get<T>(ast.value(name));
39 }
40
getOpt(AST const & ast,clingo_ast_attribute_e name)41 AST *getOpt(AST const &ast, clingo_ast_attribute_e name) {
42 if (!ast.hasValue(name)) {
43 return nullptr;
44 }
45 return mpark::get<OAST>(ast.value(name)).ast.get();
46 }
47
48 struct ASTParser {
49 public:
ASTParserGringo::Input::__anon36f400340111::ASTParser50 ASTParser(Logger &log, INongroundProgramBuilder &prg)
51 : log_(log), prg_(prg) { }
52
53 // {{{1 statement
54
parseStatementGringo::Input::__anon36f400340111::ASTParser55 void parseStatement(AST const &ast) {
56 switch (ast.type()) {
57 case clingo_ast_type_rule: {
58 return prg_.rule(get<Location>(ast, clingo_ast_attribute_location),
59 parseHeadLiteral(*get<SAST>(ast, clingo_ast_attribute_head)),
60 parseBodyLiteralVec(get<AST::ASTVec>(ast, clingo_ast_attribute_body)));
61 }
62 case clingo_ast_type_definition: {
63 return prg_.define(get<Location>(ast, clingo_ast_attribute_location),
64 get<String>(ast, clingo_ast_attribute_name), parseTerm(*get<SAST>(ast, clingo_ast_attribute_value)),
65 get<int>(ast, clingo_ast_attribute_is_default) != 0, log_);
66 }
67 case clingo_ast_type_show_signature: {
68 return prg_.showsig(get<Location>(ast, clingo_ast_attribute_location),
69 Sig(get<String>(ast, clingo_ast_attribute_name),
70 get<int>(ast, clingo_ast_attribute_arity),
71 get<int>(ast, clingo_ast_attribute_positive) == 0),
72 ast.hasValue(clingo_ast_attribute_csp) && get<int>(ast, clingo_ast_attribute_csp) != 0);
73 }
74 case clingo_ast_type_show_term: {
75 return prg_.show(get<Location>(ast, clingo_ast_attribute_location),
76 parseTerm(*get<SAST>(ast, clingo_ast_attribute_term)),
77 parseBodyLiteralVec(get<AST::ASTVec>(ast, clingo_ast_attribute_body)),
78 ast.hasValue(clingo_ast_attribute_csp) && get<int>(ast, clingo_ast_attribute_csp) != 0);
79 }
80 case clingo_ast_type_minimize: {
81 return prg_.optimize(get<Location>(ast, clingo_ast_attribute_location),
82 parseTerm(*get<SAST>(ast, clingo_ast_attribute_weight)),
83 parseTerm(*get<SAST>(ast, clingo_ast_attribute_priority)),
84 parseTermVec(get<AST::ASTVec>(ast, clingo_ast_attribute_terms)),
85 parseBodyLiteralVec(get<AST::ASTVec>(ast, clingo_ast_attribute_body)));
86 }
87 case clingo_ast_type_script: {
88 return prg_.script(get<Location>(ast, clingo_ast_attribute_location),
89 get<String>(ast, clingo_ast_attribute_name),
90 get<String>(ast, clingo_ast_attribute_code));
91 }
92 case clingo_ast_type_program: {
93 return prg_.block(get<Location>(ast, clingo_ast_attribute_location),
94 get<String>(ast, clingo_ast_attribute_name),
95 parseIdVec(get<AST::ASTVec>(ast, clingo_ast_attribute_parameters)));
96 }
97 case clingo_ast_type_external: {
98 return prg_.external(get<Location>(ast, clingo_ast_attribute_location),
99 parseAtom(*get<SAST>(ast, clingo_ast_attribute_atom)),
100 parseBodyLiteralVec(get<AST::ASTVec>(ast, clingo_ast_attribute_body)),
101 parseTerm(*get<SAST>(ast, clingo_ast_attribute_external_type)));
102 }
103 case clingo_ast_type_edge: {
104 return prg_.edge(get<Location>(ast, clingo_ast_attribute_location),
105 prg_.termvecvec(prg_.termvecvec(),
106 prg_.termvec(prg_.termvec(prg_.termvec(),
107 parseTerm(*get<SAST>(ast, clingo_ast_attribute_node_u))),
108 parseTerm(*get<SAST>(ast, clingo_ast_attribute_node_v)))),
109 parseBodyLiteralVec(get<AST::ASTVec>(ast, clingo_ast_attribute_body)));
110 }
111 case clingo_ast_type_heuristic: {
112 return prg_.heuristic(get<Location>(ast, clingo_ast_attribute_location),
113 parseAtom(*get<SAST>(ast, clingo_ast_attribute_atom)),
114 parseBodyLiteralVec(get<AST::ASTVec>(ast, clingo_ast_attribute_body)),
115 parseTerm(*get<SAST>(ast, clingo_ast_attribute_bias)),
116 parseTerm(*get<SAST>(ast, clingo_ast_attribute_priority)),
117 parseTerm(*get<SAST>(ast, clingo_ast_attribute_modifier)));
118 }
119 case clingo_ast_type_project_atom: {
120 return prg_.project(get<Location>(ast, clingo_ast_attribute_location),
121 parseAtom(*get<SAST>(ast, clingo_ast_attribute_atom)),
122 parseBodyLiteralVec(get<AST::ASTVec>(ast, clingo_ast_attribute_body)));
123 }
124 case clingo_ast_type_project_signature: {
125 return prg_.project(get<Location>(ast, clingo_ast_attribute_location),
126 Sig(get<String>(ast, clingo_ast_attribute_name),
127 get<int>(ast, clingo_ast_attribute_arity),
128 get<int>(ast, clingo_ast_attribute_positive) == 0));
129 }
130 case clingo_ast_type_defined: {
131 return prg_.defined(get<Location>(ast, clingo_ast_attribute_location),
132 Sig(get<String>(ast, clingo_ast_attribute_name),
133 get<int>(ast, clingo_ast_attribute_arity),
134 get<int>(ast, clingo_ast_attribute_positive) == 0));
135 }
136 case clingo_ast_type_theory_definition: {
137 return prg_.theorydef(get<Location>(ast, clingo_ast_attribute_location),
138 get<String>(ast, clingo_ast_attribute_name),
139 parseTheoryAtomDefinitionVec(parseTheoryTermDefinitionVec(get<AST::ASTVec>(ast, clingo_ast_attribute_terms)),
140 get<AST::ASTVec>(ast, clingo_ast_attribute_atoms)),
141 log_);
142 }
143 default: {
144 throw std::runtime_error("invalid ast: statement expected");
145 }
146 }
147 }
148
149 private:
150 template <class T>
fail_Gringo::Input::__anon36f400340111::ASTParser151 T fail_(char const *message) {
152 throw std::runtime_error(message);
153 }
154
require_Gringo::Input::__anon36f400340111::ASTParser155 bool require_(bool cond, char const *message) {
156 if (!cond) { fail_<void>(message); }
157 return false;
158 }
159
160 // {{{1 terms
161
parseIdVecGringo::Input::__anon36f400340111::ASTParser162 IdVecUid parseIdVec(AST::ASTVec const &asts) {
163 auto uid = prg_.idvec();
164 for (auto const &ast : asts) {
165 require_(ast->type() == clingo_ast_type_id, "invalid ast: id required");
166 prg_.idvec(uid, get<Location>(*ast, clingo_ast_attribute_location), get<String>(*ast, clingo_ast_attribute_name));
167 }
168 return uid;
169 }
170
parseUnOpGringo::Input::__anon36f400340111::ASTParser171 static UnOp parseUnOp(int num) {
172 switch (num) {
173 case clingo_ast_unary_operator_minus: {
174 return UnOp::NEG;
175 }
176 case clingo_ast_unary_operator_negation: {
177 return UnOp::NOT;
178 }
179 case clingo_ast_unary_operator_absolute: {
180 return UnOp::ABS;
181 }
182 default: {
183 throw std::runtime_error("invalid ast: invalid unary operator");
184 }
185 }
186 }
187
parseBinOpGringo::Input::__anon36f400340111::ASTParser188 static BinOp parseBinOp(int num) {
189 switch (num) {
190 case clingo_ast_binary_operator_xor: {
191 return BinOp::XOR;
192 }
193 case clingo_ast_binary_operator_or: {
194 return BinOp::OR;
195 }
196 case clingo_ast_binary_operator_and: {
197 return BinOp::AND;
198 }
199 case clingo_ast_binary_operator_plus: {
200 return BinOp::ADD;
201 }
202 case clingo_ast_binary_operator_minus: {
203 return BinOp::SUB;
204 }
205 case clingo_ast_binary_operator_multiplication: {
206 return BinOp::MUL;
207 }
208 case clingo_ast_binary_operator_division: {
209 return BinOp::DIV;
210 }
211 case clingo_ast_binary_operator_modulo: {
212 return BinOp::MOD;
213 }
214 case clingo_ast_binary_operator_power: {
215 return BinOp::POW;
216 }
217 default: {
218 throw std::runtime_error("invalid ast: invalid binary operator");
219 }
220 }
221 }
222
parseTermGringo::Input::__anon36f400340111::ASTParser223 TermUid parseTerm(AST const &ast) {
224 switch (ast.type()) {
225 case clingo_ast_type_variable: {
226 return prg_.term(get<Location>(ast, clingo_ast_attribute_location),
227 get<String>(ast, clingo_ast_attribute_name));
228 }
229 case clingo_ast_type_symbolic_term: {
230 return prg_.term(get<Location>(ast, clingo_ast_attribute_location),
231 get<Symbol>(ast, clingo_ast_attribute_symbol));
232 }
233 case clingo_ast_type_unary_operation: {
234 return prg_.term(get<Location>(ast, clingo_ast_attribute_location),
235 parseUnOp(get<int>(ast, clingo_ast_attribute_operator_type)),
236 parseTerm(*get<SAST>(ast, clingo_ast_attribute_argument)));
237 }
238 case clingo_ast_type_binary_operation: {
239 return prg_.term(get<Location>(ast, clingo_ast_attribute_location),
240 parseBinOp(get<int>(ast, clingo_ast_attribute_operator_type)),
241 parseTerm(*get<SAST>(ast, clingo_ast_attribute_left)),
242 parseTerm(*get<SAST>(ast, clingo_ast_attribute_right)));
243 }
244 case clingo_ast_type_interval: {
245 return prg_.term(get<Location>(ast, clingo_ast_attribute_location),
246 parseTerm(*get<SAST>(ast, clingo_ast_attribute_left)),
247 parseTerm(*get<SAST>(ast, clingo_ast_attribute_right)));
248 }
249 case clingo_ast_type_function: {
250 auto external = ast.hasValue(clingo_ast_attribute_external) && get<int>(ast, clingo_ast_attribute_external) != 0;
251 auto name = get<String>(ast, clingo_ast_attribute_name);
252 require_(!name.empty() || !external, "invalid ast: external functions must have a name");
253 return !name.empty()
254 ? prg_.term(get<Location>(ast, clingo_ast_attribute_location),
255 name,
256 prg_.termvecvec(prg_.termvecvec(),
257 parseTermVec(get<AST::ASTVec>(ast, clingo_ast_attribute_arguments))),
258 external)
259 : prg_.term(get<Location>(ast, clingo_ast_attribute_location),
260 parseTermVec(get<AST::ASTVec>(ast, clingo_ast_attribute_arguments)),
261 true);
262 }
263 case clingo_ast_type_pool: {
264 return prg_.pool(get<Location>(ast, clingo_ast_attribute_location),
265 parseTermVec(get<AST::ASTVec>(ast, clingo_ast_attribute_arguments)));
266 }
267 default: {
268 throw std::runtime_error("invalid ast: term expected");
269 }
270 }
271 }
272
parseTermVecGringo::Input::__anon36f400340111::ASTParser273 TermVecUid parseTermVec(AST::ASTVec const &asts) {
274 TermVecUid uid = prg_.termvec();
275 for (auto const &ast : asts) {
276 prg_.termvec(uid, parseTerm(*ast));
277 }
278 return uid;
279 }
280
parseCSPMulTermGringo::Input::__anon36f400340111::ASTParser281 CSPMulTermUid parseCSPMulTerm(AST const &ast) {
282 require_(ast.type() == clingo_ast_type_csp_product, "invalid ast: csp product required");
283 auto const *variable = getOpt(ast, clingo_ast_attribute_variable);
284 return variable != nullptr
285 ? prg_.cspmulterm(get<Location>(ast, clingo_ast_attribute_location),
286 parseTerm(*get<SAST>(ast, clingo_ast_attribute_coefficient)),
287 parseTerm(*variable))
288 : prg_.cspmulterm(get<Location>(ast, clingo_ast_attribute_location),
289 parseTerm(*get<SAST>(ast, clingo_ast_attribute_coefficient)));
290 }
291
parseCSPAddTermGringo::Input::__anon36f400340111::ASTParser292 CSPAddTermUid parseCSPAddTerm(AST const &ast) {
293 require_(ast.type() == clingo_ast_type_csp_sum, "invalid ast: csp sum required");
294 auto const &terms = get<AST::ASTVec>(ast, clingo_ast_attribute_terms);
295 require_(!terms.empty(), "invalid ast: csp sums terms must not be empty");
296 auto it = terms.begin();
297 auto ie = terms.end();
298 auto uid = prg_.cspaddterm(get<Location>(**it, clingo_ast_attribute_location),
299 parseCSPMulTerm(**it));
300 for (++it; it != ie; ++it) {
301 uid = prg_.cspaddterm(get<Location>(**it, clingo_ast_attribute_location),
302 uid,
303 parseCSPMulTerm(**it), true);
304
305 }
306 return uid;
307 }
308
parseTheoryTermGringo::Input::__anon36f400340111::ASTParser309 TheoryTermUid parseTheoryTerm(AST const &ast) {
310 switch (ast.type()) {
311 case clingo_ast_type_symbolic_term : {
312 return prg_.theorytermvalue(get<Location>(ast, clingo_ast_attribute_location), get<Symbol>(ast, clingo_ast_attribute_symbol));
313 }
314 case clingo_ast_type_variable: {
315 return prg_.theorytermvar(get<Location>(ast, clingo_ast_attribute_location), get<String>(ast, clingo_ast_attribute_name));
316 }
317 case clingo_ast_type_theory_sequence: {
318 switch (get<int>(ast, clingo_ast_attribute_sequence_type)) {
319 case clingo_ast_theory_sequence_type_tuple: {
320 return prg_.theorytermtuple(get<Location>(ast, clingo_ast_attribute_location),
321 parseTheoryOptermVec(get<AST::ASTVec>(ast, clingo_ast_attribute_terms)));
322 }
323 case clingo_ast_theory_sequence_type_list: {
324 return prg_.theoryoptermlist(get<Location>(ast, clingo_ast_attribute_location),
325 parseTheoryOptermVec(get<AST::ASTVec>(ast, clingo_ast_attribute_terms)));
326 }
327 case clingo_ast_theory_sequence_type_set: {
328 return prg_.theorytermset(get<Location>(ast, clingo_ast_attribute_location),
329 parseTheoryOptermVec(get<AST::ASTVec>(ast, clingo_ast_attribute_terms)));
330 }
331 default: {
332 throw std::runtime_error("invalid ast: invalid theory sequence type");
333
334 }
335 }
336 }
337 case clingo_ast_type_theory_function: {
338 return prg_.theorytermfun(get<Location>(ast, clingo_ast_attribute_location),
339 get<String>(ast, clingo_ast_attribute_name),
340 parseTheoryOptermVec(get<AST::ASTVec>(ast, clingo_ast_attribute_arguments)));
341 }
342 case clingo_ast_type_theory_unparsed_term: {
343 return prg_.theorytermopterm(get<Location>(ast, clingo_ast_attribute_location),
344 parseTheoryUnparsedTermElements(get<AST::ASTVec>(ast, clingo_ast_attribute_elements)));
345 }
346 default: {
347 throw std::runtime_error("invalid ast: theory term expected");
348 }
349 }
350 }
351
352
parseTheoryOptermVecGringo::Input::__anon36f400340111::ASTParser353 TheoryOptermVecUid parseTheoryOptermVec(AST::ASTVec const &asts) {
354 auto uid = prg_.theoryopterms();
355 for (auto const &ast : asts) {
356 uid = prg_.theoryopterms(uid, get<Location>(*ast, clingo_ast_attribute_location), parseTheoryOpterm(*ast));
357 }
358 return uid;
359 }
360
parseTheoryOpVecGringo::Input::__anon36f400340111::ASTParser361 TheoryOpVecUid parseTheoryOpVec(AST::StrVec const &strs) {
362 auto uid = prg_.theoryops();
363 for (auto const &str : strs) {
364 uid = prg_.theoryops(uid, str);
365 }
366 return uid;
367 }
368
parseTheoryOptermGringo::Input::__anon36f400340111::ASTParser369 TheoryOptermUid parseTheoryOpterm(AST const &ast) {
370 if (ast.type() == clingo_ast_type_theory_unparsed_term) {
371 return parseTheoryUnparsedTermElements(get<AST::ASTVec>(ast, clingo_ast_attribute_elements));
372 }
373 return prg_.theoryopterm(prg_.theoryops(), parseTheoryTerm(ast));
374 }
375
parseTheoryUnparsedTermElementsGringo::Input::__anon36f400340111::ASTParser376 TheoryOptermUid parseTheoryUnparsedTermElements(AST::ASTVec const &asts) {
377 require_(!asts.empty(), "invalid ast: unparsed term list must not be empty");
378 auto it = asts.begin();
379 auto ie = asts.end();
380 auto uid = prg_.theoryopterm(parseTheoryOpVec(get<AST::StrVec>(**it, clingo_ast_attribute_operators)),
381 parseTheoryTerm(*get<SAST>(**it, clingo_ast_attribute_term)));
382 for (++it; it != ie; ++it) {
383 auto const &operators = get<AST::StrVec>(**it, clingo_ast_attribute_operators);
384 require_(!operators.empty(), "invalid ast: at least one operator necessary on right-hand-side of unparsed theory term");
385 uid = prg_.theoryopterm(uid,
386 parseTheoryOpVec(operators),
387 parseTheoryTerm(*get<SAST>(**it, clingo_ast_attribute_term)));
388 }
389 return uid;
390 }
391
392 // {{{1 literals
393
parseAtomGringo::Input::__anon36f400340111::ASTParser394 TermUid parseAtom(AST &ast) {
395 require_(ast.type() == clingo_ast_type_symbolic_atom, "invalid ast: symbolic atom expected");
396 return parseTerm(*get<SAST>(ast, clingo_ast_attribute_symbol));
397 }
398
parseSignGringo::Input::__anon36f400340111::ASTParser399 static NAF parseSign(int sign) {
400 switch (sign) {
401 case clingo_ast_sign_no_sign: {
402 return NAF::POS;
403 }
404 case clingo_ast_sign_negation: {
405 return NAF::NOT;
406 }
407 case clingo_ast_sign_double_negation: {
408 return NAF::NOTNOT;
409 }
410 default: {
411 throw std::runtime_error("invalid ast: invalid sign");
412 }
413 }
414 }
415
parseRelationGringo::Input::__anon36f400340111::ASTParser416 static Relation parseRelation(int relation) {
417 switch (relation) {
418 case clingo_ast_comparison_operator_less_equal: {
419 return Relation::LEQ;
420 }
421 case clingo_ast_comparison_operator_less_than: {
422 return Relation::LT;
423 }
424 case clingo_ast_comparison_operator_greater_equal: {
425 return Relation::GEQ;
426 }
427 case clingo_ast_comparison_operator_greater_than: {
428 return Relation::GT;
429 }
430 case clingo_ast_comparison_operator_equal: {
431 return Relation::EQ;
432 }
433 case clingo_ast_comparison_operator_not_equal: {
434 return Relation::NEQ;
435 }
436 default: {
437 throw std::runtime_error("invalid ast: invalid sign");
438 }
439 }
440 }
441
parseLiteralGringo::Input::__anon36f400340111::ASTParser442 LitUid parseLiteral(AST const &ast) {
443 switch (ast.type()) {
444 case clingo_ast_type_literal: {
445 auto loc = get<Location>(ast, clingo_ast_attribute_location);
446 auto sign = parseSign(get<int>(ast, clingo_ast_attribute_sign));
447 auto const &atom = *get<SAST>(ast, clingo_ast_attribute_atom);
448
449 switch (atom.type()) {
450 case clingo_ast_type_boolean_constant: {
451 int cmp = sign == NAF::NOT ? 1 : 0;
452 return prg_.boollit(loc,
453 get<int>(atom, clingo_ast_attribute_value) != cmp);
454 }
455 case clingo_ast_type_symbolic_atom: {
456 return prg_.predlit(loc,
457 sign,
458 parseAtom(*get<SAST>(ast, clingo_ast_attribute_atom)));
459 }
460 case clingo_ast_type_comparison: {
461 auto rel = parseRelation(get<int>(atom, clingo_ast_attribute_comparison));
462 return prg_.rellit(loc,
463 sign != NAF::NOT ? rel : neg(rel),
464 parseTerm(*get<SAST>(atom, clingo_ast_attribute_left)),
465 parseTerm(*get<SAST>(atom, clingo_ast_attribute_right)));
466 }
467 default: {
468 throw std::runtime_error("invalid ast: atom expected");
469 }
470 }
471 }
472 case clingo_ast_type_csp_literal: {
473 auto const &guards = get<AST::ASTVec>(ast, clingo_ast_attribute_guards);
474 require_(!guards.empty(), "invalid ast: csp literals need at least one guard");
475 auto it = guards.begin();
476 auto ie = guards.end();
477 auto uid = prg_.csplit(get<Location>(ast, clingo_ast_attribute_location),
478 parseCSPAddTerm(*get<SAST>(ast, clingo_ast_attribute_term)),
479 parseRelation(get<int>(**it, clingo_ast_attribute_comparison)),
480 parseCSPAddTerm(*get<SAST>(**it, clingo_ast_attribute_term)));
481 for (++it; it != ie; ++it) {
482 uid = prg_.csplit(get<Location>(ast, clingo_ast_attribute_location),
483 uid,
484 parseRelation(get<int>(**it, clingo_ast_attribute_comparison)),
485 parseCSPAddTerm(*get<SAST>(**it, clingo_ast_attribute_term)));
486 }
487 return prg_.csplit(uid);
488 }
489 default: {
490 throw std::runtime_error("invalid ast: (CSP) literal expected");
491 }
492 }
493 }
494
parseLiteralVecGringo::Input::__anon36f400340111::ASTParser495 LitVecUid parseLiteralVec(AST::ASTVec const &asts) {
496 auto uid = prg_.litvec();
497 for (auto const &ast : asts) {
498 uid = prg_.litvec(uid, parseLiteral(*ast));
499 }
500 return uid;
501 }
502
503 // {{{1 aggregates
504
parseAggregateFunctionGringo::Input::__anon36f400340111::ASTParser505 static AggregateFunction parseAggregateFunction(int fun) {
506 switch (fun) {
507 case clingo_ast_aggregate_function_count: {
508 return AggregateFunction::COUNT;
509 }
510 case clingo_ast_aggregate_function_sum: {
511 return AggregateFunction::SUM;
512 }
513 case clingo_ast_aggregate_function_sump: {
514 return AggregateFunction::SUMP;
515 }
516 case clingo_ast_aggregate_function_min: {
517 return AggregateFunction::MIN;
518 }
519 case clingo_ast_aggregate_function_max: {
520 return AggregateFunction::MAX;
521 }
522 default: {
523 throw std::runtime_error("invalid ast: invalid aggregate function");
524 }
525 };
526 }
527
parseBoundsGringo::Input::__anon36f400340111::ASTParser528 BoundVecUid parseBounds(AST const &ast) {
529 auto ret = prg_.boundvec();
530 auto const *right = getOpt(ast, clingo_ast_attribute_right_guard);
531 if (right != nullptr) {
532 ret = prg_.boundvec(ret,
533 parseRelation(get<int>(*right, clingo_ast_attribute_comparison)),
534 parseTerm(*get<SAST>(*right, clingo_ast_attribute_term)));
535 }
536 auto const *left = getOpt(ast, clingo_ast_attribute_left_guard);
537 if (left != nullptr) {
538 ret = prg_.boundvec(ret,
539 inv(parseRelation(get<int>(*left, clingo_ast_attribute_comparison))),
540 parseTerm(*get<SAST>(*left, clingo_ast_attribute_term)));
541 }
542 return ret;
543 }
544
parseCondLitVecGringo::Input::__anon36f400340111::ASTParser545 CondLitVecUid parseCondLitVec(AST::ASTVec const &asts) {
546 auto uid = prg_.condlitvec();
547 for (auto const &ast : asts) {
548 uid = prg_.condlitvec(uid,
549 parseLiteral(*get<SAST>(*ast, clingo_ast_attribute_literal)),
550 parseLiteralVec(get<AST::ASTVec>(*ast, clingo_ast_attribute_condition)));
551 }
552 return uid;
553 }
554
parseHdAggrElemVecGringo::Input::__anon36f400340111::ASTParser555 HdAggrElemVecUid parseHdAggrElemVec(AST::ASTVec const &asts) {
556 auto uid = prg_.headaggrelemvec();
557 for (auto const &ast : asts) {
558 require_(ast->type() == clingo_ast_type_head_aggregate_element, "invalid ast: head aggregate element expected");
559 auto const &clit = get<SAST>(*ast, clingo_ast_attribute_condition);
560 require_(clit->type() == clingo_ast_type_conditional_literal, "invalid ast: conditional literal expected");
561 uid = prg_.headaggrelemvec(uid,
562 parseTermVec(get<AST::ASTVec>(*ast, clingo_ast_attribute_terms)),
563 parseLiteral(*get<SAST>(*clit, clingo_ast_attribute_literal)),
564 parseLiteralVec(get<AST::ASTVec>(*clit, clingo_ast_attribute_condition)));
565 }
566 return uid;
567 }
568
parseBdAggrElemVecGringo::Input::__anon36f400340111::ASTParser569 BdAggrElemVecUid parseBdAggrElemVec(AST::ASTVec const &asts) {
570 auto uid = prg_.bodyaggrelemvec();
571 for (auto const &ast : asts) {
572 require_(ast->type() == clingo_ast_type_body_aggregate_element, "invalid ast: body aggregate element expected");
573 uid = prg_.bodyaggrelemvec(uid,
574 parseTermVec(get<AST::ASTVec>(*ast, clingo_ast_attribute_terms)),
575 parseLiteralVec(get<AST::ASTVec>(*ast, clingo_ast_attribute_condition)));
576 }
577 return uid;
578 }
579
parseTheoryElemVecGringo::Input::__anon36f400340111::ASTParser580 TheoryElemVecUid parseTheoryElemVec(AST::ASTVec const &asts) {
581 auto uid = prg_.theoryelems();
582 for (auto const &ast : asts) {
583 uid = prg_.theoryelems(uid,
584 parseTheoryOptermVec(get<AST::ASTVec>(*ast, clingo_ast_attribute_terms)),
585 parseLiteralVec(get<AST::ASTVec>(*ast, clingo_ast_attribute_condition)));
586 }
587 return uid;
588 }
589
parseCSPElemVecGringo::Input::__anon36f400340111::ASTParser590 CSPElemVecUid parseCSPElemVec(AST::ASTVec const &asts) {
591 auto ret = prg_.cspelemvec();
592 for (auto const &ast : asts) {
593 require_(ast->type() == clingo_ast_type_disjoint_element, "invalid ast: disjoint element expected");
594 ret = prg_.cspelemvec(ret,
595 get<Location>(*ast, clingo_ast_attribute_location),
596 parseTermVec(get<AST::ASTVec>(*ast, clingo_ast_attribute_terms)),
597 parseCSPAddTerm(*get<SAST>(*ast, clingo_ast_attribute_term)),
598 parseLiteralVec(get<AST::ASTVec>(*ast, clingo_ast_attribute_condition)));
599 }
600 return ret;
601 }
602
parseTheoryAtomGringo::Input::__anon36f400340111::ASTParser603 TheoryAtomUid parseTheoryAtom(AST const &ast) {
604 require_(ast.type() == clingo_ast_type_theory_atom, "invalid ast: theory atom expected");
605 auto const &loc = get<Location>(ast, clingo_ast_attribute_location);
606 auto const *guard = getOpt(ast, clingo_ast_attribute_guard);
607 auto term = parseTerm(*get<SAST>(ast, clingo_ast_attribute_term));
608 auto elements = parseTheoryElemVec(get<AST::ASTVec>(ast, clingo_ast_attribute_elements));
609 return guard != nullptr
610 ? prg_.theoryatom(term,
611 elements,
612 get<String>(*guard, clingo_ast_attribute_operator_name),
613 loc,
614 parseTheoryOpterm(*get<SAST>(*guard, clingo_ast_attribute_term)))
615 : prg_.theoryatom(term, elements);
616
617 }
618
619 // {{{1 heads
620
parseHeadLiteralGringo::Input::__anon36f400340111::ASTParser621 HdLitUid parseHeadLiteral(AST const &ast) {
622 switch (ast.type()) {
623 case clingo_ast_type_literal:
624 case clingo_ast_type_csp_literal: {
625 return prg_.headlit(parseLiteral(ast));
626 }
627 case clingo_ast_type_disjunction: {
628 return prg_.disjunction(get<Location>(ast, clingo_ast_attribute_location),
629 parseCondLitVec(get<AST::ASTVec>(ast, clingo_ast_attribute_elements)));
630 }
631 case clingo_ast_type_aggregate: {
632 return prg_.headaggr(get<Location>(ast, clingo_ast_attribute_location),
633 AggregateFunction::COUNT,
634 parseBounds(ast),
635 parseCondLitVec(get<AST::ASTVec>(ast, clingo_ast_attribute_elements)));
636 }
637 case clingo_ast_type_head_aggregate: {
638 return prg_.headaggr(get<Location>(ast, clingo_ast_attribute_location),
639 parseAggregateFunction(get<int>(ast, clingo_ast_attribute_function)),
640 parseBounds(ast),
641 parseHdAggrElemVec(get<AST::ASTVec>(ast, clingo_ast_attribute_elements)));
642 }
643 case clingo_ast_type_theory_atom: {
644 auto const &loc = get<Location>(ast, clingo_ast_attribute_location);
645 return prg_.headaggr(loc, parseTheoryAtom(ast));
646 }
647 default: {
648 throw std::runtime_error("invalid ast: head literal expected");
649 }
650 }
651 }
652
653 // {{{1 bodies
654
parseBodyLiteralVecGringo::Input::__anon36f400340111::ASTParser655 BdLitVecUid parseBodyLiteralVec(AST::ASTVec const &asts) {
656 auto uid = prg_.body();
657 for (auto const &lit : asts) {
658 switch (lit->type()) {
659 case clingo_ast_type_literal: {
660 auto const &loc = get<Location>(*lit, clingo_ast_attribute_location);
661 auto sign = parseSign(get<int>(*lit, clingo_ast_attribute_sign));
662 auto const &atom = *get<SAST>(*lit, clingo_ast_attribute_atom);
663 switch (atom.type()) {
664 case clingo_ast_type_aggregate: {
665 uid = prg_.bodyaggr(uid, loc, sign, AggregateFunction::COUNT,
666 parseBounds(atom),
667 parseCondLitVec(get<AST::ASTVec>(atom, clingo_ast_attribute_elements)));
668 break;
669 }
670 case clingo_ast_type_body_aggregate: {
671 uid = prg_.bodyaggr(uid, loc, sign,
672 parseAggregateFunction(get<int>(atom, clingo_ast_attribute_function)),
673 parseBounds(atom),
674 parseBdAggrElemVec(get<AST::ASTVec>(atom, clingo_ast_attribute_elements)));
675 break;
676 }
677 case clingo_ast_type_theory_atom: {
678 uid = prg_.bodyaggr(uid, loc, sign, parseTheoryAtom(atom));
679 break;
680 }
681 case clingo_ast_type_disjoint: {
682 uid = prg_.disjoint(uid, loc, sign,
683 parseCSPElemVec(get<AST::ASTVec>(atom, clingo_ast_attribute_elements)));
684 break;
685 }
686 default: {
687 uid = prg_.bodylit(uid, parseLiteral(*lit));
688 break;
689 }
690 }
691 break;
692 }
693 case clingo_ast_type_conditional_literal: {
694 uid = prg_.conjunction(uid,
695 get<Location>(*lit, clingo_ast_attribute_location),
696 parseLiteral(*get<SAST>(*lit, clingo_ast_attribute_literal)),
697 parseLiteralVec(get<AST::ASTVec>(*lit, clingo_ast_attribute_condition)));
698 break;
699 }
700 default: {
701 throw std::runtime_error("invalid ast: body literal expected");
702 }
703 }
704 }
705 return uid;
706 }
707
708 // {{{1 theory definitions
709
parseTheoryOperatorTypeGringo::Input::__anon36f400340111::ASTParser710 static TheoryOperatorType parseTheoryOperatorType(int num) {
711 switch (num) {
712 case clingo_ast_theory_operator_type_unary: {
713 return TheoryOperatorType::Unary;
714 }
715 case clingo_ast_theory_operator_type_binary_left: {
716 return TheoryOperatorType::BinaryLeft;
717 }
718 case clingo_ast_theory_operator_type_binary_right: {
719 return TheoryOperatorType::BinaryRight;
720 }
721 default: {
722 throw std::runtime_error("invalid ast: invalid theory operator type");
723 }
724 }
725 }
726
parseTheoryOpDefGringo::Input::__anon36f400340111::ASTParser727 TheoryOpDefUid parseTheoryOpDef(AST const &ast) {
728 require_(ast.type() == clingo_ast_type_theory_operator_definition, "invalid ast: theory operator definition expected");
729 return prg_.theoryopdef(get<Location>(ast, clingo_ast_attribute_location),
730 get<String>(ast, clingo_ast_attribute_name),
731 get<int>(ast, clingo_ast_attribute_priority),
732 parseTheoryOperatorType(get<int>(ast, clingo_ast_attribute_operator_type)));
733 }
734
parseTheoryOpDefVecGringo::Input::__anon36f400340111::ASTParser735 TheoryOpDefVecUid parseTheoryOpDefVec(AST::ASTVec const &asts) {
736 auto uid = prg_.theoryopdefs();
737 for (auto const &ast : asts) {
738 prg_.theoryopdefs(uid, parseTheoryOpDef(*ast));
739 }
740 return uid;
741 }
742
parseTheoryAtomTypeGringo::Input::__anon36f400340111::ASTParser743 static TheoryAtomType parseTheoryAtomType(int num) {
744 switch (num) {
745 case clingo_ast_theory_atom_definition_type_head: {
746 return TheoryAtomType::Head;
747 }
748 case clingo_ast_theory_atom_definition_type_body: {
749 return TheoryAtomType::Body;
750 }
751 case clingo_ast_theory_atom_definition_type_any: {
752 return TheoryAtomType::Any;
753 }
754 case clingo_ast_theory_atom_definition_type_directive: {
755 return TheoryAtomType::Directive;
756 }
757 default: {
758 throw std::runtime_error("invalid ast: invalid theory atom type");
759 }
760 };
761 }
762
parseTheoryAtomDefinitionGringo::Input::__anon36f400340111::ASTParser763 TheoryAtomDefUid parseTheoryAtomDefinition(AST const &ast) {
764 require_(ast.type() == clingo_ast_type_theory_atom_definition, "invalid ast: theory atom definition expected");
765 auto const *guard = getOpt(ast, clingo_ast_attribute_guard);
766 auto const &loc = get<Location>(ast, clingo_ast_attribute_location);
767 auto name = get<String>(ast, clingo_ast_attribute_name);
768 auto arity = get<int>(ast, clingo_ast_attribute_arity);
769 auto term = get<String>(ast, clingo_ast_attribute_term);
770 auto type = parseTheoryAtomType(get<int>(ast, clingo_ast_attribute_atom_type));
771 return guard != nullptr
772 ? prg_.theoryatomdef(loc, name, arity, term, type,
773 parseTheoryOpVec(get<AST::StrVec>(*guard, clingo_ast_attribute_operators)),
774 get<String>(*guard, clingo_ast_attribute_term))
775 : prg_.theoryatomdef(loc, name, arity, term, type);
776 }
777
parseTheoryAtomDefinitionVecGringo::Input::__anon36f400340111::ASTParser778 TheoryDefVecUid parseTheoryAtomDefinitionVec(TheoryDefVecUid uid, AST::ASTVec const &asts) {
779 for (auto const &ast : asts) {
780 prg_.theorydefs(uid, parseTheoryAtomDefinition(*ast));
781 }
782 return uid;
783 }
784
parseTheoryTermDefinitionGringo::Input::__anon36f400340111::ASTParser785 TheoryTermDefUid parseTheoryTermDefinition(AST const &ast) {
786 return prg_.theorytermdef(get<Location>(ast, clingo_ast_attribute_location),
787 get<String>(ast, clingo_ast_attribute_name),
788 parseTheoryOpDefVec(get<AST::ASTVec>(ast, clingo_ast_attribute_operators)),
789 log_);
790 }
791
parseTheoryTermDefinitionVecGringo::Input::__anon36f400340111::ASTParser792 TheoryDefVecUid parseTheoryTermDefinitionVec(AST::ASTVec const &asts) {
793 auto uid = prg_.theorydefs();
794 for (auto const &ast : asts) {
795 prg_.theorydefs(uid, parseTheoryTermDefinition(*ast));
796 }
797 return uid;
798 }
799
800 // 1}}}
801
802 Logger &log_;
803 INongroundProgramBuilder &prg_;
804 };
805
806 } // namespace
807
parse(INongroundProgramBuilder & prg,Logger & log,AST const & ast)808 void parse(INongroundProgramBuilder &prg, Logger &log, AST const &ast) {
809 ASTParser{log, prg}.parseStatement(ast);
810 }
811
812 } } // namespace Input Gringo
813