spot  2.10.5.dev
parsetl.hh
Go to the documentation of this file.
1 // A Bison parser, made by GNU Bison 3.8.2.
2 
3 // Skeleton interface for Bison LALR(1) parsers in C++
4 
5 // Copyright (C) 2002-2015, 2018-2021 Free Software Foundation, Inc.
6 
7 // This program is free software: you can redistribute it and/or modify
8 // it under the terms of the GNU General Public License as published by
9 // the Free Software Foundation, either version 3 of the License, or
10 // (at your option) any later version.
11 
12 // This program is distributed in the hope that it will be useful,
13 // but WITHOUT ANY WARRANTY; without even the implied warranty of
14 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 // GNU General Public License for more details.
16 
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <https://www.gnu.org/licenses/>.
19 
20 // As a special exception, you may create a larger work that contains
21 // part or all of the Bison parser skeleton and distribute that work
22 // under terms of your choice, so long as that work isn't itself a
23 // parser generator using the skeleton or a modified version thereof
24 // as a parser skeleton. Alternatively, if you modify or redistribute
25 // the parser skeleton itself, you may (at your option) remove this
26 // special exception, which will cause the skeleton and the resulting
27 // Bison output files to be licensed under the GNU General Public
28 // License without this special exception.
29 
30 // This special exception was added by the Free Software Foundation in
31 // version 2.2 of Bison.
32 
33 
39 // C++ LALR(1) parser skeleton written by Akim Demaille.
40 
41 // DO NOT RELY ON FEATURES THAT ARE NOT DOCUMENTED in the manual,
42 // especially those whose name start with YY_ or yy_. They are
43 // private implementation details that can be changed or removed.
44 
45 #ifndef YY_TLYY_PARSETL_HH_INCLUDED
46 # define YY_TLYY_PARSETL_HH_INCLUDED
47 // "%code requires" blocks.
48 #line 37 "parsetl.yy"
49 
50 #include "config.h"
51 #include <string>
52 #include <sstream>
53 #include <variant>
54 #include <spot/tl/parse.hh>
55 #include <spot/tl/formula.hh>
56 #include <spot/tl/print.hh>
57 
58  struct minmax_t { unsigned min, max; };
59 
60  // pnode (parsing node) is simular to fnode (formula node) except
61  // that n-ary operators will delay their construction until all
62  // children are known; this is a hack to speedup the parsing,
63  // because n-ary operator usually do a lot of work on construction
64  // (sorting all children if the operator is commutative, removing
65  // duplicates if applicable, etc.). Building n-ary nodes by
66  // repeatedly calling the binary constructor as we did in the past
67  // has a prohibitive cost. See issue #500.
68 
69  struct nary
70  {
71  std::vector<const spot::fnode*> children;
72  spot::op kind;
73  };
74 
75  struct pnode
76  {
77  // Hold either a constructed formula, or an n-ary operator that we
78  // will construct only when it is combined with a different
79  // operator.
80  std::variant<const spot::fnode*, nary> data;
81  // Record whether this pnode has been transformed into a fnode( or
82  // moved to another pnode). If that occurred, the ownership of
83  // any fnode we store has been transfered to the constructed fnode
84  // (or to the other pnode), and our destructor has nothing to do.
85  // This is the usual case while parsing a formula without error.
86  // However during error recovering, the parser may have to discard
87  // unused pnode, in which case we have to remember to free fnode
88  // during destruction.
89  //
90  // We have to track this used status because pnode are destructed
91  // whenever the parser pops a token, and as of Bison 3.7.6, the
92  // handling of "%destructor" is broken when
93  // "%define api.value.type variant" is used. See
94  // https://lists.gnu.org/archive/html/bug-bison/2022-03/msg00000.html
95  bool used = false;
96 
97  pnode()
98  : data(nullptr)
99  {
100  }
101 
102  pnode(const spot::fnode* ltl)
103  : data(ltl)
104  {
105  }
106 
107  // We only support move construction.
108  pnode(const pnode& other) = delete;
109  pnode& operator=(const pnode& other) = delete;
110 
111  pnode(pnode&& other)
112  : data(std::move(other.data))
113  {
114  other.used = true;
115  }
116 
117  pnode& operator=(pnode&& other)
118  {
119  data = std::move(other.data);
120  other.used = true;
121  return *this;
122  }
123 
124  ~pnode()
125  {
126  if (used)
127  return;
128  if (auto* n = std::get_if<nary>(&data))
129  {
130  for (auto f: n->children)
131  f->destroy();
132  }
133  else
134  {
135  auto* f = std::get<const spot::fnode*>(data);
136  // The only case where we expect f to be nullptr, is if
137  // parse_ap() return nullptr: then $$ is unset when YYERROR
138  // is called.
139  if (f)
140  f->destroy();
141  }
142  }
143 
144  // Create a new n-ary node from left and right.
145  // This will empty left and right so that their
146  // destructor do nothing.
147  pnode(spot::op o, pnode&& left, pnode&& right)
148  : data(nary{})
149  {
150  nary& n = std::get<nary>(data);
151  n.kind = o;
152  if (auto* nleft = std::get_if<nary>(&left.data);
153  nleft && nleft->kind == o)
154  std::swap(n.children, nleft->children);
155  else
156  n.children.push_back(left);
157  if (auto* nright = std::get_if<nary>(&right.data);
158  nright && nright->kind == o)
159  {
160  auto& rch = nright->children;
161  n.children.insert(n.children.end(), rch.begin(), rch.end());
162  rch.clear();
163  }
164  else
165  {
166  n.children.push_back(right);
167  }
168  }
169 
170  operator const spot::fnode*()
171  {
172  used = true;
173  if (auto* n = std::get_if<nary>(&data))
174  {
175  return spot::fnode::multop(n->kind, n->children);
176  }
177  else
178  {
179  return std::get<const spot::fnode*>(data);
180  }
181  }
182 
183  // Convert to a temporary formula, for printing, do not mark as
184  // used.
185  const spot::formula tmp() const
186  {
187  const spot::fnode* f;
188  if (auto* n = std::get_if<nary>(&data))
189  {
190  for (auto c: n->children)
191  c->clone();
192  f = spot::fnode::multop(n->kind, n->children);
193  }
194  else
195  {
196  f = std::get<const spot::fnode*>(data);
197  assert(f != nullptr);
198  f->clone();
199  }
200  return spot::formula(f);
201  }
202  };
203 
204 
205 
206 #line 207 "parsetl.hh"
207 
208 
209 # include <cstdlib> // std::abort
210 # include <iostream>
211 # include <stdexcept>
212 # include <string>
213 # include <vector>
214 
215 #if defined __cplusplus
216 # define YY_CPLUSPLUS __cplusplus
217 #else
218 # define YY_CPLUSPLUS 199711L
219 #endif
220 
221 // Support move semantics when possible.
222 #if 201103L <= YY_CPLUSPLUS
223 # define YY_MOVE std::move
224 # define YY_MOVE_OR_COPY move
225 # define YY_MOVE_REF(Type) Type&&
226 # define YY_RVREF(Type) Type&&
227 # define YY_COPY(Type) Type
228 #else
229 # define YY_MOVE
230 # define YY_MOVE_OR_COPY copy
231 # define YY_MOVE_REF(Type) Type&
232 # define YY_RVREF(Type) const Type&
233 # define YY_COPY(Type) const Type&
234 #endif
235 
236 // Support noexcept when possible.
237 #if 201103L <= YY_CPLUSPLUS
238 # define YY_NOEXCEPT noexcept
239 # define YY_NOTHROW
240 #else
241 # define YY_NOEXCEPT
242 # define YY_NOTHROW throw ()
243 #endif
244 
245 // Support constexpr when possible.
246 #if 201703 <= YY_CPLUSPLUS
247 # define YY_CONSTEXPR constexpr
248 #else
249 # define YY_CONSTEXPR
250 #endif
251 
252 
253 
254 #ifndef YY_ATTRIBUTE_PURE
255 # if defined __GNUC__ && 2 < __GNUC__ + (96 <= __GNUC_MINOR__)
256 # define YY_ATTRIBUTE_PURE __attribute__ ((__pure__))
257 # else
258 # define YY_ATTRIBUTE_PURE
259 # endif
260 #endif
261 
262 #ifndef YY_ATTRIBUTE_UNUSED
263 # if defined __GNUC__ && 2 < __GNUC__ + (7 <= __GNUC_MINOR__)
264 # define YY_ATTRIBUTE_UNUSED __attribute__ ((__unused__))
265 # else
266 # define YY_ATTRIBUTE_UNUSED
267 # endif
268 #endif
269 
270 /* Suppress unused-variable warnings by "using" E. */
271 #if ! defined lint || defined __GNUC__
272 # define YY_USE(E) ((void) (E))
273 #else
274 # define YY_USE(E) /* empty */
275 #endif
276 
277 /* Suppress an incorrect diagnostic about yylval being uninitialized. */
278 #if defined __GNUC__ && ! defined __ICC && 406 <= __GNUC__ * 100 + __GNUC_MINOR__
279 # if __GNUC__ * 100 + __GNUC_MINOR__ < 407
280 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
281  _Pragma ("GCC diagnostic push") \
282  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")
283 # else
284 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
285  _Pragma ("GCC diagnostic push") \
286  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"") \
287  _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
288 # endif
289 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \
290  _Pragma ("GCC diagnostic pop")
291 #else
292 # define YY_INITIAL_VALUE(Value) Value
293 #endif
294 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
295 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
296 # define YY_IGNORE_MAYBE_UNINITIALIZED_END
297 #endif
298 #ifndef YY_INITIAL_VALUE
299 # define YY_INITIAL_VALUE(Value) /* Nothing. */
300 #endif
301 
302 #if defined __cplusplus && defined __GNUC__ && ! defined __ICC && 6 <= __GNUC__
303 # define YY_IGNORE_USELESS_CAST_BEGIN \
304  _Pragma ("GCC diagnostic push") \
305  _Pragma ("GCC diagnostic ignored \"-Wuseless-cast\"")
306 # define YY_IGNORE_USELESS_CAST_END \
307  _Pragma ("GCC diagnostic pop")
308 #endif
309 #ifndef YY_IGNORE_USELESS_CAST_BEGIN
310 # define YY_IGNORE_USELESS_CAST_BEGIN
311 # define YY_IGNORE_USELESS_CAST_END
312 #endif
313 
314 # ifndef YY_CAST
315 # ifdef __cplusplus
316 # define YY_CAST(Type, Val) static_cast<Type> (Val)
317 # define YY_REINTERPRET_CAST(Type, Val) reinterpret_cast<Type> (Val)
318 # else
319 # define YY_CAST(Type, Val) ((Type) (Val))
320 # define YY_REINTERPRET_CAST(Type, Val) ((Type) (Val))
321 # endif
322 # endif
323 # ifndef YY_NULLPTR
324 # if defined __cplusplus
325 # if 201103L <= __cplusplus
326 # define YY_NULLPTR nullptr
327 # else
328 # define YY_NULLPTR 0
329 # endif
330 # else
331 # define YY_NULLPTR ((void*)0)
332 # endif
333 # endif
334 
335 /* Debug traces. */
336 #ifndef TLYYDEBUG
337 # if defined YYDEBUG
338 #if YYDEBUG
339 # define TLYYDEBUG 1
340 # else
341 # define TLYYDEBUG 0
342 # endif
343 # else /* ! defined YYDEBUG */
344 # define TLYYDEBUG 1
345 # endif /* ! defined YYDEBUG */
346 #endif /* ! defined TLYYDEBUG */
347 
348 namespace tlyy {
349 #line 350 "parsetl.hh"
350 
351 
352 
353 
355  class parser
356  {
357  public:
358 #ifdef TLYYSTYPE
359 # ifdef __GNUC__
360 # pragma GCC message "bison: do not #define TLYYSTYPE in C++, use %define api.value.type"
361 # endif
362  typedef TLYYSTYPE value_type;
363 #else
370  {
371  public:
374 
376  value_type () YY_NOEXCEPT
377  : yyraw_ ()
378  {}
379 
381  template <typename T>
382  value_type (YY_RVREF (T) t)
383  {
384  new (yyas_<T> ()) T (YY_MOVE (t));
385  }
386 
387 #if 201103L <= YY_CPLUSPLUS
389  value_type (const self_type&) = delete;
391  self_type& operator= (const self_type&) = delete;
392 #endif
393 
395  ~value_type () YY_NOEXCEPT
396  {}
397 
398 # if 201103L <= YY_CPLUSPLUS
400  template <typename T, typename... U>
401  T&
402  emplace (U&&... u)
403  {
404  return *new (yyas_<T> ()) T (std::forward <U>(u)...);
405  }
406 # else
408  template <typename T>
409  T&
411  {
412  return *new (yyas_<T> ()) T ();
413  }
414 
416  template <typename T>
417  T&
418  emplace (const T& t)
419  {
420  return *new (yyas_<T> ()) T (t);
421  }
422 # endif
423 
426  template <typename T>
427  T&
428  build ()
429  {
430  return emplace<T> ();
431  }
432 
435  template <typename T>
436  T&
437  build (const T& t)
438  {
439  return emplace<T> (t);
440  }
441 
443  template <typename T>
444  T&
445  as () YY_NOEXCEPT
446  {
447  return *yyas_<T> ();
448  }
449 
451  template <typename T>
452  const T&
453  as () const YY_NOEXCEPT
454  {
455  return *yyas_<T> ();
456  }
457 
466  template <typename T>
467  void
468  swap (self_type& that) YY_NOEXCEPT
469  {
470  std::swap (as<T> (), that.as<T> ());
471  }
472 
476  template <typename T>
477  void
478  move (self_type& that)
479  {
480 # if 201103L <= YY_CPLUSPLUS
481  emplace<T> (std::move (that.as<T> ()));
482 # else
483  emplace<T> ();
484  swap<T> (that);
485 # endif
486  that.destroy<T> ();
487  }
488 
489 # if 201103L <= YY_CPLUSPLUS
491  template <typename T>
492  void
493  move (self_type&& that)
494  {
495  emplace<T> (std::move (that.as<T> ()));
496  that.destroy<T> ();
497  }
498 #endif
499 
501  template <typename T>
502  void
503  copy (const self_type& that)
504  {
505  emplace<T> (that.as<T> ());
506  }
507 
509  template <typename T>
510  void
512  {
513  as<T> ().~T ();
514  }
515 
516  private:
517 #if YY_CPLUSPLUS < 201103L
519  value_type (const self_type&);
521  self_type& operator= (const self_type&);
522 #endif
523 
525  template <typename T>
526  T*
527  yyas_ () YY_NOEXCEPT
528  {
529  void *yyp = yyraw_;
530  return static_cast<T*> (yyp);
531  }
532 
534  template <typename T>
535  const T*
536  yyas_ () const YY_NOEXCEPT
537  {
538  const void *yyp = yyraw_;
539  return static_cast<const T*> (yyp);
540  }
541 
543  union union_type
544  {
545  // sqbracketargs
546  // gotoargs
547  // starargs
548  // fstarargs
549  // equalargs
550  // delayargs
551  char dummy1[sizeof (minmax_t)];
552 
553  // atomprop
554  // booleanatom
555  // sere
556  // bracedsere
557  // parenthesedsubformula
558  // boolformula
559  // subformula
560  // lbtformula
561  char dummy2[sizeof (pnode)];
562 
563  // "(...) block"
564  // "{...} block"
565  // "{...}! block"
566  // "atomic proposition"
567  char dummy3[sizeof (std::string)];
568 
569  // "number for square bracket operator"
570  // "SVA delay operator"
571  // sqbkt_num
572  char dummy4[sizeof (unsigned)];
573  };
574 
576  enum { size = sizeof (union_type) };
577 
579  union
580  {
582  long double yyalign_me_;
584  char yyraw_[size];
585  };
586  };
587 
588 #endif
591 
593  typedef spot::location location_type;
594 
596  struct syntax_error : std::runtime_error
597  {
598  syntax_error (const location_type& l, const std::string& m)
599  : std::runtime_error (m)
600  , location (l)
601  {}
602 
603  syntax_error (const syntax_error& s)
604  : std::runtime_error (s.what ())
605  , location (s.location)
606  {}
607 
608  ~syntax_error () YY_NOEXCEPT YY_NOTHROW;
609 
610  location_type location;
611  };
612 
614  struct token
615  {
616  enum token_kind_type
617  {
618  TLYYEMPTY = -2,
619  TLYYEOF = 0, // "end of file"
620  TLYYerror = 256, // error
621  TLYYUNDEF = 257, // "invalid token"
622  START_LTL = 258, // "LTL start marker"
623  START_LBT = 259, // "LBT start marker"
624  START_SERE = 260, // "SERE start marker"
625  START_BOOL = 261, // "BOOLEAN start marker"
626  PAR_OPEN = 262, // "opening parenthesis"
627  PAR_CLOSE = 263, // "closing parenthesis"
628  PAR_BLOCK = 264, // "(...) block"
629  BRA_BLOCK = 265, // "{...} block"
630  BRA_BANG_BLOCK = 266, // "{...}! block"
631  BRACE_OPEN = 267, // "opening brace"
632  BRACE_CLOSE = 268, // "closing brace"
633  BRACE_BANG_CLOSE = 269, // "closing brace-bang"
634  OP_OR = 270, // "or operator"
635  OP_XOR = 271, // "xor operator"
636  OP_AND = 272, // "and operator"
637  OP_SHORT_AND = 273, // "short and operator"
638  OP_IMPLIES = 274, // "implication operator"
639  OP_EQUIV = 275, // "equivalent operator"
640  OP_U = 276, // "until operator"
641  OP_R = 277, // "release operator"
642  OP_W = 278, // "weak until operator"
643  OP_M = 279, // "strong release operator"
644  OP_F = 280, // "sometimes operator"
645  OP_G = 281, // "always operator"
646  OP_X = 282, // "next operator"
647  OP_STRONG_X = 283, // "strong next operator"
648  OP_NOT = 284, // "not operator"
649  OP_XREP = 285, // "X[.] operator"
650  OP_FREP = 286, // "F[.] operator"
651  OP_GREP = 287, // "G[.] operator"
652  OP_STAR = 288, // "star operator"
653  OP_BSTAR = 289, // "bracket star operator"
654  OP_BFSTAR = 290, // "bracket fusion-star operator"
655  OP_PLUS = 291, // "plus operator"
656  OP_FPLUS = 292, // "fusion-plus operator"
657  OP_STAR_OPEN = 293, // "opening bracket for star operator"
658  OP_FSTAR_OPEN = 294, // "opening bracket for fusion-star operator"
659  OP_EQUAL_OPEN = 295, // "opening bracket for equal operator"
660  OP_GOTO_OPEN = 296, // "opening bracket for goto operator"
661  OP_SQBKT_CLOSE = 297, // "closing bracket"
662  OP_SQBKT_STRONG_CLOSE = 298, // "closing !]"
663  OP_SQBKT_NUM = 299, // "number for square bracket operator"
664  OP_UNBOUNDED = 300, // "unbounded mark"
665  OP_SQBKT_SEP = 301, // "separator for square bracket operator"
666  OP_UCONCAT = 302, // "universal concat operator"
667  OP_ECONCAT = 303, // "existential concat operator"
668  OP_UCONCAT_NONO = 304, // "universal non-overlapping concat operator"
669  OP_ECONCAT_NONO = 305, // "existential non-overlapping concat operator"
670  OP_FIRST_MATCH = 306, // "first_match"
671  ATOMIC_PROP = 307, // "atomic proposition"
672  OP_CONCAT = 308, // "concat operator"
673  OP_FUSION = 309, // "fusion operator"
674  CONST_TRUE = 310, // "constant true"
675  CONST_FALSE = 311, // "constant false"
676  END_OF_INPUT = 312, // "end of formula"
677  OP_POST_NEG = 313, // "negative suffix"
678  OP_POST_POS = 314, // "positive suffix"
679  OP_DELAY_N = 315, // "SVA delay operator"
680  OP_DELAY_OPEN = 316, // "opening bracket for SVA delay operator"
681  OP_DELAY_PLUS = 317, // "##[+] operator"
682  OP_DELAY_STAR = 318 // "##[*] operator"
683  };
685  typedef token_kind_type yytokentype;
686  };
687 
689  typedef token::token_kind_type token_kind_type;
690 
692  typedef token_kind_type token_type;
693 
695  struct symbol_kind
696  {
698  {
699  YYNTOKENS = 80,
700  S_YYEMPTY = -2,
701  S_YYEOF = 0, // "end of file"
702  S_YYerror = 1, // error
703  S_YYUNDEF = 2, // "invalid token"
704  S_START_LTL = 3, // "LTL start marker"
705  S_START_LBT = 4, // "LBT start marker"
706  S_START_SERE = 5, // "SERE start marker"
707  S_START_BOOL = 6, // "BOOLEAN start marker"
708  S_PAR_OPEN = 7, // "opening parenthesis"
709  S_PAR_CLOSE = 8, // "closing parenthesis"
710  S_PAR_BLOCK = 9, // "(...) block"
711  S_BRA_BLOCK = 10, // "{...} block"
712  S_BRA_BANG_BLOCK = 11, // "{...}! block"
713  S_BRACE_OPEN = 12, // "opening brace"
714  S_BRACE_CLOSE = 13, // "closing brace"
715  S_BRACE_BANG_CLOSE = 14, // "closing brace-bang"
716  S_OP_OR = 15, // "or operator"
717  S_OP_XOR = 16, // "xor operator"
718  S_OP_AND = 17, // "and operator"
719  S_OP_SHORT_AND = 18, // "short and operator"
720  S_OP_IMPLIES = 19, // "implication operator"
721  S_OP_EQUIV = 20, // "equivalent operator"
722  S_OP_U = 21, // "until operator"
723  S_OP_R = 22, // "release operator"
724  S_OP_W = 23, // "weak until operator"
725  S_OP_M = 24, // "strong release operator"
726  S_OP_F = 25, // "sometimes operator"
727  S_OP_G = 26, // "always operator"
728  S_OP_X = 27, // "next operator"
729  S_OP_STRONG_X = 28, // "strong next operator"
730  S_OP_NOT = 29, // "not operator"
731  S_OP_XREP = 30, // "X[.] operator"
732  S_OP_FREP = 31, // "F[.] operator"
733  S_OP_GREP = 32, // "G[.] operator"
734  S_OP_STAR = 33, // "star operator"
735  S_OP_BSTAR = 34, // "bracket star operator"
736  S_OP_BFSTAR = 35, // "bracket fusion-star operator"
737  S_OP_PLUS = 36, // "plus operator"
738  S_OP_FPLUS = 37, // "fusion-plus operator"
739  S_OP_STAR_OPEN = 38, // "opening bracket for star operator"
740  S_OP_FSTAR_OPEN = 39, // "opening bracket for fusion-star operator"
741  S_OP_EQUAL_OPEN = 40, // "opening bracket for equal operator"
742  S_OP_GOTO_OPEN = 41, // "opening bracket for goto operator"
743  S_OP_SQBKT_CLOSE = 42, // "closing bracket"
744  S_OP_SQBKT_STRONG_CLOSE = 43, // "closing !]"
745  S_OP_SQBKT_NUM = 44, // "number for square bracket operator"
746  S_OP_UNBOUNDED = 45, // "unbounded mark"
747  S_OP_SQBKT_SEP = 46, // "separator for square bracket operator"
748  S_OP_UCONCAT = 47, // "universal concat operator"
749  S_OP_ECONCAT = 48, // "existential concat operator"
750  S_OP_UCONCAT_NONO = 49, // "universal non-overlapping concat operator"
751  S_OP_ECONCAT_NONO = 50, // "existential non-overlapping concat operator"
752  S_OP_FIRST_MATCH = 51, // "first_match"
753  S_ATOMIC_PROP = 52, // "atomic proposition"
754  S_OP_CONCAT = 53, // "concat operator"
755  S_OP_FUSION = 54, // "fusion operator"
756  S_CONST_TRUE = 55, // "constant true"
757  S_CONST_FALSE = 56, // "constant false"
758  S_END_OF_INPUT = 57, // "end of formula"
759  S_OP_POST_NEG = 58, // "negative suffix"
760  S_OP_POST_POS = 59, // "positive suffix"
761  S_OP_DELAY_N = 60, // "SVA delay operator"
762  S_OP_DELAY_OPEN = 61, // "opening bracket for SVA delay operator"
763  S_OP_DELAY_PLUS = 62, // "##[+] operator"
764  S_OP_DELAY_STAR = 63, // "##[*] operator"
765  S_64_ = 64, // '!'
766  S_65_ = 65, // '&'
767  S_66_ = 66, // '|'
768  S_67_ = 67, // '^'
769  S_68_i_ = 68, // 'i'
770  S_69_e_ = 69, // 'e'
771  S_70_X_ = 70, // 'X'
772  S_71_F_ = 71, // 'F'
773  S_72_G_ = 72, // 'G'
774  S_73_U_ = 73, // 'U'
775  S_74_V_ = 74, // 'V'
776  S_75_R_ = 75, // 'R'
777  S_76_W_ = 76, // 'W'
778  S_77_M_ = 77, // 'M'
779  S_78_t_ = 78, // 't'
780  S_79_f_ = 79, // 'f'
781  S_YYACCEPT = 80, // $accept
782  S_result = 81, // result
783  S_emptyinput = 82, // emptyinput
784  S_enderror = 83, // enderror
785  S_OP_SQBKT_SEP_unbounded = 84, // OP_SQBKT_SEP_unbounded
786  S_OP_SQBKT_SEP_opt = 85, // OP_SQBKT_SEP_opt
787  S_error_opt = 86, // error_opt
788  S_sqbkt_num = 87, // sqbkt_num
789  S_sqbracketargs = 88, // sqbracketargs
790  S_gotoargs = 89, // gotoargs
791  S_kleen_star = 90, // kleen_star
792  S_starargs = 91, // starargs
793  S_fstarargs = 92, // fstarargs
794  S_equalargs = 93, // equalargs
795  S_delayargs = 94, // delayargs
796  S_atomprop = 95, // atomprop
797  S_booleanatom = 96, // booleanatom
798  S_sere = 97, // sere
799  S_bracedsere = 98, // bracedsere
800  S_parenthesedsubformula = 99, // parenthesedsubformula
801  S_boolformula = 100, // boolformula
802  S_subformula = 101, // subformula
803  S_lbtformula = 102 // lbtformula
804  };
805  };
806 
809 
812 
819  template <typename Base>
820  struct basic_symbol : Base
821  {
823  typedef Base super_type;
824 
826  basic_symbol () YY_NOEXCEPT
827  : value ()
828  , location ()
829  {}
830 
831 #if 201103L <= YY_CPLUSPLUS
833  basic_symbol (basic_symbol&& that)
834  : Base (std::move (that))
835  , value ()
836  , location (std::move (that.location))
837  {
838  switch (this->kind ())
839  {
840  case symbol_kind::S_sqbracketargs: // sqbracketargs
841  case symbol_kind::S_gotoargs: // gotoargs
842  case symbol_kind::S_starargs: // starargs
843  case symbol_kind::S_fstarargs: // fstarargs
844  case symbol_kind::S_equalargs: // equalargs
845  case symbol_kind::S_delayargs: // delayargs
846  value.move< minmax_t > (std::move (that.value));
847  break;
848 
849  case symbol_kind::S_atomprop: // atomprop
850  case symbol_kind::S_booleanatom: // booleanatom
851  case symbol_kind::S_sere: // sere
852  case symbol_kind::S_bracedsere: // bracedsere
853  case symbol_kind::S_parenthesedsubformula: // parenthesedsubformula
854  case symbol_kind::S_boolformula: // boolformula
855  case symbol_kind::S_subformula: // subformula
856  case symbol_kind::S_lbtformula: // lbtformula
857  value.move< pnode > (std::move (that.value));
858  break;
859 
860  case symbol_kind::S_PAR_BLOCK: // "(...) block"
861  case symbol_kind::S_BRA_BLOCK: // "{...} block"
862  case symbol_kind::S_BRA_BANG_BLOCK: // "{...}! block"
863  case symbol_kind::S_ATOMIC_PROP: // "atomic proposition"
864  value.move< std::string > (std::move (that.value));
865  break;
866 
867  case symbol_kind::S_OP_SQBKT_NUM: // "number for square bracket operator"
868  case symbol_kind::S_OP_DELAY_N: // "SVA delay operator"
869  case symbol_kind::S_sqbkt_num: // sqbkt_num
870  value.move< unsigned > (std::move (that.value));
871  break;
872 
873  default:
874  break;
875  }
876 
877  }
878 #endif
879 
881  basic_symbol (const basic_symbol& that);
882 
884 #if 201103L <= YY_CPLUSPLUS
885  basic_symbol (typename Base::kind_type t, location_type&& l)
886  : Base (t)
887  , location (std::move (l))
888  {}
889 #else
890  basic_symbol (typename Base::kind_type t, const location_type& l)
891  : Base (t)
892  , location (l)
893  {}
894 #endif
895 
896 #if 201103L <= YY_CPLUSPLUS
897  basic_symbol (typename Base::kind_type t, minmax_t&& v, location_type&& l)
898  : Base (t)
899  , value (std::move (v))
900  , location (std::move (l))
901  {}
902 #else
903  basic_symbol (typename Base::kind_type t, const minmax_t& v, const location_type& l)
904  : Base (t)
905  , value (v)
906  , location (l)
907  {}
908 #endif
909 
910 #if 201103L <= YY_CPLUSPLUS
911  basic_symbol (typename Base::kind_type t, pnode&& v, location_type&& l)
912  : Base (t)
913  , value (std::move (v))
914  , location (std::move (l))
915  {}
916 #else
917  basic_symbol (typename Base::kind_type t, const pnode& v, const location_type& l)
918  : Base (t)
919  , value (v)
920  , location (l)
921  {}
922 #endif
923 
924 #if 201103L <= YY_CPLUSPLUS
925  basic_symbol (typename Base::kind_type t, std::string&& v, location_type&& l)
926  : Base (t)
927  , value (std::move (v))
928  , location (std::move (l))
929  {}
930 #else
931  basic_symbol (typename Base::kind_type t, const std::string& v, const location_type& l)
932  : Base (t)
933  , value (v)
934  , location (l)
935  {}
936 #endif
937 
938 #if 201103L <= YY_CPLUSPLUS
939  basic_symbol (typename Base::kind_type t, unsigned&& v, location_type&& l)
940  : Base (t)
941  , value (std::move (v))
942  , location (std::move (l))
943  {}
944 #else
945  basic_symbol (typename Base::kind_type t, const unsigned& v, const location_type& l)
946  : Base (t)
947  , value (v)
948  , location (l)
949  {}
950 #endif
951 
954  {
955  clear ();
956  }
957 
958 
959 
961  void clear () YY_NOEXCEPT
962  {
963  // User destructor.
964  symbol_kind_type yykind = this->kind ();
965  basic_symbol<Base>& yysym = *this;
966  (void) yysym;
967  switch (yykind)
968  {
969  default:
970  break;
971  }
972 
973  // Value type destructor.
974 switch (yykind)
975  {
976  case symbol_kind::S_sqbracketargs: // sqbracketargs
977  case symbol_kind::S_gotoargs: // gotoargs
978  case symbol_kind::S_starargs: // starargs
979  case symbol_kind::S_fstarargs: // fstarargs
980  case symbol_kind::S_equalargs: // equalargs
981  case symbol_kind::S_delayargs: // delayargs
982  value.template destroy< minmax_t > ();
983  break;
984 
985  case symbol_kind::S_atomprop: // atomprop
986  case symbol_kind::S_booleanatom: // booleanatom
987  case symbol_kind::S_sere: // sere
988  case symbol_kind::S_bracedsere: // bracedsere
989  case symbol_kind::S_parenthesedsubformula: // parenthesedsubformula
990  case symbol_kind::S_boolformula: // boolformula
991  case symbol_kind::S_subformula: // subformula
992  case symbol_kind::S_lbtformula: // lbtformula
993  value.template destroy< pnode > ();
994  break;
995 
996  case symbol_kind::S_PAR_BLOCK: // "(...) block"
997  case symbol_kind::S_BRA_BLOCK: // "{...} block"
998  case symbol_kind::S_BRA_BANG_BLOCK: // "{...}! block"
999  case symbol_kind::S_ATOMIC_PROP: // "atomic proposition"
1000  value.template destroy< std::string > ();
1001  break;
1002 
1003  case symbol_kind::S_OP_SQBKT_NUM: // "number for square bracket operator"
1004  case symbol_kind::S_OP_DELAY_N: // "SVA delay operator"
1005  case symbol_kind::S_sqbkt_num: // sqbkt_num
1006  value.template destroy< unsigned > ();
1007  break;
1008 
1009  default:
1010  break;
1011  }
1012 
1013  Base::clear ();
1014  }
1015 
1017  std::string name () const YY_NOEXCEPT
1018  {
1019  return parser::symbol_name (this->kind ());
1020  }
1021 
1023  symbol_kind_type type_get () const YY_NOEXCEPT;
1024 
1026  bool empty () const YY_NOEXCEPT;
1027 
1029  void move (basic_symbol& s);
1030 
1033 
1036 
1037  private:
1038 #if YY_CPLUSPLUS < 201103L
1040  basic_symbol& operator= (const basic_symbol& that);
1041 #endif
1042  };
1043 
1045  struct by_kind
1046  {
1048  typedef token_kind_type kind_type;
1049 
1051  by_kind () YY_NOEXCEPT;
1052 
1053 #if 201103L <= YY_CPLUSPLUS
1055  by_kind (by_kind&& that) YY_NOEXCEPT;
1056 #endif
1057 
1059  by_kind (const by_kind& that) YY_NOEXCEPT;
1060 
1062  by_kind (kind_type t) YY_NOEXCEPT;
1063 
1064 
1065 
1067  void clear () YY_NOEXCEPT;
1068 
1070  void move (by_kind& that);
1071 
1074  symbol_kind_type kind () const YY_NOEXCEPT;
1075 
1077  symbol_kind_type type_get () const YY_NOEXCEPT;
1078 
1082  };
1083 
1085  typedef by_kind by_type;
1086 
1089  {
1092 
1094  symbol_type () YY_NOEXCEPT {}
1095 
1097 #if 201103L <= YY_CPLUSPLUS
1098  symbol_type (int tok, location_type l)
1099  : super_type (token_kind_type (tok), std::move (l))
1100 #else
1101  symbol_type (int tok, const location_type& l)
1102  : super_type (token_kind_type (tok), l)
1103 #endif
1104  {}
1105 #if 201103L <= YY_CPLUSPLUS
1106  symbol_type (int tok, std::string v, location_type l)
1107  : super_type (token_kind_type (tok), std::move (v), std::move (l))
1108 #else
1109  symbol_type (int tok, const std::string& v, const location_type& l)
1110  : super_type (token_kind_type (tok), v, l)
1111 #endif
1112  {}
1113 #if 201103L <= YY_CPLUSPLUS
1114  symbol_type (int tok, unsigned v, location_type l)
1115  : super_type (token_kind_type (tok), std::move (v), std::move (l))
1116 #else
1117  symbol_type (int tok, const unsigned& v, const location_type& l)
1118  : super_type (token_kind_type (tok), v, l)
1119 #endif
1120  {}
1121  };
1122 
1124  parser (spot::parse_error_list &error_list_yyarg, spot::environment &parse_environment_yyarg, spot::formula &result_yyarg);
1125  virtual ~parser ();
1126 
1127 #if 201103L <= YY_CPLUSPLUS
1129  parser (const parser&) = delete;
1131  parser& operator= (const parser&) = delete;
1132 #endif
1133 
1137 
1140  virtual int parse ();
1141 
1142 #if TLYYDEBUG
1144  std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
1146  void set_debug_stream (std::ostream &);
1147 
1149  typedef int debug_level_type;
1151  debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
1154 #endif
1155 
1159  virtual void error (const location_type& loc, const std::string& msg);
1160 
1162  void error (const syntax_error& err);
1163 
1166  static std::string symbol_name (symbol_kind_type yysymbol);
1167 
1168  // Implementation of make_symbol for each token kind.
1169 #if 201103L <= YY_CPLUSPLUS
1170  static
1171  symbol_type
1172  make_TLYYEOF (location_type l)
1173  {
1174  return symbol_type (token::TLYYEOF, std::move (l));
1175  }
1176 #else
1177  static
1178  symbol_type
1179  make_TLYYEOF (const location_type& l)
1180  {
1181  return symbol_type (token::TLYYEOF, l);
1182  }
1183 #endif
1184 #if 201103L <= YY_CPLUSPLUS
1185  static
1186  symbol_type
1187  make_TLYYerror (location_type l)
1188  {
1189  return symbol_type (token::TLYYerror, std::move (l));
1190  }
1191 #else
1192  static
1193  symbol_type
1194  make_TLYYerror (const location_type& l)
1195  {
1196  return symbol_type (token::TLYYerror, l);
1197  }
1198 #endif
1199 #if 201103L <= YY_CPLUSPLUS
1200  static
1201  symbol_type
1202  make_TLYYUNDEF (location_type l)
1203  {
1204  return symbol_type (token::TLYYUNDEF, std::move (l));
1205  }
1206 #else
1207  static
1208  symbol_type
1209  make_TLYYUNDEF (const location_type& l)
1210  {
1211  return symbol_type (token::TLYYUNDEF, l);
1212  }
1213 #endif
1214 #if 201103L <= YY_CPLUSPLUS
1215  static
1216  symbol_type
1217  make_START_LTL (location_type l)
1218  {
1219  return symbol_type (token::START_LTL, std::move (l));
1220  }
1221 #else
1222  static
1223  symbol_type
1224  make_START_LTL (const location_type& l)
1225  {
1226  return symbol_type (token::START_LTL, l);
1227  }
1228 #endif
1229 #if 201103L <= YY_CPLUSPLUS
1230  static
1231  symbol_type
1232  make_START_LBT (location_type l)
1233  {
1234  return symbol_type (token::START_LBT, std::move (l));
1235  }
1236 #else
1237  static
1238  symbol_type
1239  make_START_LBT (const location_type& l)
1240  {
1241  return symbol_type (token::START_LBT, l);
1242  }
1243 #endif
1244 #if 201103L <= YY_CPLUSPLUS
1245  static
1246  symbol_type
1247  make_START_SERE (location_type l)
1248  {
1249  return symbol_type (token::START_SERE, std::move (l));
1250  }
1251 #else
1252  static
1253  symbol_type
1254  make_START_SERE (const location_type& l)
1255  {
1256  return symbol_type (token::START_SERE, l);
1257  }
1258 #endif
1259 #if 201103L <= YY_CPLUSPLUS
1260  static
1261  symbol_type
1262  make_START_BOOL (location_type l)
1263  {
1264  return symbol_type (token::START_BOOL, std::move (l));
1265  }
1266 #else
1267  static
1268  symbol_type
1269  make_START_BOOL (const location_type& l)
1270  {
1271  return symbol_type (token::START_BOOL, l);
1272  }
1273 #endif
1274 #if 201103L <= YY_CPLUSPLUS
1275  static
1276  symbol_type
1277  make_PAR_OPEN (location_type l)
1278  {
1279  return symbol_type (token::PAR_OPEN, std::move (l));
1280  }
1281 #else
1282  static
1283  symbol_type
1284  make_PAR_OPEN (const location_type& l)
1285  {
1286  return symbol_type (token::PAR_OPEN, l);
1287  }
1288 #endif
1289 #if 201103L <= YY_CPLUSPLUS
1290  static
1291  symbol_type
1292  make_PAR_CLOSE (location_type l)
1293  {
1294  return symbol_type (token::PAR_CLOSE, std::move (l));
1295  }
1296 #else
1297  static
1298  symbol_type
1299  make_PAR_CLOSE (const location_type& l)
1300  {
1301  return symbol_type (token::PAR_CLOSE, l);
1302  }
1303 #endif
1304 #if 201103L <= YY_CPLUSPLUS
1305  static
1306  symbol_type
1307  make_PAR_BLOCK (std::string v, location_type l)
1308  {
1309  return symbol_type (token::PAR_BLOCK, std::move (v), std::move (l));
1310  }
1311 #else
1312  static
1313  symbol_type
1314  make_PAR_BLOCK (const std::string& v, const location_type& l)
1315  {
1316  return symbol_type (token::PAR_BLOCK, v, l);
1317  }
1318 #endif
1319 #if 201103L <= YY_CPLUSPLUS
1320  static
1321  symbol_type
1322  make_BRA_BLOCK (std::string v, location_type l)
1323  {
1324  return symbol_type (token::BRA_BLOCK, std::move (v), std::move (l));
1325  }
1326 #else
1327  static
1328  symbol_type
1329  make_BRA_BLOCK (const std::string& v, const location_type& l)
1330  {
1331  return symbol_type (token::BRA_BLOCK, v, l);
1332  }
1333 #endif
1334 #if 201103L <= YY_CPLUSPLUS
1335  static
1336  symbol_type
1337  make_BRA_BANG_BLOCK (std::string v, location_type l)
1338  {
1339  return symbol_type (token::BRA_BANG_BLOCK, std::move (v), std::move (l));
1340  }
1341 #else
1342  static
1343  symbol_type
1344  make_BRA_BANG_BLOCK (const std::string& v, const location_type& l)
1345  {
1346  return symbol_type (token::BRA_BANG_BLOCK, v, l);
1347  }
1348 #endif
1349 #if 201103L <= YY_CPLUSPLUS
1350  static
1351  symbol_type
1352  make_BRACE_OPEN (location_type l)
1353  {
1354  return symbol_type (token::BRACE_OPEN, std::move (l));
1355  }
1356 #else
1357  static
1358  symbol_type
1359  make_BRACE_OPEN (const location_type& l)
1360  {
1361  return symbol_type (token::BRACE_OPEN, l);
1362  }
1363 #endif
1364 #if 201103L <= YY_CPLUSPLUS
1365  static
1366  symbol_type
1367  make_BRACE_CLOSE (location_type l)
1368  {
1369  return symbol_type (token::BRACE_CLOSE, std::move (l));
1370  }
1371 #else
1372  static
1373  symbol_type
1374  make_BRACE_CLOSE (const location_type& l)
1375  {
1376  return symbol_type (token::BRACE_CLOSE, l);
1377  }
1378 #endif
1379 #if 201103L <= YY_CPLUSPLUS
1380  static
1381  symbol_type
1382  make_BRACE_BANG_CLOSE (location_type l)
1383  {
1384  return symbol_type (token::BRACE_BANG_CLOSE, std::move (l));
1385  }
1386 #else
1387  static
1388  symbol_type
1389  make_BRACE_BANG_CLOSE (const location_type& l)
1390  {
1391  return symbol_type (token::BRACE_BANG_CLOSE, l);
1392  }
1393 #endif
1394 #if 201103L <= YY_CPLUSPLUS
1395  static
1396  symbol_type
1397  make_OP_OR (location_type l)
1398  {
1399  return symbol_type (token::OP_OR, std::move (l));
1400  }
1401 #else
1402  static
1403  symbol_type
1404  make_OP_OR (const location_type& l)
1405  {
1406  return symbol_type (token::OP_OR, l);
1407  }
1408 #endif
1409 #if 201103L <= YY_CPLUSPLUS
1410  static
1411  symbol_type
1412  make_OP_XOR (location_type l)
1413  {
1414  return symbol_type (token::OP_XOR, std::move (l));
1415  }
1416 #else
1417  static
1418  symbol_type
1419  make_OP_XOR (const location_type& l)
1420  {
1421  return symbol_type (token::OP_XOR, l);
1422  }
1423 #endif
1424 #if 201103L <= YY_CPLUSPLUS
1425  static
1426  symbol_type
1427  make_OP_AND (location_type l)
1428  {
1429  return symbol_type (token::OP_AND, std::move (l));
1430  }
1431 #else
1432  static
1433  symbol_type
1434  make_OP_AND (const location_type& l)
1435  {
1436  return symbol_type (token::OP_AND, l);
1437  }
1438 #endif
1439 #if 201103L <= YY_CPLUSPLUS
1440  static
1441  symbol_type
1442  make_OP_SHORT_AND (location_type l)
1443  {
1444  return symbol_type (token::OP_SHORT_AND, std::move (l));
1445  }
1446 #else
1447  static
1448  symbol_type
1449  make_OP_SHORT_AND (const location_type& l)
1450  {
1451  return symbol_type (token::OP_SHORT_AND, l);
1452  }
1453 #endif
1454 #if 201103L <= YY_CPLUSPLUS
1455  static
1456  symbol_type
1457  make_OP_IMPLIES (location_type l)
1458  {
1459  return symbol_type (token::OP_IMPLIES, std::move (l));
1460  }
1461 #else
1462  static
1463  symbol_type
1464  make_OP_IMPLIES (const location_type& l)
1465  {
1466  return symbol_type (token::OP_IMPLIES, l);
1467  }
1468 #endif
1469 #if 201103L <= YY_CPLUSPLUS
1470  static
1471  symbol_type
1472  make_OP_EQUIV (location_type l)
1473  {
1474  return symbol_type (token::OP_EQUIV, std::move (l));
1475  }
1476 #else
1477  static
1478  symbol_type
1479  make_OP_EQUIV (const location_type& l)
1480  {
1481  return symbol_type (token::OP_EQUIV, l);
1482  }
1483 #endif
1484 #if 201103L <= YY_CPLUSPLUS
1485  static
1486  symbol_type
1487  make_OP_U (location_type l)
1488  {
1489  return symbol_type (token::OP_U, std::move (l));
1490  }
1491 #else
1492  static
1493  symbol_type
1494  make_OP_U (const location_type& l)
1495  {
1496  return symbol_type (token::OP_U, l);
1497  }
1498 #endif
1499 #if 201103L <= YY_CPLUSPLUS
1500  static
1501  symbol_type
1502  make_OP_R (location_type l)
1503  {
1504  return symbol_type (token::OP_R, std::move (l));
1505  }
1506 #else
1507  static
1508  symbol_type
1509  make_OP_R (const location_type& l)
1510  {
1511  return symbol_type (token::OP_R, l);
1512  }
1513 #endif
1514 #if 201103L <= YY_CPLUSPLUS
1515  static
1516  symbol_type
1517  make_OP_W (location_type l)
1518  {
1519  return symbol_type (token::OP_W, std::move (l));
1520  }
1521 #else
1522  static
1523  symbol_type
1524  make_OP_W (const location_type& l)
1525  {
1526  return symbol_type (token::OP_W, l);
1527  }
1528 #endif
1529 #if 201103L <= YY_CPLUSPLUS
1530  static
1531  symbol_type
1532  make_OP_M (location_type l)
1533  {
1534  return symbol_type (token::OP_M, std::move (l));
1535  }
1536 #else
1537  static
1538  symbol_type
1539  make_OP_M (const location_type& l)
1540  {
1541  return symbol_type (token::OP_M, l);
1542  }
1543 #endif
1544 #if 201103L <= YY_CPLUSPLUS
1545  static
1546  symbol_type
1547  make_OP_F (location_type l)
1548  {
1549  return symbol_type (token::OP_F, std::move (l));
1550  }
1551 #else
1552  static
1553  symbol_type
1554  make_OP_F (const location_type& l)
1555  {
1556  return symbol_type (token::OP_F, l);
1557  }
1558 #endif
1559 #if 201103L <= YY_CPLUSPLUS
1560  static
1561  symbol_type
1562  make_OP_G (location_type l)
1563  {
1564  return symbol_type (token::OP_G, std::move (l));
1565  }
1566 #else
1567  static
1568  symbol_type
1569  make_OP_G (const location_type& l)
1570  {
1571  return symbol_type (token::OP_G, l);
1572  }
1573 #endif
1574 #if 201103L <= YY_CPLUSPLUS
1575  static
1576  symbol_type
1577  make_OP_X (location_type l)
1578  {
1579  return symbol_type (token::OP_X, std::move (l));
1580  }
1581 #else
1582  static
1583  symbol_type
1584  make_OP_X (const location_type& l)
1585  {
1586  return symbol_type (token::OP_X, l);
1587  }
1588 #endif
1589 #if 201103L <= YY_CPLUSPLUS
1590  static
1591  symbol_type
1592  make_OP_STRONG_X (location_type l)
1593  {
1594  return symbol_type (token::OP_STRONG_X, std::move (l));
1595  }
1596 #else
1597  static
1598  symbol_type
1599  make_OP_STRONG_X (const location_type& l)
1600  {
1601  return symbol_type (token::OP_STRONG_X, l);
1602  }
1603 #endif
1604 #if 201103L <= YY_CPLUSPLUS
1605  static
1606  symbol_type
1607  make_OP_NOT (location_type l)
1608  {
1609  return symbol_type (token::OP_NOT, std::move (l));
1610  }
1611 #else
1612  static
1613  symbol_type
1614  make_OP_NOT (const location_type& l)
1615  {
1616  return symbol_type (token::OP_NOT, l);
1617  }
1618 #endif
1619 #if 201103L <= YY_CPLUSPLUS
1620  static
1621  symbol_type
1622  make_OP_XREP (location_type l)
1623  {
1624  return symbol_type (token::OP_XREP, std::move (l));
1625  }
1626 #else
1627  static
1628  symbol_type
1629  make_OP_XREP (const location_type& l)
1630  {
1631  return symbol_type (token::OP_XREP, l);
1632  }
1633 #endif
1634 #if 201103L <= YY_CPLUSPLUS
1635  static
1636  symbol_type
1637  make_OP_FREP (location_type l)
1638  {
1639  return symbol_type (token::OP_FREP, std::move (l));
1640  }
1641 #else
1642  static
1643  symbol_type
1644  make_OP_FREP (const location_type& l)
1645  {
1646  return symbol_type (token::OP_FREP, l);
1647  }
1648 #endif
1649 #if 201103L <= YY_CPLUSPLUS
1650  static
1651  symbol_type
1652  make_OP_GREP (location_type l)
1653  {
1654  return symbol_type (token::OP_GREP, std::move (l));
1655  }
1656 #else
1657  static
1658  symbol_type
1659  make_OP_GREP (const location_type& l)
1660  {
1661  return symbol_type (token::OP_GREP, l);
1662  }
1663 #endif
1664 #if 201103L <= YY_CPLUSPLUS
1665  static
1666  symbol_type
1667  make_OP_STAR (location_type l)
1668  {
1669  return symbol_type (token::OP_STAR, std::move (l));
1670  }
1671 #else
1672  static
1673  symbol_type
1674  make_OP_STAR (const location_type& l)
1675  {
1676  return symbol_type (token::OP_STAR, l);
1677  }
1678 #endif
1679 #if 201103L <= YY_CPLUSPLUS
1680  static
1681  symbol_type
1682  make_OP_BSTAR (location_type l)
1683  {
1684  return symbol_type (token::OP_BSTAR, std::move (l));
1685  }
1686 #else
1687  static
1688  symbol_type
1689  make_OP_BSTAR (const location_type& l)
1690  {
1691  return symbol_type (token::OP_BSTAR, l);
1692  }
1693 #endif
1694 #if 201103L <= YY_CPLUSPLUS
1695  static
1696  symbol_type
1697  make_OP_BFSTAR (location_type l)
1698  {
1699  return symbol_type (token::OP_BFSTAR, std::move (l));
1700  }
1701 #else
1702  static
1703  symbol_type
1704  make_OP_BFSTAR (const location_type& l)
1705  {
1706  return symbol_type (token::OP_BFSTAR, l);
1707  }
1708 #endif
1709 #if 201103L <= YY_CPLUSPLUS
1710  static
1711  symbol_type
1712  make_OP_PLUS (location_type l)
1713  {
1714  return symbol_type (token::OP_PLUS, std::move (l));
1715  }
1716 #else
1717  static
1718  symbol_type
1719  make_OP_PLUS (const location_type& l)
1720  {
1721  return symbol_type (token::OP_PLUS, l);
1722  }
1723 #endif
1724 #if 201103L <= YY_CPLUSPLUS
1725  static
1726  symbol_type
1727  make_OP_FPLUS (location_type l)
1728  {
1729  return symbol_type (token::OP_FPLUS, std::move (l));
1730  }
1731 #else
1732  static
1733  symbol_type
1734  make_OP_FPLUS (const location_type& l)
1735  {
1736  return symbol_type (token::OP_FPLUS, l);
1737  }
1738 #endif
1739 #if 201103L <= YY_CPLUSPLUS
1740  static
1741  symbol_type
1742  make_OP_STAR_OPEN (location_type l)
1743  {
1744  return symbol_type (token::OP_STAR_OPEN, std::move (l));
1745  }
1746 #else
1747  static
1748  symbol_type
1749  make_OP_STAR_OPEN (const location_type& l)
1750  {
1751  return symbol_type (token::OP_STAR_OPEN, l);
1752  }
1753 #endif
1754 #if 201103L <= YY_CPLUSPLUS
1755  static
1756  symbol_type
1757  make_OP_FSTAR_OPEN (location_type l)
1758  {
1759  return symbol_type (token::OP_FSTAR_OPEN, std::move (l));
1760  }
1761 #else
1762  static
1763  symbol_type
1764  make_OP_FSTAR_OPEN (const location_type& l)
1765  {
1766  return symbol_type (token::OP_FSTAR_OPEN, l);
1767  }
1768 #endif
1769 #if 201103L <= YY_CPLUSPLUS
1770  static
1771  symbol_type
1772  make_OP_EQUAL_OPEN (location_type l)
1773  {
1774  return symbol_type (token::OP_EQUAL_OPEN, std::move (l));
1775  }
1776 #else
1777  static
1778  symbol_type
1779  make_OP_EQUAL_OPEN (const location_type& l)
1780  {
1781  return symbol_type (token::OP_EQUAL_OPEN, l);
1782  }
1783 #endif
1784 #if 201103L <= YY_CPLUSPLUS
1785  static
1786  symbol_type
1787  make_OP_GOTO_OPEN (location_type l)
1788  {
1789  return symbol_type (token::OP_GOTO_OPEN, std::move (l));
1790  }
1791 #else
1792  static
1793  symbol_type
1794  make_OP_GOTO_OPEN (const location_type& l)
1795  {
1796  return symbol_type (token::OP_GOTO_OPEN, l);
1797  }
1798 #endif
1799 #if 201103L <= YY_CPLUSPLUS
1800  static
1801  symbol_type
1802  make_OP_SQBKT_CLOSE (location_type l)
1803  {
1804  return symbol_type (token::OP_SQBKT_CLOSE, std::move (l));
1805  }
1806 #else
1807  static
1808  symbol_type
1809  make_OP_SQBKT_CLOSE (const location_type& l)
1810  {
1811  return symbol_type (token::OP_SQBKT_CLOSE, l);
1812  }
1813 #endif
1814 #if 201103L <= YY_CPLUSPLUS
1815  static
1816  symbol_type
1817  make_OP_SQBKT_STRONG_CLOSE (location_type l)
1818  {
1819  return symbol_type (token::OP_SQBKT_STRONG_CLOSE, std::move (l));
1820  }
1821 #else
1822  static
1823  symbol_type
1824  make_OP_SQBKT_STRONG_CLOSE (const location_type& l)
1825  {
1826  return symbol_type (token::OP_SQBKT_STRONG_CLOSE, l);
1827  }
1828 #endif
1829 #if 201103L <= YY_CPLUSPLUS
1830  static
1831  symbol_type
1832  make_OP_SQBKT_NUM (unsigned v, location_type l)
1833  {
1834  return symbol_type (token::OP_SQBKT_NUM, std::move (v), std::move (l));
1835  }
1836 #else
1837  static
1838  symbol_type
1839  make_OP_SQBKT_NUM (const unsigned& v, const location_type& l)
1840  {
1841  return symbol_type (token::OP_SQBKT_NUM, v, l);
1842  }
1843 #endif
1844 #if 201103L <= YY_CPLUSPLUS
1845  static
1846  symbol_type
1847  make_OP_UNBOUNDED (location_type l)
1848  {
1849  return symbol_type (token::OP_UNBOUNDED, std::move (l));
1850  }
1851 #else
1852  static
1853  symbol_type
1854  make_OP_UNBOUNDED (const location_type& l)
1855  {
1856  return symbol_type (token::OP_UNBOUNDED, l);
1857  }
1858 #endif
1859 #if 201103L <= YY_CPLUSPLUS
1860  static
1861  symbol_type
1862  make_OP_SQBKT_SEP (location_type l)
1863  {
1864  return symbol_type (token::OP_SQBKT_SEP, std::move (l));
1865  }
1866 #else
1867  static
1868  symbol_type
1869  make_OP_SQBKT_SEP (const location_type& l)
1870  {
1871  return symbol_type (token::OP_SQBKT_SEP, l);
1872  }
1873 #endif
1874 #if 201103L <= YY_CPLUSPLUS
1875  static
1876  symbol_type
1877  make_OP_UCONCAT (location_type l)
1878  {
1879  return symbol_type (token::OP_UCONCAT, std::move (l));
1880  }
1881 #else
1882  static
1883  symbol_type
1884  make_OP_UCONCAT (const location_type& l)
1885  {
1886  return symbol_type (token::OP_UCONCAT, l);
1887  }
1888 #endif
1889 #if 201103L <= YY_CPLUSPLUS
1890  static
1891  symbol_type
1892  make_OP_ECONCAT (location_type l)
1893  {
1894  return symbol_type (token::OP_ECONCAT, std::move (l));
1895  }
1896 #else
1897  static
1898  symbol_type
1899  make_OP_ECONCAT (const location_type& l)
1900  {
1901  return symbol_type (token::OP_ECONCAT, l);
1902  }
1903 #endif
1904 #if 201103L <= YY_CPLUSPLUS
1905  static
1906  symbol_type
1907  make_OP_UCONCAT_NONO (location_type l)
1908  {
1909  return symbol_type (token::OP_UCONCAT_NONO, std::move (l));
1910  }
1911 #else
1912  static
1913  symbol_type
1914  make_OP_UCONCAT_NONO (const location_type& l)
1915  {
1916  return symbol_type (token::OP_UCONCAT_NONO, l);
1917  }
1918 #endif
1919 #if 201103L <= YY_CPLUSPLUS
1920  static
1921  symbol_type
1922  make_OP_ECONCAT_NONO (location_type l)
1923  {
1924  return symbol_type (token::OP_ECONCAT_NONO, std::move (l));
1925  }
1926 #else
1927  static
1928  symbol_type
1929  make_OP_ECONCAT_NONO (const location_type& l)
1930  {
1931  return symbol_type (token::OP_ECONCAT_NONO, l);
1932  }
1933 #endif
1934 #if 201103L <= YY_CPLUSPLUS
1935  static
1936  symbol_type
1937  make_OP_FIRST_MATCH (location_type l)
1938  {
1939  return symbol_type (token::OP_FIRST_MATCH, std::move (l));
1940  }
1941 #else
1942  static
1943  symbol_type
1944  make_OP_FIRST_MATCH (const location_type& l)
1945  {
1946  return symbol_type (token::OP_FIRST_MATCH, l);
1947  }
1948 #endif
1949 #if 201103L <= YY_CPLUSPLUS
1950  static
1951  symbol_type
1952  make_ATOMIC_PROP (std::string v, location_type l)
1953  {
1954  return symbol_type (token::ATOMIC_PROP, std::move (v), std::move (l));
1955  }
1956 #else
1957  static
1958  symbol_type
1959  make_ATOMIC_PROP (const std::string& v, const location_type& l)
1960  {
1961  return symbol_type (token::ATOMIC_PROP, v, l);
1962  }
1963 #endif
1964 #if 201103L <= YY_CPLUSPLUS
1965  static
1966  symbol_type
1967  make_OP_CONCAT (location_type l)
1968  {
1969  return symbol_type (token::OP_CONCAT, std::move (l));
1970  }
1971 #else
1972  static
1973  symbol_type
1974  make_OP_CONCAT (const location_type& l)
1975  {
1976  return symbol_type (token::OP_CONCAT, l);
1977  }
1978 #endif
1979 #if 201103L <= YY_CPLUSPLUS
1980  static
1981  symbol_type
1982  make_OP_FUSION (location_type l)
1983  {
1984  return symbol_type (token::OP_FUSION, std::move (l));
1985  }
1986 #else
1987  static
1988  symbol_type
1989  make_OP_FUSION (const location_type& l)
1990  {
1991  return symbol_type (token::OP_FUSION, l);
1992  }
1993 #endif
1994 #if 201103L <= YY_CPLUSPLUS
1995  static
1996  symbol_type
1997  make_CONST_TRUE (location_type l)
1998  {
1999  return symbol_type (token::CONST_TRUE, std::move (l));
2000  }
2001 #else
2002  static
2003  symbol_type
2004  make_CONST_TRUE (const location_type& l)
2005  {
2006  return symbol_type (token::CONST_TRUE, l);
2007  }
2008 #endif
2009 #if 201103L <= YY_CPLUSPLUS
2010  static
2011  symbol_type
2012  make_CONST_FALSE (location_type l)
2013  {
2014  return symbol_type (token::CONST_FALSE, std::move (l));
2015  }
2016 #else
2017  static
2018  symbol_type
2019  make_CONST_FALSE (const location_type& l)
2020  {
2021  return symbol_type (token::CONST_FALSE, l);
2022  }
2023 #endif
2024 #if 201103L <= YY_CPLUSPLUS
2025  static
2026  symbol_type
2027  make_END_OF_INPUT (location_type l)
2028  {
2029  return symbol_type (token::END_OF_INPUT, std::move (l));
2030  }
2031 #else
2032  static
2033  symbol_type
2034  make_END_OF_INPUT (const location_type& l)
2035  {
2036  return symbol_type (token::END_OF_INPUT, l);
2037  }
2038 #endif
2039 #if 201103L <= YY_CPLUSPLUS
2040  static
2041  symbol_type
2042  make_OP_POST_NEG (location_type l)
2043  {
2044  return symbol_type (token::OP_POST_NEG, std::move (l));
2045  }
2046 #else
2047  static
2048  symbol_type
2049  make_OP_POST_NEG (const location_type& l)
2050  {
2051  return symbol_type (token::OP_POST_NEG, l);
2052  }
2053 #endif
2054 #if 201103L <= YY_CPLUSPLUS
2055  static
2056  symbol_type
2057  make_OP_POST_POS (location_type l)
2058  {
2059  return symbol_type (token::OP_POST_POS, std::move (l));
2060  }
2061 #else
2062  static
2063  symbol_type
2064  make_OP_POST_POS (const location_type& l)
2065  {
2066  return symbol_type (token::OP_POST_POS, l);
2067  }
2068 #endif
2069 #if 201103L <= YY_CPLUSPLUS
2070  static
2071  symbol_type
2072  make_OP_DELAY_N (unsigned v, location_type l)
2073  {
2074  return symbol_type (token::OP_DELAY_N, std::move (v), std::move (l));
2075  }
2076 #else
2077  static
2078  symbol_type
2079  make_OP_DELAY_N (const unsigned& v, const location_type& l)
2080  {
2081  return symbol_type (token::OP_DELAY_N, v, l);
2082  }
2083 #endif
2084 #if 201103L <= YY_CPLUSPLUS
2085  static
2086  symbol_type
2087  make_OP_DELAY_OPEN (location_type l)
2088  {
2089  return symbol_type (token::OP_DELAY_OPEN, std::move (l));
2090  }
2091 #else
2092  static
2093  symbol_type
2094  make_OP_DELAY_OPEN (const location_type& l)
2095  {
2096  return symbol_type (token::OP_DELAY_OPEN, l);
2097  }
2098 #endif
2099 #if 201103L <= YY_CPLUSPLUS
2100  static
2101  symbol_type
2102  make_OP_DELAY_PLUS (location_type l)
2103  {
2104  return symbol_type (token::OP_DELAY_PLUS, std::move (l));
2105  }
2106 #else
2107  static
2108  symbol_type
2109  make_OP_DELAY_PLUS (const location_type& l)
2110  {
2111  return symbol_type (token::OP_DELAY_PLUS, l);
2112  }
2113 #endif
2114 #if 201103L <= YY_CPLUSPLUS
2115  static
2116  symbol_type
2117  make_OP_DELAY_STAR (location_type l)
2118  {
2119  return symbol_type (token::OP_DELAY_STAR, std::move (l));
2120  }
2121 #else
2122  static
2123  symbol_type
2124  make_OP_DELAY_STAR (const location_type& l)
2125  {
2126  return symbol_type (token::OP_DELAY_STAR, l);
2127  }
2128 #endif
2129 
2130 
2131  class context
2132  {
2133  public:
2134  context (const parser& yyparser, const symbol_type& yyla);
2135  const symbol_type& lookahead () const YY_NOEXCEPT { return yyla_; }
2136  symbol_kind_type token () const YY_NOEXCEPT { return yyla_.kind (); }
2137  const location_type& location () const YY_NOEXCEPT { return yyla_.location; }
2138 
2142  int expected_tokens (symbol_kind_type yyarg[], int yyargn) const;
2143 
2144  private:
2145  const parser& yyparser_;
2146  const symbol_type& yyla_;
2147  };
2148 
2149  private:
2150 #if YY_CPLUSPLUS < 201103L
2152  parser (const parser&);
2154  parser& operator= (const parser&);
2155 #endif
2156 
2157 
2159  typedef short state_type;
2160 
2162  int yy_syntax_error_arguments_ (const context& yyctx,
2163  symbol_kind_type yyarg[], int yyargn) const;
2164 
2167  virtual std::string yysyntax_error_ (const context& yyctx) const;
2171  static state_type yy_lr_goto_state_ (state_type yystate, int yysym);
2172 
2175  static bool yy_pact_value_is_default_ (int yyvalue) YY_NOEXCEPT;
2176 
2179  static bool yy_table_value_is_error_ (int yyvalue) YY_NOEXCEPT;
2180 
2181  static const signed char yypact_ninf_;
2182  static const signed char yytable_ninf_;
2183 
2187  static symbol_kind_type yytranslate_ (int t) YY_NOEXCEPT;
2188 
2190  static std::string yytnamerr_ (const char *yystr);
2191 
2193  static const char* const yytname_[];
2194 
2195 
2196  // Tables.
2197  // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
2198  // STATE-NUM.
2199  static const short yypact_[];
2200 
2201  // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM.
2202  // Performed when YYTABLE does not specify something else to do. Zero
2203  // means the default is an error.
2204  static const unsigned char yydefact_[];
2205 
2206  // YYPGOTO[NTERM-NUM].
2207  static const short yypgoto_[];
2208 
2209  // YYDEFGOTO[NTERM-NUM].
2210  static const unsigned char yydefgoto_[];
2211 
2212  // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If
2213  // positive, shift that token. If negative, reduce the rule whose
2214  // number is the opposite. If YYTABLE_NINF, syntax error.
2215  static const short yytable_[];
2216 
2217  static const short yycheck_[];
2218 
2219  // YYSTOS[STATE-NUM] -- The symbol kind of the accessing symbol of
2220  // state STATE-NUM.
2221  static const signed char yystos_[];
2222 
2223  // YYR1[RULE-NUM] -- Symbol kind of the left-hand side of rule RULE-NUM.
2224  static const signed char yyr1_[];
2225 
2226  // YYR2[RULE-NUM] -- Number of symbols on the right-hand side of rule RULE-NUM.
2227  static const signed char yyr2_[];
2228 
2229 
2230 #if TLYYDEBUG
2231  // YYRLINE[YYN] -- Source line where rule number YYN was defined.
2232  static const short yyrline_[];
2234  virtual void yy_reduce_print_ (int r) const;
2236  virtual void yy_stack_print_ () const;
2237 
2239  int yydebug_;
2241  std::ostream* yycdebug_;
2242 
2246  template <typename Base>
2247  void yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const;
2248 #endif
2249 
2254  template <typename Base>
2255  void yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const;
2256 
2257  private:
2259  struct by_state
2260  {
2262  by_state () YY_NOEXCEPT;
2263 
2265  typedef state_type kind_type;
2266 
2268  by_state (kind_type s) YY_NOEXCEPT;
2269 
2271  by_state (const by_state& that) YY_NOEXCEPT;
2272 
2274  void clear () YY_NOEXCEPT;
2275 
2277  void move (by_state& that);
2278 
2281  symbol_kind_type kind () const YY_NOEXCEPT;
2282 
2285  enum { empty_state = 0 };
2286 
2289  state_type state;
2290  };
2291 
2293  struct stack_symbol_type : basic_symbol<by_state>
2294  {
2296  typedef basic_symbol<by_state> super_type;
2298  stack_symbol_type ();
2300  stack_symbol_type (YY_RVREF (stack_symbol_type) that);
2302  stack_symbol_type (state_type s, YY_MOVE_REF (symbol_type) sym);
2303 #if YY_CPLUSPLUS < 201103L
2306  stack_symbol_type& operator= (stack_symbol_type& that);
2307 
2310  stack_symbol_type& operator= (const stack_symbol_type& that);
2311 #endif
2312  };
2313 
2315  template <typename T, typename S = std::vector<T> >
2316  class stack
2317  {
2318  public:
2319  // Hide our reversed order.
2320  typedef typename S::iterator iterator;
2321  typedef typename S::const_iterator const_iterator;
2322  typedef typename S::size_type size_type;
2323  typedef typename std::ptrdiff_t index_type;
2324 
2325  stack (size_type n = 200) YY_NOEXCEPT
2326  : seq_ (n)
2327  {}
2328 
2329 #if 201103L <= YY_CPLUSPLUS
2331  stack (const stack&) = delete;
2333  stack& operator= (const stack&) = delete;
2334 #endif
2335 
2339  const T&
2340  operator[] (index_type i) const
2341  {
2342  return seq_[size_type (size () - 1 - i)];
2343  }
2344 
2348  T&
2349  operator[] (index_type i)
2350  {
2351  return seq_[size_type (size () - 1 - i)];
2352  }
2353 
2357  void
2358  push (YY_MOVE_REF (T) t)
2359  {
2360  seq_.push_back (T ());
2361  operator[] (0).move (t);
2362  }
2363 
2365  void
2366  pop (std::ptrdiff_t n = 1) YY_NOEXCEPT
2367  {
2368  for (; 0 < n; --n)
2369  seq_.pop_back ();
2370  }
2371 
2373  void
2374  clear () YY_NOEXCEPT
2375  {
2376  seq_.clear ();
2377  }
2378 
2380  index_type
2381  size () const YY_NOEXCEPT
2382  {
2383  return index_type (seq_.size ());
2384  }
2385 
2387  const_iterator
2388  begin () const YY_NOEXCEPT
2389  {
2390  return seq_.begin ();
2391  }
2392 
2394  const_iterator
2395  end () const YY_NOEXCEPT
2396  {
2397  return seq_.end ();
2398  }
2399 
2401  class slice
2402  {
2403  public:
2404  slice (const stack& stack, index_type range) YY_NOEXCEPT
2405  : stack_ (stack)
2406  , range_ (range)
2407  {}
2408 
2409  const T&
2410  operator[] (index_type i) const
2411  {
2412  return stack_[range_ - i];
2413  }
2414 
2415  private:
2416  const stack& stack_;
2417  index_type range_;
2418  };
2419 
2420  private:
2421 #if YY_CPLUSPLUS < 201103L
2423  stack (const stack&);
2425  stack& operator= (const stack&);
2426 #endif
2428  S seq_;
2429  };
2430 
2431 
2433  typedef stack<stack_symbol_type> stack_type;
2434 
2436  stack_type yystack_;
2437 
2443  void yypush_ (const char* m, YY_MOVE_REF (stack_symbol_type) sym);
2444 
2451  void yypush_ (const char* m, state_type s, YY_MOVE_REF (symbol_type) sym);
2452 
2454  void yypop_ (int n = 1) YY_NOEXCEPT;
2455 
2457  enum
2458  {
2459  yylast_ = 2385,
2460  yynnts_ = 23,
2461  yyfinal_ = 79
2462  };
2463 
2464 
2465  // User arguments.
2466  spot::parse_error_list &error_list;
2467  spot::environment &parse_environment;
2468  spot::formula &result;
2469 
2470  };
2471 
2472 
2473 } // tlyy
2474 #line 2475 "parsetl.hh"
2475 
2476 
2477 
2478 
2479 #endif // !YY_TLYY_PARSETL_HH_INCLUDED
An environment that describes atomic propositions.
Definition: environment.hh:33
Actual storage for formula nodes.
Definition: formula.hh:128
static const fnode * multop(op o, std::vector< const fnode * > l)
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:134
Main class for temporal logic formula.
Definition: formula.hh:715
Definition: parsetl.hh:2132
int expected_tokens(symbol_kind_type yyarg[], int yyargn) const
Present a slice of the top of a stack.
Definition: parsetl.hh:2402
Definition: parsetl.hh:370
value_type self_type
Type of *this.
Definition: parsetl.hh:373
T & build()
Definition: parsetl.hh:428
T & as()
Accessor to a built T.
Definition: parsetl.hh:445
void move(self_type &that)
Definition: parsetl.hh:478
void destroy()
Destroy the stored T.
Definition: parsetl.hh:511
value_type()
Empty construction.
Definition: parsetl.hh:376
char yyraw_[size]
A buffer large enough to store any of the semantic values.
Definition: parsetl.hh:584
T & emplace()
Instantiate an empty T in here.
Definition: parsetl.hh:410
void swap(self_type &that)
Definition: parsetl.hh:468
long double yyalign_me_
Strongest alignment constraints.
Definition: parsetl.hh:582
void copy(const self_type &that)
Copy the content of that to this.
Definition: parsetl.hh:503
~value_type()
Destruction, allowed only if empty.
Definition: parsetl.hh:395
const T & as() const
Const accessor to a built T (for printer).
Definition: parsetl.hh:453
T & emplace(const T &t)
Instantiate a T in here from t.
Definition: parsetl.hh:418
T & build(const T &t)
Definition: parsetl.hh:437
value_type(const T &t)
Construct and fill.
Definition: parsetl.hh:382
A Bison parser.
Definition: parsetl.hh:356
parser(spot::parse_error_list &error_list_yyarg, spot::environment &parse_environment_yyarg, spot::formula &result_yyarg)
Build a parser object.
token::token_kind_type token_kind_type
Token kind, as returned by yylex.
Definition: parsetl.hh:689
void set_debug_level(debug_level_type l)
Set the current debugging level.
static const symbol_kind_type YYNTOKENS
The number of tokens.
Definition: parsetl.hh:811
int debug_level_type
Type for debugging levels.
Definition: parsetl.hh:1149
symbol_kind::symbol_kind_type symbol_kind_type
(Internal) symbol kind.
Definition: parsetl.hh:808
value_type semantic_type
Backward compatibility (Bison 3.8).
Definition: parsetl.hh:590
virtual void error(const location_type &loc, const std::string &msg)
int operator()()
void set_debug_stream(std::ostream &)
Set the current debugging stream.
debug_level_type debug_level() const
The current debugging level.
token_kind_type token_type
Backward compatibility alias (Bison 3.6).
Definition: parsetl.hh:692
std::ostream & debug_stream() const
The current debugging stream.
static std::string symbol_name(symbol_kind_type yysymbol)
virtual int parse()
spot::location location_type
Symbol locations.
Definition: parsetl.hh:593
void error(const syntax_error &err)
Report a syntax error.
LTL/PSL formula interface.
op
Operator types.
Definition: formula.hh:79
std::list< one_parse_error > parse_error_list
A list of parser diagnostics, as filled by parse.
Definition: parse.hh:42
Definition: parsetl.hh:58
Definition: parsetl.hh:70
Definition: parsetl.hh:76
Definition: parsetl.hh:821
basic_symbol(const basic_symbol &that)
Copy constructor.
value_type value
The semantic value.
Definition: parsetl.hh:1032
symbol_kind_type type_get() const
Backward compatibility (Bison 3.6).
void clear()
Destroy contents, and record that is empty.
Definition: parsetl.hh:961
std::string name() const
The user-facing name of this symbol.
Definition: parsetl.hh:1017
location_type location
The location.
Definition: parsetl.hh:1035
bool empty() const
Whether empty.
~basic_symbol()
Destroy the symbol.
Definition: parsetl.hh:953
Base super_type
Alias to Base.
Definition: parsetl.hh:823
void move(basic_symbol &s)
Destructive move, s is emptied into this.
basic_symbol()
Default constructor.
Definition: parsetl.hh:826
basic_symbol(typename Base::kind_type t, const location_type &l)
Constructors for typed symbols.
Definition: parsetl.hh:890
Type access provider for token (enum) based symbols.
Definition: parsetl.hh:1046
symbol_kind_type kind_
Definition: parsetl.hh:1081
void move(by_kind &that)
Steal the symbol kind from that.
symbol_kind_type type_get() const
Backward compatibility (Bison 3.6).
symbol_kind_type kind() const
token_kind_type kind_type
The symbol kind as needed by the constructor.
Definition: parsetl.hh:1048
by_kind(const by_kind &that)
Copy constructor.
by_kind()
Default constructor.
by_kind(kind_type t)
Constructor from (external) token numbers.
void clear()
Record that this symbol is empty.
Symbol kinds.
Definition: parsetl.hh:696
symbol_kind_type
Definition: parsetl.hh:698
@ YYNTOKENS
Number of tokens.
Definition: parsetl.hh:699
"External" symbols: returned by the scanner.
Definition: parsetl.hh:1089
symbol_type()
Empty symbol.
Definition: parsetl.hh:1094
basic_symbol< by_kind > super_type
Superclass.
Definition: parsetl.hh:1091
Syntax errors thrown from user actions.
Definition: parsetl.hh:597
Token kinds.
Definition: parsetl.hh:615
token_kind_type yytokentype
Backward compatibility alias (Bison 3.6).
Definition: parsetl.hh:685

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1