diff options
Diffstat (limited to 'test/spass/iaparser.c')
| -rw-r--r-- | test/spass/iaparser.c | 1773 |
1 files changed, 1773 insertions, 0 deletions
diff --git a/test/spass/iaparser.c b/test/spass/iaparser.c new file mode 100644 index 00000000..4fa86979 --- /dev/null +++ b/test/spass/iaparser.c @@ -0,0 +1,1773 @@ +/* A Bison parser, made from iaparser.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 ia_parse +#define yylex ia_lex +#define yyerror ia_error +#define yylval ia_lval +#define yychar ia_char +#define yydebug ia_debug +#define yynerrs ia_nerrs + + +/* Tokens. */ +#ifndef YYTOKENTYPE +# define YYTOKENTYPE + /* Put the tokens into the symbol table, so that GDB and other debuggers + know about them. */ + enum yytokentype { + IA_AND = 258, + IA_EQUAL = 259, + IA_EQUIV = 260, + IA_EXISTS = 261, + IA_FALSE = 262, + IA_FORALL = 263, + IA_IMPLIED = 264, + IA_IMPLIES = 265, + IA_NOT = 266, + IA_OR = 267, + IA_PROVE = 268, + IA_TRUE = 269, + IA_NUM = 270, + IA_ID = 271 + }; +#endif +#define IA_AND 258 +#define IA_EQUAL 259 +#define IA_EQUIV 260 +#define IA_EXISTS 261 +#define IA_FALSE 262 +#define IA_FORALL 263 +#define IA_IMPLIED 264 +#define IA_IMPLIES 265 +#define IA_NOT 266 +#define IA_OR 267 +#define IA_PROVE 268 +#define IA_TRUE 269 +#define IA_NUM 270 +#define IA_ID 271 + + + + +/* Copy the first part of user declarations. */ +#line 48 "iaparser.y" + + +#include "flags.h" +#include "ia.h" +#include "symbol.h" +#include "term.h" +#include "foldfg.h" +#include "clause.h" + +extern NAT dfg_LINENUMBER; /* Defined in dfgparser.y */ +LIST ia_PROOFREQUEST; /* A pair! */ +FLAGSTORE ia_FLAGS; + +void yyerror(const char*); +int yylex(void); /* Defined in iascanner.l */ + +static SYMBOL ia_Symbol(char*, NAT); +static TERM ia_CreateQuantifier(SYMBOL, LIST, TERM); + +static __inline__ void ia_StringFree(char* String) +{ + memory_Free(String, sizeof(char)*(strlen(String)+1)); +} + +static __inline__ TERM ia_TermCreate(char* Name, LIST Arguments) +/* Look up the symbol, check its arity and create the term */ +{ + return term_Create(ia_Symbol(Name,list_Length(Arguments)), Arguments); +} + +/**************************************************************/ +/* Functions to check the arity of symbols */ +/**************************************************************/ + +static void ia_SymCheck(SYMBOL, NAT); + +/**************************************************************/ +/* 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 ia_VARLIST; +static BOOL ia_VARDECL; + +static void ia_VarStart(void); +static void ia_VarStop(void); +static void ia_VarBacktrack(void); +static void ia_VarCheck(void); +static SYMBOL ia_VarLookup(char*); + +#define YY_INPUT(buf,result,max_size) \ +{ \ + int c = getc(ia_in); \ + result = (c == EOF) ? YY_NULL : (buf[0] = c, 1); \ +} + +#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 113 "iaparser.y" +typedef union { + int number; + char* string; + SYMBOL symbol; + TERM term; + LIST list; +} yystype; +/* Line 193 of /opt/gnu//share/bison/yacc.c. */ +#line 187 "iaparser.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 208 "iaparser.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 83 + +/* YYNTOKENS -- Number of terminals. */ +#define YYNTOKENS 23 +/* YYNNTS -- Number of nonterminals. */ +#define YYNNTS 16 +/* YYNRULES -- Number of rules. */ +#define YYNRULES 36 +/* YYNRULES -- Number of states. */ +#define YYNSTATES 77 + +/* YYTRANSLATE(YYLEX) -- Bison symbol number corresponding to YYLEX. */ +#define YYUNDEFTOK 2 +#define YYMAXUTOK 271 + +#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, + 17, 19, 2, 2, 18, 2, 20, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 21, 2, 22, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 2, 2, 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 +}; + +#if YYDEBUG +/* YYPRHS[YYN] -- Index of the first RHS symbol of rule number YYN in + YYRHS. */ +static const unsigned char yyprhs[] = +{ + 0, 0, 3, 4, 14, 16, 20, 22, 24, 26, + 31, 38, 43, 48, 49, 50, 61, 62, 63, 74, + 76, 78, 80, 82, 84, 86, 88, 90, 92, 94, + 96, 100, 102, 107, 110, 114, 116 +}; + +/* YYRHS -- A `-1'-separated list of the rules' RHS. */ +static const yysigned_char yyrhs[] = +{ + 24, 0, -1, -1, 13, 17, 26, 18, 37, 18, + 15, 19, 20, -1, 26, -1, 25, 18, 26, -1, + 34, -1, 14, -1, 7, -1, 11, 17, 26, 19, + -1, 31, 17, 26, 18, 26, 19, -1, 32, 17, + 25, 19, -1, 34, 17, 25, 19, -1, -1, -1, + 33, 17, 21, 27, 35, 28, 22, 18, 26, 19, + -1, -1, -1, 34, 17, 21, 29, 35, 30, 22, + 18, 26, 19, -1, 4, -1, 5, -1, 9, -1, + 10, -1, 3, -1, 12, -1, 6, -1, 8, -1, + 16, -1, 15, -1, 36, -1, 35, 18, 36, -1, + 34, -1, 34, 17, 34, 19, -1, 21, 22, -1, + 21, 38, 22, -1, 34, -1, 38, 18, 34, -1 +}; + +/* YYRLINE[YYN] -- source line where rule number YYN was defined. */ +static const unsigned char yyrline[] = +{ + 0, 136, 136, 137, 149, 150, 153, 154, 155, 156, + 158, 160, 162, 164, 165, 164, 170, 171, 170, 179, + 180, 181, 182, 185, 186, 189, 190, 193, 194, 197, + 198, 201, 211, 232, 233, 236, 237 +}; +#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", "IA_AND", "IA_EQUAL", "IA_EQUIV", + "IA_EXISTS", "IA_FALSE", "IA_FORALL", "IA_IMPLIED", "IA_IMPLIES", + "IA_NOT", "IA_OR", "IA_PROVE", "IA_TRUE", "IA_NUM", "IA_ID", "'('", + "','", "')'", "'.'", "'['", "']'", "$accept", "proofrequest", + "termlist", "term", "@1", "@2", "@3", "@4", "binsymbol", "nsymbol", + "quantsymbol", "id", "qtermlist", "qterm", "labellistopt", "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, 40, 44, 41, + 46, 91, 93 +}; +# endif + +/* YYR1[YYN] -- Symbol number of symbol that rule YYN derives. */ +static const unsigned char yyr1[] = +{ + 0, 23, 24, 24, 25, 25, 26, 26, 26, 26, + 26, 26, 26, 27, 28, 26, 29, 30, 26, 31, + 31, 31, 31, 32, 32, 33, 33, 34, 34, 35, + 35, 36, 36, 37, 37, 38, 38 +}; + +/* YYR2[YYN] -- Number of symbols composing right hand side of rule YYN. */ +static const unsigned char yyr2[] = +{ + 0, 2, 0, 9, 1, 3, 1, 1, 1, 4, + 6, 4, 4, 0, 0, 10, 0, 0, 10, 1, + 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, + 3, 1, 4, 2, 3, 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[] = +{ + 2, 0, 0, 0, 1, 23, 19, 20, 25, 8, + 26, 21, 22, 0, 24, 7, 28, 27, 0, 0, + 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 4, 13, 16, 0, 9, 33, + 35, 0, 0, 0, 0, 11, 0, 0, 12, 0, + 34, 0, 0, 5, 31, 14, 29, 17, 36, 0, + 10, 0, 0, 0, 0, 3, 0, 30, 0, 0, + 32, 0, 0, 0, 0, 15, 18 +}; + +/* YYDEFGOTO[NTERM-NUM]. */ +static const yysigned_char yydefgoto[] = +{ + -1, 2, 33, 34, 46, 63, 47, 64, 19, 20, + 21, 22, 55, 56, 31, 41 +}; + +/* YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing + STATE-NUM. */ +#define YYPACT_NINF -29 +static const yysigned_char yypact[] = +{ + -12, 12, 35, 0, -29, -29, -29, -29, -29, -29, + -29, -29, -29, 19, -29, -29, -29, -29, 20, 22, + 40, 41, 42, 0, 31, 0, 0, 43, 39, 18, + 8, 38, 44, 7, -29, -29, -29, 9, -29, -29, + -29, -5, 46, 0, 0, -29, 16, 16, -29, 16, + -29, 47, 48, -29, 53, 45, -29, 45, -29, 51, + -29, 16, 16, 50, 52, -29, 54, -29, 57, 58, + -29, 0, 0, 59, 60, -29, -29 +}; + +/* YYPGOTO[NTERM-NUM]. */ +static const yysigned_char yypgoto[] = +{ + -29, -29, 37, -3, -29, -29, -29, -29, -29, -29, + -29, -28, 30, 21, -29, -29 +}; + +/* 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 char yytable[] = +{ + 18, 1, 40, 5, 6, 7, 8, 9, 10, 11, + 12, 13, 14, 49, 15, 16, 17, 50, 54, 54, + 29, 58, 32, 16, 17, 44, 45, 44, 48, 3, + 39, 16, 17, 66, 54, 4, 23, 38, 24, 25, + 52, 53, 5, 6, 7, 8, 9, 10, 11, 12, + 13, 14, 30, 15, 16, 17, 42, 26, 27, 28, + 36, 51, 43, 62, 35, 37, 59, 60, 73, 74, + 61, 65, 68, 70, 69, 71, 72, 57, 75, 76, + 0, 0, 0, 67 +}; + +static const yysigned_char yycheck[] = +{ + 3, 13, 30, 3, 4, 5, 6, 7, 8, 9, + 10, 11, 12, 18, 14, 15, 16, 22, 46, 47, + 23, 49, 25, 15, 16, 18, 19, 18, 19, 17, + 22, 15, 16, 61, 62, 0, 17, 19, 18, 17, + 43, 44, 3, 4, 5, 6, 7, 8, 9, 10, + 11, 12, 21, 14, 15, 16, 18, 17, 17, 17, + 21, 15, 18, 18, 21, 28, 19, 19, 71, 72, + 17, 20, 22, 19, 22, 18, 18, 47, 19, 19, + -1, -1, -1, 62 +}; + +/* YYSTOS[STATE-NUM] -- The (internal number of the) accessing + symbol of state STATE-NUM. */ +static const unsigned char yystos[] = +{ + 0, 13, 24, 17, 0, 3, 4, 5, 6, 7, + 8, 9, 10, 11, 12, 14, 15, 16, 26, 31, + 32, 33, 34, 17, 18, 17, 17, 17, 17, 26, + 21, 37, 26, 25, 26, 21, 21, 25, 19, 22, + 34, 38, 18, 18, 18, 19, 27, 29, 19, 18, + 22, 15, 26, 26, 34, 35, 36, 35, 34, 19, + 19, 17, 18, 28, 30, 20, 34, 36, 22, 22, + 19, 18, 18, 26, 26, 19, 19 +}; + +#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 136 "iaparser.y" + { YYABORT; } + break; + + case 3: +#line 137 "iaparser.y" + { + ia_VarCheck(); + ia_PROOFREQUEST = list_PairCreate(yyvsp[-6].term,yyvsp[-4].list); + flag_SetFlagValue(ia_FLAGS,flag_TIMELIMIT,yyvsp[-2].number); + YYACCEPT; + } + break; + + case 4: +#line 149 "iaparser.y" + { yyval.list = list_List(yyvsp[0].term); } + break; + + case 5: +#line 150 "iaparser.y" + { yyval.list = list_Nconc(yyvsp[-2].list, list_List(yyvsp[0].term)); } + break; + + case 6: +#line 153 "iaparser.y" + { yyval.term = ia_TermCreate(yyvsp[0].string, list_Nil()); } + break; + + case 7: +#line 154 "iaparser.y" + { yyval.term = term_Create(fol_True(),list_Nil()); } + break; + + case 8: +#line 155 "iaparser.y" + { yyval.term = term_Create(fol_False(),list_Nil()); } + break; + + case 9: +#line 157 "iaparser.y" + { yyval.term = term_Create(fol_Not(),list_List(yyvsp[-1].term)); } + break; + + case 10: +#line 159 "iaparser.y" + { yyval.term = term_Create(yyvsp[-5].symbol, list_Cons(yyvsp[-3].term, list_List(yyvsp[-1].term))); } + break; + + case 11: +#line 161 "iaparser.y" + { yyval.term = term_Create(yyvsp[-3].symbol, yyvsp[-1].list); } + break; + + case 12: +#line 163 "iaparser.y" + { yyval.term = ia_TermCreate(yyvsp[-3].string, yyvsp[-1].list); } + break; + + case 13: +#line 164 "iaparser.y" + { ia_VarStart(); } + break; + + case 14: +#line 165 "iaparser.y" + { ia_VarStop(); } + break; + + case 15: +#line 167 "iaparser.y" + { ia_VarBacktrack(); + yyval.term = ia_CreateQuantifier(yyvsp[-9].symbol,yyvsp[-5].list,yyvsp[-1].term); + } + break; + + case 16: +#line 170 "iaparser.y" + { ia_VarStart(); } + break; + + case 17: +#line 171 "iaparser.y" + { ia_VarStop(); } + break; + + case 18: +#line 173 "iaparser.y" + { misc_StartUserErrorReport(); + misc_UserErrorReport("\n Line %d: SPASS can't handle the quantifier %s.\n", dfg_LINENUMBER, yyvsp[-9].string); + misc_FinishUserErrorReport(); + } + break; + + case 19: +#line 179 "iaparser.y" + { yyval.symbol = fol_Equality(); } + break; + + case 20: +#line 180 "iaparser.y" + { yyval.symbol = fol_Equiv(); } + break; + + case 21: +#line 181 "iaparser.y" + { yyval.symbol = fol_Implied(); } + break; + + case 22: +#line 182 "iaparser.y" + { yyval.symbol = fol_Implies(); } + break; + + case 23: +#line 185 "iaparser.y" + { yyval.symbol = fol_And(); } + break; + + case 24: +#line 186 "iaparser.y" + { yyval.symbol = fol_Or(); } + break; + + case 25: +#line 189 "iaparser.y" + { yyval.symbol = fol_Exist(); } + break; + + case 26: +#line 190 "iaparser.y" + { yyval.symbol = fol_All(); } + break; + + case 27: +#line 193 "iaparser.y" + { yyval.string = yyvsp[0].string; } + break; + + case 28: +#line 194 "iaparser.y" + { yyval.string = string_IntToString(yyvsp[0].number); } + break; + + case 29: +#line 197 "iaparser.y" + { yyval.list = list_List(yyvsp[0].term); } + break; + + case 30: +#line 198 "iaparser.y" + { yyval.list = list_Nconc(yyvsp[-2].list, list_List(yyvsp[0].term)); } + break; + + case 31: +#line 201 "iaparser.y" + { SYMBOL s = ia_Symbol(yyvsp[0].string,0); + if (!symbol_IsVariable(s)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Line %d: %s",dfg_LINENUMBER, + symbol_Name(s)); + misc_UserErrorReport(" is not a variable.\n"); + misc_FinishUserErrorReport(); + } + yyval.term = term_Create(s, list_Nil()); + } + break; + + case 32: +#line 211 "iaparser.y" + { SYMBOL p, v; + p = ia_Symbol(yyvsp[-3].string, 1); + if (!symbol_IsPredicate(p)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Line %d: %s",dfg_LINENUMBER, + symbol_Name(p)); + misc_UserErrorReport(" is not a predicate.\n"); + misc_FinishUserErrorReport(); + } + v = ia_Symbol(yyvsp[-1].string, 0); + if (!symbol_IsVariable(v)) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Line %d: %s",dfg_LINENUMBER, + symbol_Name(v)); + misc_UserErrorReport(" is not a variable.\n"); + misc_FinishUserErrorReport(); + } + yyval.term = term_Create(p, list_List(term_Create(v,list_Nil()))); + } + break; + + case 33: +#line 232 "iaparser.y" + { yyval.list = list_Nil(); } + break; + + case 34: +#line 233 "iaparser.y" + { yyval.list = yyvsp[-1].list; } + break; + + case 35: +#line 236 "iaparser.y" + { yyval.list = list_List(yyvsp[0].string); } + break; + + case 36: +#line 237 "iaparser.y" + { yyval.list = list_Nconc(yyvsp[-2].list, list_List(yyvsp[0].string)); } + break; + + + } + +/* Line 1016 of /opt/gnu//share/bison/yacc.c. */ +#line 1290 "iaparser.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 240 "iaparser.y" + + + +void yyerror(const char *s) +{ + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Line %i: %s\n", dfg_LINENUMBER, s); + misc_FinishUserErrorReport(); + +} + +LIST ia_GetNextRequest(FILE* Input, FLAGSTORE Flags) +/************************************************************** + INPUT: An input file containing one proof request from KIV. + RETURNS: The proof request as pair (formula, labellist), + list_Nil(), if EOF was reached. + EFFECT: Reads ONE proof request from the file. + <Input> may also be a UNIX pipe. +***************************************************************/ +{ + extern FILE* ia_in; /* defined in kivscanner */ + + ia_in = Input; + ia_PROOFREQUEST = list_Nil(); + ia_FLAGS = Flags; + ia_parse(); + + return ia_PROOFREQUEST; +} + + +/**************************************************************/ +/* Static Functions */ +/**************************************************************/ + +static SYMBOL ia_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; + + symbol = symbol_Lookup(Name); + if (symbol != 0) { + ia_StringFree(Name); + ia_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 = ia_VarLookup(Name); + } + return symbol; +} + + +static TERM ia_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; +} + + +/**************************************************************/ +/* Functions for the Symbol Table */ +/**************************************************************/ + +static void ia_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 + a warning is printed to stderr and the program exits. +***************************************************************/ +{ + /* Check if the specified arity corresponds with the actual arity */ + if (symbol_Arity(Symbol) != symbol_ArbitraryArity() && + symbol_Arity(Symbol) != Arity) { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Line %u: Symbol %s", dfg_LINENUMBER, symbol_Name(Symbol)); + misc_UserErrorReport(" was declared with arity %u.\n", symbol_Arity(Symbol)); + misc_FinishUserErrorReport(); + } +} + + +/**************************************************************/ +/* Functions for the Variable Table */ +/**************************************************************/ + +typedef struct { + char* name; + SYMBOL symbol; +} IA_VARENTRY, *IA_VAR; + +static __inline__ char* ia_VarName(IA_VAR Entry) +{ + return Entry->name; +} + +static __inline__ SYMBOL ia_VarSymbol(IA_VAR Entry) +{ + return Entry->symbol; +} + +static __inline__ IA_VAR ia_VarCreate(void) +{ + return (IA_VAR) memory_Malloc(sizeof(IA_VARENTRY)); +} + +static void ia_VarFree(IA_VAR Entry) +{ + ia_StringFree(Entry->name); + memory_Free(Entry, sizeof(IA_VARENTRY)); +} + +static void ia_VarStart(void) +{ + ia_VARLIST = list_Push(list_Nil(), ia_VARLIST); + ia_VARDECL = TRUE; +} + +static void ia_VarStop(void) +{ + ia_VARDECL = FALSE; +} + +static void ia_VarBacktrack(void) +{ + list_DeleteWithElement(list_Top(ia_VARLIST), (void (*)(POINTER)) ia_VarFree); + ia_VARLIST = list_Pop(ia_VARLIST); +} + +static void ia_VarCheck(void) +/* Should be called after a complete clause or formula was parsed */ +{ + if (!list_Empty(ia_VARLIST)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In ia_VarCheck: List of variables should be empty!\n"); + misc_FinishErrorReport(); + } + symbol_ResetStandardVarCounter(); +} + +static SYMBOL ia_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 <ia_VARDECL> + is TRUE, a new variable is created, else an error + message is printed and the program exits. +***************************************************************/ +{ + LIST scan, scan2; + SYMBOL symbol; + + symbol = symbol_Null(); + + scan = ia_VARLIST; + scan2 = list_Nil(); + while (!list_Empty(scan) && list_Empty(scan2)) { + scan2 = list_Car(scan); + while (!list_Empty(scan2) && + !string_Equal(ia_VarName(list_Car(scan2)), Name)) + scan2 = list_Cdr(scan2); + scan = list_Cdr(scan); + } + + if (!list_Empty(scan2)) { + /* Found variable */ + ia_StringFree(Name); + symbol = ia_VarSymbol(list_Car(scan2)); + } else { + /* Variable not found */ + if (ia_VARDECL) { + IA_VAR newEntry = ia_VarCreate(); + newEntry->name = Name; + newEntry->symbol = symbol_CreateStandardVariable(); + /* Add <newentry> to the first list in ia_VARLIST */ + list_Rplaca(ia_VARLIST, list_Cons(newEntry,list_Car(ia_VARLIST))); + symbol = ia_VarSymbol(newEntry); + } else { + misc_StartUserErrorReport(); + misc_UserErrorReport("\n Line %u: Free Variable %s.\n", dfg_LINENUMBER, Name); + misc_FinishUserErrorReport(); + } + } + return symbol; +} + |