Google Git
Sign in
fuchsia / third_party / github.com / llvm / llvm-test-suite / 315e03c706ca8847bcc6f17f5c1a7d95d674c054 / . / MultiSource / Applications / SPASS / dfgparser.c
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; }
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 <label> may be NULL, if no
label was specified for that term.
<UserDefinedPrecedence> contains symbols sorted by decreasing
precedence. This list will only be changed, if the precedence
is explicitly defined in the input file. This can be done
by the 'set_precedence' flag in the SPASS settings list in
the DFG input file.
CAUTION: The weight of the clauses is not correct and the literals
are not oriented!
***************************************************************/
{
LIST scan, tupel;
TERM clauseTerm;
NAT bottom;
dfg_Init(File, Flags, Precedence); /* Initialize the parser and scanner */
bottom = stack_Bottom();
dfg_parse(); /* Invoke the parser */
#ifdef CHECK
if (!stack_Empty(bottom)) {
misc_StartErrorReport();
misc_ErrorReport("\n In dfg_DFGParser: Stack not empty!\n");
misc_FinishErrorReport();
}
#endif
dfg_SymCleanUp();
/* Remove clause labels and create clauses from the terms */
for (scan = dfg_AXCLAUSES; !list_Empty(scan); scan = list_Cdr(scan)) {
tupel = list_Car(scan);
clauseTerm = list_PairSecond(tupel);
list_Rplaca(scan, dfg_CreateClauseFromTerm(clauseTerm,TRUE, Flags, Precedence));
if (list_PairFirst(tupel) != NULL) /* Label is defined */
string_StringFree(list_PairFirst(tupel)); /* Delete the label */
list_PairFree(tupel);
}
/* Since dfg_CreateClauseFromTerm() returns NULL for trivial tautologies */
/* we now delete those NULL pointers from the clause list. */
dfg_AXCLAUSES = list_PointerDeleteElement(dfg_AXCLAUSES, NULL);
for (scan = dfg_CONCLAUSES; !list_Empty(scan); scan = list_Cdr(scan)) {
tupel = list_Car(scan);
clauseTerm = list_PairSecond(tupel);
list_Rplaca(scan, dfg_CreateClauseFromTerm(clauseTerm,FALSE, Flags, Precedence));
if (list_PairFirst(tupel) != NULL) /* Label is defined */
string_StringFree(list_PairFirst(tupel)); /* Delete the label */
list_PairFree(tupel);
}
/* Since dfg_CreateClauseFromTerm() returns NULL for trivial tautologies */
/* we now delete those NULL pointers from the clause list. */
dfg_CONCLAUSES = list_PointerDeleteElement(dfg_CONCLAUSES, NULL);
/* Delete the proof list */
dfg_DeleteProofList(dfg_PROOFLIST);
/* Delete the list_of_terms, since it'll be ignored */
term_DeleteTermList(dfg_TERMLIST);
scan = list_Nconc(dfg_AXCLAUSES, dfg_CONCLAUSES);
*Axioms = list_Nconc(*Axioms, dfg_AXIOMLIST);
*Conjectures = list_Nconc(*Conjectures, dfg_CONJECLIST);
*SortDecl = list_Nconc(*SortDecl, dfg_SORTDECLLIST);
list_NReverse(dfg_USERPRECEDENCE);
*UserDefinedPrecedence = list_Nconc(*UserDefinedPrecedence, dfg_USERPRECEDENCE);
return scan;
}
LIST dfg_ProofParser(FILE* File, FLAGSTORE Flags, PRECEDENCE Precedence)
/**************************************************************
INPUT: The input file containing clauses in DFG syntax,
a flag store and a precedence used to memorize settings
from the file.
RETURNS: A list of tuples (label,clause,justificationlist,splitlevel,origin)
representing a proof.
EFFECT: Reads inputs clauses with labels and the proof lists
from the input file.
The elements of the list are lists with five items.
1. the label (a string) of a clause,
2. the clause in TERM format,
3. the list of justification labels (strings, too),
4. the split level of the clause,
5. the origin of the clause (RULE struct from clause.h).
Note that the justification list is empty for input
clauses.
***************************************************************/
{
LIST scan, tupel;
TERM term;
NAT bottom;
dfg_Init(File, Flags, Precedence); /* Initialize the parser and scanner */
bottom = stack_Bottom();
dfg_parse(); /* Invoke the parser */
#ifdef CHECK
if (!stack_Empty(bottom)) {
misc_StartErrorReport();
misc_ErrorReport("\n In dfg_ProofParser: Stack not empty!\n");
misc_FinishErrorReport();
}
#endif
dfg_SymCleanUp();
/* Build the union of axiom and conjecture clauses */
dfg_AXCLAUSES = list_Nconc(dfg_AXCLAUSES, dfg_CONCLAUSES);
dfg_CONCLAUSES = list_Nil();
for (scan = dfg_AXCLAUSES; !list_Empty(scan); scan = list_Cdr(scan)) {
tupel = list_Car(scan);
term = list_PairSecond(tupel);
if (list_PairFirst(tupel) == NULL) {
/* Ignore input clauses without label */
term_Delete(term);
list_PairFree(tupel);
list_Rplaca(scan, NULL);
} else
/* Expand the pair to a tuple */
/* (label,clause,justificationlist, split level, origin) */
/* For input clauses the justificationlist is empty. */
/* Input clauses have split level 0. */
list_Rplacd(tupel, list_Cons(term,list_Cons(list_Nil(),list_Cons(0, list_List((POINTER)INPUT)))));
}
/* Now delete the list items without labels */
dfg_AXCLAUSES = list_PointerDeleteElement(dfg_AXCLAUSES, NULL);
/* Delete the formula lists */
dfg_DeleteFormulaPairList(dfg_AXIOMLIST);
dfg_DeleteFormulaPairList(dfg_CONJECLIST);
/* Delete the list of sort declarations */
dfg_DeleteFormulaPairList(dfg_SORTDECLLIST);
/* Delete the list_of_terms, since it'll be ignored */
term_DeleteTermList(dfg_TERMLIST);
/* Finally append the proof list to the list of input clauses with labels */
dfg_PROOFLIST = list_NReverse(dfg_PROOFLIST);
dfg_AXCLAUSES = list_Nconc(dfg_AXCLAUSES, dfg_PROOFLIST);
return dfg_AXCLAUSES;
}
LIST dfg_TermParser(FILE* File, FLAGSTORE Flags, PRECEDENCE Precedence)
/**************************************************************
INPUT: The input file containing a list of terms in DFG syntax,
a flag store and a precedence used to memorize settings
from the file.
RETURNS: The list of terms from <File>.
EFFECT: Reads terms from the list_of_terms from the input file.
***************************************************************/
{
NAT bottom;
dfg_Init(File, Flags, Precedence); /* Initialize the parser and scanner */
bottom = stack_Bottom();
dfg_parse(); /* Invoke the parser */
#ifdef CHECK
if (!stack_Empty(bottom)) {
misc_StartErrorReport();
misc_ErrorReport("\n In dfg_TermParser: Stack not empty!\n");
misc_FinishErrorReport();
}
#endif
dfg_SymCleanUp();
/* Delete the clause lists */
dfg_DeleteFormulaPairList(dfg_AXCLAUSES);
dfg_DeleteFormulaPairList(dfg_CONCLAUSES);
/* Delete the formula lists */
dfg_DeleteFormulaPairList(dfg_AXIOMLIST);
dfg_DeleteFormulaPairList(dfg_CONJECLIST);
/* Delete the proof list */
dfg_DeleteProofList(dfg_PROOFLIST);
/* Delete the list of sort declarations */
dfg_DeleteFormulaPairList(dfg_SORTDECLLIST);
return dfg_TERMLIST;
}
void dfg_DeleteFormulaPairList(LIST FormulaPairs)
/**************************************************************
INPUT: A list of pairs (label, formula).
RETURNS: Nothing.
EFFECT: The list and the pairs with their strings and terms
are completely deleted.
***************************************************************/
{
LIST pair;
for ( ; !list_Empty(FormulaPairs); FormulaPairs = list_Pop(FormulaPairs)) {
pair = list_Car(FormulaPairs); /* (label, term) */
term_Delete(list_PairSecond(pair));
if (list_PairFirst(pair) != NULL)
string_StringFree(list_PairFirst(pair)); /* Free the label */
list_PairFree(pair);
}
}
void dfg_StripLabelsFromList(LIST FormulaPairs)
/**************************************************************
INPUT: A list of pairs (label, formula).
RETURNS: Nothing.
EFFECT: The pairs are replaced by the respective formula
and the pairs with their label strings are deleted.
***************************************************************/
{
LIST pair, scan;
for (scan = FormulaPairs; !list_Empty(scan); scan = list_Cdr(scan)) {
pair = list_Car(scan); /* (label, term) */
list_Rplaca(scan, list_PairSecond(pair));
if (list_PairFirst(pair) != NULL)
string_StringFree(list_PairFirst(pair)); /* Free the label */
list_PairFree(pair);
}
}
void dfg_DeleteProofList(LIST Proof)
/**************************************************************
INPUT: A list of tuples (label, term, justificationlist, split level).
RETURNS: Nothing.
EFFECT: All memory used by the proof list is freed.
The labels must NOT be NULL entries!
***************************************************************/
{
/* Delete the proof list */
for ( ; !list_Empty(Proof); Proof = list_Pop(Proof)) {
LIST tupel = list_Car(Proof);
string_StringFree(list_First(tupel));
term_Delete(list_Second(tupel));
dfg_DeleteStringList(list_Third(tupel));
list_Delete(tupel);
}
}
/**************************************************************/
/* Static Functions */
/**************************************************************/
static void dfg_SymbolDecl(int SymbolType, char* Name, int Arity)
/**************************************************************
INPUT: The type of a symbol, the name, and the arity.
RETURNS: Nothing.
EFFECT: This function handles the declaration of symbols.
If <Arity> is -2, it means that the arity of the symbol
was not specified, if it is -1 the symbol is declared
with arbitrary arity. User defined symbols with arbitrary
arity are not allowed.
The <Name> is deleted.
***************************************************************/
{
NAT arity, length;
SYMBOL symbol;
switch (Arity) {
case -2: /* not specified */
arity = 0;
break;
case -1:
misc_StartUserErrorReport();
misc_UserErrorReport("\n Line %u: symbols with arbitrary arity are not allowed.\n",
dfg_LINENUMBER);
misc_FinishUserErrorReport();
default:
arity = Arity;
}
/* Pay attention to the maximum symbol name length */
length = strlen(Name);
if (length >= symbol__SYMBOLMAXLEN)
Name[symbol__SYMBOLMAXLEN-1] = '\0';
/* Check if this symbol was declared earlier */
symbol = symbol_Lookup(Name);
if (symbol != 0) {
/* Symbol was declared before */
/* Check if the old and new symbol type are equal */
if ((SymbolType == DFG_FUNC && !symbol_IsFunction(symbol)) ||
(SymbolType == DFG_PRDICAT && !symbol_IsPredicate(symbol)) ||
((SymbolType == DFG_OPERAT || SymbolType == DFG_QUANTIF) &&
!symbol_IsJunctor(symbol))) {
misc_StartUserErrorReport();
misc_UserErrorReport("\n Line %u: symbol %s was already declared as ",
dfg_LINENUMBER, Name);
switch (symbol_Type(symbol)) {
case symbol_CONSTANT:
case symbol_FUNCTION:
misc_UserErrorReport("function.\n"); break;
case symbol_PREDICATE:
misc_UserErrorReport("predicate.\n"); break;
case symbol_JUNCTOR:
misc_UserErrorReport("junctor.\n"); break;
default:
misc_UserErrorReport("unknown type.\n");
}
misc_FinishUserErrorReport();
}
/* Now check the old and new arity if specified */
if (Arity != -2 && Arity != symbol_Arity(symbol)) {
misc_StartUserErrorReport();
misc_UserErrorReport("\n Line %u: symbol %s was already declared with arity %d\n",
dfg_LINENUMBER, Name, symbol_Arity(symbol));
misc_FinishUserErrorReport();
}
} else {
/* Symbol was not declared before */
switch (SymbolType) {
case DFG_FUNC:
symbol = symbol_CreateFunction(Name, arity, symbol_STATLEX,dfg_PRECEDENCE);
break;
case DFG_PRDICAT:
symbol = symbol_CreatePredicate(Name, arity,symbol_STATLEX,dfg_PRECEDENCE);
break;
default:
symbol = symbol_CreateJunctor(Name, arity, symbol_STATLEX, dfg_PRECEDENCE);
}
if (Arity == -2)
/* Arity wasn't specified so check the arity for each occurrence */
dfg_SymAdd(symbol);
}
if (length >= symbol__SYMBOLMAXLEN) {
/* To avoid a memory error restore the old string length */
Name[symbol__SYMBOLMAXLEN-1] = ' '; /* Something != '\0' */
}
string_StringFree(Name); /* Name was copied */
}
static SYMBOL dfg_Symbol(char* Name, NAT Arity)
/**************************************************************
INPUT: The name of a symbol and the actual arity of the symbol.
RETURNS: The corresponding SYMBOL.
EFFECT: This function checks if the <Name> was declared as
symbol or variable. If not, an error message is printed
to stderr.
The <Name> is deleted.
***************************************************************/
{
SYMBOL symbol;
char old;
NAT length;
old = ' '; /* Just to avoid a compiler warning */
/* Pay attention to the maximum symbol name length */
length = strlen(Name);
if (length >= symbol__SYMBOLMAXLEN) {
old = Name[symbol__SYMBOLMAXLEN-1];
Name[symbol__SYMBOLMAXLEN-1] = '\0';
}
symbol = symbol_Lookup(Name);
if (length >= symbol__SYMBOLMAXLEN) {
/* To avoid a memory error restore the old string */
Name[symbol__SYMBOLMAXLEN-1] = old;
}
if (symbol != 0) {
string_StringFree(Name);
dfg_SymCheck(symbol, Arity); /* Check the arity */
} else {
/* Variable */
if (Arity > 0) {
misc_StartUserErrorReport();
misc_UserErrorReport("\n Line %d: Undefined symbol %s.\n",dfg_LINENUMBER,Name);
misc_FinishUserErrorReport();
}
symbol = dfg_VarLookup(Name);
}
return symbol;
}
TERM dfg_CreateQuantifier(SYMBOL Symbol, LIST VarTermList, TERM Term)
/**************************************************************
INPUT: A quantifier symbol, a list possibly containing sorts,
and a term.
RETURNS: The created quantifier term..
***************************************************************/
{
LIST varlist, sortlist, scan;
TERM helpterm;
/* First collect the variable symbols in varlist and the sorts in sortlist */
varlist = sortlist = list_Nil();
for ( ; !list_Empty(VarTermList); VarTermList = list_Pop(VarTermList)) {
helpterm = list_Car(VarTermList);
if (term_IsVariable(helpterm)) {
varlist = list_Nconc(varlist, list_List((POINTER)term_TopSymbol(helpterm)));
term_Delete(helpterm);
} else {
SYMBOL var = term_TopSymbol(term_FirstArgument(helpterm));
varlist = list_Nconc(varlist, list_List((POINTER)var));
sortlist = list_Nconc(sortlist, list_List(helpterm));
}
}
varlist = list_PointerDeleteDuplicates(varlist);
/* Now create terms from the variables */
for (scan = varlist; !list_Empty(scan); scan = list_Cdr(scan))
list_Rplaca(scan, term_Create((SYMBOL)list_Car(scan), list_Nil()));
if (!list_Empty(sortlist)) {
if (symbol_Equal(fol_All(), Symbol)) {
/* The conjunction of all sortterms implies the Term */
if (symbol_Equal(fol_Or(), term_TopSymbol(Term))) {
/* Special treatment if <Term> is a term with "or" like */
/* in clauses: add all sort terms negated to the args */
/* of the "or" */
for (scan = sortlist; !list_Empty(scan); scan = list_Cdr(scan))
/* Negate the sort terms */
list_Rplaca(scan, term_Create(fol_Not(), list_List(list_Car(scan))));
sortlist = list_Nconc(sortlist, term_ArgumentList(Term));
term_RplacArgumentList(Term, sortlist);
} else {
/* No "or" term, so build the implication term */
if (list_Empty(list_Cdr(sortlist))) {
/* Only one sort term */
list_Rplacd(sortlist, list_List(Term));
Term = term_Create(fol_Implies(), sortlist);
} else {
/* More than one sort term */
helpterm = term_Create(fol_And(), sortlist);
Term = term_Create(fol_Implies(), list_Cons(helpterm, list_List(Term)));
}
}
} else if (symbol_Equal(fol_Exist(), Symbol)) {
/* Quantify the conjunction of all sort terms and <Term> */
if (symbol_Equal(fol_And(), term_TopSymbol(Term))) {
/* Special treatment if <Term> has an "and" as top symbol: */
/* just add the sort terms to the args of the "and". */
sortlist = list_Nconc(sortlist, term_ArgumentList(Term));
term_RplacArgumentList(Term, sortlist);
} else {
sortlist = list_Nconc(sortlist, list_List(Term));
Term = term_Create(fol_And(), sortlist);
}
}
}
helpterm = fol_CreateQuantifier(Symbol, varlist, list_List(Term));
return helpterm;
}
CLAUSE dfg_CreateClauseFromTerm(TERM Clause, BOOL IsAxiom, FLAGSTORE Flags,
PRECEDENCE Precedence)
/**************************************************************
INPUT: A clause term, a boolean value, a flag store and a precedence.
RETURNS: The clause term converted to a CLAUSE or NULL if the
clause is a trivial tautology (the clause contains
the literal "true" or "not(false)" ).
EFFECT: This function converts a clause stored as term into an
EARL clause structure.
If 'IsAxiom' is TRUE the clause is treated as axiom
clause else as conjecture clause.
The function deletes the literals "false" and "not(true)"
if they occur in <Clause>.
The contents of the flag store and the precedence are changed
because the parser read flag and precedence settings from
MEMORY: The clause term is deleted.
***************************************************************/
{
LIST literals, scan;
TERM literal;
CLAUSE result;
if (term_TopSymbol(Clause) == fol_All()) {
/* Remove and free the quantifier and the OR term */
literals = term_ArgumentList(term_SecondArgument(Clause));
term_RplacArgumentList(term_SecondArgument(Clause), list_Nil());
} else {
/* Remove and free the OR term */
literals = term_ArgumentList(Clause);
term_RplacArgumentList(Clause, list_Nil());
}
term_Delete(Clause);
for (scan = literals; !list_Empty(scan); scan = list_Cdr(scan)) {
literal = (TERM) list_Car(scan);
if (symbol_IsPredicate(term_TopSymbol(literal))) { /* Positive literal */
if (fol_IsTrue(literal)) {
/* Clause is a tautology */
list_PointerDeleteElement(literals, NULL);
/* Remove possible NULL elements to avoid a crash in term_Delete */
term_DeleteTermList(literals);
return (CLAUSE) NULL;
} else if (fol_IsFalse(literal)) {
/* Ignore this literal */
term_Delete(literal);
list_Rplaca(scan, NULL); /* Mark the actual list element */
}
} else {
/* Found a negative literal */
TERM atom = term_FirstArgument(literal);
if (fol_IsFalse(atom)) {
/* Clause is a tautology */
list_PointerDeleteElement(literals, NULL);
/* Remove possible NULL elements to avoid a crash in term_Delete */
term_DeleteTermList(literals);
return (CLAUSE) NULL;
} else if (fol_IsTrue(atom)) {
/* Ignore this literal */
term_Delete(literal);
list_Rplaca(literals, NULL); /* Mark the actual list element */
}
}
}
literals = list_PointerDeleteElement(literals, NULL);
/* Remove the special literals treated above from the list */
result = clause_CreateFromLiterals(literals, FALSE, !IsAxiom, FALSE, Flags, Precedence);
/* Don't create sorts! */
list_Delete(literals);
return result;
}
static void dfg_SubSort(char* Name1, char* Name2)
/**************************************************************
INPUT: Two sort symbol names.
RETURNS: Nothing.
EFFECT: This functions adds the formula
forall([U], implies(Name1(U), Name2(U)))
to the list of axiom formulas. Both <Name1> and <Name2>
are deleted.
***************************************************************/
{
SYMBOL s1, s2;
TERM varterm, t1, t2, term;
s1 = dfg_Symbol(Name1, 1); /* Should be unary predicates */
s2 = dfg_Symbol(Name2, 1);
if (!symbol_IsPredicate(s1)) {
misc_StartUserErrorReport();
misc_UserErrorReport("\n Line %d: Symbol is not a sort predicate.\n", dfg_LINENUMBER);
misc_FinishUserErrorReport();
}
if (!symbol_IsPredicate(s2)) {
misc_StartUserErrorReport();
misc_UserErrorReport("\n Line %d: Symbol is not a sort predicate.\n", dfg_LINENUMBER);
misc_FinishUserErrorReport();
}
varterm = term_Create(symbol_CreateStandardVariable(), list_Nil());
symbol_ResetStandardVarCounter();
t1 = term_Create(s1, list_List(varterm));
t2 = term_Create(s2, list_List(term_Copy(varterm)));
term = term_Create(fol_Implies(), list_Cons(t1, list_List(t2)));
term = fol_CreateQuantifier(fol_All(), list_List(term_Copy(varterm)),
list_List(term));
dfg_SORTDECLLIST = list_Nconc(dfg_SORTDECLLIST, list_List(list_PairCreate(NULL,term)));
}
static void dfg_SymbolGenerated(SYMBOL SortPredicate, BOOL FreelyGenerated,
LIST GeneratedBy)
/**************************************************************
INPUT: A sort predicate, a boolean flag, and a list of function
symbol names.
RETURNS: Nothing.
EFFECT: This function stores the information that the <SortPredicate>
is generated by the function symbols from the <GeneratedBy>
list. The list contains only symbol names!
The <SortPredicate> AND the symbols from the list get
the property GENERATED. Additionally the symbols get
the property FREELY, if the flag <FreelyGenerated> is TRUE.
***************************************************************/
{
SYMBOL symbol;
LIST scan;
if (!symbol_IsPredicate(SortPredicate)) {
misc_StartUserErrorReport();
misc_UserErrorReport("\n Line %d: Symbol is not a sort predicate.\n", dfg_LINENUMBER);
misc_FinishUserErrorReport();
}
/* First reset the old information */
symbol_RemoveProperty(SortPredicate, GENERATED);
symbol_RemoveProperty(SortPredicate, FREELY);
list_Delete(symbol_GeneratedBy(SortPredicate));
/* Now set the new information */
symbol_AddProperty(SortPredicate, GENERATED);
if (FreelyGenerated)
symbol_AddProperty(SortPredicate, FREELY);
for (scan = GeneratedBy; !list_Empty(scan); scan = list_Cdr(scan)) {
symbol = symbol_Lookup(list_Car(scan));
if (symbol == 0) {
misc_StartUserErrorReport();
misc_UserErrorReport("\n Line %d: undefined symbol %s.\n", dfg_LINENUMBER,
(char*)list_Car(scan));
misc_FinishUserErrorReport();
} else if (!symbol_IsFunction(symbol)) { /* must be function or constant */
misc_StartUserErrorReport();
misc_UserErrorReport("\n Line %d: Symbol is not a function.\n", dfg_LINENUMBER);
misc_FinishUserErrorReport();
}
string_StringFree(list_Car(scan));
list_Rplaca(scan, (POINTER)symbol); /* change the name list to a symbol list */
/* Set GENERATED properties for generating symbols */
symbol_AddProperty(symbol, GENERATED);
if (FreelyGenerated)
symbol_AddProperty(symbol, FREELY);
}
symbol_SetGeneratedBy(SortPredicate, GeneratedBy);
}
/**************************************************************/
/* Functions for the Symbol Table */
/**************************************************************/
typedef struct {
SYMBOL symbol;
BOOL valid;
int arity;
} DFG_SYMENTRY, *DFG_SYM;
static __inline__ DFG_SYM dfg_SymCreate(void)
{
return (DFG_SYM) memory_Malloc(sizeof(DFG_SYMENTRY));
}
static __inline__ void dfg_SymFree(DFG_SYM Entry)
{
memory_Free(Entry, sizeof(DFG_SYMENTRY));
}
static void dfg_SymAdd(SYMBOL Symbol)
/**************************************************************
INPUT: A symbol.
RETURNS: Nothing.
EFFECT: This function adds 'Symbol' to the symbol list.
The arity of these symbols will be checked every time
the symbol occurs.
***************************************************************/
{
DFG_SYM newEntry = dfg_SymCreate();
newEntry->symbol = Symbol;
newEntry->valid = FALSE;
newEntry->arity = 0;
dfg_SYMBOLLIST = list_Cons(newEntry, dfg_SYMBOLLIST);
}
static void dfg_SymCheck(SYMBOL Symbol, NAT Arity)
/**************************************************************
INPUT: A symbol and the current arity of this symbol.
RETURNS: Nothing.
EFFECT: This function compares the previous arity of 'Symbol'
with the actual 'Arity'. If these values differ
the symbol's arity is set to arbitrary.
The arity of symbols whose arity was specified in
the symbol declaration section is checked and a warning
is printed to stderr in case of differences.
***************************************************************/
{
LIST scan = dfg_SYMBOLLIST;
while (!list_Empty(scan)) {
DFG_SYM actEntry = (DFG_SYM) list_Car(scan);
if (actEntry->symbol == Symbol) {
if (actEntry->valid) {
if (actEntry->arity != Arity) {
misc_StartUserErrorReport();
misc_UserErrorReport("\n Line %u:", dfg_LINENUMBER);
misc_UserErrorReport(" The actual arity %u", Arity);
misc_UserErrorReport(" of symbol %s differs", symbol_Name(Symbol));
misc_UserErrorReport(" from the previous arity %u.\n", actEntry->arity);
misc_FinishUserErrorReport();
}
} else {
/* Not valid => first time */
actEntry->arity = Arity;
actEntry->valid = TRUE;
}
return;
}
scan = list_Cdr(scan);
}
/* Symbol isn't in SymbolList, so its arity was specified. */
/* Check if the specified arity corresponds with the actual arity */
if (symbol_Arity(Symbol) != Arity) {
misc_StartUserErrorReport();
misc_UserErrorReport("\n Line %u: Symbol %s was declared with arity %u.\n",
dfg_LINENUMBER, symbol_Name(Symbol), symbol_Arity(Symbol));
misc_FinishUserErrorReport();
}
}
static void dfg_SymCleanUp(void)
/**************************************************************
INPUT: None.
RETURNS: Nothing.
EFFECT: This function corrects all symbols whose arity wasn't
specified in the symbol declaration section but seem
to occur with always the same arity.
The memory for the symbol list is freed.
***************************************************************/
{
while (!list_Empty(dfg_SYMBOLLIST)) {
DFG_SYM actEntry = (DFG_SYM) list_Car(dfg_SYMBOLLIST);
SYMBOL actSymbol = actEntry->symbol;
if (actEntry->arity != symbol_Arity(actSymbol))
symbol_SetArity(actSymbol, actEntry->arity);
dfg_SymFree(actEntry);
dfg_SYMBOLLIST = list_Pop(dfg_SYMBOLLIST);
}
}
/**************************************************************/
/* Functions for the Variable Table */
/**************************************************************/
typedef struct {
char* name;
SYMBOL symbol;
} DFG_VARENTRY, *DFG_VAR;
static __inline__ char* dfg_VarName(DFG_VAR Entry)
{
return Entry->name;
}
static __inline__ SYMBOL dfg_VarSymbol(DFG_VAR Entry)
{
return Entry->symbol;
}
static __inline__ DFG_VAR dfg_VarCreate(void)
{
return (DFG_VAR) memory_Malloc(sizeof(DFG_VARENTRY));
}
static void dfg_VarFree(DFG_VAR Entry)
{
string_StringFree(Entry->name);
memory_Free(Entry, sizeof(DFG_VARENTRY));
}
static void dfg_VarStart(void)
{
dfg_VARLIST = list_Push(list_Nil(), dfg_VARLIST);
dfg_VARDECL = TRUE;
}
static void dfg_VarStop(void)
{
dfg_VARDECL = FALSE;
}
static void dfg_VarBacktrack(void)
{
list_DeleteWithElement(list_Top(dfg_VARLIST), (void (*)(POINTER)) dfg_VarFree);
dfg_VARLIST = list_Pop(dfg_VARLIST);
}
static void dfg_VarCheck(void)
/* Should be called after a complete clause or formula was parsed */
{
if (!list_Empty(dfg_VARLIST)) {
misc_StartErrorReport();
misc_ErrorReport("\n In dfg_VarCheck: List of variables should be empty!\n");
misc_FinishErrorReport();
}
symbol_ResetStandardVarCounter();
}
static SYMBOL dfg_VarLookup(char* Name)
/**************************************************************
INPUT: A variable name.
RETURNS: The corresponding variable symbol.
EFFECT: If the variable name was quantified before, the
corresponding symbol is returned and the <Name> is freed.
If the variable name was not quantified, and <dfg_VARDECL>
is TRUE, a new variable is created, else an error
message is printed and the program exits.
***************************************************************/
{
LIST scan, scan2;
SYMBOL symbol = symbol_Null();
scan = dfg_VARLIST;
scan2 = list_Nil();
while (!list_Empty(scan) && list_Empty(scan2)) {
scan2 = list_Car(scan);
while (!list_Empty(scan2) &&
(!string_Equal(dfg_VarName(list_Car(scan2)), Name)))
scan2 = list_Cdr(scan2);
scan = list_Cdr(scan);
}
if (!list_Empty(scan2)) {
/* Found variable */
string_StringFree(Name);
symbol = dfg_VarSymbol(list_Car(scan2));
} else {
/* Variable not found */
if (dfg_VARDECL) {
DFG_VAR newEntry = dfg_VarCreate();
newEntry->name = Name;
newEntry->symbol = symbol_CreateStandardVariable();
/* Add <newentry> to the first list in dfg_VARLIST */
list_Rplaca(dfg_VARLIST, list_Cons(newEntry,list_Car(dfg_VARLIST)));
symbol = dfg_VarSymbol(newEntry);
} else {
misc_StartUserErrorReport();
misc_UserErrorReport("\n Line %u: Free Variable %s.\n", dfg_LINENUMBER, Name);
misc_FinishUserErrorReport();
}
}
return symbol;
}