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