From 6c196ec8a41d6ed506c133c8b33dba9684f9a7a6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 12:34:43 +0000 Subject: Updated raytracer test. Added SPASS test. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- test/spass/dfgparser.c | 3728 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 3728 insertions(+) create mode 100644 test/spass/dfgparser.c (limited to 'test/spass/dfgparser.c') diff --git a/test/spass/dfgparser.c b/test/spass/dfgparser.c new file mode 100644 index 00000000..3691271b --- /dev/null +++ b/test/spass/dfgparser.c @@ -0,0 +1,3728 @@ +/* A Bison parser, made from dfgparser.y, by GNU bison 1.75. */ + +/* Skeleton parser for Yacc-like parsing with Bison, + Copyright (C) 1984, 1989, 1990, 2000, 2001, 2002 Free Software Foundation, Inc. + + This program is free software; you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation; either version 2, or (at your option) + any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program; if not, write to the Free Software + Foundation, Inc., 59 Temple Place - Suite 330, + Boston, MA 02111-1307, USA. */ + +/* As a special exception, when this file is copied by Bison into a + Bison output file, you may use that output file without restriction. + This special exception was added by the Free Software Foundation + in version 1.24 of Bison. */ + +/* Written by Richard Stallman by simplifying the original so called + ``semantic'' parser. */ + +/* All symbols defined below should begin with yy or YY, to avoid + infringing on user name space. This should be done even for local + variables, as they might otherwise be expanded by user macros. + There are some unavoidable exceptions within include files to + define necessary library symbols; they are noted "INFRINGES ON + USER NAME SPACE" below. */ + +/* Identify Bison output. */ +#define YYBISON 1 + +/* Pure parsers. */ +#define YYPURE 0 + +/* Using locations. */ +#define YYLSP_NEEDED 0 + +/* If NAME_PREFIX is specified substitute the variables and functions + names. */ +#define yyparse dfg_parse +#define yylex dfg_lex +#define yyerror dfg_error +#define yylval dfg_lval +#define yychar dfg_char +#define yydebug dfg_debug +#define yynerrs dfg_nerrs + + +/* Tokens. */ +#ifndef YYTOKENTYPE +# define YYTOKENTYPE + /* Put the tokens into the symbol table, so that GDB and other debuggers + know about them. */ + enum yytokentype { + DFG_AND = 258, + DFG_AUTHOR = 259, + DFG_AXIOMS = 260, + DFG_BEGPROB = 261, + DFG_BY = 262, + DFG_CLAUSE = 263, + DFG_CLOSEBRACE = 264, + DFG_CLSLIST = 265, + DFG_CNF = 266, + DFG_CONJECS = 267, + DFG_DATE = 268, + DFG_DECLLIST = 269, + DFG_DESC = 270, + DFG_DESCLIST = 271, + DFG_DNF = 272, + DFG_DOMPRED = 273, + DFG_ENDLIST = 274, + DFG_ENDPROB = 275, + DFG_EQUAL = 276, + DFG_EQUIV = 277, + DFG_EXISTS = 278, + DFG_FALSE = 279, + DFG_FORMLIST = 280, + DFG_FORMULA = 281, + DFG_FORALL = 282, + DFG_FREELY = 283, + DFG_FUNC = 284, + DFG_GENERATED = 285, + DFG_GENSET = 286, + DFG_HYPOTH = 287, + DFG_IMPLIED = 288, + DFG_IMPLIES = 289, + DFG_LOGIC = 290, + DFG_NAME = 291, + DFG_NOT = 292, + DFG_OPENBRACE = 293, + DFG_OPERAT = 294, + DFG_OR = 295, + DFG_PREC = 296, + DFG_PRED = 297, + DFG_PRDICAT = 298, + DFG_PRFLIST = 299, + DFG_QUANTIF = 300, + DFG_SATIS = 301, + DFG_SETFLAG = 302, + DFG_SETTINGS = 303, + DFG_SYMLIST = 304, + DFG_SORT = 305, + DFG_SORTS = 306, + DFG_STATUS = 307, + DFG_STEP = 308, + DFG_SUBSORT = 309, + DFG_TERMLIST = 310, + DFG_TRUE = 311, + DFG_UNKNOWN = 312, + DFG_UNSATIS = 313, + DFG_VERSION = 314, + DFG_NUM = 315, + DFG_MINUS1 = 316, + DFG_ID = 317, + DFG_TEXT = 318 + }; +#endif +#define DFG_AND 258 +#define DFG_AUTHOR 259 +#define DFG_AXIOMS 260 +#define DFG_BEGPROB 261 +#define DFG_BY 262 +#define DFG_CLAUSE 263 +#define DFG_CLOSEBRACE 264 +#define DFG_CLSLIST 265 +#define DFG_CNF 266 +#define DFG_CONJECS 267 +#define DFG_DATE 268 +#define DFG_DECLLIST 269 +#define DFG_DESC 270 +#define DFG_DESCLIST 271 +#define DFG_DNF 272 +#define DFG_DOMPRED 273 +#define DFG_ENDLIST 274 +#define DFG_ENDPROB 275 +#define DFG_EQUAL 276 +#define DFG_EQUIV 277 +#define DFG_EXISTS 278 +#define DFG_FALSE 279 +#define DFG_FORMLIST 280 +#define DFG_FORMULA 281 +#define DFG_FORALL 282 +#define DFG_FREELY 283 +#define DFG_FUNC 284 +#define DFG_GENERATED 285 +#define DFG_GENSET 286 +#define DFG_HYPOTH 287 +#define DFG_IMPLIED 288 +#define DFG_IMPLIES 289 +#define DFG_LOGIC 290 +#define DFG_NAME 291 +#define DFG_NOT 292 +#define DFG_OPENBRACE 293 +#define DFG_OPERAT 294 +#define DFG_OR 295 +#define DFG_PREC 296 +#define DFG_PRED 297 +#define DFG_PRDICAT 298 +#define DFG_PRFLIST 299 +#define DFG_QUANTIF 300 +#define DFG_SATIS 301 +#define DFG_SETFLAG 302 +#define DFG_SETTINGS 303 +#define DFG_SYMLIST 304 +#define DFG_SORT 305 +#define DFG_SORTS 306 +#define DFG_STATUS 307 +#define DFG_STEP 308 +#define DFG_SUBSORT 309 +#define DFG_TERMLIST 310 +#define DFG_TRUE 311 +#define DFG_UNKNOWN 312 +#define DFG_UNSATIS 313 +#define DFG_VERSION 314 +#define DFG_NUM 315 +#define DFG_MINUS1 316 +#define DFG_ID 317 +#define DFG_TEXT 318 + + + + +/* Copy the first part of user declarations. */ +#line 48 "dfgparser.y" + + +#include +#include "dfg.h" +#include "symbol.h" +#include "term.h" +#include "foldfg.h" +#include "stringsx.h" + +/* Used for the texts from description section. */ +typedef struct { + char* name; + char* author; + char* version; + char* logic; + DFG_STATE status; + char* description; + char* date; +} DFG_DESCRIPTIONTYPE; + +static DFG_DESCRIPTIONTYPE dfg_DESC; +static LIST dfg_AXIOMLIST; +static LIST dfg_CONJECLIST; +static LIST dfg_SORTDECLLIST; +/* symbol precedence explicitly defined by user */ +static LIST dfg_USERPRECEDENCE; +static LIST dfg_AXCLAUSES; +static LIST dfg_CONCLAUSES; +static LIST dfg_PROOFLIST; /* list_of_proofs */ +static LIST dfg_TERMLIST; /* list_of_terms */ +static BOOL dfg_IGNORE; /* tokens are ignored while TRUE */ +static FLAGSTORE dfg_FLAGS; +static PRECEDENCE dfg_PRECEDENCE; + +/* used also in the scanner */ +NAT dfg_LINENUMBER; +BOOL dfg_IGNORETEXT; + +void yyerror(const char*); +int yylex(void); /* Defined in dfgscanner.l */ + +static void dfg_SymbolDecl(int, char*, int); +static SYMBOL dfg_Symbol(char*, NAT); +static void dfg_SubSort(char*, char*); +static void dfg_SymbolGenerated(SYMBOL, BOOL, LIST); + +static __inline__ TERM dfg_TermCreate(char* Name, LIST Arguments) +/* Look up the symbol, check its arity and create the term */ +{ + SYMBOL s; + NAT arity; + arity = list_Length(Arguments); + s = dfg_Symbol(Name, arity); /* Frees the string */ + if (!symbol_IsVariable(s) && !symbol_IsFunction(s)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Line %d: is not a function.\n", dfg_LINENUMBER); + misc_FinishUserErrorReport(); + } + return term_Create(s, Arguments); +} + +static __inline__ TERM dfg_AtomCreate(char* Name, LIST Arguments) +/* Look up the symbol, check its arity and create the atom term */ +{ + SYMBOL s; + s = dfg_Symbol(Name, list_Length(Arguments)); /* Frees the string */ + if (symbol_IsVariable(s) || !symbol_IsPredicate(s)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Line %d: Symbol is not a predicate.\n", dfg_LINENUMBER); + misc_FinishUserErrorReport(); + } + return term_Create(s, Arguments); +} + +static __inline__ void dfg_DeleteStringList(LIST List) +{ + list_DeleteWithElement(List, (void (*)(POINTER)) string_StringFree); +} + +/**************************************************************/ +/* Functions that handle symbols with unspecified arity */ +/**************************************************************/ + +/* The symbol list holds all symbols whose arity wasn't */ +/* specified in the symbol declaration section. */ +/* If the arity of a symbol was not specified in this section */ +/* it is first set to 0. If the symbol occurs with always the */ +/* same arity 'A' the arity of this symbol is set to 'A'. */ +static LIST dfg_SYMBOLLIST; + +static void dfg_SymAdd(SYMBOL); +static void dfg_SymCheck(SYMBOL, NAT); +static void dfg_SymCleanUp(void); + +/**************************************************************/ +/* Functions that handle variable names */ +/**************************************************************/ + +/* List of quantified variables in the current input formula. */ +/* This list is used to find symbols that by mistake weren't */ +/* declared in the symbol declaration section */ +/* --> free variables */ +/* This is a list of lists, since each time a quantifier is */ +/* reached, a new list is added to the global list. */ +static LIST dfg_VARLIST; +static BOOL dfg_VARDECL; + +static void dfg_VarStart(void); +static void dfg_VarStop(void); +static void dfg_VarBacktrack(void); +static void dfg_VarCheck(void); +static SYMBOL dfg_VarLookup(char*); + +#define YYERROR_VERBOSE + + + +/* Enabling traces. */ +#ifndef YYDEBUG +# define YYDEBUG 0 +#endif + +/* Enabling verbose error messages. */ +#ifdef YYERROR_VERBOSE +# undef YYERROR_VERBOSE +# define YYERROR_VERBOSE 1 +#else +# define YYERROR_VERBOSE 0 +#endif + +#ifndef YYSTYPE +#line 165 "dfgparser.y" +typedef union { + int number; + char* string; + SYMBOL symbol; + SPROPERTY property; + TERM term; + LIST list; + DFG_STATE state; + BOOL bool; +} yystype; +/* Line 193 of /opt/gnu//share/bison/yacc.c. */ +#line 336 "dfgparser.c" +# define YYSTYPE yystype +# define YYSTYPE_IS_TRIVIAL 1 +#endif + +#ifndef YYLTYPE +typedef struct yyltype +{ + int first_line; + int first_column; + int last_line; + int last_column; +} yyltype; +# define YYLTYPE yyltype +# define YYLTYPE_IS_TRIVIAL 1 +#endif + +/* Copy the second part of user declarations. */ + + +/* Line 213 of /opt/gnu//share/bison/yacc.c. */ +#line 357 "dfgparser.c" + +#if ! defined (yyoverflow) || YYERROR_VERBOSE + +/* The parser invokes alloca or malloc; define the necessary symbols. */ + +# if YYSTACK_USE_ALLOCA +# define YYSTACK_ALLOC alloca +# else +# ifndef YYSTACK_USE_ALLOCA +# if defined (alloca) || defined (_ALLOCA_H) +# define YYSTACK_ALLOC alloca +# else +# ifdef __GNUC__ +# define YYSTACK_ALLOC __builtin_alloca +# endif +# endif +# endif +# endif + +# ifdef YYSTACK_ALLOC + /* Pacify GCC's `empty if-body' warning. */ +# define YYSTACK_FREE(Ptr) do { /* empty */; } while (0) +# else +# if defined (__STDC__) || defined (__cplusplus) +# include /* INFRINGES ON USER NAME SPACE */ +# define YYSIZE_T size_t +# endif +# define YYSTACK_ALLOC malloc +# define YYSTACK_FREE free +# endif +#endif /* ! defined (yyoverflow) || YYERROR_VERBOSE */ + + +#if (! defined (yyoverflow) \ + && (! defined (__cplusplus) \ + || (YYLTYPE_IS_TRIVIAL && YYSTYPE_IS_TRIVIAL))) + +/* A type that is properly aligned for any stack member. */ +union yyalloc +{ + short yyss; + YYSTYPE yyvs; + }; + +/* The size of the maximum gap between one aligned stack and the next. */ +# define YYSTACK_GAP_MAX (sizeof (union yyalloc) - 1) + +/* The size of an array large to enough to hold all stacks, each with + N elements. */ +# define YYSTACK_BYTES(N) \ + ((N) * (sizeof (short) + sizeof (YYSTYPE)) \ + + YYSTACK_GAP_MAX) + +/* Copy COUNT objects from FROM to TO. The source and destination do + not overlap. */ +# ifndef YYCOPY +# if 1 < __GNUC__ +# define YYCOPY(To, From, Count) \ + __builtin_memcpy (To, From, (Count) * sizeof (*(From))) +# else +# define YYCOPY(To, From, Count) \ + do \ + { \ + register YYSIZE_T yyi; \ + for (yyi = 0; yyi < (Count); yyi++) \ + (To)[yyi] = (From)[yyi]; \ + } \ + while (0) +# endif +# endif + +/* Relocate STACK from its old location to the new one. The + local variables YYSIZE and YYSTACKSIZE give the old and new number of + elements in the stack, and YYPTR gives the new location of the + stack. Advance YYPTR to a properly aligned location for the next + stack. */ +# define YYSTACK_RELOCATE(Stack) \ + do \ + { \ + YYSIZE_T yynewbytes; \ + YYCOPY (&yyptr->Stack, Stack, yysize); \ + Stack = &yyptr->Stack; \ + yynewbytes = yystacksize * sizeof (*Stack) + YYSTACK_GAP_MAX; \ + yyptr += yynewbytes / sizeof (*yyptr); \ + } \ + while (0) + +#endif + +#if defined (__STDC__) || defined (__cplusplus) + typedef signed char yysigned_char; +#else + typedef short yysigned_char; +#endif + +/* YYFINAL -- State number of the termination state. */ +#define YYFINAL 4 +#define YYLAST 506 + +/* YYNTOKENS -- Number of terminals. */ +#define YYNTOKENS 71 +/* YYNNTS -- Number of nonterminals. */ +#define YYNNTS 100 +/* YYNRULES -- Number of rules. */ +#define YYNRULES 196 +/* YYNRULES -- Number of states. */ +#define YYNSTATES 477 + +/* YYTRANSLATE(YYLEX) -- Bison symbol number corresponding to YYLEX. */ +#define YYUNDEFTOK 2 +#define YYMAXUTOK 318 + +#define YYTRANSLATE(X) \ + ((unsigned)(X) <= YYMAXUTOK ? yytranslate[X] : YYUNDEFTOK) + +/* YYTRANSLATE[YYLEX] -- Bison symbol number corresponding to YYLEX. */ +static const unsigned char yytranslate[] = +{ + 0, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 64, 65, 2, 2, 69, 2, 66, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 70, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 67, 2, 68, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 1, 2, 3, 4, + 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, + 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, + 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, + 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, + 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, + 55, 56, 57, 58, 59, 60, 61, 62, 63 +}; + +#if YYDEBUG +/* YYPRHS[YYN] -- Index of the first RHS symbol of rule number YYN in + YYRHS. */ +static const unsigned short yyprhs[] = +{ + 0, 0, 3, 14, 26, 32, 38, 44, 50, 51, + 57, 58, 64, 65, 71, 73, 75, 77, 84, 85, + 95, 96, 102, 104, 108, 110, 116, 117, 123, 125, + 129, 131, 137, 138, 144, 146, 150, 151, 157, 159, + 163, 165, 171, 172, 178, 180, 184, 186, 192, 194, + 196, 197, 203, 204, 207, 209, 217, 220, 228, 229, + 230, 242, 252, 253, 255, 257, 261, 263, 267, 276, + 278, 280, 281, 284, 285, 293, 294, 297, 299, 304, + 311, 316, 317, 318, 329, 330, 332, 334, 338, 340, + 342, 344, 346, 348, 350, 352, 354, 356, 358, 360, + 362, 364, 368, 370, 375, 376, 379, 390, 391, 403, + 404, 412, 413, 415, 417, 418, 419, 430, 435, 437, + 441, 443, 448, 450, 454, 456, 458, 460, 467, 472, + 473, 481, 482, 484, 486, 495, 500, 502, 507, 509, + 513, 514, 517, 518, 528, 529, 545, 547, 551, 552, + 557, 561, 567, 568, 572, 574, 576, 578, 580, 582, + 584, 586, 588, 590, 591, 595, 603, 605, 607, 608, + 611, 612, 619, 620, 624, 625, 628, 634, 635, 645, + 647, 651, 652, 656, 661, 666, 673, 675, 679, 681, + 688, 689, 692, 694, 697, 703, 705 +}; + +/* YYRHS -- A `-1'-separated list of the rules' RHS. */ +static const short yyrhs[] = +{ + 72, 0, -1, 6, 64, 121, 65, 66, 73, 82, + 159, 20, 66, -1, 16, 66, 74, 75, 78, 79, + 76, 77, 80, 19, 66, -1, 36, 64, 63, 65, + 66, -1, 4, 64, 63, 65, 66, -1, 52, 64, + 81, 65, 66, -1, 15, 64, 63, 65, 66, -1, + -1, 59, 64, 63, 65, 66, -1, -1, 35, 64, + 63, 65, 66, -1, -1, 13, 64, 63, 65, 66, + -1, 46, -1, 58, -1, 57, -1, 83, 99, 110, + 124, 143, 155, -1, -1, 49, 66, 84, 87, 90, + 92, 95, 19, 66, -1, -1, 29, 67, 85, 68, + 66, -1, 86, -1, 85, 69, 86, -1, 121, -1, + 64, 121, 69, 98, 65, -1, -1, 43, 67, 88, + 68, 66, -1, 89, -1, 88, 69, 89, -1, 121, + -1, 64, 121, 69, 98, 65, -1, -1, 51, 67, + 91, 68, 66, -1, 121, -1, 91, 69, 121, -1, + -1, 39, 67, 93, 68, 66, -1, 94, -1, 93, + 69, 94, -1, 121, -1, 64, 121, 69, 98, 65, + -1, -1, 45, 67, 96, 68, 66, -1, 97, -1, + 96, 69, 97, -1, 121, -1, 64, 121, 69, 98, + 65, -1, 61, -1, 60, -1, -1, 14, 66, 100, + 19, 66, -1, -1, 100, 101, -1, 104, -1, 54, + 64, 121, 69, 121, 65, 66, -1, 136, 66, -1, + 42, 64, 121, 69, 107, 65, 66, -1, -1, -1, + 27, 64, 67, 102, 122, 103, 68, 69, 136, 65, + 66, -1, 50, 121, 105, 30, 7, 67, 106, 68, + 66, -1, -1, 28, -1, 121, -1, 106, 69, 121, + -1, 121, -1, 107, 69, 121, -1, 25, 64, 109, + 65, 66, 111, 19, 66, -1, 5, -1, 12, -1, + -1, 110, 108, -1, -1, 111, 26, 64, 116, 112, + 65, 66, -1, -1, 69, 121, -1, 136, -1, 37, + 64, 113, 65, -1, 118, 64, 113, 69, 113, 65, + -1, 119, 64, 117, 65, -1, -1, -1, 120, 64, + 67, 114, 122, 115, 68, 69, 113, 65, -1, -1, + 113, -1, 113, -1, 117, 69, 113, -1, 22, -1, + 33, -1, 34, -1, 3, -1, 40, -1, 23, -1, + 27, -1, 62, -1, 60, -1, 47, -1, 18, -1, + 41, -1, 123, -1, 122, 69, 123, -1, 121, -1, + 121, 64, 121, 65, -1, -1, 124, 125, -1, 10, + 64, 109, 69, 11, 65, 66, 127, 19, 66, -1, + -1, 10, 64, 109, 69, 17, 65, 66, 126, 137, + 19, 66, -1, -1, 127, 8, 64, 128, 112, 65, + 66, -1, -1, 129, -1, 132, -1, -1, -1, 27, + 64, 67, 130, 122, 131, 68, 69, 132, 65, -1, + 40, 64, 133, 65, -1, 134, -1, 133, 69, 134, + -1, 136, -1, 37, 64, 136, 65, -1, 136, -1, + 135, 69, 136, -1, 121, -1, 56, -1, 24, -1, + 21, 64, 141, 69, 141, 65, -1, 121, 64, 142, + 65, -1, -1, 137, 8, 64, 138, 112, 65, 66, + -1, -1, 139, -1, 140, -1, 23, 64, 67, 135, + 68, 69, 140, 65, -1, 3, 64, 133, 65, -1, + 121, -1, 121, 64, 142, 65, -1, 141, -1, 142, + 69, 141, -1, -1, 143, 144, -1, -1, 44, 64, + 121, 65, 66, 145, 146, 19, 66, -1, -1, 146, + 53, 64, 150, 69, 154, 69, 121, 69, 67, 147, + 68, 148, 65, 66, -1, 150, -1, 147, 69, 150, + -1, -1, 69, 67, 149, 68, -1, 150, 70, 150, + -1, 149, 69, 150, 70, 150, -1, -1, 152, 151, + 153, -1, 121, -1, 37, -1, 22, -1, 33, -1, + 34, -1, 3, -1, 40, -1, 27, -1, 23, -1, + -1, 64, 117, 65, -1, 64, 67, 122, 68, 69, + 113, 65, -1, 129, -1, 139, -1, -1, 155, 156, + -1, -1, 55, 66, 157, 158, 19, 66, -1, -1, + 158, 141, 66, -1, -1, 159, 160, -1, 31, 66, + 168, 19, 66, -1, -1, 48, 64, 121, 161, 65, + 66, 162, 19, 66, -1, 63, -1, 38, 163, 9, + -1, -1, 163, 164, 66, -1, 41, 64, 165, 65, + -1, 18, 64, 170, 65, -1, 47, 64, 62, 69, + 98, 65, -1, 166, -1, 165, 69, 166, -1, 121, + -1, 64, 121, 69, 60, 167, 65, -1, -1, 69, + 62, -1, 169, -1, 168, 169, -1, 32, 67, 170, + 68, 66, -1, 121, -1, 170, 69, 121, -1 +}; + +/* YYRLINE[YYN] -- source line where rule number YYN was defined. */ +static const unsigned short yyrline[] = +{ + 0, 206, 206, 218, 229, 233, 237, 241, 245, 246, + 250, 251, 255, 256, 260, 261, 262, 269, 281, 282, + 291, 292, 295, 296, 299, 300, 304, 305, 308, 309, + 312, 313, 316, 317, 320, 321, 324, 325, 328, 329, + 332, 333, 336, 337, 340, 341, 344, 345, 348, 349, + 356, 357, 362, 363, 366, 367, 369, 370, 372, 373, + 372, 382, 386, 387, 390, 391, 394, 395, 402, 412, + 413, 416, 417, 420, 421, 435, 436, 439, 440, 442, + 444, 446, 447, 446, 454, 455, 458, 460, 464, 465, + 466, 469, 470, 473, 474, 477, 483, 485, 487, 489, + 493, 495, 499, 510, 534, 535, 538, 548, 547, 554, + 555, 569, 570, 573, 574, 575, 574, 582, 586, 588, + 592, 593, 597, 598, 601, 603, 605, 607, 609, 616, + 617, 620, 621, 624, 625, 628, 635, 637, 641, 643, + 651, 652, 656, 655, 669, 670, 691, 693, 698, 699, + 702, 710, 721, 720, 732, 733, 734, 735, 736, 737, + 738, 739, 740, 743, 744, 745, 748, 749, 757, 758, + 761, 761, 768, 769, 776, 777, 780, 781, 781, 789, + 792, 795, 796, 799, 800, 820, 832, 833, 836, 848, + 865, 866, 883, 884, 887, 891, 892 +}; +#endif + +#if YYDEBUG || YYERROR_VERBOSE +/* YYTNME[SYMBOL-NUM] -- String name of the symbol SYMBOL-NUM. + First, the terminals, then, starting at YYNTOKENS, nonterminals. */ +static const char *const yytname[] = +{ + "$end", "error", "$undefined", "DFG_AND", "DFG_AUTHOR", "DFG_AXIOMS", + "DFG_BEGPROB", "DFG_BY", "DFG_CLAUSE", "DFG_CLOSEBRACE", "DFG_CLSLIST", + "DFG_CNF", "DFG_CONJECS", "DFG_DATE", "DFG_DECLLIST", "DFG_DESC", + "DFG_DESCLIST", "DFG_DNF", "DFG_DOMPRED", "DFG_ENDLIST", "DFG_ENDPROB", + "DFG_EQUAL", "DFG_EQUIV", "DFG_EXISTS", "DFG_FALSE", "DFG_FORMLIST", + "DFG_FORMULA", "DFG_FORALL", "DFG_FREELY", "DFG_FUNC", "DFG_GENERATED", + "DFG_GENSET", "DFG_HYPOTH", "DFG_IMPLIED", "DFG_IMPLIES", "DFG_LOGIC", + "DFG_NAME", "DFG_NOT", "DFG_OPENBRACE", "DFG_OPERAT", "DFG_OR", + "DFG_PREC", "DFG_PRED", "DFG_PRDICAT", "DFG_PRFLIST", "DFG_QUANTIF", + "DFG_SATIS", "DFG_SETFLAG", "DFG_SETTINGS", "DFG_SYMLIST", "DFG_SORT", + "DFG_SORTS", "DFG_STATUS", "DFG_STEP", "DFG_SUBSORT", "DFG_TERMLIST", + "DFG_TRUE", "DFG_UNKNOWN", "DFG_UNSATIS", "DFG_VERSION", "DFG_NUM", + "DFG_MINUS1", "DFG_ID", "DFG_TEXT", "'('", "')'", "'.'", "'['", "']'", + "','", "':'", "$accept", "problem", "description", "name", "author", + "status", "desctext", "versionopt", "logicopt", "dateopt", "log_state", + "logicalpart", "symbollistopt", "functionsopt", "functionlist", "func", + "predicatesopt", "predicatelist", "pred", "sortsopt", "sortlist", + "operatorsopt", "operatorlist", "op", "quantifiersopt", + "quantifierlist", "quant", "number", "declarationlistopt", + "decllistopt", "decl", "@1", "@2", "gendecl", "freelyopt", "funclist", + "sortdecl", "formulalist", "origin", "formulalistsopt", + "formulalistopt", "labelopt", "formula", "@3", "@4", "formulaopt", + "arglist", "binsymbol", "nsymbol", "quantsymbol", "id", "qtermlist", + "qterm", "clauselistsopt", "clauselist", "@5", "cnfclausesopt", + "cnfclauseopt", "cnfclause", "@6", "@7", "cnfclausebody", "litlist", + "lit", "atomlist", "atom", "dnfclausesopt", "dnfclauseopt", "dnfclause", + "dnfclausebody", "term", "termlist", "prooflistsopt", "prooflist", "@8", + "prooflistopt", "parentlist", "assoclistopt", "assoclist", + "id_or_formula", "@9", "anysymbol", "optargs", "clause", + "listOfTermsopt", "listOfTerms", "@10", "terms", "settinglistsopt", + "settinglist", "@11", "flags", "spassflags", "spassflag", "preclist", + "precitem", "statopt", "gsettings", "gsetting", "labellist", 0 +}; +#endif + +# ifdef YYPRINT +/* YYTOKNUM[YYLEX-NUM] -- Internal token number corresponding to + token YYLEX-NUM. */ +static const unsigned short yytoknum[] = +{ + 0, 256, 257, 258, 259, 260, 261, 262, 263, 264, + 265, 266, 267, 268, 269, 270, 271, 272, 273, 274, + 275, 276, 277, 278, 279, 280, 281, 282, 283, 284, + 285, 286, 287, 288, 289, 290, 291, 292, 293, 294, + 295, 296, 297, 298, 299, 300, 301, 302, 303, 304, + 305, 306, 307, 308, 309, 310, 311, 312, 313, 314, + 315, 316, 317, 318, 40, 41, 46, 91, 93, 44, + 58 +}; +# endif + +/* YYR1[YYN] -- Symbol number of symbol that rule YYN derives. */ +static const unsigned char yyr1[] = +{ + 0, 71, 72, 73, 74, 75, 76, 77, 78, 78, + 79, 79, 80, 80, 81, 81, 81, 82, 83, 83, + 84, 84, 85, 85, 86, 86, 87, 87, 88, 88, + 89, 89, 90, 90, 91, 91, 92, 92, 93, 93, + 94, 94, 95, 95, 96, 96, 97, 97, 98, 98, + 99, 99, 100, 100, 101, 101, 101, 101, 102, 103, + 101, 104, 105, 105, 106, 106, 107, 107, 108, 109, + 109, 110, 110, 111, 111, 112, 112, 113, 113, 113, + 113, 114, 115, 113, 116, 116, 117, 117, 118, 118, + 118, 119, 119, 120, 120, 121, 121, 121, 121, 121, + 122, 122, 123, 123, 124, 124, 125, 126, 125, 127, + 127, 128, 128, 129, 130, 131, 129, 132, 133, 133, + 134, 134, 135, 135, 136, 136, 136, 136, 136, 137, + 137, 138, 138, 139, 139, 140, 141, 141, 142, 142, + 143, 143, 145, 144, 146, 146, 147, 147, 148, 148, + 149, 149, 151, 150, 152, 152, 152, 152, 152, 152, + 152, 152, 152, 153, 153, 153, 154, 154, 155, 155, + 157, 156, 158, 158, 159, 159, 160, 161, 160, 162, + 162, 163, 163, 164, 164, 164, 165, 165, 166, 166, + 167, 167, 168, 168, 169, 170, 170 +}; + +/* YYR2[YYN] -- Number of symbols composing right hand side of rule YYN. */ +static const unsigned char yyr2[] = +{ + 0, 2, 10, 11, 5, 5, 5, 5, 0, 5, + 0, 5, 0, 5, 1, 1, 1, 6, 0, 9, + 0, 5, 1, 3, 1, 5, 0, 5, 1, 3, + 1, 5, 0, 5, 1, 3, 0, 5, 1, 3, + 1, 5, 0, 5, 1, 3, 1, 5, 1, 1, + 0, 5, 0, 2, 1, 7, 2, 7, 0, 0, + 11, 9, 0, 1, 1, 3, 1, 3, 8, 1, + 1, 0, 2, 0, 7, 0, 2, 1, 4, 6, + 4, 0, 0, 10, 0, 1, 1, 3, 1, 1, + 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, + 1, 3, 1, 4, 0, 2, 10, 0, 11, 0, + 7, 0, 1, 1, 0, 0, 10, 4, 1, 3, + 1, 4, 1, 3, 1, 1, 1, 6, 4, 0, + 7, 0, 1, 1, 8, 4, 1, 4, 1, 3, + 0, 2, 0, 9, 0, 15, 1, 3, 0, 4, + 3, 5, 0, 3, 1, 1, 1, 1, 1, 1, + 1, 1, 1, 0, 3, 7, 1, 1, 0, 2, + 0, 6, 0, 3, 0, 2, 5, 0, 9, 1, + 3, 0, 3, 4, 4, 6, 1, 3, 1, 6, + 0, 2, 1, 2, 5, 1, 3 +}; + +/* YYDEFACT[STATE-NAME] -- Default rule to reduce with in state + STATE-NUM when YYTABLE doesn't specify something else to do. Zero + means the default is an error. */ +static const unsigned char yydefact[] = +{ + 0, 0, 0, 0, 1, 98, 99, 97, 96, 95, + 0, 0, 0, 0, 18, 0, 0, 174, 50, 0, + 0, 20, 0, 0, 71, 0, 0, 8, 0, 26, + 0, 0, 0, 175, 52, 104, 0, 0, 0, 10, + 0, 0, 32, 2, 0, 0, 0, 0, 72, 140, + 0, 0, 0, 0, 0, 0, 0, 22, 24, 0, + 0, 36, 0, 0, 192, 177, 0, 0, 126, 0, + 0, 0, 0, 125, 53, 54, 124, 0, 0, 0, + 105, 168, 4, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 28, 30, 0, 0, 42, 0, 0, + 193, 0, 51, 0, 0, 0, 62, 0, 0, 56, + 69, 70, 0, 0, 0, 141, 17, 5, 0, 0, + 0, 0, 12, 0, 21, 23, 0, 0, 0, 0, + 34, 0, 0, 0, 195, 0, 176, 0, 136, 0, + 58, 0, 63, 0, 0, 138, 0, 0, 0, 0, + 0, 169, 9, 0, 14, 16, 15, 0, 0, 0, + 0, 49, 48, 0, 0, 27, 29, 0, 0, 0, + 0, 38, 40, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 128, 0, 73, 0, 0, 170, + 11, 0, 0, 0, 0, 25, 0, 33, 35, 0, + 0, 0, 0, 0, 44, 46, 19, 194, 196, 181, + 179, 0, 0, 0, 102, 59, 100, 0, 66, 0, + 0, 139, 0, 0, 0, 0, 172, 6, 0, 0, + 3, 31, 0, 37, 39, 0, 0, 0, 0, 0, + 137, 127, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 142, 0, 7, 0, 0, 0, 43, + 45, 180, 0, 0, 0, 0, 178, 0, 101, 0, + 57, 67, 0, 64, 55, 68, 84, 109, 107, 144, + 0, 0, 13, 41, 0, 0, 0, 0, 182, 103, + 0, 0, 0, 91, 88, 93, 94, 89, 90, 0, + 92, 85, 75, 0, 0, 0, 77, 0, 129, 0, + 171, 173, 47, 0, 0, 188, 0, 186, 0, 0, + 61, 65, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 184, 0, 183, 0, 0, 0, 0, + 76, 0, 0, 86, 0, 81, 111, 106, 0, 0, + 143, 0, 0, 187, 0, 60, 78, 74, 0, 80, + 0, 0, 0, 0, 75, 112, 113, 131, 108, 159, + 156, 162, 161, 157, 158, 155, 160, 154, 0, 152, + 190, 185, 0, 87, 82, 0, 0, 0, 0, 0, + 75, 132, 133, 0, 163, 0, 0, 79, 0, 114, + 0, 0, 118, 120, 0, 0, 0, 0, 166, 167, + 0, 0, 153, 191, 189, 0, 0, 0, 117, 0, + 110, 0, 0, 0, 0, 0, 0, 0, 115, 0, + 119, 135, 0, 122, 130, 0, 0, 164, 0, 0, + 121, 0, 0, 0, 0, 83, 0, 0, 123, 0, + 0, 0, 0, 0, 146, 0, 0, 134, 148, 0, + 165, 116, 0, 0, 147, 0, 0, 0, 0, 145, + 149, 0, 0, 0, 150, 0, 151 +}; + +/* YYDEFGOTO[NTERM-NUM]. */ +static const short yydefgoto[] = +{ + -1, 2, 14, 20, 27, 87, 122, 39, 54, 160, + 157, 17, 18, 29, 56, 57, 42, 92, 93, 61, + 129, 97, 170, 171, 133, 203, 204, 163, 24, 46, + 74, 180, 244, 75, 143, 272, 217, 48, 112, 35, + 222, 324, 343, 361, 398, 302, 344, 303, 304, 305, + 76, 215, 216, 49, 80, 308, 307, 364, 365, 416, + 439, 366, 401, 402, 432, 306, 330, 390, 391, 392, + 145, 146, 81, 115, 279, 309, 453, 463, 467, 378, + 394, 379, 412, 410, 116, 151, 226, 254, 22, 33, + 101, 211, 238, 265, 316, 317, 396, 63, 64, 135 +}; + +/* YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing + STATE-NUM. */ +#define YYPACT_NINF -356 +static const short yypact[] = +{ + 9, -32, 35, 232, -356, -356, -356, -356, -356, -356, + -6, 13, 67, 20, 45, 53, 30, -356, 110, 46, + 118, 121, -12, 73, -356, 91, 84, 113, 112, 141, + 123, 128, 132, -356, -356, 175, 152, 161, 155, 191, + 2, 162, 180, -356, 204, 232, 214, 173, -356, 252, + 176, 206, 209, 213, 226, 232, 47, -356, -356, 80, + 218, 254, 224, -14, -356, -356, 230, 233, -356, 234, + 241, 232, 242, -356, -356, -356, 243, 237, 21, 244, + -356, 260, -356, 246, 245, 250, 251, 294, 247, 248, + 2, 232, 93, -356, -356, 232, 255, 272, 232, 253, + -356, 256, -356, 232, 257, 232, 290, 232, 232, -356, + -356, -356, 258, 21, 261, -356, 271, -356, 262, 264, + 14, 263, 317, 108, -356, -356, 265, 266, 80, 119, + -356, 85, 268, 312, -356, 124, -356, 270, 273, 269, + -356, 274, -356, 309, 275, -356, -52, 276, 277, 232, + 279, -356, -356, 281, -356, -356, -356, 284, 287, 288, + 321, -356, -356, 286, 108, -356, -356, 289, 232, 232, + 138, -356, -356, 156, 291, 293, 232, -17, 232, 232, + 232, 232, 346, 232, -356, 232, -356, 40, 296, -356, + -356, 297, 299, 302, 300, -356, 303, -356, -356, 285, + 301, 85, 232, 143, -356, -356, -356, -356, -356, -356, + -356, 337, 16, 304, 298, 306, -356, 32, -356, 311, + 305, -356, 56, 308, 314, 310, -356, -356, 315, 318, + -356, -356, 108, -356, -356, 313, 319, 156, -2, 320, + -356, -356, 232, 232, 316, 322, 232, 232, 323, 324, + 307, 325, 326, -356, 240, -356, 327, 329, 108, -356, + -356, -356, 331, 332, 334, 333, -356, 335, -356, 336, + -356, -356, 145, -356, -356, -356, 96, -356, -356, -356, + 338, 340, -356, -356, 342, 232, 163, 339, -356, -356, + 239, 343, 232, -356, -356, -356, -356, -356, -356, 344, + -356, -356, 341, 347, 348, 350, -356, 3, -356, -15, + -356, -356, -356, 42, 232, -356, 43, -356, 349, 351, + -356, -356, 96, 232, 352, 96, 96, 353, 355, 357, + 57, 358, 361, -356, 359, -356, 163, 108, 360, 362, + -356, 363, 364, -356, 44, -356, -13, -356, 366, 365, + -356, 168, 372, -356, 369, -356, -356, -356, 96, -356, + 96, 232, 371, 373, 341, -356, -356, 0, -356, -356, + -356, -356, -356, -356, -356, -356, -356, -356, 367, -356, + 370, -356, 375, -356, 306, 374, 228, 377, 379, 380, + 341, -356, -356, 50, 381, 376, 382, -356, 383, -356, + 384, 66, -356, -356, 386, 228, 387, 385, -356, -356, + 388, 7, -356, -356, -356, 389, 232, 239, -356, 228, + -356, 69, 239, 393, 232, 232, 90, 96, 306, 390, + -356, -356, 153, -356, -356, 391, 179, -356, 396, 395, + -356, 397, 239, 398, 401, -356, 402, 399, -356, 168, + 96, 409, 408, 185, -356, 410, 411, -356, 405, 168, + -356, -356, 400, 412, -356, 168, 413, 198, 345, -356, + -356, 168, 168, 394, -356, 168, -356 +}; + +/* YYPGOTO[NTERM-NUM]. */ +static const short yypgoto[] = +{ + -356, -356, -356, -356, -356, -356, -356, -356, -356, -356, + -356, -356, -356, -356, -356, 392, -356, -356, 259, -356, + -356, -356, -356, 202, -356, -356, 216, -152, -356, -356, + -356, -356, -356, -356, -356, -356, -356, -356, 267, -356, + -356, -340, -267, -356, -356, -356, 70, -356, -356, -356, + -3, -355, 235, -356, -356, -356, -356, -356, 87, -356, + -356, 33, 78, 68, -356, -45, -356, -356, 92, 39, + -101, 328, -356, -356, -356, -356, -356, -356, -356, -308, + -356, -356, -356, -356, -356, -356, -356, -356, -356, -356, + -356, -356, -356, -356, -356, 154, -356, -356, 425, 207 +}; + +/* YYTABLE[YYPACT[STATE-NUM]]. What to do in state STATE-NUM. If + positive, shift that token. If negative, reduce the rule which + number is the opposite. If zero, do what YYDEFACT says. + If YYTABLE_NINF, parse error. */ +#define YYTABLE_NINF -1 +static const unsigned short yytable[] = +{ + 10, 77, 139, 388, 331, 99, 384, 261, 30, 301, + 293, 328, 196, 184, 362, 1, 262, 185, 62, 31, + 5, 209, 329, 389, 387, 5, 110, 363, 67, 294, + 295, 68, 3, 111, 296, 4, 32, 58, 332, 263, + 297, 298, 65, 6, 299, 264, 210, 300, 6, 7, + 407, 223, 88, 388, 7, 339, 94, 224, 342, 11, + 154, 428, 8, 73, 9, 348, 55, 8, 106, 9, + 436, 155, 156, 389, 425, 249, 349, 362, 213, 12, + 257, 240, 250, 13, 221, 185, 15, 58, 126, 19, + 363, 382, 130, 383, 16, 134, 21, 245, 5, 293, + 138, 246, 141, 5, 144, 138, 284, 333, 335, 359, + 25, 176, 336, 360, 5, 89, 90, 67, 294, 295, + 68, 6, 26, 296, 23, 94, 6, 7, 172, 297, + 298, 418, 7, 299, 431, 419, 300, 6, 419, 34, + 8, 454, 9, 7, 91, 8, 188, 9, 37, 169, + 28, 464, 73, 281, 36, 437, 8, 468, 9, 360, + 438, 127, 128, 473, 474, 198, 199, 476, 161, 162, + 205, 369, 38, 208, 5, 138, 138, 214, 218, 40, + 220, 5, 138, 455, 41, 354, 5, 167, 168, 43, + 370, 371, 175, 176, 44, 372, 45, 6, 172, 235, + 47, 373, 374, 7, 6, 375, 200, 201, 376, 6, + 7, 236, 237, 291, 292, 7, 8, 50, 9, 52, + 202, 441, 442, 8, 51, 9, 53, 314, 8, 59, + 9, 60, 5, 66, 205, 67, 62, 78, 68, 267, + 214, 69, 82, 271, 273, 319, 5, 444, 243, 67, + 5, 138, 68, 458, 459, 6, 70, 5, 5, 280, + 67, 7, 79, 68, 71, 400, 470, 471, 72, 6, + 73, 83, 84, 6, 8, 7, 9, 85, 86, 7, + 6, 6, 134, 315, 73, 95, 7, 7, 8, 321, + 9, 98, 8, 96, 9, 73, 102, 103, 104, 8, + 8, 9, 9, 109, 114, 105, 107, 108, 113, 121, + 118, 334, 117, 119, 124, 120, 123, 132, 142, 136, + 340, 137, 131, 147, 140, 149, 150, 158, 152, 153, + 159, 174, 165, 315, 164, 173, 177, 178, 179, 182, + 194, 403, 186, 181, 183, 189, 187, 190, 377, 191, + 192, 195, 193, 219, 232, 197, 239, 206, 214, 207, + 403, 225, 242, 227, 228, 229, 230, 233, 231, 241, + 248, 276, 429, 251, 403, 243, 253, 433, 247, 252, + 148, 255, 258, 256, 269, 259, 266, 166, 270, 274, + 275, 277, 278, 282, 283, 285, 286, 448, 287, 288, + 289, 318, 388, 234, 310, 290, 311, 312, 322, 320, + 323, 325, 326, 214, 327, 472, 338, 341, 337, 346, + 345, 435, 214, 347, 350, 351, 355, 356, 352, 357, + 367, 368, 380, 358, 381, 385, 393, 386, 413, 395, + 397, 399, 404, 405, 406, 411, 377, 414, 417, 363, + 423, 415, 420, 260, 422, 440, 377, 424, 427, 434, + 443, 445, 377, 446, 475, 449, 447, 465, 377, 377, + 450, 451, 377, 457, 462, 460, 461, 466, 268, 469, + 408, 426, 125, 421, 456, 409, 452, 430, 100, 0, + 353, 0, 313, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 212 +}; + +static const short yycheck[] = +{ + 3, 46, 103, 3, 19, 19, 361, 9, 20, 276, + 3, 8, 164, 65, 27, 6, 18, 69, 32, 31, + 18, 38, 19, 23, 364, 18, 5, 40, 21, 22, + 23, 24, 64, 12, 27, 0, 48, 40, 53, 41, + 33, 34, 45, 41, 37, 47, 63, 40, 41, 47, + 390, 11, 55, 3, 47, 322, 59, 17, 325, 65, + 46, 416, 60, 56, 62, 8, 64, 60, 71, 62, + 425, 57, 58, 23, 67, 19, 19, 27, 179, 66, + 232, 65, 26, 16, 185, 69, 66, 90, 91, 36, + 40, 358, 95, 360, 49, 98, 66, 65, 18, 3, + 103, 69, 105, 18, 107, 108, 258, 65, 65, 65, + 64, 69, 69, 69, 18, 68, 69, 21, 22, 23, + 24, 41, 4, 27, 14, 128, 41, 47, 131, 33, + 34, 65, 47, 37, 65, 69, 40, 41, 69, 66, + 60, 449, 62, 47, 64, 60, 149, 62, 64, 64, + 29, 459, 56, 254, 63, 65, 60, 465, 62, 69, + 427, 68, 69, 471, 472, 168, 169, 475, 60, 61, + 173, 3, 59, 176, 18, 178, 179, 180, 181, 67, + 183, 18, 185, 450, 43, 337, 18, 68, 69, 66, + 22, 23, 68, 69, 66, 27, 64, 41, 201, 202, + 25, 33, 34, 47, 41, 37, 68, 69, 40, 41, + 47, 68, 69, 68, 69, 47, 60, 65, 62, 64, + 64, 68, 69, 60, 63, 62, 35, 64, 60, 67, + 62, 51, 18, 19, 237, 21, 32, 64, 24, 242, + 243, 27, 66, 246, 247, 290, 18, 68, 69, 21, + 18, 254, 24, 68, 69, 41, 42, 18, 18, 19, + 21, 47, 10, 24, 50, 37, 68, 69, 54, 41, + 56, 65, 63, 41, 60, 47, 62, 64, 52, 47, + 41, 41, 285, 286, 56, 67, 47, 47, 60, 292, + 62, 67, 60, 39, 62, 56, 66, 64, 64, 60, + 60, 62, 62, 66, 44, 64, 64, 64, 64, 15, + 65, 314, 66, 63, 66, 64, 69, 45, 28, 66, + 323, 65, 67, 65, 67, 64, 55, 64, 66, 65, + 13, 19, 66, 336, 69, 67, 66, 64, 69, 30, + 19, 386, 66, 69, 69, 66, 69, 66, 351, 65, + 63, 65, 64, 7, 69, 66, 19, 66, 361, 66, + 405, 65, 64, 66, 65, 63, 66, 66, 65, 65, + 65, 64, 417, 65, 419, 69, 66, 422, 67, 65, + 113, 66, 69, 65, 68, 66, 66, 128, 66, 66, + 66, 66, 66, 66, 65, 64, 64, 442, 64, 66, + 65, 62, 3, 201, 66, 69, 66, 65, 64, 66, + 69, 64, 64, 416, 64, 70, 65, 65, 69, 64, + 67, 424, 425, 66, 66, 64, 66, 65, 69, 66, + 64, 66, 60, 69, 65, 64, 69, 64, 62, 69, + 65, 67, 65, 64, 64, 64, 449, 65, 64, 40, + 65, 68, 66, 237, 67, 65, 459, 69, 69, 66, + 69, 65, 465, 68, 70, 67, 69, 67, 471, 472, + 69, 69, 475, 65, 69, 65, 65, 65, 243, 66, + 393, 411, 90, 405, 451, 393, 447, 419, 63, -1, + 336, -1, 285, -1, -1, -1, -1, -1, -1, -1, + -1, -1, -1, -1, -1, -1, 178 +}; + +/* YYSTOS[STATE-NUM] -- The (internal number of the) accessing + symbol of state STATE-NUM. */ +static const unsigned char yystos[] = +{ + 0, 6, 72, 64, 0, 18, 41, 47, 60, 62, + 121, 65, 66, 16, 73, 66, 49, 82, 83, 36, + 74, 66, 159, 14, 99, 64, 4, 75, 29, 84, + 20, 31, 48, 160, 66, 110, 63, 64, 59, 78, + 67, 43, 87, 66, 66, 64, 100, 25, 108, 124, + 65, 63, 64, 35, 79, 64, 85, 86, 121, 67, + 51, 90, 32, 168, 169, 121, 19, 21, 24, 27, + 42, 50, 54, 56, 101, 104, 121, 136, 64, 10, + 125, 143, 66, 65, 63, 64, 52, 76, 121, 68, + 69, 64, 88, 89, 121, 67, 39, 92, 67, 19, + 169, 161, 66, 64, 64, 64, 121, 64, 64, 66, + 5, 12, 109, 64, 44, 144, 155, 66, 65, 63, + 64, 15, 77, 69, 66, 86, 121, 68, 69, 91, + 121, 67, 45, 95, 121, 170, 66, 65, 121, 141, + 67, 121, 28, 105, 121, 141, 142, 65, 109, 64, + 55, 156, 66, 65, 46, 57, 58, 81, 64, 13, + 80, 60, 61, 98, 69, 66, 89, 68, 69, 64, + 93, 94, 121, 67, 19, 68, 69, 66, 64, 69, + 102, 69, 30, 69, 65, 69, 66, 69, 121, 66, + 66, 65, 63, 64, 19, 65, 98, 66, 121, 121, + 68, 69, 64, 96, 97, 121, 66, 66, 121, 38, + 63, 162, 142, 141, 121, 122, 123, 107, 121, 7, + 121, 141, 111, 11, 17, 65, 157, 66, 65, 63, + 66, 65, 69, 66, 94, 121, 68, 69, 163, 19, + 65, 65, 64, 69, 103, 65, 69, 67, 65, 19, + 26, 65, 65, 66, 158, 66, 65, 98, 69, 66, + 97, 9, 18, 41, 47, 164, 66, 121, 123, 68, + 66, 121, 106, 121, 66, 66, 64, 66, 66, 145, + 19, 141, 66, 65, 98, 64, 64, 64, 66, 65, + 69, 68, 69, 3, 22, 23, 27, 33, 34, 37, + 40, 113, 116, 118, 119, 120, 136, 127, 126, 146, + 66, 66, 65, 170, 64, 121, 165, 166, 62, 136, + 66, 121, 64, 69, 112, 64, 64, 64, 8, 19, + 137, 19, 53, 65, 121, 65, 69, 69, 65, 113, + 121, 65, 113, 113, 117, 67, 64, 66, 8, 19, + 66, 64, 69, 166, 98, 66, 65, 66, 69, 65, + 69, 114, 27, 40, 128, 129, 132, 64, 66, 3, + 22, 23, 27, 33, 34, 37, 40, 121, 150, 152, + 60, 65, 113, 113, 122, 64, 64, 112, 3, 23, + 138, 139, 140, 69, 151, 69, 167, 65, 115, 67, + 37, 133, 134, 136, 65, 64, 64, 112, 129, 139, + 154, 64, 153, 62, 65, 68, 130, 64, 65, 69, + 66, 133, 67, 65, 69, 67, 117, 69, 122, 136, + 134, 65, 135, 136, 66, 121, 122, 65, 113, 131, + 65, 68, 69, 69, 68, 65, 68, 69, 136, 67, + 69, 69, 140, 147, 150, 113, 132, 65, 68, 69, + 65, 65, 69, 148, 150, 67, 65, 149, 150, 66, + 68, 69, 70, 150, 150, 70, 150 +}; + +#if ! defined (YYSIZE_T) && defined (__SIZE_TYPE__) +# define YYSIZE_T __SIZE_TYPE__ +#endif +#if ! defined (YYSIZE_T) && defined (size_t) +# define YYSIZE_T size_t +#endif +#if ! defined (YYSIZE_T) +# if defined (__STDC__) || defined (__cplusplus) +# include /* INFRINGES ON USER NAME SPACE */ +# define YYSIZE_T size_t +# endif +#endif +#if ! defined (YYSIZE_T) +# define YYSIZE_T unsigned int +#endif + +#define yyerrok (yyerrstatus = 0) +#define yyclearin (yychar = YYEMPTY) +#define YYEMPTY -2 +#define YYEOF 0 + +#define YYACCEPT goto yyacceptlab +#define YYABORT goto yyabortlab +#define YYERROR goto yyerrlab1 + +/* Like YYERROR except do call yyerror. This remains here temporarily + to ease the transition to the new meaning of YYERROR, for GCC. + Once GCC version 2 has supplanted version 1, this can go. */ + +#define YYFAIL goto yyerrlab + +#define YYRECOVERING() (!!yyerrstatus) + +#define YYBACKUP(Token, Value) \ +do \ + if (yychar == YYEMPTY && yylen == 1) \ + { \ + yychar = (Token); \ + yylval = (Value); \ + yychar1 = YYTRANSLATE (yychar); \ + YYPOPSTACK; \ + goto yybackup; \ + } \ + else \ + { \ + yyerror ("syntax error: cannot back up"); \ + YYERROR; \ + } \ +while (0) + +#define YYTERROR 1 +#define YYERRCODE 256 + +/* YYLLOC_DEFAULT -- Compute the default location (before the actions + are run). */ + +#ifndef YYLLOC_DEFAULT +# define YYLLOC_DEFAULT(Current, Rhs, N) \ + Current.first_line = Rhs[1].first_line; \ + Current.first_column = Rhs[1].first_column; \ + Current.last_line = Rhs[N].last_line; \ + Current.last_column = Rhs[N].last_column; +#endif + +/* YYLEX -- calling `yylex' with the right arguments. */ + +#define YYLEX yylex () + +/* Enable debugging if requested. */ +#if YYDEBUG + +# ifndef YYFPRINTF +# include /* INFRINGES ON USER NAME SPACE */ +# define YYFPRINTF fprintf +# endif + +# define YYDPRINTF(Args) \ +do { \ + if (yydebug) \ + YYFPRINTF Args; \ +} while (0) +# define YYDSYMPRINT(Args) \ +do { \ + if (yydebug) \ + yysymprint Args; \ +} while (0) +/* Nonzero means print parse trace. It is left uninitialized so that + multiple parsers can coexist. */ +int yydebug; +#else /* !YYDEBUG */ +# define YYDPRINTF(Args) +# define YYDSYMPRINT(Args) +#endif /* !YYDEBUG */ + +/* YYINITDEPTH -- initial size of the parser's stacks. */ +#ifndef YYINITDEPTH +# define YYINITDEPTH 200 +#endif + +/* YYMAXDEPTH -- maximum size the stacks can grow to (effective only + if the built-in stack extension method is used). + + Do not make this value too large; the results are undefined if + SIZE_MAX < YYSTACK_BYTES (YYMAXDEPTH) + evaluated with infinite-precision integer arithmetic. */ + +#if YYMAXDEPTH == 0 +# undef YYMAXDEPTH +#endif + +#ifndef YYMAXDEPTH +# define YYMAXDEPTH 10000 +#endif + + + +#if YYERROR_VERBOSE + +# ifndef yystrlen +# if defined (__GLIBC__) && defined (_STRING_H) +# define yystrlen strlen +# else +/* Return the length of YYSTR. */ +static YYSIZE_T +# if defined (__STDC__) || defined (__cplusplus) +yystrlen (const char *yystr) +# else +yystrlen (yystr) + const char *yystr; +# endif +{ + register const char *yys = yystr; + + while (*yys++ != '\0') + continue; + + return yys - yystr - 1; +} +# endif +# endif + +# ifndef yystpcpy +# if defined (__GLIBC__) && defined (_STRING_H) && defined (_GNU_SOURCE) +# define yystpcpy stpcpy +# else +/* Copy YYSRC to YYDEST, returning the address of the terminating '\0' in + YYDEST. */ +static char * +# if defined (__STDC__) || defined (__cplusplus) +yystpcpy (char *yydest, const char *yysrc) +# else +yystpcpy (yydest, yysrc) + char *yydest; + const char *yysrc; +# endif +{ + register char *yyd = yydest; + register const char *yys = yysrc; + + while ((*yyd++ = *yys++) != '\0') + continue; + + return yyd - 1; +} +# endif +# endif + +#endif /* !YYERROR_VERBOSE */ + + + +#if YYDEBUG +/*-----------------------------. +| Print this symbol on YYOUT. | +`-----------------------------*/ + +static void +#if defined (__STDC__) || defined (__cplusplus) +yysymprint (FILE* yyout, int yytype, YYSTYPE yyvalue) +#else +yysymprint (yyout, yytype, yyvalue) + FILE* yyout; + int yytype; + YYSTYPE yyvalue; +#endif +{ + /* Pacify ``unused variable'' warnings. */ + (void) yyvalue; + + if (yytype < YYNTOKENS) + { + YYFPRINTF (yyout, "token %s (", yytname[yytype]); +# ifdef YYPRINT + YYPRINT (yyout, yytoknum[yytype], yyvalue); +# endif + } + else + YYFPRINTF (yyout, "nterm %s (", yytname[yytype]); + + switch (yytype) + { + default: + break; + } + YYFPRINTF (yyout, ")"); +} +#endif /* YYDEBUG. */ + + +/*-----------------------------------------------. +| Release the memory associated to this symbol. | +`-----------------------------------------------*/ + +static void +#if defined (__STDC__) || defined (__cplusplus) +yydestruct (int yytype, YYSTYPE yyvalue) +#else +yydestruct (yytype, yyvalue) + int yytype; + YYSTYPE yyvalue; +#endif +{ + /* Pacify ``unused variable'' warnings. */ + (void) yyvalue; + + switch (yytype) + { + default: + break; + } +} + + + +/* The user can define YYPARSE_PARAM as the name of an argument to be passed + into yyparse. The argument should have type void *. + It should actually point to an object. + Grammar actions can access the variable by casting it + to the proper pointer type. */ + +#ifdef YYPARSE_PARAM +# if defined (__STDC__) || defined (__cplusplus) +# define YYPARSE_PARAM_ARG void *YYPARSE_PARAM +# define YYPARSE_PARAM_DECL +# else +# define YYPARSE_PARAM_ARG YYPARSE_PARAM +# define YYPARSE_PARAM_DECL void *YYPARSE_PARAM; +# endif +#else /* !YYPARSE_PARAM */ +# define YYPARSE_PARAM_ARG +# define YYPARSE_PARAM_DECL +#endif /* !YYPARSE_PARAM */ + +/* Prevent warning if -Wstrict-prototypes. */ +#ifdef __GNUC__ +# ifdef YYPARSE_PARAM +int yyparse (void *); +# else +int yyparse (void); +# endif +#endif + + +/* The lookahead symbol. */ +int yychar; + +/* The semantic value of the lookahead symbol. */ +YYSTYPE yylval; + +/* Number of parse errors so far. */ +int yynerrs; + + +int +yyparse (YYPARSE_PARAM_ARG) + YYPARSE_PARAM_DECL +{ + + register int yystate; + register int yyn; + int yyresult; + /* Number of tokens to shift before error messages enabled. */ + int yyerrstatus; + /* Lookahead token as an internal (translated) token number. */ + int yychar1 = 0; + + /* Three stacks and their tools: + `yyss': related to states, + `yyvs': related to semantic values, + `yyls': related to locations. + + Refer to the stacks thru separate pointers, to allow yyoverflow + to reallocate them elsewhere. */ + + /* The state stack. */ + short yyssa[YYINITDEPTH]; + short *yyss = yyssa; + register short *yyssp; + + /* The semantic value stack. */ + YYSTYPE yyvsa[YYINITDEPTH]; + YYSTYPE *yyvs = yyvsa; + register YYSTYPE *yyvsp; + + + +#define YYPOPSTACK (yyvsp--, yyssp--) + + YYSIZE_T yystacksize = YYINITDEPTH; + + /* The variables used to return semantic value and location from the + action routines. */ + YYSTYPE yyval; + + + /* When reducing, the number of symbols on the RHS of the reduced + rule. */ + int yylen; + + YYDPRINTF ((stderr, "Starting parse\n")); + + yystate = 0; + yyerrstatus = 0; + yynerrs = 0; + yychar = YYEMPTY; /* Cause a token to be read. */ + + /* Initialize stack pointers. + Waste one element of value and location stack + so that they stay on the same level as the state stack. + The wasted elements are never initialized. */ + + yyssp = yyss; + yyvsp = yyvs; + + goto yysetstate; + +/*------------------------------------------------------------. +| yynewstate -- Push a new state, which is found in yystate. | +`------------------------------------------------------------*/ + yynewstate: + /* In all cases, when you get here, the value and location stacks + have just been pushed. so pushing a state here evens the stacks. + */ + yyssp++; + + yysetstate: + *yyssp = yystate; + + if (yyssp >= yyss + yystacksize - 1) + { + /* Get the current used size of the three stacks, in elements. */ + YYSIZE_T yysize = yyssp - yyss + 1; + +#ifdef yyoverflow + { + /* Give user a chance to reallocate the stack. Use copies of + these so that the &'s don't force the real ones into + memory. */ + YYSTYPE *yyvs1 = yyvs; + short *yyss1 = yyss; + + + /* Each stack pointer address is followed by the size of the + data in use in that stack, in bytes. This used to be a + conditional around just the two extra args, but that might + be undefined if yyoverflow is a macro. */ + yyoverflow ("parser stack overflow", + &yyss1, yysize * sizeof (*yyssp), + &yyvs1, yysize * sizeof (*yyvsp), + + &yystacksize); + + yyss = yyss1; + yyvs = yyvs1; + } +#else /* no yyoverflow */ +# ifndef YYSTACK_RELOCATE + goto yyoverflowlab; +# else + /* Extend the stack our own way. */ + if (yystacksize >= YYMAXDEPTH) + goto yyoverflowlab; + yystacksize *= 2; + if (yystacksize > YYMAXDEPTH) + yystacksize = YYMAXDEPTH; + + { + short *yyss1 = yyss; + union yyalloc *yyptr = + (union yyalloc *) YYSTACK_ALLOC (YYSTACK_BYTES (yystacksize)); + if (! yyptr) + goto yyoverflowlab; + YYSTACK_RELOCATE (yyss); + YYSTACK_RELOCATE (yyvs); + +# undef YYSTACK_RELOCATE + if (yyss1 != yyssa) + YYSTACK_FREE (yyss1); + } +# endif +#endif /* no yyoverflow */ + + yyssp = yyss + yysize - 1; + yyvsp = yyvs + yysize - 1; + + + YYDPRINTF ((stderr, "Stack size increased to %lu\n", + (unsigned long int) yystacksize)); + + if (yyssp >= yyss + yystacksize - 1) + YYABORT; + } + + YYDPRINTF ((stderr, "Entering state %d\n", yystate)); + + goto yybackup; + +/*-----------. +| yybackup. | +`-----------*/ +yybackup: + +/* Do appropriate processing given the current state. */ +/* Read a lookahead token if we need one and don't already have one. */ +/* yyresume: */ + + /* First try to decide what to do without reference to lookahead token. */ + + yyn = yypact[yystate]; + if (yyn == YYPACT_NINF) + goto yydefault; + + /* Not known => get a lookahead token if don't already have one. */ + + /* yychar is either YYEMPTY or YYEOF + or a valid token in external form. */ + + if (yychar == YYEMPTY) + { + YYDPRINTF ((stderr, "Reading a token: ")); + yychar = YYLEX; + } + + /* Convert token to internal form (in yychar1) for indexing tables with. */ + + if (yychar <= 0) /* This means end of input. */ + { + yychar1 = 0; + yychar = YYEOF; /* Don't call YYLEX any more. */ + + YYDPRINTF ((stderr, "Now at end of input.\n")); + } + else + { + yychar1 = YYTRANSLATE (yychar); + + /* We have to keep this `#if YYDEBUG', since we use variables + which are defined only if `YYDEBUG' is set. */ + YYDPRINTF ((stderr, "Next token is ")); + YYDSYMPRINT ((stderr, yychar1, yylval)); + YYDPRINTF ((stderr, "\n")); + } + + /* If the proper action on seeing token YYCHAR1 is to reduce or to + detect an error, take that action. */ + yyn += yychar1; + if (yyn < 0 || YYLAST < yyn || yycheck[yyn] != yychar1) + goto yydefault; + yyn = yytable[yyn]; + if (yyn <= 0) + { + if (yyn == 0 || yyn == YYTABLE_NINF) + goto yyerrlab; + yyn = -yyn; + goto yyreduce; + } + + if (yyn == YYFINAL) + YYACCEPT; + + /* Shift the lookahead token. */ + YYDPRINTF ((stderr, "Shifting token %d (%s), ", + yychar, yytname[yychar1])); + + /* Discard the token being shifted unless it is eof. */ + if (yychar != YYEOF) + yychar = YYEMPTY; + + *++yyvsp = yylval; + + + /* Count tokens shifted since error; after three, turn off error + status. */ + if (yyerrstatus) + yyerrstatus--; + + yystate = yyn; + goto yynewstate; + + +/*-----------------------------------------------------------. +| yydefault -- do the default action for the current state. | +`-----------------------------------------------------------*/ +yydefault: + yyn = yydefact[yystate]; + if (yyn == 0) + goto yyerrlab; + goto yyreduce; + + +/*-----------------------------. +| yyreduce -- Do a reduction. | +`-----------------------------*/ +yyreduce: + /* yyn is the number of a rule to reduce with. */ + yylen = yyr2[yyn]; + + /* If YYLEN is nonzero, implement the default value of the action: + `$$ = $1'. + + Otherwise, the following line sets YYVAL to garbage. + This behavior is undocumented and Bison + users should not rely upon it. Assigning to YYVAL + unconditionally makes the parser a bit smaller, and it avoids a + GCC warning that YYVAL may be used uninitialized. */ + yyval = yyvsp[1-yylen]; + + + +#if YYDEBUG + /* We have to keep this `#if YYDEBUG', since we use variables which + are defined only if `YYDEBUG' is set. */ + if (yydebug) + { + int yyi; + + YYFPRINTF (stderr, "Reducing via rule %d (line %d), ", + yyn - 1, yyrline[yyn]); + + /* Print the symbols being reduced, and their result. */ + for (yyi = yyprhs[yyn]; yyrhs[yyi] >= 0; yyi++) + YYFPRINTF (stderr, "%s ", yytname[yyrhs[yyi]]); + YYFPRINTF (stderr, " -> %s\n", yytname[yyr1[yyn]]); + } +#endif + switch (yyn) + { + case 2: +#line 210 "dfgparser.y" + { string_StringFree(yyvsp[-7].string); + YYACCEPT; /* Stop immediately */ } + break; + + case 4: +#line 230 "dfgparser.y" + { dfg_DESC.name = yyvsp[-2].string; } + break; + + case 5: +#line 234 "dfgparser.y" + { dfg_DESC.author = yyvsp[-2].string; } + break; + + case 6: +#line 238 "dfgparser.y" + { dfg_DESC.status = yyvsp[-2].state; } + break; + + case 7: +#line 242 "dfgparser.y" + { dfg_DESC.description = yyvsp[-2].string; } + break; + + case 9: +#line 247 "dfgparser.y" + { dfg_DESC.version = yyvsp[-2].string; } + break; + + case 11: +#line 252 "dfgparser.y" + { dfg_DESC.logic = yyvsp[-2].string; } + break; + + case 13: +#line 257 "dfgparser.y" + { dfg_DESC.date = yyvsp[-2].string; } + break; + + case 14: +#line 260 "dfgparser.y" + { yyval.state = DFG_SATISFIABLE; } + break; + + case 15: +#line 261 "dfgparser.y" + { yyval.state = DFG_UNSATISFIABLE; } + break; + + case 16: +#line 262 "dfgparser.y" + { yyval.state = DFG_UNKNOWNSTATE; } + break; + + case 24: +#line 299 "dfgparser.y" + { dfg_SymbolDecl(DFG_FUNC, yyvsp[0].string, -2); } + break; + + case 25: +#line 301 "dfgparser.y" + { dfg_SymbolDecl(DFG_FUNC, yyvsp[-3].string, yyvsp[-1].number); } + break; + + case 30: +#line 312 "dfgparser.y" + { dfg_SymbolDecl(DFG_PRDICAT, yyvsp[0].string, -2); } + break; + + case 31: +#line 313 "dfgparser.y" + { dfg_SymbolDecl(DFG_PRDICAT, yyvsp[-3].string, yyvsp[-1].number); } + break; + + case 34: +#line 320 "dfgparser.y" + { dfg_SymbolDecl(DFG_PRDICAT, yyvsp[0].string, 1); } + break; + + case 35: +#line 321 "dfgparser.y" + { dfg_SymbolDecl(DFG_PRDICAT, yyvsp[0].string, 1); } + break; + + case 40: +#line 332 "dfgparser.y" + { dfg_SymbolDecl(DFG_OPERAT, yyvsp[0].string, -2); } + break; + + case 41: +#line 333 "dfgparser.y" + { dfg_SymbolDecl(DFG_OPERAT, yyvsp[-3].string, yyvsp[-1].number); } + break; + + case 46: +#line 344 "dfgparser.y" + { dfg_SymbolDecl(DFG_QUANTIF, yyvsp[0].string, -2); } + break; + + case 47: +#line 345 "dfgparser.y" + { dfg_SymbolDecl(DFG_QUANTIF, yyvsp[-3].string, yyvsp[-1].number); } + break; + + case 48: +#line 348 "dfgparser.y" + { yyval.number = -1; } + break; + + case 49: +#line 349 "dfgparser.y" + { yyval.number = yyvsp[0].number; } + break; + + case 55: +#line 368 "dfgparser.y" + { dfg_SubSort(yyvsp[-4].string,yyvsp[-2].string); } + break; + + case 56: +#line 369 "dfgparser.y" + { dfg_SORTDECLLIST = list_Nconc(dfg_SORTDECLLIST,list_List(list_PairCreate(NULL,yyvsp[-1].term))); } + break; + + case 57: +#line 371 "dfgparser.y" + { string_StringFree(yyvsp[-4].string); } + break; + + case 58: +#line 372 "dfgparser.y" + { dfg_VarStart(); } + break; + + case 59: +#line 373 "dfgparser.y" + { dfg_VarStop(); } + break; + + case 60: +#line 374 "dfgparser.y" + { TERM term; + dfg_VarBacktrack(); + dfg_VarCheck(); + term = dfg_CreateQuantifier(fol_All(),yyvsp[-6].list,yyvsp[-2].term); + dfg_SORTDECLLIST = list_Nconc(dfg_SORTDECLLIST,list_List(list_PairCreate(NULL,term))); + } + break; + + case 61: +#line 383 "dfgparser.y" + { dfg_SymbolGenerated(dfg_Symbol(yyvsp[-7].string,1), yyvsp[-6].bool, yyvsp[-2].list); } + break; + + case 62: +#line 386 "dfgparser.y" + { yyval.bool = FALSE; } + break; + + case 63: +#line 387 "dfgparser.y" + { yyval.bool = TRUE; } + break; + + case 64: +#line 390 "dfgparser.y" + { yyval.list = list_List(yyvsp[0].string); } + break; + + case 65: +#line 391 "dfgparser.y" + { yyval.list = list_Cons(yyvsp[0].string, yyvsp[-2].list); } + break; + + case 66: +#line 394 "dfgparser.y" + { string_StringFree(yyvsp[0].string); } + break; + + case 67: +#line 395 "dfgparser.y" + { string_StringFree(yyvsp[0].string); } + break; + + case 68: +#line 404 "dfgparser.y" + { list_NReverse(yyvsp[-2].list); + if (yyvsp[-5].bool) /* Axioms */ + dfg_AXIOMLIST = list_Nconc(dfg_AXIOMLIST, yyvsp[-2].list); + else + dfg_CONJECLIST = list_Nconc(dfg_CONJECLIST, yyvsp[-2].list); + } + break; + + case 69: +#line 412 "dfgparser.y" + { yyval.bool = TRUE; } + break; + + case 70: +#line 413 "dfgparser.y" + { yyval.bool = FALSE; } + break; + + case 73: +#line 420 "dfgparser.y" + { yyval.list = list_Nil(); } + break; + + case 74: +#line 422 "dfgparser.y" + { LIST pair; + if (yyvsp[-3].term == NULL) { /* No term */ + if (yyvsp[-2].string != NULL) + string_StringFree(yyvsp[-2].string); + yyval.list = yyvsp[-6].list; + } else { + pair = list_PairCreate(yyvsp[-2].string, yyvsp[-3].term); + yyval.list = list_Cons(pair, yyvsp[-6].list); + } + dfg_VarCheck(); + } + break; + + case 75: +#line 435 "dfgparser.y" + { yyval.string = NULL; } + break; + + case 76: +#line 436 "dfgparser.y" + { yyval.string = yyvsp[0].string; } + break; + + case 77: +#line 439 "dfgparser.y" + { yyval.term = yyvsp[0].term; } + break; + + case 78: +#line 441 "dfgparser.y" + { yyval.term = dfg_IGNORE ? NULL : term_Create(fol_Not(),list_List(yyvsp[-1].term)); } + break; + + case 79: +#line 443 "dfgparser.y" + { yyval.term = dfg_IGNORE ? NULL : term_Create(yyvsp[-5].symbol, list_Cons(yyvsp[-3].term, list_List(yyvsp[-1].term))); } + break; + + case 80: +#line 445 "dfgparser.y" + { yyval.term = dfg_IGNORE ? NULL : term_Create(yyvsp[-3].symbol, yyvsp[-1].list); } + break; + + case 81: +#line 446 "dfgparser.y" + { dfg_VarStart(); } + break; + + case 82: +#line 447 "dfgparser.y" + { dfg_VarStop(); } + break; + + case 83: +#line 449 "dfgparser.y" + { dfg_VarBacktrack(); + yyval.term = dfg_IGNORE ? NULL : dfg_CreateQuantifier(yyvsp[-9].symbol,yyvsp[-5].list,yyvsp[-1].term); + } + break; + + case 84: +#line 454 "dfgparser.y" + { yyval.term = NULL; } + break; + + case 85: +#line 455 "dfgparser.y" + { yyval.term = yyvsp[0].term; } + break; + + case 86: +#line 459 "dfgparser.y" + { yyval.list = dfg_IGNORE ? list_Nil() : list_List(yyvsp[0].term); } + break; + + case 87: +#line 461 "dfgparser.y" + { yyval.list = dfg_IGNORE ? yyvsp[-2].list : list_Nconc(yyvsp[-2].list, list_List(yyvsp[0].term)); } + break; + + case 88: +#line 464 "dfgparser.y" + { yyval.symbol = fol_Equiv(); } + break; + + case 89: +#line 465 "dfgparser.y" + { yyval.symbol = fol_Implied(); } + break; + + case 90: +#line 466 "dfgparser.y" + { yyval.symbol = fol_Implies(); } + break; + + case 91: +#line 469 "dfgparser.y" + { yyval.symbol = fol_And(); } + break; + + case 92: +#line 470 "dfgparser.y" + { yyval.symbol = fol_Or(); } + break; + + case 93: +#line 473 "dfgparser.y" + { yyval.symbol = fol_Exist(); } + break; + + case 94: +#line 474 "dfgparser.y" + { yyval.symbol = fol_All(); } + break; + + case 95: +#line 477 "dfgparser.y" + { if (dfg_IGNORE) { + string_StringFree(yyvsp[0].string); + yyval.string = NULL; + } else + yyval.string = yyvsp[0].string; + } + break; + + case 96: +#line 484 "dfgparser.y" + { yyval.string = dfg_IGNORE ? NULL : string_IntToString(yyvsp[0].number); } + break; + + case 97: +#line 486 "dfgparser.y" + { yyval.string = dfg_IGNORE ? NULL : string_StringCopy("set_flag"); } + break; + + case 98: +#line 488 "dfgparser.y" + { yyval.string = dfg_IGNORE ? NULL : string_StringCopy("set_DomPred"); } + break; + + case 99: +#line 490 "dfgparser.y" + { yyval.string = dfg_IGNORE ? NULL : string_StringCopy("set_precedence"); } + break; + + case 100: +#line 494 "dfgparser.y" + { yyval.list = dfg_IGNORE ? list_Nil() : list_List(yyvsp[0].term); } + break; + + case 101: +#line 496 "dfgparser.y" + { yyval.list = dfg_IGNORE ? yyvsp[-2].list : list_Nconc(yyvsp[-2].list, list_List(yyvsp[0].term)); } + break; + + case 102: +#line 500 "dfgparser.y" + { if (!dfg_IGNORE) { + SYMBOL s = dfg_Symbol(yyvsp[0].string,0); + if (!symbol_IsVariable(s)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Line %d: Symbol is not a variable.\n",dfg_LINENUMBER); + misc_FinishUserErrorReport(); + } + yyval.term = term_Create(s, list_Nil()); + } + } + break; + + case 103: +#line 511 "dfgparser.y" + { if (!dfg_IGNORE) { + SYMBOL p, v; + p = dfg_Symbol(yyvsp[-3].string, 1); + if (!symbol_IsPredicate(p)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Line %d: Symbol is not a predicate.\n",dfg_LINENUMBER); + misc_FinishUserErrorReport(); + } + v = dfg_Symbol(yyvsp[-1].string, 0); + if (!symbol_IsVariable(v)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Line %d: Symbol is not a variable.\n",dfg_LINENUMBER); + misc_FinishUserErrorReport(); + } + yyval.term = term_Create(p, list_List(term_Create(v,list_Nil()))); + } + } + break; + + case 106: +#line 541 "dfgparser.y" + { list_NReverse(yyvsp[-2].list); + if (yyvsp[-7].bool) /* Axioms */ + dfg_AXCLAUSES = list_Nconc(dfg_AXCLAUSES, yyvsp[-2].list); + else + dfg_CONCLAUSES = list_Nconc(dfg_CONCLAUSES, yyvsp[-2].list); + } + break; + + case 107: +#line 548 "dfgparser.y" + { stack_Push((POINTER)dfg_IGNORE); dfg_IGNORE = TRUE; } + break; + + case 108: +#line 551 "dfgparser.y" + { dfg_IGNORE = (BOOL)stack_PopResult(); } + break; + + case 109: +#line 554 "dfgparser.y" + { yyval.list = list_Nil(); } + break; + + case 110: +#line 556 "dfgparser.y" + { LIST pair; + if (yyvsp[-3].term == NULL) { /* No clause */ + if (yyvsp[-2].string != NULL) + string_StringFree(yyvsp[-2].string); + yyval.list = yyvsp[-6].list; + } else { + pair = list_PairCreate(yyvsp[-2].string, yyvsp[-3].term); + yyval.list = list_Cons(pair, yyvsp[-6].list); + } + dfg_VarCheck(); + } + break; + + case 111: +#line 569 "dfgparser.y" + { yyval.term = NULL; } + break; + + case 112: +#line 570 "dfgparser.y" + { yyval.term = yyvsp[0].term; } + break; + + case 113: +#line 573 "dfgparser.y" + { yyval.term = yyvsp[0].term; } + break; + + case 114: +#line 574 "dfgparser.y" + { dfg_VarStart(); } + break; + + case 115: +#line 575 "dfgparser.y" + { dfg_VarStop(); } + break; + + case 116: +#line 577 "dfgparser.y" + { dfg_VarBacktrack(); + yyval.term = dfg_IGNORE ? NULL : dfg_CreateQuantifier(fol_All(),yyvsp[-5].list,yyvsp[-1].term); + } + break; + + case 117: +#line 583 "dfgparser.y" + { yyval.term = dfg_IGNORE ? NULL : term_Create(fol_Or(), yyvsp[-1].list); } + break; + + case 118: +#line 587 "dfgparser.y" + { yyval.list = dfg_IGNORE ? list_Nil() : list_List(yyvsp[0].term); } + break; + + case 119: +#line 589 "dfgparser.y" + { yyval.list = dfg_IGNORE ? yyvsp[-2].list : list_Nconc(yyvsp[-2].list, list_List(yyvsp[0].term)); } + break; + + case 120: +#line 592 "dfgparser.y" + { yyval.term = yyvsp[0].term; } + break; + + case 121: +#line 594 "dfgparser.y" + { yyval.term = dfg_IGNORE ? yyvsp[-1].term : term_Create(fol_Not(),list_List(yyvsp[-1].term)); } + break; + + case 122: +#line 597 "dfgparser.y" + { yyval.list = list_List(yyvsp[0].term); } + break; + + case 123: +#line 598 "dfgparser.y" + { yyval.list = list_Nconc(yyvsp[-2].list, list_List(yyvsp[0].term)); } + break; + + case 124: +#line 602 "dfgparser.y" + { yyval.term = dfg_IGNORE ? NULL : dfg_AtomCreate(yyvsp[0].string,list_Nil()); } + break; + + case 125: +#line 604 "dfgparser.y" + { yyval.term = dfg_IGNORE ? NULL : term_Create(fol_True(),list_Nil()); } + break; + + case 126: +#line 606 "dfgparser.y" + { yyval.term = dfg_IGNORE ? NULL : term_Create(fol_False(),list_Nil()); } + break; + + case 127: +#line 608 "dfgparser.y" + { yyval.term = dfg_IGNORE ? NULL : term_Create(fol_Equality(),list_Cons(yyvsp[-3].term,list_List(yyvsp[-1].term))); } + break; + + case 128: +#line 610 "dfgparser.y" + { yyval.term = dfg_IGNORE ? NULL : dfg_AtomCreate(yyvsp[-3].string, yyvsp[-1].list); } + break; + + case 136: +#line 636 "dfgparser.y" + { yyval.term = dfg_IGNORE ? NULL : dfg_TermCreate(yyvsp[0].string,list_Nil()); } + break; + + case 137: +#line 638 "dfgparser.y" + { yyval.term = dfg_IGNORE ? NULL : dfg_TermCreate(yyvsp[-3].string, yyvsp[-1].list); } + break; + + case 138: +#line 642 "dfgparser.y" + { yyval.list = dfg_IGNORE ? list_Nil() : list_List(yyvsp[0].term); } + break; + + case 139: +#line 644 "dfgparser.y" + { yyval.list = dfg_IGNORE ? yyvsp[-2].list : list_Nconc(yyvsp[-2].list,list_List(yyvsp[0].term)); } + break; + + case 142: +#line 656 "dfgparser.y" + { if (!string_Equal(yyvsp[-2].string,"SPASS")) { + stack_Push((POINTER)dfg_IGNORE); + dfg_IGNORE = TRUE; + } + } + break; + + case 143: +#line 663 "dfgparser.y" + { if (!string_Equal(yyvsp[-6].string,"SPASS")) + dfg_IGNORE = (BOOL)stack_PopResult(); + string_StringFree(yyvsp[-6].string); + } + break; + + case 145: +#line 672 "dfgparser.y" + { if (!dfg_IGNORE && yyvsp[-11].string!=NULL && yyvsp[-9].term!=NULL && !list_Empty(yyvsp[-4].list)) { + LIST tupel; + RULE Rule = clause_GetOriginFromString(yyvsp[-7].string); + string_StringFree(yyvsp[-7].string); + /* Build a tuple (label,clause,parentlist,split level,origin) */ + tupel = list_Cons((POINTER)yyvsp[-2].number,list_List((POINTER)Rule)); + tupel = list_Cons(yyvsp[-11].string,list_Cons(yyvsp[-9].term,list_Cons(yyvsp[-4].list,tupel))); + dfg_PROOFLIST = list_Cons(tupel, dfg_PROOFLIST); + } else { + /* ignore DNF clauses and clauses with incomplete data */ + if (yyvsp[-11].string != NULL) string_StringFree(yyvsp[-11].string); + if (yyvsp[-9].term != NULL) term_Delete(yyvsp[-9].term); + if (yyvsp[-7].string != NULL) string_StringFree(yyvsp[-7].string); + dfg_DeleteStringList(yyvsp[-4].list); + } + dfg_VarCheck(); + } + break; + + case 146: +#line 692 "dfgparser.y" + { yyval.list = (dfg_IGNORE||yyvsp[0].string==NULL) ? list_Nil() : list_List(yyvsp[0].string); } + break; + + case 147: +#line 694 "dfgparser.y" + { yyval.list = (dfg_IGNORE||yyvsp[0].string==NULL) ? yyvsp[-2].list : list_Nconc(yyvsp[-2].list, list_List(yyvsp[0].string)); } + break; + + case 148: +#line 698 "dfgparser.y" + { yyval.number = 0; } + break; + + case 149: +#line 699 "dfgparser.y" + { yyval.number = yyvsp[-1].number; } + break; + + case 150: +#line 703 "dfgparser.y" + { if (!dfg_IGNORE && yyvsp[-2].string!=NULL && yyvsp[0].string!=NULL && string_Equal(yyvsp[-2].string,"splitlevel")) + string_StringToInt(yyvsp[0].string, TRUE, &yyval.number); + else + yyval.number = 0; + if (yyvsp[-2].string != NULL) string_StringFree(yyvsp[-2].string); + if (yyvsp[0].string != NULL) string_StringFree(yyvsp[0].string); + } + break; + + case 151: +#line 711 "dfgparser.y" + { if (!dfg_IGNORE && yyvsp[-2].string!=NULL && yyvsp[0].string!=NULL && string_Equal(yyvsp[-2].string,"splitlevel")) + string_StringToInt(yyvsp[0].string, TRUE, &yyval.number); + else + yyval.number = yyvsp[-4].number; + if (yyvsp[-2].string != NULL) string_StringFree(yyvsp[-2].string); + if (yyvsp[0].string != NULL) string_StringFree(yyvsp[0].string); + } + break; + + case 152: +#line 721 "dfgparser.y" + { stack_Push((POINTER) dfg_IGNORE); dfg_IGNORE = TRUE; } + break; + + case 153: +#line 723 "dfgparser.y" + { dfg_IGNORE = (BOOL) stack_PopResult(); + if (yyvsp[0].bool) { + if (yyvsp[-2].string != NULL) string_StringFree(yyvsp[-2].string); + yyval.string = NULL; + } else + yyval.string = yyvsp[-2].string; + } + break; + + case 154: +#line 732 "dfgparser.y" + { yyval.string = yyvsp[0].string; } + break; + + case 155: +#line 733 "dfgparser.y" + { yyval.string = NULL; } + break; + + case 156: +#line 734 "dfgparser.y" + { yyval.string = NULL; } + break; + + case 157: +#line 735 "dfgparser.y" + { yyval.string = NULL; } + break; + + case 158: +#line 736 "dfgparser.y" + { yyval.string = NULL; } + break; + + case 159: +#line 737 "dfgparser.y" + { yyval.string = NULL; } + break; + + case 160: +#line 738 "dfgparser.y" + { yyval.string = NULL; } + break; + + case 161: +#line 739 "dfgparser.y" + { yyval.string = NULL; } + break; + + case 162: +#line 740 "dfgparser.y" + { yyval.string = NULL; } + break; + + case 163: +#line 743 "dfgparser.y" + { yyval.bool = FALSE; } + break; + + case 164: +#line 744 "dfgparser.y" + { yyval.bool = TRUE; } + break; + + case 165: +#line 745 "dfgparser.y" + { yyval.bool = TRUE; } + break; + + case 166: +#line 748 "dfgparser.y" + { yyval.term = yyvsp[0].term; } + break; + + case 167: +#line 749 "dfgparser.y" + { yyval.term = NULL; } + break; + + case 170: +#line 761 "dfgparser.y" + { dfg_VarStart(); } + break; + + case 171: +#line 762 "dfgparser.y" + { + dfg_VarStop(); + dfg_VarBacktrack(); + dfg_VarCheck(); } + break; + + case 173: +#line 769 "dfgparser.y" + { dfg_TERMLIST = list_Nconc(dfg_TERMLIST, list_List(yyvsp[-1].term)); } + break; + + case 177: +#line 781 "dfgparser.y" + { if (string_Equal(yyvsp[0].string,"SPASS")) + dfg_IGNORETEXT = FALSE; + string_StringFree(yyvsp[0].string); + } + break; + + case 178: +#line 786 "dfgparser.y" + { dfg_IGNORETEXT = TRUE; } + break; + + case 179: +#line 789 "dfgparser.y" + { /* no SPASS flags */ + string_StringFree(yyvsp[0].string); + } + break; + + case 184: +#line 801 "dfgparser.y" + { SYMBOL s; + for ( ; !list_Empty(yyvsp[-1].list); yyvsp[-1].list = list_Pop(yyvsp[-1].list)) { + s = symbol_Lookup(list_Car(yyvsp[-1].list)); + if (s == 0) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Undefined symbol %s", list_Car(yyvsp[-1].list)); + misc_UserErrorReport(" in DomPred list.\n"); + misc_FinishUserErrorReport(); + } + if (!symbol_IsPredicate(s)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Symbol %s isn't a predicate", list_Car(yyvsp[-1].list)); + misc_UserErrorReport(" in DomPred list.\n"); + misc_FinishUserErrorReport(); + } + string_StringFree(list_Car(yyvsp[-1].list)); + symbol_AddProperty(s, DOMPRED); + } + } + break; + + case 185: +#line 821 "dfgparser.y" + { int flag = flag_Id(yyvsp[-3].string); + if (flag == -1) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Found unknown flag %s", yyvsp[-3].string); + misc_FinishUserErrorReport(); + } + string_StringFree(yyvsp[-3].string); + flag_SetFlagValue(dfg_FLAGS, flag, yyvsp[-1].number); + } + break; + + case 188: +#line 837 "dfgparser.y" + { SYMBOL s = symbol_Lookup(yyvsp[0].string); + if (s == 0) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Undefined symbol %s ", yyvsp[0].string); + misc_UserErrorReport(" in precedence list.\n"); + misc_FinishUserErrorReport(); + } + string_StringFree(yyvsp[0].string); + symbol_SetIncreasedOrdering(dfg_PRECEDENCE, s); + dfg_USERPRECEDENCE = list_Cons((POINTER)s, dfg_USERPRECEDENCE); + } + break; + + case 189: +#line 849 "dfgparser.y" + { SYMBOL s = symbol_Lookup(yyvsp[-4].string); + if (s == 0) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Undefined symbol %s", yyvsp[-4].string); + misc_UserErrorReport("in precedence list.\n"); + misc_FinishUserErrorReport(); + } + string_StringFree(yyvsp[-4].string); + symbol_SetIncreasedOrdering(dfg_PRECEDENCE, s); + dfg_USERPRECEDENCE = list_Cons((POINTER)s, dfg_USERPRECEDENCE); + symbol_SetWeight(s, yyvsp[-2].number); + if (yyvsp[-1].property != 0) + symbol_AddProperty(s, yyvsp[-1].property); + } + break; + + case 190: +#line 865 "dfgparser.y" + { yyval.property = 0; /* left */ } + break; + + case 191: +#line 867 "dfgparser.y" + { if (yyvsp[0].string[1] != '\0' || + (yyvsp[0].string[0]!='l' && yyvsp[0].string[0]!='m' && yyvsp[0].string[0]!='r')) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Invalid symbol status %s", yyvsp[0].string); + misc_UserErrorReport(" in precedence list."); + misc_FinishUserErrorReport(); + } + switch (yyvsp[0].string[0]) { + case 'm': yyval.property = ORDMUL; break; + case 'r': yyval.property = ORDRIGHT; break; + default: yyval.property = 0; + } + string_StringFree(yyvsp[0].string); + } + break; + + case 194: +#line 888 "dfgparser.y" + { dfg_DeleteStringList(yyvsp[-2].list); } + break; + + case 195: +#line 891 "dfgparser.y" + { yyval.list = list_List(yyvsp[0].string); } + break; + + case 196: +#line 892 "dfgparser.y" + { yyval.list = list_Nconc(yyvsp[-2].list, list_List(yyvsp[0].string)); } + break; + + + } + +/* Line 1016 of /opt/gnu//share/bison/yacc.c. */ +#line 2471 "dfgparser.c" + + yyvsp -= yylen; + yyssp -= yylen; + + +#if YYDEBUG + if (yydebug) + { + short *yyssp1 = yyss - 1; + YYFPRINTF (stderr, "state stack now"); + while (yyssp1 != yyssp) + YYFPRINTF (stderr, " %d", *++yyssp1); + YYFPRINTF (stderr, "\n"); + } +#endif + + *++yyvsp = yyval; + + + /* Now `shift' the result of the reduction. Determine what state + that goes to, based on the state we popped back to and the rule + number reduced by. */ + + yyn = yyr1[yyn]; + + yystate = yypgoto[yyn - YYNTOKENS] + *yyssp; + if (0 <= yystate && yystate <= YYLAST && yycheck[yystate] == *yyssp) + yystate = yytable[yystate]; + else + yystate = yydefgoto[yyn - YYNTOKENS]; + + goto yynewstate; + + +/*------------------------------------. +| yyerrlab -- here on detecting error | +`------------------------------------*/ +yyerrlab: + /* If not already recovering from an error, report this error. */ + if (!yyerrstatus) + { + ++yynerrs; +#if YYERROR_VERBOSE + yyn = yypact[yystate]; + + if (YYPACT_NINF < yyn && yyn < YYLAST) + { + YYSIZE_T yysize = 0; + int yytype = YYTRANSLATE (yychar); + char *yymsg; + int yyx, yycount; + + yycount = 0; + /* Start YYX at -YYN if negative to avoid negative indexes in + YYCHECK. */ + for (yyx = yyn < 0 ? -yyn : 0; + yyx < (int) (sizeof (yytname) / sizeof (char *)); yyx++) + if (yycheck[yyx + yyn] == yyx && yyx != YYTERROR) + yysize += yystrlen (yytname[yyx]) + 15, yycount++; + yysize += yystrlen ("parse error, unexpected ") + 1; + yysize += yystrlen (yytname[yytype]); + yymsg = (char *) YYSTACK_ALLOC (yysize); + if (yymsg != 0) + { + char *yyp = yystpcpy (yymsg, "parse error, unexpected "); + yyp = yystpcpy (yyp, yytname[yytype]); + + if (yycount < 5) + { + yycount = 0; + for (yyx = yyn < 0 ? -yyn : 0; + yyx < (int) (sizeof (yytname) / sizeof (char *)); + yyx++) + if (yycheck[yyx + yyn] == yyx && yyx != YYTERROR) + { + const char *yyq = ! yycount ? ", expecting " : " or "; + yyp = yystpcpy (yyp, yyq); + yyp = yystpcpy (yyp, yytname[yyx]); + yycount++; + } + } + yyerror (yymsg); + YYSTACK_FREE (yymsg); + } + else + yyerror ("parse error; also virtual memory exhausted"); + } + else +#endif /* YYERROR_VERBOSE */ + yyerror ("parse error"); + } + goto yyerrlab1; + + +/*----------------------------------------------------. +| yyerrlab1 -- error raised explicitly by an action. | +`----------------------------------------------------*/ +yyerrlab1: + if (yyerrstatus == 3) + { + /* If just tried and failed to reuse lookahead token after an + error, discard it. */ + + /* Return failure if at end of input. */ + if (yychar == YYEOF) + { + /* Pop the error token. */ + YYPOPSTACK; + /* Pop the rest of the stack. */ + while (yyssp > yyss) + { + YYDPRINTF ((stderr, "Error: popping ")); + YYDSYMPRINT ((stderr, + yystos[*yyssp], + *yyvsp)); + YYDPRINTF ((stderr, "\n")); + yydestruct (yystos[*yyssp], *yyvsp); + YYPOPSTACK; + } + YYABORT; + } + + YYDPRINTF ((stderr, "Discarding token %d (%s).\n", + yychar, yytname[yychar1])); + yydestruct (yychar1, yylval); + yychar = YYEMPTY; + } + + /* Else will try to reuse lookahead token after shifting the error + token. */ + + yyerrstatus = 3; /* Each real token shifted decrements this. */ + + for (;;) + { + yyn = yypact[yystate]; + if (yyn != YYPACT_NINF) + { + yyn += YYTERROR; + if (0 <= yyn && yyn <= YYLAST && yycheck[yyn] == YYTERROR) + { + yyn = yytable[yyn]; + if (0 < yyn) + break; + } + } + + /* Pop the current state because it cannot handle the error token. */ + if (yyssp == yyss) + YYABORT; + + YYDPRINTF ((stderr, "Error: popping ")); + YYDSYMPRINT ((stderr, + yystos[*yyssp], *yyvsp)); + YYDPRINTF ((stderr, "\n")); + + yydestruct (yystos[yystate], *yyvsp); + yyvsp--; + yystate = *--yyssp; + + +#if YYDEBUG + if (yydebug) + { + short *yyssp1 = yyss - 1; + YYFPRINTF (stderr, "Error: state stack now"); + while (yyssp1 != yyssp) + YYFPRINTF (stderr, " %d", *++yyssp1); + YYFPRINTF (stderr, "\n"); + } +#endif + } + + if (yyn == YYFINAL) + YYACCEPT; + + YYDPRINTF ((stderr, "Shifting error token, ")); + + *++yyvsp = yylval; + + + yystate = yyn; + goto yynewstate; + + +/*-------------------------------------. +| yyacceptlab -- YYACCEPT comes here. | +`-------------------------------------*/ +yyacceptlab: + yyresult = 0; + goto yyreturn; + +/*-----------------------------------. +| yyabortlab -- YYABORT comes here. | +`-----------------------------------*/ +yyabortlab: + yyresult = 1; + goto yyreturn; + +#ifndef yyoverflow +/*----------------------------------------------. +| yyoverflowlab -- parser overflow comes here. | +`----------------------------------------------*/ +yyoverflowlab: + yyerror ("parser stack overflow"); + yyresult = 2; + /* Fall through. */ +#endif + +yyreturn: +#ifndef yyoverflow + if (yyss != yyssa) + YYSTACK_FREE (yyss); +#endif + return yyresult; +} + + +#line 895 "dfgparser.y" + + +void yyerror(const char *s) +{ + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Line %i: %s\n", dfg_LINENUMBER, s); + misc_FinishUserErrorReport(); +} + +static void dfg_Init(FILE* Input, FLAGSTORE Flags, PRECEDENCE Precedence) +/************************************************************** + INPUT: The input file stream for the parser, a flag store and + a precedence. + RETURNS: Nothing. + EFFECT: The parser and scanner are initialized. + The parser will use the flag store and the precedence + to memorize the settings from the input file. +***************************************************************/ +{ + extern FILE* dfg_in; /* declared in dfgscanner */ + + dfg_in = Input; + dfg_LINENUMBER = 1; + dfg_IGNORETEXT = TRUE; + dfg_AXIOMLIST = list_Nil(); + dfg_CONJECLIST = list_Nil(); + dfg_SORTDECLLIST = list_Nil(); + dfg_USERPRECEDENCE = list_Nil(); + dfg_AXCLAUSES = list_Nil(); + dfg_CONCLAUSES = list_Nil(); + dfg_PROOFLIST = list_Nil(); + dfg_TERMLIST = list_Nil(); + dfg_SYMBOLLIST = list_Nil(); + dfg_VARLIST = list_Nil(); + dfg_VARDECL = FALSE; + dfg_IGNORE = FALSE; + dfg_FLAGS = Flags; + dfg_PRECEDENCE = Precedence; + dfg_DESC.name = (char*) NULL; + dfg_DESC.author = (char*) NULL; + dfg_DESC.version = (char*) NULL; + dfg_DESC.logic = (char*) NULL; + dfg_DESC.status = DFG_UNKNOWNSTATE; + dfg_DESC.description = (char*) NULL; + dfg_DESC.date = (char*) NULL; +} + + +void dfg_Free(void) +/************************************************************** + INPUT: None. + RETURNS: Nothing. + EFFECT: Frees memory used by the problem description. +***************************************************************/ +{ + if (dfg_DESC.name != NULL) + string_StringFree(dfg_DESC.name); + if (dfg_DESC.author != NULL) + string_StringFree(dfg_DESC.author); + if (dfg_DESC.version != NULL) + string_StringFree(dfg_DESC.version); + if (dfg_DESC.logic != NULL) + string_StringFree(dfg_DESC.logic); + if (dfg_DESC.description != NULL) + string_StringFree(dfg_DESC.description); + if(dfg_DESC.date != NULL) + string_StringFree(dfg_DESC.date); +} + +const char* dfg_ProblemName(void) +/************************************************************** + INPUT: None. + RETURNS: The problem's name from the description section. +***************************************************************/ +{ + return dfg_DESC.name; +} + +const char* dfg_ProblemAuthor(void) +/************************************************************** + INPUT: None. + RETURNS: The problem's author from the description section. +***************************************************************/ +{ + return dfg_DESC.author; +} + +const char* dfg_ProblemVersion(void) +/************************************************************** + INPUT: None. + RETURNS: The problem's version from the description section. +***************************************************************/ +{ + return dfg_DESC.version; +} + +const char* dfg_ProblemLogic(void) +/************************************************************** + INPUT: None. + RETURNS: The problem's logic from the description section. +***************************************************************/ +{ + return dfg_DESC.logic; +} + +DFG_STATE dfg_ProblemStatus(void) +/************************************************************** + INPUT: None. + RETURNS: The problem's status from the description section. +***************************************************************/ +{ + return dfg_DESC.status; +} + +const char* dfg_ProblemStatusString(void) +/************************************************************** + INPUT: None. + RETURNS: The string representation of the problem's status. +***************************************************************/ +{ + const char* result = ""; + + switch (dfg_DESC.status) { + case DFG_SATISFIABLE: + result = "satisfiable"; break; + case DFG_UNSATISFIABLE: + result = "unsatisfiable"; break; + case DFG_UNKNOWNSTATE: + result = "unknown"; break; + default: + misc_StartErrorReport(); + misc_ErrorReport("\n In dfg_ProblemStatusString: Invalid status.\n"); + misc_FinishErrorReport(); + } + return result; +} + +const char* dfg_ProblemDescription(void) +/************************************************************** + INPUT: None. + RETURNS: The problem's description from the description section. +***************************************************************/ +{ + return dfg_DESC.description; +} + +const char* dfg_ProblemDate(void) +/************************************************************** + INPUT: None. + RETURNS: The problem's date from the description section. +***************************************************************/ +{ + return dfg_DESC.date; +} + +void dfg_FPrintDescription(FILE* File) +/************************************************************** + INPUT: A file stream. + RETURNS: Nothing. + EFFECT: The description section from the input file + is printed to 'File'. You must call the parser first + before calling this function. +***************************************************************/ +{ + fputs("list_of_descriptions.\n name(", File); + if (dfg_DESC.name != NULL) + fputs(dfg_DESC.name, File); + else + fputs("{* *}", File); + fputs(").\n author(", File); + if (dfg_DESC.author != NULL) + fputs(dfg_DESC.author, File); + else + fputs("{* *}", File); + fputs(").\n", File); + if (dfg_DESC.version != NULL) { + fputs(" version(", File); + fputs(dfg_DESC.version, File); + fputs(").\n", File); + } + if (dfg_DESC.logic != NULL) { + fputs(" logic(", File); + fputs(dfg_DESC.logic, File); + fputs(").\n", File); + } + fputs(" status(", File); + fputs(dfg_ProblemStatusString(), File); + fputs(").\n description(", File); + if (dfg_DESC.description != NULL) + fputs(dfg_DESC.description, File); + else + fputs("{* *}", File); + fputs(").\n", File); + if (dfg_DESC.date != NULL) { + fputs(" date(", File); + fputs(dfg_DESC.date, File); + fputs(").\n", File); + } + fputs("end_of_list.", File); +} + + +LIST dfg_DFGParser(FILE* File, FLAGSTORE Flags, PRECEDENCE Precedence, + LIST* Axioms, LIST* Conjectures, LIST* SortDecl, + LIST* UserDefinedPrecedence) +/************************************************************** + INPUT: The input file containing clauses or formulae in DFG syntax, + a flag store and a precedence used to memorize settings + from the file. + Axioms, Conjectures, SortDecl and UserDefinedPrecedence are + pointers to lists used as return values. + RETURNS: The list of clauses from File. + EFFECT: Reads formulae and clauses from the input file. + The axioms, conjectures, sort declarations and user-defined + precedences are appended to the respective lists, the lists + are not deleted! + All lists except the clause list contain pairs + (label, term), where