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// {{{1 preamble 26%require "2.5" 27//%define api.namespace {Gringo::Input::NonGroundGrammar} 28%define namespace "Gringo::Input::NonGroundGrammar" 29//%define api.prefix {GringoNonGroundGrammar_} 30%name-prefix "GringoNonGroundGrammar_" 31//%define parse.error verbose 32%error-verbose 33//%define api.location.type {DefaultLocation} 34%define location_type "DefaultLocation" 35%locations 36%defines 37%parse-param { Gringo::Input::NonGroundParser *lexer } 38%lex-param { Gringo::Input::NonGroundParser *lexer } 39%skeleton "lalr1.cc" 40//%define parse.trace 41//%debug 42 43// {{{1 auxiliary code 44 45%code requires 46{ 47 #include "gringo/input/programbuilder.hh" 48 #include "potassco/basic_types.h" 49 50 namespace Gringo { namespace Input { class NonGroundParser; } } 51 52 struct DefaultLocation : Gringo::Location { 53 DefaultLocation() : Location("<undef>", 0, 0, "<undef>", 0, 0) { } 54 }; 55 56} 57 58%{ 59 60#include "gringo/input/nongroundparser.hh" 61#include "gringo/input/programbuilder.hh" 62#include <climits> 63 64#define BUILDER (lexer->builder()) 65#define LOGGER (lexer->logger()) 66#define YYLLOC_DEFAULT(Current, Rhs, N) \ 67 do { \ 68 if (N) { \ 69 (Current).beginFilename = YYRHSLOC (Rhs, 1).beginFilename; \ 70 (Current).beginLine = YYRHSLOC (Rhs, 1).beginLine; \ 71 (Current).beginColumn = YYRHSLOC (Rhs, 1).beginColumn; \ 72 (Current).endFilename = YYRHSLOC (Rhs, N).endFilename; \ 73 (Current).endLine = YYRHSLOC (Rhs, N).endLine; \ 74 (Current).endColumn = YYRHSLOC (Rhs, N).endColumn; \ 75 } \ 76 else { \ 77 (Current).beginFilename = YYRHSLOC (Rhs, 0).endFilename; \ 78 (Current).beginLine = YYRHSLOC (Rhs, 0).endLine; \ 79 (Current).beginColumn = YYRHSLOC (Rhs, 0).endColumn; \ 80 (Current).endFilename = YYRHSLOC (Rhs, 0).endFilename; \ 81 (Current).endLine = YYRHSLOC (Rhs, 0).endLine; \ 82 (Current).endColumn = YYRHSLOC (Rhs, 0).endColumn; \ 83 } \ 84 } \ 85 while (false) 86 87using namespace Gringo; 88using namespace Gringo::Input; 89 90int GringoNonGroundGrammar_lex(void *value, Gringo::Location* loc, NonGroundParser *lexer) { 91 return lexer->lex(value, *loc); 92} 93 94%} 95 96%code { 97 98void NonGroundGrammar::parser::error(DefaultLocation const &l, std::string const &msg) { 99 lexer->parseError(l, msg); 100} 101 102} 103 104// {{{1 nonterminals 105 106// {{{2 union type for stack elements 107%union 108{ 109 IdVecUid idlist; 110 CSPLitUid csplit; 111 CSPAddTermUid cspaddterm; 112 CSPMulTermUid cspmulterm; 113 CSPElemVecUid cspelemvec; 114 TermUid term; 115 TermVecUid termvec; 116 TermVecVecUid termvecvec; 117 LitVecUid litvec; 118 LitUid lit; 119 BdAggrElemVecUid bodyaggrelemvec; 120 CondLitVecUid condlitlist; 121 HdAggrElemVecUid headaggrelemvec; 122 BoundVecUid bounds; 123 BdLitVecUid body; 124 HdLitUid head; 125 Relation rel; 126 AggregateFunction fun; 127 struct { 128 NAF first; 129 CSPElemVecUid second; 130 } disjoint; 131 struct { 132 uintptr_t first; 133 unsigned second; 134 } pair; 135 struct { 136 TermVecUid first; 137 LitVecUid second; 138 } bodyaggrelem; 139 struct { 140 LitUid first; 141 LitVecUid second; 142 } lbodyaggrelem; 143 struct { 144 AggregateFunction fun; 145 unsigned choice : 1; 146 unsigned elems : 31; 147 } aggr; 148 struct { 149 Relation rel; 150 TermUid term; 151 } bound; 152 struct { 153 TermUid first; 154 TermUid second; 155 } termpair; 156 unsigned uid; 157 uintptr_t str; 158 int num; 159 Potassco::Heuristic_t::E heu; 160 TheoryOpVecUid theoryOps; 161 TheoryTermUid theoryTerm; 162 TheoryOptermUid theoryOpterm; 163 TheoryOptermVecUid theoryOpterms; 164 TheoryElemVecUid theoryElems; 165 struct { 166 TheoryOptermVecUid first; 167 LitVecUid second; 168 } theoryElem; 169 TheoryAtomUid theoryAtom; 170 TheoryOpDefUid theoryOpDef; 171 TheoryOpDefVecUid theoryOpDefs; 172 TheoryTermDefUid theoryTermDef; 173 TheoryAtomDefUid theoryAtomDef; 174 TheoryDefVecUid theoryDefs; 175 TheoryAtomType theoryAtomType; 176} 177 178// }}}2 179 180// TODO: improve naming scheme 181%type <term> constterm term tuple theory_atom_name atom 182%type <termvec> termvec ntermvec consttermvec unaryargvec optimizetuple tuplevec tuplevec_sem 183%type <termvecvec> argvec constargvec binaryargvec 184%type <lit> literal 185%type <litvec> litvec nlitvec optcondition 186%type <bodyaggrelem> bodyaggrelem 187%type <lbodyaggrelem> altbodyaggrelem conjunction 188%type <bodyaggrelemvec> bodyaggrelemvec 189%type <condlitlist> altbodyaggrelemvec altheadaggrelemvec disjunctionsep disjunction 190%type <headaggrelemvec> headaggrelemvec 191%type <cspelemvec> cspelemvec ncspelemvec 192%type <bound> upper 193%type <body> bodycomma bodydot bodyconddot optimizelitvec optimizecond 194%type <head> head 195%type <uid> lubodyaggregate luheadaggregate 196%type <str> identifier theory_definition_identifier theory_op 197%type <fun> aggregatefunction 198%type <aggr> bodyaggregate headaggregate 199%type <rel> cmp csp_rel 200%type <termpair> optimizeweight 201%type <cspmulterm> csp_mul_term 202%type <cspaddterm> csp_add_term 203%type <csplit> csp_literal 204%type <disjoint> disjoint 205%type <idlist> idlist nidlist 206%type <theoryOps> theory_op_list theory_operator_list theory_operator_nlist 207%type <theoryTerm> theory_term 208%type <theoryOpterm> theory_opterm 209%type <theoryOpterms> theory_opterm_list theory_opterm_nlist 210%type <theoryElem> theory_atom_element 211%type <theoryElems> theory_atom_element_list theory_atom_element_nlist 212%type <theoryAtom> theory_atom 213%type <theoryTermDef> theory_term_definition 214%type <theoryAtomDef> theory_atom_definition 215%type <theoryOpDef> theory_operator_definition 216%type <theoryOpDefs> theory_operator_definition_nlist theory_operator_definiton_list 217%type <theoryDefs> theory_definition_nlist theory_definition_list 218%type <theoryAtomType> theory_atom_type 219 220// {{{1 terminals 221 222%token 223 ADD "+" 224 AND "&" 225 EQ "=" 226 AT "@" 227 BASE "#base" 228 BNOT "~" 229 COLON ":" 230 COMMA "," 231 CONST "#const" 232 COUNT "#count" 233 CSP "$" 234 CSP_ADD "$+" 235 CSP_SUB "$-" 236 CSP_MUL "$*" 237 CSP_LEQ "$<=" 238 CSP_LT "$<" 239 CSP_GT "$>" 240 CSP_GEQ "$>=" 241 CSP_EQ "$=" 242 CSP_NEQ "$!=" 243 CUMULATIVE "#cumulative" 244 DISJOINT "#disjoint" 245 DOT "." 246 DOTS ".." 247 END 0 "<EOF>" 248 EXTERNAL "#external" 249 DEFINED "#defined" 250 FALSE "#false" 251 FORGET "#forget" 252 GEQ ">=" 253 GT ">" 254 IF ":-" 255 INCLUDE "#include" 256 INFIMUM "#inf" 257 LBRACE "{" 258 LBRACK "[" 259 LEQ "<=" 260 LPAREN "(" 261 LT "<" 262 MAX "#max" 263 MAXIMIZE "#maximize" 264 MIN "#min" 265 MINIMIZE "#minimize" 266 MOD "\\" 267 MUL "*" 268 NEQ "!=" 269 POW "**" 270 QUESTION "?" 271 RBRACE "}" 272 RBRACK "]" 273 RPAREN ")" 274 SEM ";" 275 SHOW "#show" 276 EDGE "#edge" 277 PROJECT "#project" 278 HEURISTIC "#heuristic" 279 SHOWSIG "#showsig" 280 SLASH "/" 281 SUB "-" 282 SUM "#sum" 283 SUMP "#sum+" 284 SUPREMUM "#sup" 285 TRUE "#true" 286 BLOCK "#program" 287 UBNOT 288 UMINUS 289 VBAR "|" 290 VOLATILE "#volatile" 291 WIF ":~" 292 XOR "^" 293 PARSE_LP "<program>" 294 PARSE_DEF "<define>" 295 ANY "any" 296 UNARY "unary" 297 BINARY "binary" 298 LEFT "left" 299 RIGHT "right" 300 HEAD "head" 301 BODY "body" 302 DIRECTIVE "directive" 303 THEORY "#theory" 304 SYNC "EOF" 305 306 307%token <num> 308 NUMBER "<NUMBER>" 309 310%token <str> 311 ANONYMOUS "<ANONYMOUS>" 312 IDENTIFIER "<IDENTIFIER>" 313 SCRIPT "<SCRIPT>" 314 CODE "<CODE>" 315 STRING "<STRING>" 316 VARIABLE "<VARIABLE>" 317 THEORY_OP "<THEORYOP>" 318 NOT "not" 319 DEFAULT "default" 320 OVERRIDE "override" 321 322// {{{2 operator precedence and associativity 323 324%left DOTS 325%left XOR 326%left QUESTION 327%left AND 328%left ADD SUB 329%left MUL SLASH MOD 330%right POW 331%left UMINUS UBNOT 332 333// }}}1 334 335%% 336 337// {{{1 logic program and global definitions 338 339start 340 : PARSE_LP program 341 | PARSE_DEF define SYNC 342 ; 343 344program 345 : program statement 346 | 347 ; 348 349// Note: skip until the next "." in case of an error and switch back to normal lexing 350 351statement 352 : SYNC 353 | DOT { lexer->parseError(@$, "syntax error, unexpected ."); } 354 | error disable_theory_lexing DOT 355 | error disable_theory_lexing SYNC 356 ; 357 358identifier 359 : IDENTIFIER[a] { $$ = $a; } 360 | DEFAULT[a] { $$ = $a; } 361 | OVERRIDE[a] { $$ = $a; } 362 ; 363 364// {{{1 terms 365// {{{2 constterms are terms without variables and pooling operators 366 367constterm 368 : constterm[a] XOR constterm[b] { $$ = BUILDER.term(@$, BinOp::XOR, $a, $b); } 369 | constterm[a] QUESTION constterm[b] { $$ = BUILDER.term(@$, BinOp::OR, $a, $b); } 370 | constterm[a] AND constterm[b] { $$ = BUILDER.term(@$, BinOp::AND, $a, $b); } 371 | constterm[a] ADD constterm[b] { $$ = BUILDER.term(@$, BinOp::ADD, $a, $b); } 372 | constterm[a] SUB constterm[b] { $$ = BUILDER.term(@$, BinOp::SUB, $a, $b); } 373 | constterm[a] MUL constterm[b] { $$ = BUILDER.term(@$, BinOp::MUL, $a, $b); } 374 | constterm[a] SLASH constterm[b] { $$ = BUILDER.term(@$, BinOp::DIV, $a, $b); } 375 | constterm[a] MOD constterm[b] { $$ = BUILDER.term(@$, BinOp::MOD, $a, $b); } 376 | constterm[a] POW constterm[b] { $$ = BUILDER.term(@$, BinOp::POW, $a, $b); } 377 | SUB constterm[a] %prec UMINUS { $$ = BUILDER.term(@$, UnOp::NEG, $a); } 378 | BNOT constterm[a] %prec UBNOT { $$ = BUILDER.term(@$, UnOp::NOT, $a); } 379 | LPAREN RPAREN { $$ = BUILDER.term(@$, BUILDER.termvec(), false); } 380 | LPAREN COMMA RPAREN { $$ = BUILDER.term(@$, BUILDER.termvec(), true); } 381 | LPAREN consttermvec[a] RPAREN { $$ = BUILDER.term(@$, $a, false); } 382 | LPAREN consttermvec[a] COMMA RPAREN { $$ = BUILDER.term(@$, $a, true); } 383 | identifier[a] LPAREN constargvec[b] RPAREN { $$ = BUILDER.term(@$, String::fromRep($a), $b, false); } 384 | AT[l] identifier[a] LPAREN constargvec[b] RPAREN { $$ = BUILDER.term(@$, String::fromRep($a), $b, true); } 385 | VBAR[l] constterm[a] VBAR { $$ = BUILDER.term(@$, UnOp::ABS, $a); } 386 | identifier[a] { $$ = BUILDER.term(@$, Symbol::createId(String::fromRep($a))); } 387 | AT[l] identifier[a] { $$ = BUILDER.term(@$, String::fromRep($a), BUILDER.termvecvec(BUILDER.termvecvec(), BUILDER.termvec()), true); } 388 | NUMBER[a] { $$ = BUILDER.term(@$, Symbol::createNum($a)); } 389 | STRING[a] { $$ = BUILDER.term(@$, Symbol::createStr(String::fromRep($a))); } 390 | INFIMUM[a] { $$ = BUILDER.term(@$, Symbol::createInf()); } 391 | SUPREMUM[a] { $$ = BUILDER.term(@$, Symbol::createSup()); } 392 ; 393 394// {{{2 arguments lists for functions in constant terms 395 396consttermvec 397 : constterm[a] { $$ = BUILDER.termvec(BUILDER.termvec(), $a); } 398 | consttermvec[a] COMMA constterm[b] { $$ = BUILDER.termvec($a, $b); } 399 ; 400 401constargvec 402 : consttermvec[a] { $$ = BUILDER.termvecvec(BUILDER.termvecvec(), $a); } 403 | { $$ = BUILDER.termvecvec(BUILDER.termvecvec(), BUILDER.termvec()); } 404 ; 405 406// {{{2 terms including variables 407 408term 409 : term[a] DOTS term[b] { $$ = BUILDER.term(@$, $a, $b); } 410 | term[a] XOR term[b] { $$ = BUILDER.term(@$, BinOp::XOR, $a, $b); } 411 | term[a] QUESTION term[b] { $$ = BUILDER.term(@$, BinOp::OR, $a, $b); } 412 | term[a] AND term[b] { $$ = BUILDER.term(@$, BinOp::AND, $a, $b); } 413 | term[a] ADD term[b] { $$ = BUILDER.term(@$, BinOp::ADD, $a, $b); } 414 | term[a] SUB term[b] { $$ = BUILDER.term(@$, BinOp::SUB, $a, $b); } 415 | term[a] MUL term[b] { $$ = BUILDER.term(@$, BinOp::MUL, $a, $b); } 416 | term[a] SLASH term[b] { $$ = BUILDER.term(@$, BinOp::DIV, $a, $b); } 417 | term[a] MOD term[b] { $$ = BUILDER.term(@$, BinOp::MOD, $a, $b); } 418 | term[a] POW term[b] { $$ = BUILDER.term(@$, BinOp::POW, $a, $b); } 419 | SUB term[a] %prec UMINUS { $$ = BUILDER.term(@$, UnOp::NEG, $a); } 420 | BNOT term[a] %prec UBNOT { $$ = BUILDER.term(@$, UnOp::NOT, $a); } 421 | LPAREN tuplevec[a] RPAREN { $$ = BUILDER.pool(@$, $a); } 422 | identifier[a] LPAREN argvec[b] RPAREN { $$ = BUILDER.term(@$, String::fromRep($a), $b, false); } 423 | AT identifier[a] LPAREN argvec[b] RPAREN { $$ = BUILDER.term(@$, String::fromRep($a), $b, true); } 424 | VBAR unaryargvec[a] VBAR { $$ = BUILDER.term(@$, UnOp::ABS, $a); } 425 | identifier[a] { $$ = BUILDER.term(@$, Symbol::createId(String::fromRep($a))); } 426 | AT[l] identifier[a] { $$ = BUILDER.term(@$, String::fromRep($a), BUILDER.termvecvec(BUILDER.termvecvec(), BUILDER.termvec()), true); } 427 | NUMBER[a] { $$ = BUILDER.term(@$, Symbol::createNum($a)); } 428 | STRING[a] { $$ = BUILDER.term(@$, Symbol::createStr(String::fromRep($a))); } 429 | INFIMUM[a] { $$ = BUILDER.term(@$, Symbol::createInf()); } 430 | SUPREMUM[a] { $$ = BUILDER.term(@$, Symbol::createSup()); } 431 | VARIABLE[a] { $$ = BUILDER.term(@$, String::fromRep($a)); } 432 | ANONYMOUS[a] { $$ = BUILDER.term(@$, String("_")); } 433 ; 434 435// {{{2 argument lists for unary operations 436 437unaryargvec 438 : term[a] { $$ = BUILDER.termvec(BUILDER.termvec(), $a); } 439 | unaryargvec[a] SEM term[b] { $$ = BUILDER.termvec($a, $b); } 440 ; 441 442// {{{2 argument lists for functions 443 444ntermvec 445 : term[a] { $$ = BUILDER.termvec(BUILDER.termvec(), $a); } 446 | ntermvec[a] COMMA term[b] { $$ = BUILDER.termvec($a, $b); } 447 ; 448 449termvec 450 : ntermvec[a] { $$ = $a; } 451 | { $$ = BUILDER.termvec(); } 452 ; 453 454tuple 455 : ntermvec[a] COMMA { $$ = BUILDER.term(@$, $a, true); } 456 | ntermvec[a] { $$ = BUILDER.term(@$, $a, false); } 457 | COMMA { $$ = BUILDER.term(@$, BUILDER.termvec(), true); } 458 | { $$ = BUILDER.term(@$, BUILDER.termvec(), false); } 459 460tuplevec_sem 461 : tuple[b] SEM { $$ = BUILDER.termvec(BUILDER.termvec(), $b); } 462 | tuplevec_sem[a] tuple[b] SEM { $$ = BUILDER.termvec($a, $b); } 463 464tuplevec 465 : tuple[b] { $$ = BUILDER.termvec(BUILDER.termvec(), $b); } 466 | tuplevec_sem[a] tuple[b] { $$ = BUILDER.termvec($a, $b); } 467 468argvec 469 : termvec[b] { $$ = BUILDER.termvecvec(BUILDER.termvecvec(), $b); } 470 | argvec[a] SEM termvec[b] { $$ = BUILDER.termvecvec($a, $b); } 471 ; 472 473binaryargvec 474 : term[a] COMMA term[b] { $$ = BUILDER.termvecvec(BUILDER.termvecvec(), BUILDER.termvec(BUILDER.termvec(BUILDER.termvec(), $a), $b)); } 475 | binaryargvec[vec] SEM term[a] COMMA term[b] { $$ = BUILDER.termvecvec($vec, BUILDER.termvec(BUILDER.termvec(BUILDER.termvec(), $a), $b)); } 476 ; 477 478// TODO: I might have to create tuples differently 479// parse a tuple as a list of terms 480// each term is either a tuple or a term -> which afterwards is turned into a pool! 481 482// {{{1 literals 483 484cmp 485 : GT { $$ = Relation::GT; } 486 | LT { $$ = Relation::LT; } 487 | GEQ { $$ = Relation::GEQ; } 488 | LEQ { $$ = Relation::LEQ; } 489 | EQ { $$ = Relation::EQ; } 490 | NEQ { $$ = Relation::NEQ; } 491 ; 492 493atom 494 : identifier[id] { $$ = BUILDER.predRep(@$, false, String::fromRep($id), BUILDER.termvecvec(BUILDER.termvecvec(), BUILDER.termvec())); } 495 | identifier[id] LPAREN argvec[tvv] RPAREN[r] { $$ = BUILDER.predRep(@$, false, String::fromRep($id), $tvv); } 496 | SUB identifier[id] { $$ = BUILDER.predRep(@$, true, String::fromRep($id), BUILDER.termvecvec(BUILDER.termvecvec(), BUILDER.termvec())); } 497 | SUB identifier[id] LPAREN argvec[tvv] RPAREN[r] { $$ = BUILDER.predRep(@$, true, String::fromRep($id), $tvv); } 498 ; 499 500literal 501 : TRUE { $$ = BUILDER.boollit(@$, true); } 502 | NOT TRUE { $$ = BUILDER.boollit(@$, false); } 503 | NOT NOT TRUE { $$ = BUILDER.boollit(@$, true); } 504 | FALSE { $$ = BUILDER.boollit(@$, false); } 505 | NOT FALSE { $$ = BUILDER.boollit(@$, true); } 506 | NOT NOT FALSE { $$ = BUILDER.boollit(@$, false); } 507 | atom[a] { $$ = BUILDER.predlit(@$, NAF::POS, $a); } 508 | NOT atom[a] { $$ = BUILDER.predlit(@$, NAF::NOT, $a); } 509 | NOT NOT atom[a] { $$ = BUILDER.predlit(@$, NAF::NOTNOT, $a); } 510 | term[l] cmp[rel] term[r] { $$ = BUILDER.rellit(@$, $rel, $l, $r); } 511 | NOT term[l] cmp[rel] term[r] { $$ = BUILDER.rellit(@$, neg($rel), $l, $r); } 512 | NOT NOT term[l] cmp[rel] term[r] { $$ = BUILDER.rellit(@$, $rel, $l, $r); } 513 | csp_literal[lit] { $$ = BUILDER.csplit($lit); } 514 ; 515 516csp_mul_term 517 : CSP term[var] CSP_MUL term[coe] { $$ = BUILDER.cspmulterm(@$, $coe, $var); } 518 | term[coe] CSP_MUL CSP term[var] { $$ = BUILDER.cspmulterm(@$, $coe, $var); } 519 | CSP term[var] { $$ = BUILDER.cspmulterm(@$, BUILDER.term(@$, Symbol::createNum(1)), $var); } 520 | term[coe] { $$ = BUILDER.cspmulterm(@$, $coe); } 521 ; 522 523csp_add_term 524 : csp_add_term[add] CSP_ADD csp_mul_term[mul] { $$ = BUILDER.cspaddterm(@$, $add, $mul, true); } 525 | csp_add_term[add] CSP_SUB csp_mul_term[mul] { $$ = BUILDER.cspaddterm(@$, $add, $mul, false); } 526 | csp_mul_term[mul] { $$ = BUILDER.cspaddterm(@$, $mul); } 527 ; 528 529csp_rel 530 : CSP_GT { $$ = Relation::GT; } 531 | CSP_LT { $$ = Relation::LT; } 532 | CSP_GEQ { $$ = Relation::GEQ; } 533 | CSP_LEQ { $$ = Relation::LEQ; } 534 | CSP_EQ { $$ = Relation::EQ; } 535 | CSP_NEQ { $$ = Relation::NEQ; } 536 ; 537 538csp_literal 539 : csp_literal[lit] csp_rel[rel] csp_add_term[b] { $$ = BUILDER.csplit(@$, $lit, $rel, $b); } 540 | csp_add_term[a] csp_rel[rel] csp_add_term[b] { $$ = BUILDER.csplit(@$, $a, $rel, $b); } 541 ; 542 543// {{{1 aggregates 544 545// {{{2 auxiliary rules 546 547nlitvec 548 : literal[lit] { $$ = BUILDER.litvec(BUILDER.litvec(), $lit); } 549 | nlitvec[vec] COMMA literal[lit] { $$ = BUILDER.litvec($vec, $lit); } 550 ; 551 552litvec 553 : nlitvec[vec] { $$ = $vec; } 554 | { $$ = BUILDER.litvec(); } 555 ; 556 557optcondition 558 : COLON litvec[vec] { $$ = $vec; } 559 | { $$ = BUILDER.litvec(); } 560 ; 561 562aggregatefunction 563 : SUM { $$ = AggregateFunction::SUM; } 564 | SUMP { $$ = AggregateFunction::SUMP; } 565 | MIN { $$ = AggregateFunction::MIN; } 566 | MAX { $$ = AggregateFunction::MAX; } 567 | COUNT { $$ = AggregateFunction::COUNT; } 568 ; 569 570// {{{2 body aggregate elements 571 572bodyaggrelem 573 : COLON litvec[cond] { $$ = { BUILDER.termvec(), $cond }; } 574 | ntermvec[args] optcondition[cond] { $$ = { $args, $cond }; } 575 ; 576 577bodyaggrelemvec 578 : bodyaggrelem[elem] { $$ = BUILDER.bodyaggrelemvec(BUILDER.bodyaggrelemvec(), $elem.first, $elem.second); } 579 | bodyaggrelemvec[vec] SEM bodyaggrelem[elem] { $$ = BUILDER.bodyaggrelemvec($vec, $elem.first, $elem.second); } 580 ; 581 582// Note: alternative syntax (without weight) 583 584altbodyaggrelem 585 : literal[lit] optcondition[cond] { $$ = { $lit, $cond }; } 586 ; 587 588altbodyaggrelemvec 589 : altbodyaggrelem[elem] { $$ = BUILDER.condlitvec(BUILDER.condlitvec(), $elem.first, $elem.second); } 590 | altbodyaggrelemvec[vec] SEM altbodyaggrelem[elem] { $$ = BUILDER.condlitvec($vec, $elem.first, $elem.second); } 591 ; 592 593// {{{2 body aggregates 594 595bodyaggregate 596 : LBRACE RBRACE { $$ = { AggregateFunction::COUNT, true, BUILDER.condlitvec() }; } 597 | LBRACE altbodyaggrelemvec[elems] RBRACE { $$ = { AggregateFunction::COUNT, true, $elems }; } 598 | aggregatefunction[fun] LBRACE RBRACE { $$ = { $fun, false, BUILDER.bodyaggrelemvec() }; } 599 | aggregatefunction[fun] LBRACE bodyaggrelemvec[elems] RBRACE { $$ = { $fun, false, $elems }; } 600 ; 601 602upper 603 : term[t] { $$ = { Relation::LEQ, $t }; } 604 | cmp[rel] term[t] { $$ = { $rel, $t }; } 605 | { $$ = { Relation::LEQ, TermUid(-1) }; } 606 ; 607 608lubodyaggregate 609 : term[l] bodyaggregate[a] upper[u] { $$ = lexer->aggregate($a.fun, $a.choice, $a.elems, lexer->boundvec(Relation::LEQ, $l, $u.rel, $u.term)); } 610 | term[l] cmp[rel] bodyaggregate[a] upper[u] { $$ = lexer->aggregate($a.fun, $a.choice, $a.elems, lexer->boundvec($rel, $l, $u.rel, $u.term)); } 611 | bodyaggregate[a] upper[u] { $$ = lexer->aggregate($a.fun, $a.choice, $a.elems, lexer->boundvec(Relation::LEQ, TermUid(-1), $u.rel, $u.term)); } 612 | theory_atom[atom] { $$ = lexer->aggregate($atom); } 613 ; 614 615// {{{2 head aggregate elements 616 617headaggrelemvec 618 : headaggrelemvec[vec] SEM termvec[tuple] COLON literal[head] optcondition[cond] { $$ = BUILDER.headaggrelemvec($vec, $tuple, $head, $cond); } 619 | termvec[tuple] COLON literal[head] optcondition[cond] { $$ = BUILDER.headaggrelemvec(BUILDER.headaggrelemvec(), $tuple, $head, $cond); } 620 ; 621 622altheadaggrelemvec 623 : literal[lit] optcondition[cond] { $$ = BUILDER.condlitvec(BUILDER.condlitvec(), $lit, $cond); } 624 | altheadaggrelemvec[vec] SEM literal[lit] optcondition[cond] { $$ = BUILDER.condlitvec($vec, $lit, $cond); } 625 ; 626 627// {{{2 head aggregates 628 629headaggregate 630 : aggregatefunction[fun] LBRACE RBRACE { $$ = { $fun, false, BUILDER.headaggrelemvec() }; } 631 | aggregatefunction[fun] LBRACE headaggrelemvec[elems] RBRACE { $$ = { $fun, false, $elems }; } 632 | LBRACE RBRACE { $$ = { AggregateFunction::COUNT, true, BUILDER.condlitvec()}; } 633 | LBRACE altheadaggrelemvec[elems] RBRACE { $$ = { AggregateFunction::COUNT, true, $elems}; } 634 ; 635 636luheadaggregate 637 : term[l] headaggregate[a] upper[u] { $$ = lexer->aggregate($a.fun, $a.choice, $a.elems, lexer->boundvec(Relation::LEQ, $l, $u.rel, $u.term)); } 638 | term[l] cmp[rel] headaggregate[a] upper[u] { $$ = lexer->aggregate($a.fun, $a.choice, $a.elems, lexer->boundvec($rel, $l, $u.rel, $u.term)); } 639 | headaggregate[a] upper[u] { $$ = lexer->aggregate($a.fun, $a.choice, $a.elems, lexer->boundvec(Relation::LEQ, TermUid(-1), $u.rel, $u.term)); } 640 | theory_atom[atom] { $$ = lexer->aggregate($atom); } 641 ; 642 643// {{{2 disjoint aggregate 644 645ncspelemvec 646 : termvec[tuple] COLON csp_add_term[add] optcondition[cond] { $$ = BUILDER.cspelemvec(BUILDER.cspelemvec(), @$, $tuple, $add, $cond); } 647 | cspelemvec[vec] SEM termvec[tuple] COLON csp_add_term[add] optcondition[cond] { $$ = BUILDER.cspelemvec($vec, @$, $tuple, $add, $cond); } 648 ; 649 650cspelemvec 651 : ncspelemvec[vec] { $$ = $vec; } 652 | { $$ = BUILDER.cspelemvec(); } 653 ; 654 655disjoint 656 : DISJOINT LBRACE cspelemvec[elems] RBRACE { $$ = { NAF::POS, $elems }; } 657 | NOT DISJOINT LBRACE cspelemvec[elems] RBRACE { $$ = { NAF::NOT, $elems }; } 658 | NOT NOT DISJOINT LBRACE cspelemvec[elems] RBRACE { $$ = { NAF::NOTNOT, $elems }; } 659 ; 660 661///}}} 662// {{{2 conjunctions 663 664conjunction 665 : literal[lit] COLON litvec[cond] { $$ = { $lit, $cond }; } 666 ; 667 668// }}} 669// {{{2 disjunctions 670 671dsym 672 : SEM 673 | VBAR 674 ; 675 676// NOTE: this is so complicated because VBAR is also used as the absolute function for terms 677// due to limited lookahead I found no reasonable way to parse p(X):|q(X) 678disjunctionsep 679 : disjunctionsep[vec] literal[lit] COMMA { $$ = BUILDER.condlitvec($vec, $lit, BUILDER.litvec()); } 680 | disjunctionsep[vec] literal[lit] dsym { $$ = BUILDER.condlitvec($vec, $lit, BUILDER.litvec()); } 681 | disjunctionsep[vec] literal[lit] COLON SEM { $$ = BUILDER.condlitvec($vec, $lit, BUILDER.litvec()); } 682 | disjunctionsep[vec] literal[lit] COLON nlitvec[cond] dsym { $$ = BUILDER.condlitvec($vec, $lit, $cond); } 683 | literal[lit] COMMA { $$ = BUILDER.condlitvec(BUILDER.condlitvec(), $lit, BUILDER.litvec()); } 684 | literal[lit] dsym { $$ = BUILDER.condlitvec(BUILDER.condlitvec(), $lit, BUILDER.litvec()); } 685 | literal[lit] COLON nlitvec[cond] dsym { $$ = BUILDER.condlitvec(BUILDER.condlitvec(), $lit, $cond); } 686 | literal[lit] COLON SEM { $$ = BUILDER.condlitvec(BUILDER.condlitvec(), $lit, BUILDER.litvec()); } 687 ; 688 689disjunction 690 : disjunctionsep[vec] literal[lit] optcondition[cond] { $$ = BUILDER.condlitvec($vec, $lit, $cond); } 691 | literal[lit] COLON litvec[cond] { $$ = BUILDER.condlitvec(BUILDER.condlitvec(), $lit, $cond); } 692 ; 693 694// {{{1 statements 695// {{{2 rules 696 697bodycomma 698 : bodycomma[body] literal[lit] COMMA { $$ = BUILDER.bodylit($body, $lit); } 699 | bodycomma[body] literal[lit] SEM { $$ = BUILDER.bodylit($body, $lit); } 700 | bodycomma[body] lubodyaggregate[aggr] COMMA { $$ = lexer->bodyaggregate($body, @aggr, NAF::POS, $aggr); } 701 | bodycomma[body] lubodyaggregate[aggr] SEM { $$ = lexer->bodyaggregate($body, @aggr, NAF::POS, $aggr); } 702 | bodycomma[body] NOT[l] lubodyaggregate[aggr] COMMA { $$ = lexer->bodyaggregate($body, @aggr + @l, NAF::NOT, $aggr); } 703 | bodycomma[body] NOT[l] lubodyaggregate[aggr] SEM { $$ = lexer->bodyaggregate($body, @aggr + @l, NAF::NOT, $aggr); } 704 | bodycomma[body] NOT[l] NOT lubodyaggregate[aggr] COMMA { $$ = lexer->bodyaggregate($body, @aggr + @l, NAF::NOTNOT, $aggr); } 705 | bodycomma[body] NOT[l] NOT lubodyaggregate[aggr] SEM { $$ = lexer->bodyaggregate($body, @aggr + @l, NAF::NOTNOT, $aggr); } 706 | bodycomma[body] conjunction[conj] SEM { $$ = BUILDER.conjunction($body, @conj, $conj.first, $conj.second); } 707 | bodycomma[body] disjoint[cons] SEM { $$ = BUILDER.disjoint($body, @cons, $cons.first, $cons.second); } 708 | { $$ = BUILDER.body(); } 709 ; 710 711bodydot 712 : bodycomma[body] literal[lit] DOT { $$ = BUILDER.bodylit($body, $lit); } 713 | bodycomma[body] lubodyaggregate[aggr] DOT { $$ = lexer->bodyaggregate($body, @aggr, NAF::POS, $aggr); } 714 | bodycomma[body] NOT[l] lubodyaggregate[aggr] DOT { $$ = lexer->bodyaggregate($body, @aggr + @l, NAF::NOT, $aggr); } 715 | bodycomma[body] NOT[l] NOT lubodyaggregate[aggr] DOT { $$ = lexer->bodyaggregate($body, @aggr + @l, NAF::NOTNOT, $aggr); } 716 | bodycomma[body] conjunction[conj] DOT { $$ = BUILDER.conjunction($body, @conj, $conj.first, $conj.second); } 717 | bodycomma[body] disjoint[cons] DOT { $$ = BUILDER.disjoint($body, @cons, $cons.first, $cons.second); } 718 ; 719 720bodyconddot 721 : DOT { $$ = BUILDER.body(); } 722 | COLON DOT { $$ = BUILDER.body(); } 723 | COLON bodydot[body] { $$ = $body; } 724 725head 726 : literal[lit] { $$ = BUILDER.headlit($lit); } 727 | disjunction[elems] { $$ = BUILDER.disjunction(@$, $elems); } 728 | luheadaggregate[aggr] { $$ = lexer->headaggregate(@$, $aggr); } 729 ; 730 731statement 732 : head[hd] DOT { BUILDER.rule(@$, $hd); } 733 | head[hd] IF DOT { BUILDER.rule(@$, $hd); } 734 | head[hd] IF bodydot[bd] { BUILDER.rule(@$, $hd, $bd); } 735 | IF bodydot[bd] { BUILDER.rule(@$, BUILDER.headlit(BUILDER.boollit(@$, false)), $bd); } 736 | IF DOT { BUILDER.rule(@$, BUILDER.headlit(BUILDER.boollit(@$, false)), BUILDER.body()); } 737 ; 738 739// {{{2 CSP 740 741statement 742 : disjoint[hd] IF bodydot[body] { BUILDER.rule(@$, BUILDER.headlit(BUILDER.boollit(@hd, false)), BUILDER.disjoint($body, @hd, inv($hd.first), $hd.second)); } 743 | disjoint[hd] IF DOT { BUILDER.rule(@$, BUILDER.headlit(BUILDER.boollit(@hd, false)), BUILDER.disjoint(BUILDER.body(), @hd, inv($hd.first), $hd.second)); } 744 | disjoint[hd] DOT { BUILDER.rule(@$, BUILDER.headlit(BUILDER.boollit(@hd, false)), BUILDER.disjoint(BUILDER.body(), @hd, inv($hd.first), $hd.second)); } 745 ; 746 747// {{{2 optimization 748 749optimizetuple 750 : COMMA ntermvec[vec] { $$ = $vec; } 751 | { $$ = BUILDER.termvec(); } 752 ; 753 754optimizeweight 755 : term[w] AT term[p] { $$ = {$w, $p}; } 756 | term[w] { $$ = {$w, BUILDER.term(@$, Symbol::createNum(0))}; } 757 ; 758 759optimizelitvec 760 : literal[lit] { $$ = BUILDER.bodylit(BUILDER.body(), $lit); } 761 | optimizelitvec[bd] COMMA literal[lit] { $$ = BUILDER.bodylit($bd, $lit); } 762 ; 763 764optimizecond 765 : COLON optimizelitvec[bd] { $$ = $bd; } 766 | COLON { $$ = BUILDER.body(); } 767 | { $$ = BUILDER.body(); } 768 ; 769 770statement 771 : WIF bodydot[bd] LBRACK optimizeweight[w] optimizetuple[t] RBRACK { BUILDER.optimize(@$, $w.first, $w.second, $t, $bd); } 772 | WIF DOT LBRACK optimizeweight[w] optimizetuple[t] RBRACK { BUILDER.optimize(@$, $w.first, $w.second, $t, BUILDER.body()); } 773 ; 774 775maxelemlist 776 : optimizeweight[w] optimizetuple[t] optimizecond[bd] { BUILDER.optimize(@$, BUILDER.term(@w, UnOp::NEG, $w.first), $w.second, $t, $bd); } 777 | maxelemlist SEM optimizeweight[w] optimizetuple[t] optimizecond[bd] { BUILDER.optimize(@$, BUILDER.term(@w, UnOp::NEG, $w.first), $w.second, $t, $bd); } 778 ; 779 780minelemlist 781 : optimizeweight[w] optimizetuple[t] optimizecond[bd] { BUILDER.optimize(@$, $w.first, $w.second, $t, $bd); } 782 | minelemlist SEM optimizeweight[w] optimizetuple[t] optimizecond[bd] { BUILDER.optimize(@$, $w.first, $w.second, $t, $bd); } 783 ; 784 785statement 786 : MINIMIZE LBRACE RBRACE DOT 787 | MAXIMIZE LBRACE RBRACE DOT 788 | MINIMIZE LBRACE minelemlist RBRACE DOT 789 | MAXIMIZE LBRACE maxelemlist RBRACE DOT 790 ; 791 792// {{{2 visibility 793 794statement 795 : SHOWSIG identifier[id] SLASH NUMBER[num] DOT { BUILDER.showsig(@$, Sig(String::fromRep($id), $num, false), false); } 796 | SHOWSIG SUB identifier[id] SLASH NUMBER[num] DOT { BUILDER.showsig(@$, Sig(String::fromRep($id), $num, true), false); } 797 | SHOW DOT { BUILDER.showsig(@$, Sig("", 0, false), false); } 798 | SHOW term[t] COLON bodydot[bd] { BUILDER.show(@$, $t, $bd, false); } 799 | SHOW term[t] DOT { BUILDER.show(@$, $t, BUILDER.body(), false); } 800 | SHOWSIG CSP identifier[id] SLASH NUMBER[num] DOT { BUILDER.showsig(@$, Sig(String::fromRep($id), $num, false), true); } 801 | SHOW CSP term[t] COLON bodydot[bd] { BUILDER.show(@$, $t, $bd, true); } 802 | SHOW CSP term[t] DOT { BUILDER.show(@$, $t, BUILDER.body(), true); } 803 ; 804 805// {{{2 warnings 806 807statement 808 : DEFINED identifier[id] SLASH NUMBER[num] DOT { BUILDER.defined(@$, Sig(String::fromRep($id), $num, false)); } 809 | DEFINED SUB identifier[id] SLASH NUMBER[num] DOT { BUILDER.defined(@$, Sig(String::fromRep($id), $num, true)); } 810 811// {{{2 acyclicity 812 813statement 814 : EDGE LPAREN binaryargvec[args] RPAREN bodyconddot[body] { BUILDER.edge(@$, $args, $body); } 815 ; 816 817// {{{2 heuristic 818 819statement 820 : HEURISTIC atom[a] bodyconddot[body] LBRACK term[t] AT term[p] COMMA term[mod] RBRACK { BUILDER.heuristic(@$, $a, $body, $t, $p, $mod); } 821 | HEURISTIC atom[a] bodyconddot[body] LBRACK term[t] COMMA term[mod] RBRACK { BUILDER.heuristic(@$, $a, $body, $t, BUILDER.term(@$, Symbol::createNum(0)), $mod); } 822 ; 823 824// {{{2 project 825 826statement 827 : PROJECT identifier[name] SLASH NUMBER[arity] DOT { BUILDER.project(@$, Sig(String::fromRep($name), $arity, false)); } 828 | PROJECT SUB identifier[name] SLASH NUMBER[arity] DOT { BUILDER.project(@$, Sig(String::fromRep($name), $arity, true)); } 829 | PROJECT atom[a] bodyconddot[body] { BUILDER.project(@$, $a, $body); } 830 ; 831 832// {{{2 constants 833 834define 835 : identifier[uid] EQ constterm[rhs] { BUILDER.define(@$, String::fromRep($uid), $rhs, false, LOGGER); } 836 ; 837 838statement 839 : CONST identifier[uid] EQ constterm[rhs] DOT { BUILDER.define(@$, String::fromRep($uid), $rhs, true, LOGGER); } 840 | CONST identifier[uid] EQ constterm[rhs] DOT LBRACK DEFAULT RBRACK { BUILDER.define(@$, String::fromRep($uid), $rhs, true, LOGGER); } 841 | CONST identifier[uid] EQ constterm[rhs] DOT LBRACK OVERRIDE RBRACK { BUILDER.define(@$, String::fromRep($uid), $rhs, false, LOGGER); } 842 ; 843 844// {{{2 scripts 845 846statement 847 : SCRIPT LPAREN IDENTIFIER[type] RPAREN CODE[code] DOT { BUILDER.script(@$, String::fromRep($type), String::fromRep($code)); } 848 ; 849 850// {{{2 include 851 852statement 853 : INCLUDE STRING[file] DOT { lexer->include(String::fromRep($file), @$, false, LOGGER); } 854 | INCLUDE LT identifier[file] GT DOT { lexer->include(String::fromRep($file), @$, true, LOGGER); } 855 ; 856 857// {{{2 blocks 858 859nidlist 860 : nidlist[list] COMMA identifier[id] { $$ = BUILDER.idvec($list, @id, String::fromRep($id)); } 861 | identifier[id] { $$ = BUILDER.idvec(BUILDER.idvec(), @id, String::fromRep($id)); } 862 ; 863 864idlist 865 : { $$ = BUILDER.idvec(); } 866 | nidlist[list] { $$ = $list; } 867 ; 868 869statement 870 : BLOCK identifier[name] LPAREN idlist[args] RPAREN DOT { BUILDER.block(@$, String::fromRep($name), $args); } 871 | BLOCK identifier[name] DOT { BUILDER.block(@$, String::fromRep($name), BUILDER.idvec()); } 872 ; 873 874// {{{2 external 875 876statement 877 : EXTERNAL atom[hd] COLON bodydot[bd] { BUILDER.external(@$, $hd, $bd, BUILDER.term(@$, Symbol::createId("false"))); } 878 | EXTERNAL atom[hd] COLON DOT { BUILDER.external(@$, $hd, BUILDER.body(), BUILDER.term(@$, Symbol::createId("false"))); } 879 | EXTERNAL atom[hd] DOT { BUILDER.external(@$, $hd, BUILDER.body(), BUILDER.term(@$, Symbol::createId("false"))); } 880 | EXTERNAL atom[hd] COLON bodydot[bd] LBRACK term[t] RBRACK { BUILDER.external(@$, $hd, $bd, $t); } 881 | EXTERNAL atom[hd] COLON DOT LBRACK term[t] RBRACK { BUILDER.external(@$, $hd, BUILDER.body(), $t); } 882 | EXTERNAL atom[hd] DOT LBRACK term[t] RBRACK { BUILDER.external(@$, $hd, BUILDER.body(), $t); } 883 ; 884 885// {{{1 theory 886 887theory_op 888 : THEORY_OP[op] { $$ = $op; } 889 | NOT[not] { $$ = $not; } 890 ; 891 892// {{{2 theory atoms 893 894theory_op_list 895 : theory_op_list[ops] theory_op[op] { $$ = BUILDER.theoryops($ops, String::fromRep($op)); } 896 | theory_op[op] { $$ = BUILDER.theoryops(BUILDER.theoryops(), String::fromRep($op)); } 897 ; 898 899theory_term 900 : LBRACE theory_opterm_list[list] RBRACE { $$ = BUILDER.theorytermset(@$, $list); } 901 | LBRACK theory_opterm_list[list] RBRACK { $$ = BUILDER.theoryoptermlist(@$, $list); } 902 | LPAREN RPAREN { $$ = BUILDER.theorytermtuple(@$, BUILDER.theoryopterms()); } 903 | LPAREN theory_opterm[term] RPAREN { $$ = BUILDER.theorytermopterm(@$, $term); } 904 | LPAREN theory_opterm[opterm] COMMA RPAREN { $$ = BUILDER.theorytermtuple(@$, BUILDER.theoryopterms(BUILDER.theoryopterms(), @opterm, $opterm)); } 905 | LPAREN theory_opterm[opterm] COMMA theory_opterm_nlist[list] RPAREN { $$ = BUILDER.theorytermtuple(@$, BUILDER.theoryopterms(@opterm, $opterm, $list)); } 906 | identifier[id] LPAREN theory_opterm_list[list] RPAREN { $$ = BUILDER.theorytermfun(@$, String::fromRep($id), $list); } 907 | identifier[id] { $$ = BUILDER.theorytermvalue(@$, Symbol::createId(String::fromRep($id))); } 908 | NUMBER[num] { $$ = BUILDER.theorytermvalue(@$, Symbol::createNum($num)); } 909 | STRING[str] { $$ = BUILDER.theorytermvalue(@$, Symbol::createStr(String::fromRep($str))); } 910 | INFIMUM { $$ = BUILDER.theorytermvalue(@$, Symbol::createInf()); } 911 | SUPREMUM { $$ = BUILDER.theorytermvalue(@$, Symbol::createSup()); } 912 | VARIABLE[var] { $$ = BUILDER.theorytermvar(@$, String::fromRep($var)); } 913 ; 914 915theory_opterm 916 : theory_opterm[opterm] theory_op_list[ops] theory_term[term] { $$ = BUILDER.theoryopterm($opterm, $ops, $term); } 917 | theory_op_list[ops] theory_term[term] { $$ = BUILDER.theoryopterm($ops, $term); } 918 | theory_term[term] { $$ = BUILDER.theoryopterm(BUILDER.theoryops(), $term); } 919 ; 920 921theory_opterm_nlist 922 : theory_opterm_nlist[list] COMMA theory_opterm[opterm] { $$ = BUILDER.theoryopterms($list, @opterm, $opterm); } 923 | theory_opterm[opterm] { $$ = BUILDER.theoryopterms(BUILDER.theoryopterms(), @opterm, $opterm); } 924 ; 925 926theory_opterm_list 927 : theory_opterm_nlist[list] { $$ = $list; } 928 | { $$ = BUILDER.theoryopterms(); } 929 ; 930 931theory_atom_element 932 : theory_opterm_nlist[list] disable_theory_lexing optcondition[cond] { $$ = { $list, $cond }; } 933 | disable_theory_lexing COLON litvec[cond] { $$ = { BUILDER.theoryopterms(), $cond }; } 934 ; 935 936theory_atom_element_nlist 937 : theory_atom_element_nlist[list] enable_theory_lexing SEM theory_atom_element[elem] { $$ = BUILDER.theoryelems($list, $elem.first, $elem.second); } 938 | theory_atom_element[elem] { $$ = BUILDER.theoryelems(BUILDER.theoryelems(), $elem.first, $elem.second); } 939 ; 940 941theory_atom_element_list 942 : theory_atom_element_nlist[list] { $$ = $list; } 943 | { $$ = BUILDER.theoryelems(); } 944 ; 945 946theory_atom_name 947 : identifier[id] { $$ = BUILDER.term(@$, String::fromRep($id), BUILDER.termvecvec(BUILDER.termvecvec(), BUILDER.termvec()), false); } 948 | identifier[id] LPAREN argvec[tvv] RPAREN[r] { $$ = BUILDER.term(@$, String::fromRep($id), $tvv, false); } 949 950theory_atom 951 : AND theory_atom_name[name] { $$ = BUILDER.theoryatom($name, BUILDER.theoryelems()); } 952 | AND theory_atom_name[name] enable_theory_lexing LBRACE theory_atom_element_list[elems] enable_theory_lexing RBRACE disable_theory_lexing { $$ = BUILDER.theoryatom($name, $elems); } 953 | AND theory_atom_name[name] enable_theory_lexing LBRACE theory_atom_element_list[elems] enable_theory_lexing RBRACE theory_op[op] theory_opterm[opterm] disable_theory_lexing { $$ = BUILDER.theoryatom($name, $elems, String::fromRep($op), @opterm, $opterm); } 954 ; 955 956// {{{2 theory definition 957 958theory_operator_nlist 959 : theory_op[op] { $$ = BUILDER.theoryops(BUILDER.theoryops(), String::fromRep($op)); } 960 | theory_operator_nlist[ops] COMMA theory_op[op] { $$ = BUILDER.theoryops($ops, String::fromRep($op)); } 961 ; 962 963theory_operator_list 964 : theory_operator_nlist[ops] { $$ = $ops; } 965 | { $$ = BUILDER.theoryops(); } 966 ; 967 968theory_operator_definition 969 : theory_op[op] enable_theory_definition_lexing COLON NUMBER[arity] COMMA UNARY { $$ = BUILDER.theoryopdef(@$, String::fromRep($op), $arity, TheoryOperatorType::Unary); } 970 | theory_op[op] enable_theory_definition_lexing COLON NUMBER[arity] COMMA BINARY COMMA LEFT { $$ = BUILDER.theoryopdef(@$, String::fromRep($op), $arity, TheoryOperatorType::BinaryLeft); } 971 | theory_op[op] enable_theory_definition_lexing COLON NUMBER[arity] COMMA BINARY COMMA RIGHT { $$ = BUILDER.theoryopdef(@$, String::fromRep($op), $arity, TheoryOperatorType::BinaryRight); } 972 ; 973 974theory_operator_definition_nlist 975 : theory_operator_definition[def] { $$ = BUILDER.theoryopdefs(BUILDER.theoryopdefs(), $def); } 976 | theory_operator_definition_nlist[defs] enable_theory_lexing SEM theory_operator_definition[def] { $$ = BUILDER.theoryopdefs($defs, $def); } 977 ; 978 979theory_operator_definiton_list 980 : theory_operator_definition_nlist[defs] { $$ = $defs; } 981 | { $$ = BUILDER.theoryopdefs(); } 982 ; 983 984theory_definition_identifier 985 : identifier[id] { $$ = $id; } 986 | LEFT { $$ = String::toRep("left"); } 987 | RIGHT { $$ = String::toRep("right"); } 988 | UNARY { $$ = String::toRep("unary"); } 989 | BINARY { $$ = String::toRep("binary"); } 990 | HEAD { $$ = String::toRep("head"); } 991 | BODY { $$ = String::toRep("body"); } 992 | ANY { $$ = String::toRep("any"); } 993 | DIRECTIVE { $$ = String::toRep("directive"); } 994 ; 995 996theory_term_definition 997 : theory_definition_identifier[name] enable_theory_lexing LBRACE theory_operator_definiton_list[ops] enable_theory_definition_lexing RBRACE { $$ = BUILDER.theorytermdef(@$, String::fromRep($name), $ops, LOGGER); } 998 ; 999 1000theory_atom_type 1001 : HEAD { $$ = TheoryAtomType::Head; } 1002 | BODY { $$ = TheoryAtomType::Body; } 1003 | ANY { $$ = TheoryAtomType::Any; } 1004 | DIRECTIVE { $$ = TheoryAtomType::Directive; } 1005 ; 1006 1007theory_atom_definition 1008 : AND theory_definition_identifier[name] SLASH NUMBER[arity] COLON theory_definition_identifier[termdef] COMMA 1009 enable_theory_lexing LBRACE theory_operator_list[ops] enable_theory_definition_lexing RBRACE COMMA theory_definition_identifier[guarddef] COMMA theory_atom_type[type] { $$ = BUILDER.theoryatomdef(@$, String::fromRep($name), $arity, String::fromRep($termdef), $type, $ops, String::fromRep($guarddef)); } 1010 | AND theory_definition_identifier[name] SLASH NUMBER[arity] COLON theory_definition_identifier[termdef] COMMA theory_atom_type[type] { $$ = BUILDER.theoryatomdef(@$, String::fromRep($name), $arity, String::fromRep($termdef), $type); } 1011 ; 1012 1013theory_definition_nlist 1014 : theory_definition_list[defs] SEM theory_atom_definition[def] { $$ = BUILDER.theorydefs($defs, $def); } 1015 | theory_definition_list[defs] SEM theory_term_definition[def] { $$ = BUILDER.theorydefs($defs, $def); } 1016 | theory_atom_definition[def] { $$ = BUILDER.theorydefs(BUILDER.theorydefs(), $def); } 1017 | theory_term_definition[def] { $$ = BUILDER.theorydefs(BUILDER.theorydefs(), $def); } 1018 ; 1019 1020theory_definition_list 1021 : theory_definition_nlist[defs] { $$ = $defs; } 1022 | { $$ = BUILDER.theorydefs(); } 1023 ; 1024 1025statement 1026 : THEORY identifier[name] enable_theory_definition_lexing LBRACE theory_definition_list[defs] RBRACE disable_theory_lexing DOT { BUILDER.theorydef(@$, String::fromRep($name), $defs, LOGGER); } 1027 ; 1028 1029// {{{2 lexing 1030 1031enable_theory_lexing 1032 : { lexer->theoryLexing(TheoryLexing::Theory); } 1033 ; 1034 1035enable_theory_definition_lexing 1036 : { lexer->theoryLexing(TheoryLexing::Definition); } 1037 ; 1038 1039disable_theory_lexing 1040 : { lexer->theoryLexing(TheoryLexing::Disabled); } 1041 ; 1042 1043// }}}1 1044