1 /* A Bison parser, made by GNU Bison 3.7.5. */
2
3 /* Bison implementation for Yacc-like parsers in C
4
5 Copyright (C) 1984, 1989-1990, 2000-2015, 2018-2021 Free Software Foundation,
6 Inc.
7
8 This program is free software: you can redistribute it and/or modify
9 it under the terms of the GNU General Public License as published by
10 the Free Software Foundation, either version 3 of the License, or
11 (at your option) any later version.
12
13 This program is distributed in the hope that it will be useful,
14 but WITHOUT ANY WARRANTY; without even the implied warranty of
15 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16 GNU General Public License for more details.
17
18 You should have received a copy of the GNU General Public License
19 along with this program. If not, see <http://www.gnu.org/licenses/>. */
20
21 /* As a special exception, you may create a larger work that contains
22 part or all of the Bison parser skeleton and distribute that work
23 under terms of your choice, so long as that work isn't itself a
24 parser generator using the skeleton or a modified version thereof
25 as a parser skeleton. Alternatively, if you modify or redistribute
26 the parser skeleton itself, you may (at your option) remove this
27 special exception, which will cause the skeleton and the resulting
28 Bison output files to be licensed under the GNU General Public
29 License without this special exception.
30
31 This special exception was added by the Free Software Foundation in
32 version 2.2 of Bison. */
33
34 /* C LALR(1) parser skeleton written by Richard Stallman, by
35 simplifying the original so-called "semantic" parser. */
36
37 /* DO NOT RELY ON FEATURES THAT ARE NOT DOCUMENTED in the manual,
38 especially those whose name start with YY_ or yy_. They are
39 private implementation details that can be changed or removed. */
40
41 /* All symbols defined below should begin with yy or YY, to avoid
42 infringing on user name space. This should be done even for local
43 variables, as they might otherwise be expanded by user macros.
44 There are some unavoidable exceptions within include files to
45 define necessary library symbols; they are noted "INFRINGES ON
46 USER NAME SPACE" below. */
47
48 /* Identify Bison output, and Bison version. */
49 #define YYBISON 30705
50
51 /* Bison version string. */
52 #define YYBISON_VERSION "3.7.5"
53
54 /* Skeleton name. */
55 #define YYSKELETON_NAME "yacc.c"
56
57 /* Pure parsers. */
58 #define YYPURE 0
59
60 /* Push parsers. */
61 #define YYPUSH 0
62
63 /* Pull parsers. */
64 #define YYPULL 1
65
66
67
68
69 /* First part of user prologue. */
70 #line 8 "parser.y"
71
72 #include <string.h>
73 #include <stdarg.h>
74 #include <fstream>
75 #include <getopt.h>
76 #define IMPLEMENTSLIST /* Special for list template handling */
77 #include "slist.h"
78 #include "hashtbl.h"
79 #include "parser_.h"
80
81 using namespace std;
82
83 /* Definitions for storing and caching of identifiers */
84 #define inputTag 0
85 #define exprTag 1
86
87 struct nodeData
88 {
nodeDatanodeData89 nodeData(const nodeData &d) { tag=d.tag; name=sdup(d.name); val=d.val; }
nodeDatanodeData90 nodeData(int t, char *n, bdd v) { tag=t; name=n; val=v; }
~nodeDatanodeData91 ~nodeData(void) { delete[] name; }
92 int tag;
93 char *name;
94 bdd val;
95 };
96
97 typedef SList<nodeData> nodeLst;
98 nodeLst inputs;
99 hashTable names;
100
101 /* Other */
102 int linenum;
103
104 bddgbchandler gbcHandler = bdd_default_gbchandler;
105
106 /* Prototypes */
107 void actInit(token *nodes, token *cache);
108 void actInputs(void);
109 void actAddInput(token *id);
110 void actAssign(token *id, token *expr);
111 void actOpr2(token *res, token *left, token *right, int opr);
112 void actNot(token *res, token *right);
113 void actId(token *res, token *id);
114 void actConst(token *res, int);
115 void actSize(token *id);
116 void actDot(token *fname, token *id);
117 void actAutoreorder(token *times, token *method);
118 void actCache(void);
119 void actTautology(token *id);
120 void actExist(token *res, token *var, token *expr);
121 void actForall(token *res, token *var, token *expr);
122 void actQuantVar2(token *res, token *id, token *list);
123 void actQuantVar1(token *res, token *id);
124 void actPrint(token *id);
125
126
127 #line 128 "parser.c"
128
129 # ifndef YY_CAST
130 # ifdef __cplusplus
131 # define YY_CAST(Type, Val) static_cast<Type> (Val)
132 # define YY_REINTERPRET_CAST(Type, Val) reinterpret_cast<Type> (Val)
133 # else
134 # define YY_CAST(Type, Val) ((Type) (Val))
135 # define YY_REINTERPRET_CAST(Type, Val) ((Type) (Val))
136 # endif
137 # endif
138 # ifndef YY_NULLPTR
139 # if defined __cplusplus
140 # if 201103L <= __cplusplus
141 # define YY_NULLPTR nullptr
142 # else
143 # define YY_NULLPTR 0
144 # endif
145 # else
146 # define YY_NULLPTR ((void*)0)
147 # endif
148 # endif
149
150 /* Use api.header.include to #include this header
151 instead of duplicating it here. */
152 #ifndef YY_YY_PARSER_H_INCLUDED
153 # define YY_YY_PARSER_H_INCLUDED
154 /* Debug traces. */
155 #ifndef YYDEBUG
156 # define YYDEBUG 0
157 #endif
158 #if YYDEBUG
159 extern int yydebug;
160 #endif
161
162 /* Token kinds. */
163 #ifndef YYTOKENTYPE
164 # define YYTOKENTYPE
165 enum yytokentype
166 {
167 YYEMPTY = -2,
168 YYEOF = 0, /* "end of file" */
169 YYerror = 256, /* error */
170 YYUNDEF = 257, /* "invalid token" */
171 T_id = 258, /* T_id */
172 T_str = 259, /* T_str */
173 T_intval = 260, /* T_intval */
174 T_true = 261, /* T_true */
175 T_false = 262, /* T_false */
176 T_initial = 263, /* T_initial */
177 T_inputs = 264, /* T_inputs */
178 T_actions = 265, /* T_actions */
179 T_size = 266, /* T_size */
180 T_dumpdot = 267, /* T_dumpdot */
181 T_autoreorder = 268, /* T_autoreorder */
182 T_reorder = 269, /* T_reorder */
183 T_win2 = 270, /* T_win2 */
184 T_win2ite = 271, /* T_win2ite */
185 T_sift = 272, /* T_sift */
186 T_siftite = 273, /* T_siftite */
187 T_none = 274, /* T_none */
188 T_cache = 275, /* T_cache */
189 T_tautology = 276, /* T_tautology */
190 T_print = 277, /* T_print */
191 T_lpar = 278, /* T_lpar */
192 T_rpar = 279, /* T_rpar */
193 T_equal = 280, /* T_equal */
194 T_semi = 281, /* T_semi */
195 T_dot = 282, /* T_dot */
196 T_exist = 283, /* T_exist */
197 T_forall = 284, /* T_forall */
198 T_biimp = 285, /* T_biimp */
199 T_imp = 286, /* T_imp */
200 T_or = 287, /* T_or */
201 T_nor = 288, /* T_nor */
202 T_xor = 289, /* T_xor */
203 T_nand = 290, /* T_nand */
204 T_and = 291, /* T_and */
205 T_not = 292 /* T_not */
206 };
207 typedef enum yytokentype yytoken_kind_t;
208 #endif
209 /* Token kinds. */
210 #define YYEMPTY -2
211 #define YYEOF 0
212 #define YYerror 256
213 #define YYUNDEF 257
214 #define T_id 258
215 #define T_str 259
216 #define T_intval 260
217 #define T_true 261
218 #define T_false 262
219 #define T_initial 263
220 #define T_inputs 264
221 #define T_actions 265
222 #define T_size 266
223 #define T_dumpdot 267
224 #define T_autoreorder 268
225 #define T_reorder 269
226 #define T_win2 270
227 #define T_win2ite 271
228 #define T_sift 272
229 #define T_siftite 273
230 #define T_none 274
231 #define T_cache 275
232 #define T_tautology 276
233 #define T_print 277
234 #define T_lpar 278
235 #define T_rpar 279
236 #define T_equal 280
237 #define T_semi 281
238 #define T_dot 282
239 #define T_exist 283
240 #define T_forall 284
241 #define T_biimp 285
242 #define T_imp 286
243 #define T_or 287
244 #define T_nor 288
245 #define T_xor 289
246 #define T_nand 290
247 #define T_and 291
248 #define T_not 292
249
250 /* Value type. */
251 #if ! defined YYSTYPE && ! defined YYSTYPE_IS_DECLARED
252 typedef int YYSTYPE;
253 # define YYSTYPE_IS_TRIVIAL 1
254 # define YYSTYPE_IS_DECLARED 1
255 #endif
256
257
258 extern YYSTYPE yylval;
259
260 int yyparse (void);
261
262 #endif /* !YY_YY_PARSER_H_INCLUDED */
263 /* Symbol kind. */
264 enum yysymbol_kind_t
265 {
266 YYSYMBOL_YYEMPTY = -2,
267 YYSYMBOL_YYEOF = 0, /* "end of file" */
268 YYSYMBOL_YYerror = 1, /* error */
269 YYSYMBOL_YYUNDEF = 2, /* "invalid token" */
270 YYSYMBOL_T_id = 3, /* T_id */
271 YYSYMBOL_T_str = 4, /* T_str */
272 YYSYMBOL_T_intval = 5, /* T_intval */
273 YYSYMBOL_T_true = 6, /* T_true */
274 YYSYMBOL_T_false = 7, /* T_false */
275 YYSYMBOL_T_initial = 8, /* T_initial */
276 YYSYMBOL_T_inputs = 9, /* T_inputs */
277 YYSYMBOL_T_actions = 10, /* T_actions */
278 YYSYMBOL_T_size = 11, /* T_size */
279 YYSYMBOL_T_dumpdot = 12, /* T_dumpdot */
280 YYSYMBOL_T_autoreorder = 13, /* T_autoreorder */
281 YYSYMBOL_T_reorder = 14, /* T_reorder */
282 YYSYMBOL_T_win2 = 15, /* T_win2 */
283 YYSYMBOL_T_win2ite = 16, /* T_win2ite */
284 YYSYMBOL_T_sift = 17, /* T_sift */
285 YYSYMBOL_T_siftite = 18, /* T_siftite */
286 YYSYMBOL_T_none = 19, /* T_none */
287 YYSYMBOL_T_cache = 20, /* T_cache */
288 YYSYMBOL_T_tautology = 21, /* T_tautology */
289 YYSYMBOL_T_print = 22, /* T_print */
290 YYSYMBOL_T_lpar = 23, /* T_lpar */
291 YYSYMBOL_T_rpar = 24, /* T_rpar */
292 YYSYMBOL_T_equal = 25, /* T_equal */
293 YYSYMBOL_T_semi = 26, /* T_semi */
294 YYSYMBOL_T_dot = 27, /* T_dot */
295 YYSYMBOL_T_exist = 28, /* T_exist */
296 YYSYMBOL_T_forall = 29, /* T_forall */
297 YYSYMBOL_T_biimp = 30, /* T_biimp */
298 YYSYMBOL_T_imp = 31, /* T_imp */
299 YYSYMBOL_T_or = 32, /* T_or */
300 YYSYMBOL_T_nor = 33, /* T_nor */
301 YYSYMBOL_T_xor = 34, /* T_xor */
302 YYSYMBOL_T_nand = 35, /* T_nand */
303 YYSYMBOL_T_and = 36, /* T_and */
304 YYSYMBOL_T_not = 37, /* T_not */
305 YYSYMBOL_YYACCEPT = 38, /* $accept */
306 YYSYMBOL_calc = 39, /* calc */
307 YYSYMBOL_initial = 40, /* initial */
308 YYSYMBOL_inputs = 41, /* inputs */
309 YYSYMBOL_inputSeq = 42, /* inputSeq */
310 YYSYMBOL_actions = 43, /* actions */
311 YYSYMBOL_actionSeq = 44, /* actionSeq */
312 YYSYMBOL_action = 45, /* action */
313 YYSYMBOL_assign = 46, /* assign */
314 YYSYMBOL_expr = 47, /* expr */
315 YYSYMBOL_quantifier = 48, /* quantifier */
316 YYSYMBOL_varlist = 49, /* varlist */
317 YYSYMBOL_size = 50, /* size */
318 YYSYMBOL_dot = 51, /* dot */
319 YYSYMBOL_reorder = 52, /* reorder */
320 YYSYMBOL_method = 53, /* method */
321 YYSYMBOL_cache = 54, /* cache */
322 YYSYMBOL_tautology = 55, /* tautology */
323 YYSYMBOL_print = 56 /* print */
324 };
325 typedef enum yysymbol_kind_t yysymbol_kind_t;
326
327
328
329
330 #ifdef short
331 # undef short
332 #endif
333
334 /* On compilers that do not define __PTRDIFF_MAX__ etc., make sure
335 <limits.h> and (if available) <stdint.h> are included
336 so that the code can choose integer types of a good width. */
337
338 #ifndef __PTRDIFF_MAX__
339 # include <limits.h> /* INFRINGES ON USER NAME SPACE */
340 # if defined __STDC_VERSION__ && 199901 <= __STDC_VERSION__
341 # include <stdint.h> /* INFRINGES ON USER NAME SPACE */
342 # define YY_STDINT_H
343 # endif
344 #endif
345
346 /* Narrow types that promote to a signed type and that can represent a
347 signed or unsigned integer of at least N bits. In tables they can
348 save space and decrease cache pressure. Promoting to a signed type
349 helps avoid bugs in integer arithmetic. */
350
351 #ifdef __INT_LEAST8_MAX__
352 typedef __INT_LEAST8_TYPE__ yytype_int8;
353 #elif defined YY_STDINT_H
354 typedef int_least8_t yytype_int8;
355 #else
356 typedef signed char yytype_int8;
357 #endif
358
359 #ifdef __INT_LEAST16_MAX__
360 typedef __INT_LEAST16_TYPE__ yytype_int16;
361 #elif defined YY_STDINT_H
362 typedef int_least16_t yytype_int16;
363 #else
364 typedef short yytype_int16;
365 #endif
366
367 /* Work around bug in HP-UX 11.23, which defines these macros
368 incorrectly for preprocessor constants. This workaround can likely
369 be removed in 2023, as HPE has promised support for HP-UX 11.23
370 (aka HP-UX 11i v2) only through the end of 2022; see Table 2 of
371 <https://h20195.www2.hpe.com/V2/getpdf.aspx/4AA4-7673ENW.pdf>. */
372 #ifdef __hpux
373 # undef UINT_LEAST8_MAX
374 # undef UINT_LEAST16_MAX
375 # define UINT_LEAST8_MAX 255
376 # define UINT_LEAST16_MAX 65535
377 #endif
378
379 #if defined __UINT_LEAST8_MAX__ && __UINT_LEAST8_MAX__ <= __INT_MAX__
380 typedef __UINT_LEAST8_TYPE__ yytype_uint8;
381 #elif (!defined __UINT_LEAST8_MAX__ && defined YY_STDINT_H \
382 && UINT_LEAST8_MAX <= INT_MAX)
383 typedef uint_least8_t yytype_uint8;
384 #elif !defined __UINT_LEAST8_MAX__ && UCHAR_MAX <= INT_MAX
385 typedef unsigned char yytype_uint8;
386 #else
387 typedef short yytype_uint8;
388 #endif
389
390 #if defined __UINT_LEAST16_MAX__ && __UINT_LEAST16_MAX__ <= __INT_MAX__
391 typedef __UINT_LEAST16_TYPE__ yytype_uint16;
392 #elif (!defined __UINT_LEAST16_MAX__ && defined YY_STDINT_H \
393 && UINT_LEAST16_MAX <= INT_MAX)
394 typedef uint_least16_t yytype_uint16;
395 #elif !defined __UINT_LEAST16_MAX__ && USHRT_MAX <= INT_MAX
396 typedef unsigned short yytype_uint16;
397 #else
398 typedef int yytype_uint16;
399 #endif
400
401 #ifndef YYPTRDIFF_T
402 # if defined __PTRDIFF_TYPE__ && defined __PTRDIFF_MAX__
403 # define YYPTRDIFF_T __PTRDIFF_TYPE__
404 # define YYPTRDIFF_MAXIMUM __PTRDIFF_MAX__
405 # elif defined PTRDIFF_MAX
406 # ifndef ptrdiff_t
407 # include <stddef.h> /* INFRINGES ON USER NAME SPACE */
408 # endif
409 # define YYPTRDIFF_T ptrdiff_t
410 # define YYPTRDIFF_MAXIMUM PTRDIFF_MAX
411 # else
412 # define YYPTRDIFF_T long
413 # define YYPTRDIFF_MAXIMUM LONG_MAX
414 # endif
415 #endif
416
417 #ifndef YYSIZE_T
418 # ifdef __SIZE_TYPE__
419 # define YYSIZE_T __SIZE_TYPE__
420 # elif defined size_t
421 # define YYSIZE_T size_t
422 # elif defined __STDC_VERSION__ && 199901 <= __STDC_VERSION__
423 # include <stddef.h> /* INFRINGES ON USER NAME SPACE */
424 # define YYSIZE_T size_t
425 # else
426 # define YYSIZE_T unsigned
427 # endif
428 #endif
429
430 #define YYSIZE_MAXIMUM \
431 YY_CAST (YYPTRDIFF_T, \
432 (YYPTRDIFF_MAXIMUM < YY_CAST (YYSIZE_T, -1) \
433 ? YYPTRDIFF_MAXIMUM \
434 : YY_CAST (YYSIZE_T, -1)))
435
436 #define YYSIZEOF(X) YY_CAST (YYPTRDIFF_T, sizeof (X))
437
438
439 /* Stored state numbers (used for stacks). */
440 typedef yytype_int8 yy_state_t;
441
442 /* State numbers in computations. */
443 typedef int yy_state_fast_t;
444
445 #ifndef YY_
446 # if defined YYENABLE_NLS && YYENABLE_NLS
447 # if ENABLE_NLS
448 # include <libintl.h> /* INFRINGES ON USER NAME SPACE */
449 # define YY_(Msgid) dgettext ("bison-runtime", Msgid)
450 # endif
451 # endif
452 # ifndef YY_
453 # define YY_(Msgid) Msgid
454 # endif
455 #endif
456
457
458 #ifndef YY_ATTRIBUTE_PURE
459 # if defined __GNUC__ && 2 < __GNUC__ + (96 <= __GNUC_MINOR__)
460 # define YY_ATTRIBUTE_PURE __attribute__ ((__pure__))
461 # else
462 # define YY_ATTRIBUTE_PURE
463 # endif
464 #endif
465
466 #ifndef YY_ATTRIBUTE_UNUSED
467 # if defined __GNUC__ && 2 < __GNUC__ + (7 <= __GNUC_MINOR__)
468 # define YY_ATTRIBUTE_UNUSED __attribute__ ((__unused__))
469 # else
470 # define YY_ATTRIBUTE_UNUSED
471 # endif
472 #endif
473
474 /* Suppress unused-variable warnings by "using" E. */
475 #if ! defined lint || defined __GNUC__
476 # define YY_USE(E) ((void) (E))
477 #else
478 # define YY_USE(E) /* empty */
479 #endif
480
481 #if defined __GNUC__ && ! defined __ICC && 407 <= __GNUC__ * 100 + __GNUC_MINOR__
482 /* Suppress an incorrect diagnostic about yylval being uninitialized. */
483 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
484 _Pragma ("GCC diagnostic push") \
485 _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"") \
486 _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
487 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \
488 _Pragma ("GCC diagnostic pop")
489 #else
490 # define YY_INITIAL_VALUE(Value) Value
491 #endif
492 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
493 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
494 # define YY_IGNORE_MAYBE_UNINITIALIZED_END
495 #endif
496 #ifndef YY_INITIAL_VALUE
497 # define YY_INITIAL_VALUE(Value) /* Nothing. */
498 #endif
499
500 #if defined __cplusplus && defined __GNUC__ && ! defined __ICC && 6 <= __GNUC__
501 # define YY_IGNORE_USELESS_CAST_BEGIN \
502 _Pragma ("GCC diagnostic push") \
503 _Pragma ("GCC diagnostic ignored \"-Wuseless-cast\"")
504 # define YY_IGNORE_USELESS_CAST_END \
505 _Pragma ("GCC diagnostic pop")
506 #endif
507 #ifndef YY_IGNORE_USELESS_CAST_BEGIN
508 # define YY_IGNORE_USELESS_CAST_BEGIN
509 # define YY_IGNORE_USELESS_CAST_END
510 #endif
511
512
513 #define YY_ASSERT(E) ((void) (0 && (E)))
514
515 #if !defined yyoverflow
516
517 /* The parser invokes alloca or malloc; define the necessary symbols. */
518
519 # ifdef YYSTACK_USE_ALLOCA
520 # if YYSTACK_USE_ALLOCA
521 # ifdef __GNUC__
522 # define YYSTACK_ALLOC __builtin_alloca
523 # elif defined __BUILTIN_VA_ARG_INCR
524 # include <alloca.h> /* INFRINGES ON USER NAME SPACE */
525 # elif defined _AIX
526 # define YYSTACK_ALLOC __alloca
527 # elif defined _MSC_VER
528 # include <malloc.h> /* INFRINGES ON USER NAME SPACE */
529 # define alloca _alloca
530 # else
531 # define YYSTACK_ALLOC alloca
532 # if ! defined _ALLOCA_H && ! defined EXIT_SUCCESS
533 # include <stdlib.h> /* INFRINGES ON USER NAME SPACE */
534 /* Use EXIT_SUCCESS as a witness for stdlib.h. */
535 # ifndef EXIT_SUCCESS
536 # define EXIT_SUCCESS 0
537 # endif
538 # endif
539 # endif
540 # endif
541 # endif
542
543 # ifdef YYSTACK_ALLOC
544 /* Pacify GCC's 'empty if-body' warning. */
545 # define YYSTACK_FREE(Ptr) do { /* empty */; } while (0)
546 # ifndef YYSTACK_ALLOC_MAXIMUM
547 /* The OS might guarantee only one guard page at the bottom of the stack,
548 and a page size can be as small as 4096 bytes. So we cannot safely
549 invoke alloca (N) if N exceeds 4096. Use a slightly smaller number
550 to allow for a few compiler-allocated temporary stack slots. */
551 # define YYSTACK_ALLOC_MAXIMUM 4032 /* reasonable circa 2006 */
552 # endif
553 # else
554 # define YYSTACK_ALLOC YYMALLOC
555 # define YYSTACK_FREE YYFREE
556 # ifndef YYSTACK_ALLOC_MAXIMUM
557 # define YYSTACK_ALLOC_MAXIMUM YYSIZE_MAXIMUM
558 # endif
559 # if (defined __cplusplus && ! defined EXIT_SUCCESS \
560 && ! ((defined YYMALLOC || defined malloc) \
561 && (defined YYFREE || defined free)))
562 # include <stdlib.h> /* INFRINGES ON USER NAME SPACE */
563 # ifndef EXIT_SUCCESS
564 # define EXIT_SUCCESS 0
565 # endif
566 # endif
567 # ifndef YYMALLOC
568 # define YYMALLOC malloc
569 # if ! defined malloc && ! defined EXIT_SUCCESS
570 void *malloc (YYSIZE_T); /* INFRINGES ON USER NAME SPACE */
571 # endif
572 # endif
573 # ifndef YYFREE
574 # define YYFREE free
575 # if ! defined free && ! defined EXIT_SUCCESS
576 void free (void *); /* INFRINGES ON USER NAME SPACE */
577 # endif
578 # endif
579 # endif
580 #endif /* !defined yyoverflow */
581
582 #if (! defined yyoverflow \
583 && (! defined __cplusplus \
584 || (defined YYSTYPE_IS_TRIVIAL && YYSTYPE_IS_TRIVIAL)))
585
586 /* A type that is properly aligned for any stack member. */
587 union yyalloc
588 {
589 yy_state_t yyss_alloc;
590 YYSTYPE yyvs_alloc;
591 };
592
593 /* The size of the maximum gap between one aligned stack and the next. */
594 # define YYSTACK_GAP_MAXIMUM (YYSIZEOF (union yyalloc) - 1)
595
596 /* The size of an array large to enough to hold all stacks, each with
597 N elements. */
598 # define YYSTACK_BYTES(N) \
599 ((N) * (YYSIZEOF (yy_state_t) + YYSIZEOF (YYSTYPE)) \
600 + YYSTACK_GAP_MAXIMUM)
601
602 # define YYCOPY_NEEDED 1
603
604 /* Relocate STACK from its old location to the new one. The
605 local variables YYSIZE and YYSTACKSIZE give the old and new number of
606 elements in the stack, and YYPTR gives the new location of the
607 stack. Advance YYPTR to a properly aligned location for the next
608 stack. */
609 # define YYSTACK_RELOCATE(Stack_alloc, Stack) \
610 do \
611 { \
612 YYPTRDIFF_T yynewbytes; \
613 YYCOPY (&yyptr->Stack_alloc, Stack, yysize); \
614 Stack = &yyptr->Stack_alloc; \
615 yynewbytes = yystacksize * YYSIZEOF (*Stack) + YYSTACK_GAP_MAXIMUM; \
616 yyptr += yynewbytes / YYSIZEOF (*yyptr); \
617 } \
618 while (0)
619
620 #endif
621
622 #if defined YYCOPY_NEEDED && YYCOPY_NEEDED
623 /* Copy COUNT objects from SRC to DST. The source and destination do
624 not overlap. */
625 # ifndef YYCOPY
626 # if defined __GNUC__ && 1 < __GNUC__
627 # define YYCOPY(Dst, Src, Count) \
628 __builtin_memcpy (Dst, Src, YY_CAST (YYSIZE_T, (Count)) * sizeof (*(Src)))
629 # else
630 # define YYCOPY(Dst, Src, Count) \
631 do \
632 { \
633 YYPTRDIFF_T yyi; \
634 for (yyi = 0; yyi < (Count); yyi++) \
635 (Dst)[yyi] = (Src)[yyi]; \
636 } \
637 while (0)
638 # endif
639 # endif
640 #endif /* !YYCOPY_NEEDED */
641
642 /* YYFINAL -- State number of the termination state. */
643 #define YYFINAL 5
644 /* YYLAST -- Last index in YYTABLE. */
645 #define YYLAST 88
646
647 /* YYNTOKENS -- Number of terminals. */
648 #define YYNTOKENS 38
649 /* YYNNTS -- Number of nonterminals. */
650 #define YYNNTS 19
651 /* YYNRULES -- Number of rules. */
652 #define YYNRULES 46
653 /* YYNSTATES -- Number of states. */
654 #define YYNSTATES 84
655
656 /* YYMAXUTOK -- Last valid token kind. */
657 #define YYMAXUTOK 292
658
659
660 /* YYTRANSLATE(TOKEN-NUM) -- Symbol number corresponding to TOKEN-NUM
661 as returned by yylex, with out-of-bounds checking. */
662 #define YYTRANSLATE(YYX) \
663 (0 <= (YYX) && (YYX) <= YYMAXUTOK \
664 ? YY_CAST (yysymbol_kind_t, yytranslate[YYX]) \
665 : YYSYMBOL_YYUNDEF)
666
667 /* YYTRANSLATE[TOKEN-NUM] -- Symbol number corresponding to TOKEN-NUM
668 as returned by yylex. */
669 static const yytype_int8 yytranslate[] =
670 {
671 0, 2, 2, 2, 2, 2, 2, 2, 2, 2,
672 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
673 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
674 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
675 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
676 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
677 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
678 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
679 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
680 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
681 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
682 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
683 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
684 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
685 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
686 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
687 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
688 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
689 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
690 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
691 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
692 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
693 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
694 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
695 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
696 2, 2, 2, 2, 2, 2, 1, 2, 3, 4,
697 5, 6, 7, 8, 9, 10, 11, 12, 13, 14,
698 15, 16, 17, 18, 19, 20, 21, 22, 23, 24,
699 25, 26, 27, 28, 29, 30, 31, 32, 33, 34,
700 35, 36, 37
701 };
702
703 #if YYDEBUG
704 /* YYRLINE[YYN] -- Source line where rule number YYN was defined. */
705 static const yytype_uint8 yyrline[] =
706 {
707 0, 96, 96, 102, 106, 110, 111, 118, 122, 123,
708 127, 128, 129, 130, 131, 132, 133, 137, 141, 142,
709 143, 144, 145, 146, 147, 148, 149, 150, 151, 152,
710 153, 157, 158, 162, 163, 168, 172, 176, 177, 181,
711 182, 183, 184, 185, 189, 193, 197
712 };
713 #endif
714
715 /** Accessing symbol of state STATE. */
716 #define YY_ACCESSING_SYMBOL(State) YY_CAST (yysymbol_kind_t, yystos[State])
717
718 #if YYDEBUG || 0
719 /* The user-facing name of the symbol whose (internal) number is
720 YYSYMBOL. No bounds checking. */
721 static const char *yysymbol_name (yysymbol_kind_t yysymbol) YY_ATTRIBUTE_UNUSED;
722
723 /* YYTNAME[SYMBOL-NUM] -- String name of the symbol SYMBOL-NUM.
724 First, the terminals, then, starting at YYNTOKENS, nonterminals. */
725 static const char *const yytname[] =
726 {
727 "\"end of file\"", "error", "\"invalid token\"", "T_id", "T_str",
728 "T_intval", "T_true", "T_false", "T_initial", "T_inputs", "T_actions",
729 "T_size", "T_dumpdot", "T_autoreorder", "T_reorder", "T_win2",
730 "T_win2ite", "T_sift", "T_siftite", "T_none", "T_cache", "T_tautology",
731 "T_print", "T_lpar", "T_rpar", "T_equal", "T_semi", "T_dot", "T_exist",
732 "T_forall", "T_biimp", "T_imp", "T_or", "T_nor", "T_xor", "T_nand",
733 "T_and", "T_not", "$accept", "calc", "initial", "inputs", "inputSeq",
734 "actions", "actionSeq", "action", "assign", "expr", "quantifier",
735 "varlist", "size", "dot", "reorder", "method", "cache", "tautology",
736 "print", YY_NULLPTR
737 };
738
739 static const char *
yysymbol_name(yysymbol_kind_t yysymbol)740 yysymbol_name (yysymbol_kind_t yysymbol)
741 {
742 return yytname[yysymbol];
743 }
744 #endif
745
746 #ifdef YYPRINT
747 /* YYTOKNUM[NUM] -- (External) token number corresponding to the
748 (internal) symbol number NUM (which must be that of a token). */
749 static const yytype_int16 yytoknum[] =
750 {
751 0, 256, 257, 258, 259, 260, 261, 262, 263, 264,
752 265, 266, 267, 268, 269, 270, 271, 272, 273, 274,
753 275, 276, 277, 278, 279, 280, 281, 282, 283, 284,
754 285, 286, 287, 288, 289, 290, 291, 292
755 };
756 #endif
757
758 #define YYPACT_NINF (-38)
759
760 #define yypact_value_is_default(Yyn) \
761 ((Yyn) == YYPACT_NINF)
762
763 #define YYTABLE_NINF (-1)
764
765 #define yytable_value_is_error(Yyn) \
766 0
767
768 /* YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
769 STATE-NUM. */
770 static const yytype_int8 yypact[] =
771 {
772 -6, 7, 15, 14, 46, -38, 49, 44, 50, -38,
773 -2, 36, -38, -38, -38, -38, 30, 74, 75, 73,
774 51, -38, 77, 78, 36, 56, -38, -38, -38, -38,
775 -38, -38, -38, -3, -38, 80, 51, -38, -38, -38,
776 -38, -38, -38, -38, -38, 58, -38, -38, -38, -38,
777 -3, 82, 82, -3, 10, -38, -38, -38, -38, 29,
778 -38, 8, 11, -38, -3, -3, -3, -3, -3, -3,
779 -3, -38, -38, -3, -3, -26, 39, -17, -17, -14,
780 -38, -38, 10, 10
781 };
782
783 /* YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM.
784 Performed when YYTABLE does not specify something else to do. Zero
785 means the default is an error. */
786 static const yytype_int8 yydefact[] =
787 {
788 0, 0, 0, 0, 0, 1, 0, 0, 0, 6,
789 0, 0, 2, 3, 5, 4, 0, 0, 0, 0,
790 0, 44, 0, 0, 7, 0, 10, 11, 12, 13,
791 14, 15, 16, 0, 35, 0, 0, 39, 40, 41,
792 42, 43, 37, 45, 46, 0, 9, 27, 28, 29,
793 0, 0, 0, 0, 17, 30, 36, 38, 8, 0,
794 34, 0, 0, 25, 0, 0, 0, 0, 0, 0,
795 0, 26, 33, 0, 0, 24, 23, 21, 22, 20,
796 19, 18, 31, 32
797 };
798
799 /* YYPGOTO[NTERM-NUM]. */
800 static const yytype_int8 yypgoto[] =
801 {
802 -38, -38, -38, -38, -38, -38, -38, 62, -38, -37,
803 -38, 35, -38, -38, -38, 52, -38, -38, -38
804 };
805
806 /* YYDEFGOTO[NTERM-NUM]. */
807 static const yytype_int8 yydefgoto[] =
808 {
809 0, 2, 3, 7, 10, 12, 24, 25, 26, 54,
810 55, 61, 27, 28, 29, 42, 30, 31, 32
811 };
812
813 /* YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If
814 positive, shift that token. If negative, reduce the rule whose
815 number is the opposite. If YYTABLE_NINF, syntax error. */
816 static const yytype_int8 yytable[] =
817 {
818 47, 14, 1, 48, 49, 65, 66, 67, 68, 69,
819 70, 72, 4, 59, 72, 5, 63, 68, 69, 70,
820 50, 69, 70, 6, 15, 51, 52, 75, 76, 77,
821 78, 79, 80, 81, 53, 73, 82, 83, 74, 16,
822 64, 65, 66, 67, 68, 69, 70, 17, 18, 19,
823 20, 8, 9, 71, 11, 33, 21, 22, 23, 64,
824 65, 66, 67, 68, 69, 70, 37, 38, 39, 40,
825 41, 66, 67, 68, 69, 70, 13, 34, 36, 35,
826 43, 44, 46, 56, 58, 60, 45, 62, 57
827 };
828
829 static const yytype_int8 yycheck[] =
830 {
831 3, 3, 8, 6, 7, 31, 32, 33, 34, 35,
832 36, 3, 5, 50, 3, 0, 53, 34, 35, 36,
833 23, 35, 36, 9, 26, 28, 29, 64, 65, 66,
834 67, 68, 69, 70, 37, 27, 73, 74, 27, 3,
835 30, 31, 32, 33, 34, 35, 36, 11, 12, 13,
836 14, 5, 3, 24, 10, 25, 20, 21, 22, 30,
837 31, 32, 33, 34, 35, 36, 15, 16, 17, 18,
838 19, 32, 33, 34, 35, 36, 26, 3, 5, 4,
839 3, 3, 26, 3, 26, 3, 24, 52, 36
840 };
841
842 /* YYSTOS[STATE-NUM] -- The (internal number of the) accessing
843 symbol of state STATE-NUM. */
844 static const yytype_int8 yystos[] =
845 {
846 0, 8, 39, 40, 5, 0, 9, 41, 5, 3,
847 42, 10, 43, 26, 3, 26, 3, 11, 12, 13,
848 14, 20, 21, 22, 44, 45, 46, 50, 51, 52,
849 54, 55, 56, 25, 3, 4, 5, 15, 16, 17,
850 18, 19, 53, 3, 3, 45, 26, 3, 6, 7,
851 23, 28, 29, 37, 47, 48, 3, 53, 26, 47,
852 3, 49, 49, 47, 30, 31, 32, 33, 34, 35,
853 36, 24, 3, 27, 27, 47, 47, 47, 47, 47,
854 47, 47, 47, 47
855 };
856
857 /* YYR1[YYN] -- Symbol number of symbol that rule YYN derives. */
858 static const yytype_int8 yyr1[] =
859 {
860 0, 38, 39, 40, 41, 42, 42, 43, 44, 44,
861 45, 45, 45, 45, 45, 45, 45, 46, 47, 47,
862 47, 47, 47, 47, 47, 47, 47, 47, 47, 47,
863 47, 48, 48, 49, 49, 50, 51, 52, 52, 53,
864 53, 53, 53, 53, 54, 55, 56
865 };
866
867 /* YYR2[YYN] -- Number of symbols on the right hand side of rule YYN. */
868 static const yytype_int8 yyr2[] =
869 {
870 0, 2, 3, 4, 3, 2, 1, 2, 3, 2,
871 1, 1, 1, 1, 1, 1, 1, 3, 3, 3,
872 3, 3, 3, 3, 3, 2, 3, 1, 1, 1,
873 1, 4, 4, 2, 1, 2, 3, 2, 3, 1,
874 1, 1, 1, 1, 1, 2, 2
875 };
876
877
878 enum { YYENOMEM = -2 };
879
880 #define yyerrok (yyerrstatus = 0)
881 #define yyclearin (yychar = YYEMPTY)
882
883 #define YYACCEPT goto yyacceptlab
884 #define YYABORT goto yyabortlab
885 #define YYERROR goto yyerrorlab
886
887
888 #define YYRECOVERING() (!!yyerrstatus)
889
890 #define YYBACKUP(Token, Value) \
891 do \
892 if (yychar == YYEMPTY) \
893 { \
894 yychar = (Token); \
895 yylval = (Value); \
896 YYPOPSTACK (yylen); \
897 yystate = *yyssp; \
898 goto yybackup; \
899 } \
900 else \
901 { \
902 yyerror (YY_("syntax error: cannot back up")); \
903 YYERROR; \
904 } \
905 while (0)
906
907 /* Backward compatibility with an undocumented macro.
908 Use YYerror or YYUNDEF. */
909 #define YYERRCODE YYUNDEF
910
911
912 /* Enable debugging if requested. */
913 #if YYDEBUG
914
915 # ifndef YYFPRINTF
916 # include <stdio.h> /* INFRINGES ON USER NAME SPACE */
917 # define YYFPRINTF fprintf
918 # endif
919
920 # define YYDPRINTF(Args) \
921 do { \
922 if (yydebug) \
923 YYFPRINTF Args; \
924 } while (0)
925
926 /* This macro is provided for backward compatibility. */
927 # ifndef YY_LOCATION_PRINT
928 # define YY_LOCATION_PRINT(File, Loc) ((void) 0)
929 # endif
930
931
932 # define YY_SYMBOL_PRINT(Title, Kind, Value, Location) \
933 do { \
934 if (yydebug) \
935 { \
936 YYFPRINTF (stderr, "%s ", Title); \
937 yy_symbol_print (stderr, \
938 Kind, Value); \
939 YYFPRINTF (stderr, "\n"); \
940 } \
941 } while (0)
942
943
944 /*-----------------------------------.
945 | Print this symbol's value on YYO. |
946 `-----------------------------------*/
947
948 static void
yy_symbol_value_print(FILE * yyo,yysymbol_kind_t yykind,YYSTYPE const * const yyvaluep)949 yy_symbol_value_print (FILE *yyo,
950 yysymbol_kind_t yykind, YYSTYPE const * const yyvaluep)
951 {
952 FILE *yyoutput = yyo;
953 YY_USE (yyoutput);
954 if (!yyvaluep)
955 return;
956 # ifdef YYPRINT
957 if (yykind < YYNTOKENS)
958 YYPRINT (yyo, yytoknum[yykind], *yyvaluep);
959 # endif
960 YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
961 YY_USE (yykind);
962 YY_IGNORE_MAYBE_UNINITIALIZED_END
963 }
964
965
966 /*---------------------------.
967 | Print this symbol on YYO. |
968 `---------------------------*/
969
970 static void
yy_symbol_print(FILE * yyo,yysymbol_kind_t yykind,YYSTYPE const * const yyvaluep)971 yy_symbol_print (FILE *yyo,
972 yysymbol_kind_t yykind, YYSTYPE const * const yyvaluep)
973 {
974 YYFPRINTF (yyo, "%s %s (",
975 yykind < YYNTOKENS ? "token" : "nterm", yysymbol_name (yykind));
976
977 yy_symbol_value_print (yyo, yykind, yyvaluep);
978 YYFPRINTF (yyo, ")");
979 }
980
981 /*------------------------------------------------------------------.
982 | yy_stack_print -- Print the state stack from its BOTTOM up to its |
983 | TOP (included). |
984 `------------------------------------------------------------------*/
985
986 static void
yy_stack_print(yy_state_t * yybottom,yy_state_t * yytop)987 yy_stack_print (yy_state_t *yybottom, yy_state_t *yytop)
988 {
989 YYFPRINTF (stderr, "Stack now");
990 for (; yybottom <= yytop; yybottom++)
991 {
992 int yybot = *yybottom;
993 YYFPRINTF (stderr, " %d", yybot);
994 }
995 YYFPRINTF (stderr, "\n");
996 }
997
998 # define YY_STACK_PRINT(Bottom, Top) \
999 do { \
1000 if (yydebug) \
1001 yy_stack_print ((Bottom), (Top)); \
1002 } while (0)
1003
1004
1005 /*------------------------------------------------.
1006 | Report that the YYRULE is going to be reduced. |
1007 `------------------------------------------------*/
1008
1009 static void
yy_reduce_print(yy_state_t * yyssp,YYSTYPE * yyvsp,int yyrule)1010 yy_reduce_print (yy_state_t *yyssp, YYSTYPE *yyvsp,
1011 int yyrule)
1012 {
1013 int yylno = yyrline[yyrule];
1014 int yynrhs = yyr2[yyrule];
1015 int yyi;
1016 YYFPRINTF (stderr, "Reducing stack by rule %d (line %d):\n",
1017 yyrule - 1, yylno);
1018 /* The symbols being reduced. */
1019 for (yyi = 0; yyi < yynrhs; yyi++)
1020 {
1021 YYFPRINTF (stderr, " $%d = ", yyi + 1);
1022 yy_symbol_print (stderr,
1023 YY_ACCESSING_SYMBOL (+yyssp[yyi + 1 - yynrhs]),
1024 &yyvsp[(yyi + 1) - (yynrhs)]);
1025 YYFPRINTF (stderr, "\n");
1026 }
1027 }
1028
1029 # define YY_REDUCE_PRINT(Rule) \
1030 do { \
1031 if (yydebug) \
1032 yy_reduce_print (yyssp, yyvsp, Rule); \
1033 } while (0)
1034
1035 /* Nonzero means print parse trace. It is left uninitialized so that
1036 multiple parsers can coexist. */
1037 int yydebug;
1038 #else /* !YYDEBUG */
1039 # define YYDPRINTF(Args) ((void) 0)
1040 # define YY_SYMBOL_PRINT(Title, Kind, Value, Location)
1041 # define YY_STACK_PRINT(Bottom, Top)
1042 # define YY_REDUCE_PRINT(Rule)
1043 #endif /* !YYDEBUG */
1044
1045
1046 /* YYINITDEPTH -- initial size of the parser's stacks. */
1047 #ifndef YYINITDEPTH
1048 # define YYINITDEPTH 200
1049 #endif
1050
1051 /* YYMAXDEPTH -- maximum size the stacks can grow to (effective only
1052 if the built-in stack extension method is used).
1053
1054 Do not make this value too large; the results are undefined if
1055 YYSTACK_ALLOC_MAXIMUM < YYSTACK_BYTES (YYMAXDEPTH)
1056 evaluated with infinite-precision integer arithmetic. */
1057
1058 #ifndef YYMAXDEPTH
1059 # define YYMAXDEPTH 10000
1060 #endif
1061
1062
1063
1064
1065
1066
1067 /*-----------------------------------------------.
1068 | Release the memory associated to this symbol. |
1069 `-----------------------------------------------*/
1070
1071 static void
yydestruct(const char * yymsg,yysymbol_kind_t yykind,YYSTYPE * yyvaluep)1072 yydestruct (const char *yymsg,
1073 yysymbol_kind_t yykind, YYSTYPE *yyvaluep)
1074 {
1075 YY_USE (yyvaluep);
1076 if (!yymsg)
1077 yymsg = "Deleting";
1078 YY_SYMBOL_PRINT (yymsg, yykind, yyvaluep, yylocationp);
1079
1080 YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
1081 YY_USE (yykind);
1082 YY_IGNORE_MAYBE_UNINITIALIZED_END
1083 }
1084
1085
1086 /* Lookahead token kind. */
1087 int yychar;
1088
1089 /* The semantic value of the lookahead symbol. */
1090 YYSTYPE yylval;
1091 /* Number of syntax errors so far. */
1092 int yynerrs;
1093
1094
1095
1096
1097 /*----------.
1098 | yyparse. |
1099 `----------*/
1100
1101 int
yyparse(void)1102 yyparse (void)
1103 {
1104 yy_state_fast_t yystate = 0;
1105 /* Number of tokens to shift before error messages enabled. */
1106 int yyerrstatus = 0;
1107
1108 /* Refer to the stacks through separate pointers, to allow yyoverflow
1109 to reallocate them elsewhere. */
1110
1111 /* Their size. */
1112 YYPTRDIFF_T yystacksize = YYINITDEPTH;
1113
1114 /* The state stack: array, bottom, top. */
1115 yy_state_t yyssa[YYINITDEPTH];
1116 yy_state_t *yyss = yyssa;
1117 yy_state_t *yyssp = yyss;
1118
1119 /* The semantic value stack: array, bottom, top. */
1120 YYSTYPE yyvsa[YYINITDEPTH];
1121 YYSTYPE *yyvs = yyvsa;
1122 YYSTYPE *yyvsp = yyvs;
1123
1124 int yyn;
1125 /* The return value of yyparse. */
1126 int yyresult;
1127 /* Lookahead symbol kind. */
1128 yysymbol_kind_t yytoken = YYSYMBOL_YYEMPTY;
1129 /* The variables used to return semantic value and location from the
1130 action routines. */
1131 YYSTYPE yyval;
1132
1133
1134
1135 #define YYPOPSTACK(N) (yyvsp -= (N), yyssp -= (N))
1136
1137 /* The number of symbols on the RHS of the reduced rule.
1138 Keep to zero when no symbol should be popped. */
1139 int yylen = 0;
1140
1141 YYDPRINTF ((stderr, "Starting parse\n"));
1142
1143 yychar = YYEMPTY; /* Cause a token to be read. */
1144 goto yysetstate;
1145
1146
1147 /*------------------------------------------------------------.
1148 | yynewstate -- push a new state, which is found in yystate. |
1149 `------------------------------------------------------------*/
1150 yynewstate:
1151 /* In all cases, when you get here, the value and location stacks
1152 have just been pushed. So pushing a state here evens the stacks. */
1153 yyssp++;
1154
1155
1156 /*--------------------------------------------------------------------.
1157 | yysetstate -- set current state (the top of the stack) to yystate. |
1158 `--------------------------------------------------------------------*/
1159 yysetstate:
1160 YYDPRINTF ((stderr, "Entering state %d\n", yystate));
1161 YY_ASSERT (0 <= yystate && yystate < YYNSTATES);
1162 YY_IGNORE_USELESS_CAST_BEGIN
1163 *yyssp = YY_CAST (yy_state_t, yystate);
1164 YY_IGNORE_USELESS_CAST_END
1165 YY_STACK_PRINT (yyss, yyssp);
1166
1167 if (yyss + yystacksize - 1 <= yyssp)
1168 #if !defined yyoverflow && !defined YYSTACK_RELOCATE
1169 goto yyexhaustedlab;
1170 #else
1171 {
1172 /* Get the current used size of the three stacks, in elements. */
1173 YYPTRDIFF_T yysize = yyssp - yyss + 1;
1174
1175 # if defined yyoverflow
1176 {
1177 /* Give user a chance to reallocate the stack. Use copies of
1178 these so that the &'s don't force the real ones into
1179 memory. */
1180 yy_state_t *yyss1 = yyss;
1181 YYSTYPE *yyvs1 = yyvs;
1182
1183 /* Each stack pointer address is followed by the size of the
1184 data in use in that stack, in bytes. This used to be a
1185 conditional around just the two extra args, but that might
1186 be undefined if yyoverflow is a macro. */
1187 yyoverflow (YY_("memory exhausted"),
1188 &yyss1, yysize * YYSIZEOF (*yyssp),
1189 &yyvs1, yysize * YYSIZEOF (*yyvsp),
1190 &yystacksize);
1191 yyss = yyss1;
1192 yyvs = yyvs1;
1193 }
1194 # else /* defined YYSTACK_RELOCATE */
1195 /* Extend the stack our own way. */
1196 if (YYMAXDEPTH <= yystacksize)
1197 goto yyexhaustedlab;
1198 yystacksize *= 2;
1199 if (YYMAXDEPTH < yystacksize)
1200 yystacksize = YYMAXDEPTH;
1201
1202 {
1203 yy_state_t *yyss1 = yyss;
1204 union yyalloc *yyptr =
1205 YY_CAST (union yyalloc *,
1206 YYSTACK_ALLOC (YY_CAST (YYSIZE_T, YYSTACK_BYTES (yystacksize))));
1207 if (! yyptr)
1208 goto yyexhaustedlab;
1209 YYSTACK_RELOCATE (yyss_alloc, yyss);
1210 YYSTACK_RELOCATE (yyvs_alloc, yyvs);
1211 # undef YYSTACK_RELOCATE
1212 if (yyss1 != yyssa)
1213 YYSTACK_FREE (yyss1);
1214 }
1215 # endif
1216
1217 yyssp = yyss + yysize - 1;
1218 yyvsp = yyvs + yysize - 1;
1219
1220 YY_IGNORE_USELESS_CAST_BEGIN
1221 YYDPRINTF ((stderr, "Stack size increased to %ld\n",
1222 YY_CAST (long, yystacksize)));
1223 YY_IGNORE_USELESS_CAST_END
1224
1225 if (yyss + yystacksize - 1 <= yyssp)
1226 YYABORT;
1227 }
1228 #endif /* !defined yyoverflow && !defined YYSTACK_RELOCATE */
1229
1230 if (yystate == YYFINAL)
1231 YYACCEPT;
1232
1233 goto yybackup;
1234
1235
1236 /*-----------.
1237 | yybackup. |
1238 `-----------*/
1239 yybackup:
1240 /* Do appropriate processing given the current state. Read a
1241 lookahead token if we need one and don't already have one. */
1242
1243 /* First try to decide what to do without reference to lookahead token. */
1244 yyn = yypact[yystate];
1245 if (yypact_value_is_default (yyn))
1246 goto yydefault;
1247
1248 /* Not known => get a lookahead token if don't already have one. */
1249
1250 /* YYCHAR is either empty, or end-of-input, or a valid lookahead. */
1251 if (yychar == YYEMPTY)
1252 {
1253 YYDPRINTF ((stderr, "Reading a token\n"));
1254 yychar = yylex ();
1255 }
1256
1257 if (yychar <= YYEOF)
1258 {
1259 yychar = YYEOF;
1260 yytoken = YYSYMBOL_YYEOF;
1261 YYDPRINTF ((stderr, "Now at end of input.\n"));
1262 }
1263 else if (yychar == YYerror)
1264 {
1265 /* The scanner already issued an error message, process directly
1266 to error recovery. But do not keep the error token as
1267 lookahead, it is too special and may lead us to an endless
1268 loop in error recovery. */
1269 yychar = YYUNDEF;
1270 yytoken = YYSYMBOL_YYerror;
1271 goto yyerrlab1;
1272 }
1273 else
1274 {
1275 yytoken = YYTRANSLATE (yychar);
1276 YY_SYMBOL_PRINT ("Next token is", yytoken, &yylval, &yylloc);
1277 }
1278
1279 /* If the proper action on seeing token YYTOKEN is to reduce or to
1280 detect an error, take that action. */
1281 yyn += yytoken;
1282 if (yyn < 0 || YYLAST < yyn || yycheck[yyn] != yytoken)
1283 goto yydefault;
1284 yyn = yytable[yyn];
1285 if (yyn <= 0)
1286 {
1287 if (yytable_value_is_error (yyn))
1288 goto yyerrlab;
1289 yyn = -yyn;
1290 goto yyreduce;
1291 }
1292
1293 /* Count tokens shifted since error; after three, turn off error
1294 status. */
1295 if (yyerrstatus)
1296 yyerrstatus--;
1297
1298 /* Shift the lookahead token. */
1299 YY_SYMBOL_PRINT ("Shifting", yytoken, &yylval, &yylloc);
1300 yystate = yyn;
1301 YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
1302 *++yyvsp = yylval;
1303 YY_IGNORE_MAYBE_UNINITIALIZED_END
1304
1305 /* Discard the shifted token. */
1306 yychar = YYEMPTY;
1307 goto yynewstate;
1308
1309
1310 /*-----------------------------------------------------------.
1311 | yydefault -- do the default action for the current state. |
1312 `-----------------------------------------------------------*/
1313 yydefault:
1314 yyn = yydefact[yystate];
1315 if (yyn == 0)
1316 goto yyerrlab;
1317 goto yyreduce;
1318
1319
1320 /*-----------------------------.
1321 | yyreduce -- do a reduction. |
1322 `-----------------------------*/
1323 yyreduce:
1324 /* yyn is the number of a rule to reduce with. */
1325 yylen = yyr2[yyn];
1326
1327 /* If YYLEN is nonzero, implement the default value of the action:
1328 '$$ = $1'.
1329
1330 Otherwise, the following line sets YYVAL to garbage.
1331 This behavior is undocumented and Bison
1332 users should not rely upon it. Assigning to YYVAL
1333 unconditionally makes the parser a bit smaller, and it avoids a
1334 GCC warning that YYVAL may be used uninitialized. */
1335 yyval = yyvsp[1-yylen];
1336
1337
1338 YY_REDUCE_PRINT (yyn);
1339 switch (yyn)
1340 {
1341 case 3: /* initial: T_initial T_intval T_intval T_semi */
1342 #line 102 "parser.y"
1343 { actInit(&yyvsp[-2],&yyvsp[-1]); }
1344 #line 1345 "parser.c"
1345 break;
1346
1347 case 4: /* inputs: T_inputs inputSeq T_semi */
1348 #line 106 "parser.y"
1349 { actInputs(); }
1350 #line 1351 "parser.c"
1351 break;
1352
1353 case 5: /* inputSeq: inputSeq T_id */
1354 #line 110 "parser.y"
1355 { actAddInput(&yyvsp[0]); }
1356 #line 1357 "parser.c"
1357 break;
1358
1359 case 6: /* inputSeq: T_id */
1360 #line 111 "parser.y"
1361 { actAddInput(&yyvsp[0]); }
1362 #line 1363 "parser.c"
1363 break;
1364
1365 case 17: /* assign: T_id T_equal expr */
1366 #line 137 "parser.y"
1367 { actAssign(&yyvsp[-2],&yyvsp[0]); }
1368 #line 1369 "parser.c"
1369 break;
1370
1371 case 18: /* expr: expr T_and expr */
1372 #line 141 "parser.y"
1373 { actOpr2(&yyval,&yyvsp[-2],&yyvsp[0],bddop_and); }
1374 #line 1375 "parser.c"
1375 break;
1376
1377 case 19: /* expr: expr T_nand expr */
1378 #line 142 "parser.y"
1379 { actOpr2(&yyval,&yyvsp[-2],&yyvsp[0],bddop_nand); }
1380 #line 1381 "parser.c"
1381 break;
1382
1383 case 20: /* expr: expr T_xor expr */
1384 #line 143 "parser.y"
1385 { actOpr2(&yyval,&yyvsp[-2],&yyvsp[0],bddop_xor); }
1386 #line 1387 "parser.c"
1387 break;
1388
1389 case 21: /* expr: expr T_or expr */
1390 #line 144 "parser.y"
1391 { actOpr2(&yyval,&yyvsp[-2],&yyvsp[0],bddop_or); }
1392 #line 1393 "parser.c"
1393 break;
1394
1395 case 22: /* expr: expr T_nor expr */
1396 #line 145 "parser.y"
1397 { actOpr2(&yyval,&yyvsp[-2],&yyvsp[0],bddop_nor); }
1398 #line 1399 "parser.c"
1399 break;
1400
1401 case 23: /* expr: expr T_imp expr */
1402 #line 146 "parser.y"
1403 { actOpr2(&yyval,&yyvsp[-2],&yyvsp[0],bddop_imp); }
1404 #line 1405 "parser.c"
1405 break;
1406
1407 case 24: /* expr: expr T_biimp expr */
1408 #line 147 "parser.y"
1409 { actOpr2(&yyval,&yyvsp[-2],&yyvsp[0],bddop_biimp); }
1410 #line 1411 "parser.c"
1411 break;
1412
1413 case 25: /* expr: T_not expr */
1414 #line 148 "parser.y"
1415 { actNot(&yyval,&yyvsp[0]); }
1416 #line 1417 "parser.c"
1417 break;
1418
1419 case 26: /* expr: T_lpar expr T_rpar */
1420 #line 149 "parser.y"
1421 { yyval.bval = yyvsp[-1].bval; }
1422 #line 1423 "parser.c"
1423 break;
1424
1425 case 27: /* expr: T_id */
1426 #line 150 "parser.y"
1427 { actId(&yyval,&yyvsp[0]); }
1428 #line 1429 "parser.c"
1429 break;
1430
1431 case 28: /* expr: T_true */
1432 #line 151 "parser.y"
1433 { yyval.bval = new bdd(bddtrue); }
1434 #line 1435 "parser.c"
1435 break;
1436
1437 case 29: /* expr: T_false */
1438 #line 152 "parser.y"
1439 { yyval.bval = new bdd(bddfalse); }
1440 #line 1441 "parser.c"
1441 break;
1442
1443 case 30: /* expr: quantifier */
1444 #line 153 "parser.y"
1445 { yyval.bval = yyvsp[0].bval; }
1446 #line 1447 "parser.c"
1447 break;
1448
1449 case 31: /* quantifier: T_exist varlist T_dot expr */
1450 #line 157 "parser.y"
1451 { actExist(&yyval,&yyvsp[-2],&yyvsp[0]); }
1452 #line 1453 "parser.c"
1453 break;
1454
1455 case 32: /* quantifier: T_forall varlist T_dot expr */
1456 #line 158 "parser.y"
1457 { actForall(&yyval,&yyvsp[-2],&yyvsp[0]); }
1458 #line 1459 "parser.c"
1459 break;
1460
1461 case 33: /* varlist: varlist T_id */
1462 #line 162 "parser.y"
1463 { actQuantVar2(&yyval,&yyvsp[0],&yyvsp[-1]); }
1464 #line 1465 "parser.c"
1465 break;
1466
1467 case 34: /* varlist: T_id */
1468 #line 163 "parser.y"
1469 { actQuantVar1(&yyval,&yyvsp[0]); }
1470 #line 1471 "parser.c"
1471 break;
1472
1473 case 35: /* size: T_size T_id */
1474 #line 168 "parser.y"
1475 { actSize(&yyvsp[0]); }
1476 #line 1477 "parser.c"
1477 break;
1478
1479 case 36: /* dot: T_dumpdot T_str T_id */
1480 #line 172 "parser.y"
1481 { actDot(&yyvsp[-1],&yyvsp[0]); }
1482 #line 1483 "parser.c"
1483 break;
1484
1485 case 37: /* reorder: T_reorder method */
1486 #line 176 "parser.y"
1487 { bdd_reorder(yyvsp[0].ival); }
1488 #line 1489 "parser.c"
1489 break;
1490
1491 case 38: /* reorder: T_autoreorder T_intval method */
1492 #line 177 "parser.y"
1493 { actAutoreorder(&yyvsp[-1],&yyvsp[0]); }
1494 #line 1495 "parser.c"
1495 break;
1496
1497 case 39: /* method: T_win2 */
1498 #line 181 "parser.y"
1499 { yyval.ival = BDD_REORDER_WIN2; }
1500 #line 1501 "parser.c"
1501 break;
1502
1503 case 40: /* method: T_win2ite */
1504 #line 182 "parser.y"
1505 { yyval.ival = BDD_REORDER_WIN2ITE; }
1506 #line 1507 "parser.c"
1507 break;
1508
1509 case 41: /* method: T_sift */
1510 #line 183 "parser.y"
1511 { yyval.ival = BDD_REORDER_SIFT; }
1512 #line 1513 "parser.c"
1513 break;
1514
1515 case 42: /* method: T_siftite */
1516 #line 184 "parser.y"
1517 { yyval.ival = BDD_REORDER_SIFTITE; }
1518 #line 1519 "parser.c"
1519 break;
1520
1521 case 43: /* method: T_none */
1522 #line 185 "parser.y"
1523 { yyval.ival = BDD_REORDER_NONE; }
1524 #line 1525 "parser.c"
1525 break;
1526
1527 case 44: /* cache: T_cache */
1528 #line 189 "parser.y"
1529 { actCache(); }
1530 #line 1531 "parser.c"
1531 break;
1532
1533 case 45: /* tautology: T_tautology T_id */
1534 #line 193 "parser.y"
1535 { actTautology(&yyvsp[0]); }
1536 #line 1537 "parser.c"
1537 break;
1538
1539 case 46: /* print: T_print T_id */
1540 #line 197 "parser.y"
1541 { actPrint(&yyvsp[0]); }
1542 #line 1543 "parser.c"
1543 break;
1544
1545
1546 #line 1547 "parser.c"
1547
1548 default: break;
1549 }
1550 /* User semantic actions sometimes alter yychar, and that requires
1551 that yytoken be updated with the new translation. We take the
1552 approach of translating immediately before every use of yytoken.
1553 One alternative is translating here after every semantic action,
1554 but that translation would be missed if the semantic action invokes
1555 YYABORT, YYACCEPT, or YYERROR immediately after altering yychar or
1556 if it invokes YYBACKUP. In the case of YYABORT or YYACCEPT, an
1557 incorrect destructor might then be invoked immediately. In the
1558 case of YYERROR or YYBACKUP, subsequent parser actions might lead
1559 to an incorrect destructor call or verbose syntax error message
1560 before the lookahead is translated. */
1561 YY_SYMBOL_PRINT ("-> $$ =", YY_CAST (yysymbol_kind_t, yyr1[yyn]), &yyval, &yyloc);
1562
1563 YYPOPSTACK (yylen);
1564 yylen = 0;
1565
1566 *++yyvsp = yyval;
1567
1568 /* Now 'shift' the result of the reduction. Determine what state
1569 that goes to, based on the state we popped back to and the rule
1570 number reduced by. */
1571 {
1572 const int yylhs = yyr1[yyn] - YYNTOKENS;
1573 const int yyi = yypgoto[yylhs] + *yyssp;
1574 yystate = (0 <= yyi && yyi <= YYLAST && yycheck[yyi] == *yyssp
1575 ? yytable[yyi]
1576 : yydefgoto[yylhs]);
1577 }
1578
1579 goto yynewstate;
1580
1581
1582 /*--------------------------------------.
1583 | yyerrlab -- here on detecting error. |
1584 `--------------------------------------*/
1585 yyerrlab:
1586 /* Make sure we have latest lookahead translation. See comments at
1587 user semantic actions for why this is necessary. */
1588 yytoken = yychar == YYEMPTY ? YYSYMBOL_YYEMPTY : YYTRANSLATE (yychar);
1589 /* If not already recovering from an error, report this error. */
1590 if (!yyerrstatus)
1591 {
1592 ++yynerrs;
1593 yyerror (YY_("syntax error"));
1594 }
1595
1596 if (yyerrstatus == 3)
1597 {
1598 /* If just tried and failed to reuse lookahead token after an
1599 error, discard it. */
1600
1601 if (yychar <= YYEOF)
1602 {
1603 /* Return failure if at end of input. */
1604 if (yychar == YYEOF)
1605 YYABORT;
1606 }
1607 else
1608 {
1609 yydestruct ("Error: discarding",
1610 yytoken, &yylval);
1611 yychar = YYEMPTY;
1612 }
1613 }
1614
1615 /* Else will try to reuse lookahead token after shifting the error
1616 token. */
1617 goto yyerrlab1;
1618
1619
1620 /*---------------------------------------------------.
1621 | yyerrorlab -- error raised explicitly by YYERROR. |
1622 `---------------------------------------------------*/
1623 yyerrorlab:
1624 /* Pacify compilers when the user code never invokes YYERROR and the
1625 label yyerrorlab therefore never appears in user code. */
1626 if (0)
1627 YYERROR;
1628
1629 /* Do not reclaim the symbols of the rule whose action triggered
1630 this YYERROR. */
1631 YYPOPSTACK (yylen);
1632 yylen = 0;
1633 YY_STACK_PRINT (yyss, yyssp);
1634 yystate = *yyssp;
1635 goto yyerrlab1;
1636
1637
1638 /*-------------------------------------------------------------.
1639 | yyerrlab1 -- common code for both syntax error and YYERROR. |
1640 `-------------------------------------------------------------*/
1641 yyerrlab1:
1642 yyerrstatus = 3; /* Each real token shifted decrements this. */
1643
1644 /* Pop stack until we find a state that shifts the error token. */
1645 for (;;)
1646 {
1647 yyn = yypact[yystate];
1648 if (!yypact_value_is_default (yyn))
1649 {
1650 yyn += YYSYMBOL_YYerror;
1651 if (0 <= yyn && yyn <= YYLAST && yycheck[yyn] == YYSYMBOL_YYerror)
1652 {
1653 yyn = yytable[yyn];
1654 if (0 < yyn)
1655 break;
1656 }
1657 }
1658
1659 /* Pop the current state because it cannot handle the error token. */
1660 if (yyssp == yyss)
1661 YYABORT;
1662
1663
1664 yydestruct ("Error: popping",
1665 YY_ACCESSING_SYMBOL (yystate), yyvsp);
1666 YYPOPSTACK (1);
1667 yystate = *yyssp;
1668 YY_STACK_PRINT (yyss, yyssp);
1669 }
1670
1671 YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
1672 *++yyvsp = yylval;
1673 YY_IGNORE_MAYBE_UNINITIALIZED_END
1674
1675
1676 /* Shift the error token. */
1677 YY_SYMBOL_PRINT ("Shifting", YY_ACCESSING_SYMBOL (yyn), yyvsp, yylsp);
1678
1679 yystate = yyn;
1680 goto yynewstate;
1681
1682
1683 /*-------------------------------------.
1684 | yyacceptlab -- YYACCEPT comes here. |
1685 `-------------------------------------*/
1686 yyacceptlab:
1687 yyresult = 0;
1688 goto yyreturn;
1689
1690
1691 /*-----------------------------------.
1692 | yyabortlab -- YYABORT comes here. |
1693 `-----------------------------------*/
1694 yyabortlab:
1695 yyresult = 1;
1696 goto yyreturn;
1697
1698
1699 #if !defined yyoverflow
1700 /*-------------------------------------------------.
1701 | yyexhaustedlab -- memory exhaustion comes here. |
1702 `-------------------------------------------------*/
1703 yyexhaustedlab:
1704 yyerror (YY_("memory exhausted"));
1705 yyresult = 2;
1706 goto yyreturn;
1707 #endif
1708
1709
1710 /*-------------------------------------------------------.
1711 | yyreturn -- parsing is finished, clean up and return. |
1712 `-------------------------------------------------------*/
1713 yyreturn:
1714 if (yychar != YYEMPTY)
1715 {
1716 /* Make sure we have latest lookahead translation. See comments at
1717 user semantic actions for why this is necessary. */
1718 yytoken = YYTRANSLATE (yychar);
1719 yydestruct ("Cleanup: discarding lookahead",
1720 yytoken, &yylval);
1721 }
1722 /* Do not reclaim the symbols of the rule whose action triggered
1723 this YYABORT or YYACCEPT. */
1724 YYPOPSTACK (yylen);
1725 YY_STACK_PRINT (yyss, yyssp);
1726 while (yyssp != yyss)
1727 {
1728 yydestruct ("Cleanup: popping",
1729 YY_ACCESSING_SYMBOL (+*yyssp), yyvsp);
1730 YYPOPSTACK (1);
1731 }
1732 #ifndef yyoverflow
1733 if (yyss != yyssa)
1734 YYSTACK_FREE (yyss);
1735 #endif
1736
1737 return yyresult;
1738 }
1739
1740 #line 199 "parser.y"
1741
1742 /*************************************************************************
1743 Main and more
1744 *************************************************************************/
1745
usage(void)1746 void usage(void)
1747 {
1748 cerr << "USAGE: bddcalc [-hg] file\n";
1749 cerr << " -h : print this message\n";
1750 cerr << " -g : disable garbage collection info\n";
1751 }
1752
1753
main(int ac,char ** av)1754 int main(int ac, char **av)
1755 {
1756 int c;
1757
1758 while ((c=getopt(ac, av, "hg")) != EOF)
1759 {
1760 switch (c)
1761 {
1762 case 'h':
1763 usage();
1764 break;
1765 case 'g':
1766 gbcHandler = bdd_default_gbchandler;
1767 break;
1768 }
1769 }
1770
1771 if (optind >= ac)
1772 usage();
1773
1774 yyin = fopen(av[optind],"r");
1775 if (!yyin)
1776 {
1777 cerr << "Could not open file: " << av[optind] << endl;
1778 exit(2);
1779 }
1780
1781 linenum = 1;
1782 bdd_setcacheratio(2);
1783 yyparse();
1784
1785 bdd_printstat();
1786 bdd_done();
1787
1788 return 0;
1789 }
1790
1791
yyerror(const char * fmt,...)1792 void yyerror(const char *fmt, ...)
1793 {
1794 va_list argp;
1795 va_start(argp,fmt);
1796 fprintf(stderr, "Parse error in (or before) line %d: ", linenum);
1797 vfprintf(stderr, fmt, argp);
1798 va_end(argp);
1799 exit(3);
1800 }
1801
1802
1803 /*************************************************************************
1804 Semantic actions
1805 *************************************************************************/
1806
actInit(token * nodes,token * cache)1807 void actInit(token *nodes, token *cache)
1808 {
1809 bdd_init(nodes->ival, cache->ival);
1810 bdd_gbc_hook(gbcHandler);
1811 bdd_reorder_verbose(0);
1812 }
1813
1814
actInputs(void)1815 void actInputs(void)
1816 {
1817 bdd_setvarnum(inputs.size());
1818
1819 int vnum=0;
1820 for (nodeLst::ite i=inputs.first() ; i.more() ; i++, vnum++)
1821 {
1822 if (names.exists((*i).name))
1823 yyerror("Redefinition of input %s", (*i).name);
1824
1825 (*i).val = bdd_ithvar(vnum);
1826 hashData hd((*i).name, 0, &(*i));
1827 names.add(hd);
1828 }
1829
1830 bdd_varblockall();
1831 }
1832
1833
actAddInput(token * id)1834 void actAddInput(token *id)
1835 {
1836 inputs.append( nodeData(inputTag,sdup(id->id),bddtrue) );
1837 }
1838
1839
actAssign(token * id,token * expr)1840 void actAssign(token *id, token *expr)
1841 {
1842 if (names.exists(id->id))
1843 yyerror("Redefinition of %s", id->id);
1844
1845 nodeData *d = new nodeData(exprTag, sdup(id->id), *expr->bval);
1846 hashData hd(d->name, 0, d);
1847 names.add(hd);
1848 delete expr->bval;
1849 }
1850
1851
actOpr2(token * res,token * left,token * right,int opr)1852 void actOpr2(token *res, token *left, token *right, int opr)
1853 {
1854 res->bval = new bdd( bdd_apply(*left->bval, *right->bval, opr) );
1855 delete left->bval;
1856 delete right->bval;
1857 }
1858
1859
actNot(token * res,token * right)1860 void actNot(token *res, token *right)
1861 {
1862 res->bval = new bdd( bdd_not(*right->bval) );
1863 delete right->bval;
1864 //printf("%5d -> %f\n", fixme, bdd_satcount(*res->bval));
1865 }
1866
1867
actId(token * res,token * id)1868 void actId(token *res, token *id)
1869 {
1870 hashData hd;
1871
1872 if (names.lookup(id->id,hd) == 0)
1873 {
1874 res->bval = new bdd( ((nodeData*)hd.def)->val );
1875 }
1876 else
1877 yyerror("Unknown variable %s", id->id);
1878 }
1879
1880
actExist(token * res,token * var,token * expr)1881 void actExist(token *res, token *var, token *expr)
1882 {
1883 res->bval = new bdd( bdd_exist(*expr->bval, *var->bval) );
1884 delete var->bval;
1885 delete expr->bval;
1886 }
1887
1888
actForall(token * res,token * var,token * expr)1889 void actForall(token *res, token *var, token *expr)
1890 {
1891 res->bval = new bdd( bdd_forall(*expr->bval, *var->bval) );
1892 delete var->bval;
1893 delete expr->bval;
1894 }
1895
1896
actQuantVar2(token * res,token * id,token * list)1897 void actQuantVar2(token *res, token *id, token *list)
1898 {
1899 hashData hd;
1900
1901 if (names.lookup(id->id,hd) == 0)
1902 {
1903 if (hd.type == inputTag)
1904 {
1905 res->bval = list->bval;
1906 *res->bval &= ((nodeData*)hd.def)->val;
1907 }
1908 else
1909 yyerror("%s is not a variable", id->id);
1910 }
1911 else
1912 yyerror("Unknown variable %s", id->id);
1913 }
1914
1915
actQuantVar1(token * res,token * id)1916 void actQuantVar1(token *res, token *id)
1917 {
1918 hashData hd;
1919
1920 if (names.lookup(id->id,hd) == 0)
1921 {
1922 if (hd.type == inputTag)
1923 res->bval = new bdd( ((nodeData*)hd.def)->val );
1924 else
1925 yyerror("%s is not a variable", id->id);
1926 }
1927 else
1928 yyerror("Unknown variable %s", id->id);
1929 }
1930
1931
actSize(token * id)1932 void actSize(token *id)
1933 {
1934 hashData hd;
1935
1936 if (names.lookup(id->id,hd) == 0)
1937 {
1938 cout << "Number of nodes used for " << id->id << " = "
1939 << bdd_nodecount(((nodeData*)hd.def)->val) << endl;
1940 }
1941 else
1942 yyerror("Unknown variable %s", id->id);
1943 }
1944
1945
actDot(token * fname,token * id)1946 void actDot(token *fname, token *id)
1947 {
1948 hashData hd;
1949
1950 if (names.lookup(id->id,hd) == 0)
1951 {
1952 if (bdd_fnprintdot(fname->str, ((nodeData*)hd.def)->val) < 0)
1953 cout << "Could not open file: " << fname->str << endl;
1954 }
1955 else
1956 yyerror("Unknown variable %s", id->id);
1957 }
1958
1959
actAutoreorder(token * times,token * method)1960 void actAutoreorder(token *times, token *method)
1961 {
1962 if (times->ival == 0)
1963 bdd_autoreorder(method->ival);
1964 else
1965 bdd_autoreorder_times(method->ival, times->ival);
1966 }
1967
1968
actCache(void)1969 void actCache(void)
1970 {
1971 bdd_printstat();
1972 }
1973
1974
actTautology(token * id)1975 void actTautology(token *id)
1976 {
1977 hashData hd;
1978
1979 if (names.lookup(id->id,hd) == 0)
1980 {
1981 if (((nodeData*)hd.def)->val == bddtrue)
1982 cout << "Formula " << id->id << " is a tautology!\n";
1983 else
1984 cout << "Formula " << id->id << " is NOT a tautology!\n";
1985 }
1986 else
1987 yyerror("Unknown variable %s", id->id);
1988 }
1989
1990
actPrint(token * id)1991 void actPrint(token *id)
1992 {
1993 hashData hd;
1994
1995 if (names.lookup(id->id,hd) == 0)
1996 cout << id->id << " = " << bddset << ((nodeData*)hd.def)->val << endl;
1997 else
1998 yyerror("Unknown variable %s", id->id);
1999 }
2000
2001 /* EOF */
2002