blob: 3691271b53b6548d9cb773130c6dadaf2ea40cf0 [file] [log] [blame]
/* 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 <ctype.h>
#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 <stdlib.h> /* 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 <stddef.h> /* 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 <stdio.h> /* 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; }