/* Skeleton output parser for bison,
   Copyright (C) 1984, 1989, 1990 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., 675 Mass Ave, Cambridge, MA 02139, 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.  */

/*
This is a parser template file, in java, for running parsers
generated by the GNU Bison parser generator.
*/

/**************************************************/

package JavaAgent.resource.fopl ;

/**************************************************/

import java.util.*;
import java.io.*;
import jbf.*;

/**************************************************/

// PREFIX



/**************************************************/

public
class YYparse {

    // Set up the fake goto mechanism
    protected int Goto;
    protected static final int yynewstate = 0;
    protected static final int yybackup = 1;
    protected static final int yydefault = 2;
    protected static final int yyreduce = 3;
    protected static final int yyerrlab = 4;
    protected static final int yyerrlab1 = 5;
    protected static final int yyerrdefault = 6;
    protected static final int yyerrpop = 7;
    protected static final int yyerrhandle = 8;

    public static final int YYCONTINUE = 1;
    public static final int YYACCEPT = 0;
    public static final int YYABORT = -1;

    public static final int YYEOF = 0;

    protected static final int YYEMPTY = -2;
    protected static final int YYTERROR = 1;
    protected static final int YYTERRCODE = 256;

// CONSTANTS

public static final int YYFINAL = 89;
public static final int YYFLAG = -32768;
public static final int YYNTBASE = 23;
public static final int YYLAST = 90;


// TOKENTYPES

public static final Integer CONSTANT = YYtokentypes.Tokentype[258];
public static final Integer VARIABLE = YYtokentypes.Tokentype[259];
public static final Integer NOT = YYtokentypes.Tokentype[260];
public static final Integer IMPLIES = YYtokentypes.Tokentype[261];
public static final Integer IFF = YYtokentypes.Tokentype[262];
public static final Integer XOR = YYtokentypes.Tokentype[263];
public static final Integer AND = YYtokentypes.Tokentype[264];
public static final Integer OR = YYtokentypes.Tokentype[265];
public static final Integer FORALL = YYtokentypes.Tokentype[266];
public static final Integer EXISTS = YYtokentypes.Tokentype[267];
public static final Integer LIST = YYtokentypes.Tokentype[268];
public static final Integer TERM = YYtokentypes.Tokentype[269];
public static final Integer LITERAL = YYtokentypes.Tokentype[270];
public static final Integer FORMULA = YYtokentypes.Tokentype[271];
public static final Integer CLAUSE = YYtokentypes.Tokentype[272];
public static final Integer CLAUSESET = YYtokentypes.Tokentype[273];
public static final Integer FORMS = YYtokentypes.Tokentype[274];


    protected int yyreturn; // see ACTIONS switch
    protected int yystate;
    protected int yyn;
    protected int yylen;
    protected int yychar; /* the lookahead symbol */
    protected int yychar1;  /* lookahead token as an internal (translated)
			   Token number */
    protected int yynerrs; /* number of parse errors so far */
    protected int yydebug; /* nonzero means print parse trace */
    protected int yyerrstatus;	/* number of tokens to shift before error
			   messages enabled */
    public StringBuffer yytext; // string for current lexeme (volatile)
    public YYlocation yyloc; // location for current lexeme
    public Integer yylval; // the semantic value of the lookahead symbol
    protected Object yyval;   // the variable used to return semantic values
			 	// from the action routines

    protected Int_Stack yyss;
    protected Object_Stack yyvs;
/*    protected loc_stack yyls;*/
    protected YYlex yylex;
    protected java.io.PrintStream yyout;

// PROCS

static final int YYTRANSLATE(int x)
	{ return ((x) <= 274 ? yytranslate[x] : 45);}



public
YYparse(YYlex yyl, java.io.PrintStream fout)
{
    yyss = new Int_Stack();
    yyvs = new Object_Stack();
    yylex = yyl;
    yylval = null;
    yytext = yyl.yylval.text();
    yyloc = yyl.yylval.location();
    yydebug = 0;
    yyout = fout;
    
}

public YYparse(YYlex yyl) {this(yyl, System.out);}

public
int
yyparse() throws Exception, IOException, EmptyStackException
{
    int ok;
    yychar1 = 0;  /* lookahead Token as an internal (translated) */
    yystate = 0;
    yyerrstatus = 0;
    yynerrs = 0;
    yychar = YYEMPTY;  /* Cause a Token to be read.  */
    yyval = null;
  
    /* 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.  */
  
    yyss.clear();
    yyvs.clear();
/*    yyls.clear();*/
    
    /* need to push a null value to match state 0 */
    yyvs.push(null);
  
    if(yydebug > 0) yyout.print("Starting parse\n");

/* Push a new state, which is found in	yystate	 .  */
/* In all cases, when you get here, the value and location stacks
   have just been pushed. so pushing a state here evens the stacks.  */
for(;;) {
branch: switch (Goto) {

case yynewstate:

  yyss.push(yystate);

  if (yydebug > 0) {
	yyout.print("Entering state ");
	yyout.print(yystate);
	yyout.print("\n");
  }

//  {Goto = yybackup; break branch;}
case 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 == YYFLAG)
    {Goto = yydefault; break branch;}

  /* 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)
    {
      if(yydebug > 0) yyout.print("Reading a token: ");
      yylval = yylex.yylex();
      yychar = yylval == null ? YYEOF : yylval.intValue();
    }

  /* 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 */

      if(yydebug > 0) yyout.print("Now at end of input.\n");
    }
  else
    {
      yychar1 = YYTRANSLATE(yychar);

      if (yydebug >= 10)
	{
	    yyout.print("Next token is ");
	    yyout.print(yychar);
	    yyout.print(" (");
	    yyout.print(yytname[yychar1]);
	    yyout.print(")\n");
	}
    }

  yyn += yychar1;
  if (yyn < 0 || yyn > YYLAST || yycheck[yyn] != yychar1)
    {Goto = yydefault; break branch;}

  yyn = yytable[yyn];

  /* yyn is what to do for this token type in this state.
     Negative => reduce, -yyn is rule number.
     Positive => shift, yyn is new state.
       New state is final state => don't bother to shift,
       just return success.
     0, or most negative number => error.  */

  if (yyn < 0)
    {
      if (yyn == YYFLAG)
	{Goto = yyerrlab; break branch;}
      yyn = -yyn;
      {Goto = yyreduce; break branch;}
    }
  else if (yyn == 0)
    {Goto = yyerrlab; break branch;}

  if (yyn == YYFINAL)
    return YYACCEPT;

  /* Shift the lookahead token.	 */

  if (yydebug > 0) {
    yyout.print("Shifting token ");
    yyout.print(yychar);
    yyout.print(" (");
    yyout.print(yytname[yychar1]);
    yyout.print("), ");
  }

  /* Discard the token being shifted unless it is eof.	*/
  if (yychar != YYEOF)
    yychar = YYEMPTY;

  yyvs.push(yylval);
/*  yyls.push(yylloc);*/

  /* count tokens shifted since error; after three, turn off error status.  */
  if (yyerrstatus > 0) yyerrstatus--;

  yystate = yyn;
  {Goto = yynewstate; break branch;}

/* Do the default action for the current state.	 */
case yydefault:

  yyn = yydefact[yystate];
  if (yyn == 0)
    {Goto = yyerrlab; break branch;}

/* Do a reduction.  yyn is the number of a rule to reduce with.	 */
case yyreduce:
  yylen = yyr2[yyn];
  if (yylen > 0)
    yyval = yyvs.tth(1-yylen); /* implement default value of the action */

  if (yydebug > 0)
    {
      int i;

      yyout.print("Reducing via rule ");
      yyout.print(yyn);
      yyout.print(" (line ");
      yyout.print(yyrline[yyn]);
      yyout.print("), ");
      /* Print the symbols being reduced, and their result.  */
      for (i = yyprhs[yyn]; yyrhs[i] > 0; i++) {
	  yyout.print(yytname[yyrhs[i]]);
	  yyout.print(" ");
      }
      yyout.print(" -> ");
      yyout.print(yytname[yyr1[yyn]]);
      yyout.print("\n");
    }

/*$*/	/* the action file gets copied in in place of this dollarsign */

/* Provide a way to avoid having return statements in the actions
   and so avoid "statement not reached" errors"
*/
yyreturn = YYCONTINUE;

switch (yyn) {

case 1:
{ parseResult = ((Term)dollar(0)); ;
    break;}
case 2:
{ parseResult = ((Literal)dollar(0)); ;
    break;}
case 3:
{ parseResult = ((Formula)dollar(0)); ;
    break;}
case 4:
{ parseResult = ((Clause)dollar(0)); ;
    break;}
case 5:
{ parseResult = ((ClauseSet)dollar(0)); ;
    break;}
case 6:
{ parseResult = ((FormulaSet)dollar(0)); ;
    break;}
case 7:
{ yyval = new FormulaSet(); ;
    break;}
case 8:
{ ((FormulaSet)dollar(0)).assert(((Formula)dollar(-1))); 
    yyval = ((FormulaSet)dollar(0)); ;
    break;}
case 9:
{ yyval = new ClauseSet(); ;
    break;}
case 10:
{ ((ClauseSet)dollar(0)).assert(((Clause)dollar(-1))); 
    yyval = ((ClauseSet)dollar(0)); ;
    break;}
case 11:
{ yyval = new Proposition(((Symbol)dollar(0))); ;
    break;}
case 12:
{ yyval = ((Formula)dollar(-1)); ;
    break;}
case 13:
{ yyval = ((Literal)dollar(0)) ;
    break;}
case 14:
{ yyval = new NegFormula(((Formula)dollar(0))); ;
    break;}
case 15:
{ ((Vector)dollar(0)).insertElementAt(((Formula)dollar(-1)), 0);
    yyval = new MultiConFormula(((Integer)dollar(-2)).intValue(), ((Vector)dollar(0))); ;
    break;}
case 16:
{ yyval = new BinConFormula(((Integer)dollar(-2)).intValue(), ((Formula)dollar(-1)), ((Formula)dollar(0))); ;
    break;}
case 17:
{ Variable.removeLocals(((Vector)dollar(-5)).size());
    yyval = new QuantFormula(((Integer)dollar(-7)).intValue(), ((Vector)dollar(-5)), ((Formula)dollar(-1))); ;
    break;}
case 18:
{ Vector res = new Vector(7, 4);
    res.addElement(((Formula)dollar(0)));
    yyval = res; ;
    break;}
case 19:
{ ((Vector)dollar(-1)).addElement(((Formula)dollar(0))); 
    yyval = ((Vector)dollar(-1)); ;
    break;}
case 20:
{ yyval = ((Integer)dollar(0)); ;
    break;}
case 21:
{ yyval = ((Integer)dollar(0)); ;
    break;}
case 22:
{ yyval = ((Integer)dollar(0)); ;
    break;}
case 23:
{ yyval = ((Integer)dollar(0)); ;
    break;}
case 24:
{ yyval = ((Integer)dollar(0)); ;
    break;}
case 25:
{ yyval = ((Integer)dollar(0)); ;
    break;}
case 26:
{ yyval = ((Integer)dollar(0)); ;
    break;}
case 27:
{ Variable.newLocal=true; ;
    break;}
case 28:
{ Variable.newLocal=false; ;
    break;}
case 29:
{ Vector res = new Vector(4, 2);
    res.addElement(((Variable)dollar(0)));
    yyval = res; ;
    break;}
case 30:
{ ((Vector)dollar(-1)).addElement(((Variable)dollar(0))); 
    yyval = ((Vector)dollar(-1)); ;
    break;}
case 31:
{ yyval = ((Variable)dollar(0)); ;
    break;}
case 32:
{ ((Variable)dollar(-2)).setType(((Symbol)dollar(-1)));
    yyval = ((Variable)dollar(-2)); ;
    break;}
case 33:
{ yyval = new Clause(((Vector)dollar(-1))); ;
    break;}
case 34:
{ yyval = new Vector(5, 3); ;
    break;}
case 35:
{ ((Vector)dollar(0)).insertElementAt(((Literal)dollar(-1)), 0); 
    yyval = ((Vector)dollar(0)); ;
    break;}
case 36:
{ yyval = new Proposition(((Symbol)dollar(0))); ;
    break;}
case 37:
{ Proposition p = new Proposition(((Symbol)dollar(-1)));
    p.negate(); 
    yyval = p ;
    break;}
case 38:
{ yyval = ((Literal)dollar(-1)) ;
    break;}
case 39:
{ ((Literal)dollar(-2)).negate(); 
    yyval = ((Literal)dollar(-2)) ;
    break;}
case 40:
{ yyval = new Literal(((Symbol)dollar(-1)), ((Vector)dollar(0))); ;
    break;}
case 41:
{ yyval = new Literal(false, EqualSy, ((Term)dollar(-1)), ((Term)dollar(0))); ;
    break;}
case 42:
{ yyval = new ConstTerm(((Symbol)dollar(0))); ;
    break;}
case 43:
{ yyval = new VarTerm(((Variable)dollar(0))); ;
    break;}
case 44:
{ yyval = new FunctTerm(((Symbol)dollar(-2)), ((Vector)dollar(-1))); ;
    break;}
case 45:
{ ((Vector)dollar(0)).insertElementAt(((Term)dollar(-1)), 0); 
    yyval = ((Vector)dollar(0)); ;
    break;}
case 46:
{ yyval = new Vector(5, 3); ;
    break;}
case 47:
{ yyval = ((Vector)dollar(0)); ;
    break;}
case 48:
{ yyval = Variable.get(new String(yytext)); ;
    break;}
case 49:
{ yyval = Symbol.get(new String(yytext)); ;
    break;}
}


  if(yyreturn != YYCONTINUE) return yyreturn;

  yyvs.popn(yylen);
  yyss.popn(yylen);
/*  yyls.popn(yylen)*/

  if (yydebug > 0)
    {
	stackdump("state stack now");
    }

  yyvs.push(yyval);

/*  yylsp++;*/
  if (yylen == 0)
    {
/*remind:
      yyls.push(yylloc);
      yyls.last_line = (yylsp-1)->last_line;
      yyls.last_column = (yylsp-1)->last_column;
      yyls.text = 0;
*/
    }
  else
    {
/* remind:
      yylsp.last_line = (yylsp+yylen-1)->last_line;
      yylsp.last_column = (yylsp+yylen-1)->last_column;
*/
    }

  /* 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 - YYNTBASE] + yyss.peek();
  if (yystate >= 0 && yystate <= YYLAST && yycheck[yystate] == yyss.peek())
    yystate = yytable[yystate];
  else
    yystate = yydefgoto[yyn - YYNTBASE];

  {Goto = yynewstate; break branch;}

case yyerrlab:	 /* here on detecting error */

  if (yyerrstatus == 0)
    /* If not already recovering from an error, report this error.  */
    {
      ++yynerrs;
	yyverror("parse error");
    }

//  {Goto = yyerrlab1; break branch;}
case yyerrlab1:	  /* here on error raised explicitly by an action */

  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)
	return YYABORT;

      if (yydebug > 0) {
	yyout.print("Discarding token ");
	yyout.print(yychar);
	yyout.print(" (");
	yyout.print(yytname[yychar1]);
	yyout.print(").\n");
      }
      yychar = YYEMPTY;
    }

  /* Else will try to reuse lookahead token
     after shifting the error token.  */

  yyerrstatus = 3;		/* Each real token shifted decrements this */

  {Goto = yyerrhandle; break branch;}

case yyerrdefault:  /* current state does not do anything special for the error token. */

/* if 0
  // This is wrong; only states that explicitly want error tokens
  // should shift them.
  yyn = yydefact[yystate];  // If its default is to accept any token, ok.  Otherwise pop it.
  if (yyn) {Goto = yydefault; break branch;}
*/

case yyerrpop:	 /* pop the current state because it cannot handle the error token */

  if (yyss.empty()) return YYABORT;
  yyvs.popn(1);
  yystate = yyss.pop();
/*  yyls.popn(1);*/

  if (yydebug > 0)
    {
	stackdump("Error: state stack now");
    }

case yyerrhandle:

  yyn = yypact[yystate];
  if (yyn == YYFLAG)
    {Goto = yyerrdefault; break branch;}

  yyn += YYTERROR;
  if (yyn < 0 || yyn > YYLAST || yycheck[yyn] != YYTERROR)
    {Goto = yyerrdefault; break branch;}

  yyn = yytable[yyn];
  if (yyn < 0)
    {
      if (yyn == YYFLAG)
	{Goto = yyerrpop; break branch;}
      yyn = -yyn;
      {Goto = yyreduce; break branch;}
    }
  else if (yyn == 0)
    {Goto = yyerrpop; break branch;}

  if (yyn == YYFINAL)
    return YYACCEPT;

  if (yydebug > 0) {yyout.println("Shifting error token, ");}

  yyvs.push(yylval);
/*  yyls.push(yyloc);*/

  yystate = yyn;
//  {Goto = yynewstate; break branch;}

}//switch
}//for(;;)

} // parse

protected
void
stackdump(String s)
{
    int i;
    int x;
    int ssp1 = yyss.depth();
    yyout.print(s);
    for(i=0;i<ssp1;i++) {
	x = yyss.ith(i);
	yyout.print(" ");
	yyout.print(x);
    }
    yyout.print("\n");
}

public
String
yyerror_verbose(String msg0) throws ParseException
{
    yyn = yypact[yystate];
    if(yyn > YYFLAG && yyn < YYLAST) {
	int size = msg0.length();
	StringBuffer msg;
	int yychar1; // a TRANSLATEd char value
	int count;
	count = 0;

	/* Start yychar1 at -yyn if nec to avoid negative indexes in yycheck.*/
	for (yychar1 = (yyn < 0 ? -yyn : 0);
		(yyn+yychar1) < (yytname.length);
		yychar1++) {
	    if((yyn+yychar1) < yycheck.length
		    && yycheck[yyn+yychar1] == yychar1) {
		size += (yytname[yychar1].length()) + 15;
		count++;
	    }
	}
	msg = new StringBuffer(size+15);
	msg.append(msg0);
	msg.append("(state " + Integer.toString(yystate) + ")");
	yychar1 = (yyn < 0)? - yyn :0;
	for(count=0,yychar1 = (yyn < 0 ? -yyn : 0);
		(yyn+yychar1) < (yytname.length) && count < 5;
		yychar1++) {
	    if((yyn+yychar1) < yycheck.length
		    && yycheck[yyn+yychar1] == yychar1) {
		msg.append(count == 0 ? ", expecting `" : " or `");
		msg.append(yytname[yychar1]);
		msg.append("'");
		count++;
	    }
	}
	return msg.toString();
    }
    return msg0;
}

public
void
yyerror(String msg, boolean verbose, boolean dumpstack) throws ParseException
{
    String s;
    if(verbose) {
	s = yyerror_verbose(msg);
    } else {
	s = msg;
    }
    yyout.print("yyerror: ");
    if(yylval.intValue() == YYEOF) {
	yyout.print("at end of file");
    } else {
	yyout.print("line ");
	yyout.print(yyloc.lineno()+1);
    }
    yyout.println(" ; " + s);
    if(dumpstack) { stackdump("yyerror: state stack"); }
    throw new ParseException(s);
}

public void yyerror(String s, boolean verbose) throws ParseException
{ yyerror(s,verbose,false); }

public void yyerror(String s) throws ParseException
{ yyerror(s,false,false); }

public void yyreturn(int t) {yyreturn = t;}

public void setdebug(boolean i) {yydebug = i?1:0;}
public void setdebug(int i) {yydebug = i>0?i:0;}

public Object dollar(int i) {return yyvs.tth(i);}


// TABLES

public static final int 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,     3,
     4,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     5,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     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,     6,     7,     8,
     9,    10,    11,    12,    13,    14,    15,    16,    17,    18,
    19,    20,    21,    22

};

public static final int yyprhs[] = {
     0,
     0,     3,     6,     9,    12,    15,    18,    19,    22,    23,
    26,    28,    32,    34,    37,    41,    45,    55,    57,    60,
    62,    64,    66,    68,    70,    72,    74,    75,    76,    78,
    81,    83,    88,    92,    93,    96,    98,   103,   107,   114,
   117,   121,   123,   125,   130,   133,   134,   136,   138

};

public static final int yyrhs[] = {
    17,
    40,     0,    18,    38,     0,    19,    26,     0,    20,    36,
     0,    21,    25,     0,    22,    24,     0,     0,    26,    24,
     0,     0,    36,    25,     0,    44,     0,     3,    27,     4,
     0,    39,     0,     8,    26,     0,    29,    26,    28,     0,
    30,    26,    26,     0,     3,    31,    32,    34,    33,     4,
     3,    27,     4,     0,    26,     0,    28,    26,     0,    12,
     0,    13,     0,     9,     0,    10,     0,    11,     0,    14,
     0,    15,     0,     0,     0,    35,     0,    34,    35,     0,
    43,     0,     3,    43,    44,     4,     0,     3,    37,     4,
     0,     0,    38,    37,     0,    44,     0,     3,     8,    44,
     4,     0,     3,    39,     4,     0,     3,     8,     3,    39,
     4,     4,     0,    44,    41,     0,     5,    40,    40,     0,
    44,     0,    43,     0,     3,    44,    41,     4,     0,    40,
    42,     0,     0,    41,     0,     7,     0,     6,     0

};

public static final int yyrline[] = {
 0,
    29,    31,    33,    35,    37,    39,    43,    45,    50,    52,
    57,    59,    63,    65,    67,    70,    72,    77,    81,    86,
    88,    92,    94,    96,   100,   102,   106,   110,   114,   118,
   123,   125,   130,   134,   136,   141,   143,   147,   149,   154,
   156,   159,   161,   163,   167,   172,   174,   178,   182

};

public static final String yytname[] = {
   "$","error","$undefined.","'('","')'",
"'='","CONSTANT","VARIABLE","NOT","IMPLIES","IFF","XOR","AND","OR","FORALL",
"EXISTS","LIST","TERM","LITERAL","FORMULA","CLAUSE","CLAUSESET","FORMS","FOPLObject",
"FOPLFormList","FOPLClauseList","FOPLFormula","FOPLBFormula","FOPL1FormList",
"FOPLmulticon","FOPLbincon","FOPLquant","LVon","LVoff","FOPL1VarSpecList","FOPLVarSpec",
"FOPLClause","SignedLit0List","SignedLit","FOPLBLiteral","FOPLTerm","FOPL1TermList",
"FOPL0TermList","tVARIABLE","tCONSTANT", null

};

public static final int yyr1[] = {
     0,
    23,    23,    23,    23,    23,    23,    24,    24,    25,    25,
    26,    26,    27,    27,    27,    27,    27,    28,    28,    29,
    29,    30,    30,    30,    31,    31,    32,    33,    34,    34,
    35,    35,    36,    37,    37,    38,    38,    38,    38,    39,
    39,    40,    40,    40,    41,    42,    42,    43,    44

};

public static final int yyr2[] = {
     0,
     2,     2,     2,     2,     2,     2,     0,     2,     0,     2,
     1,     3,     1,     2,     3,     3,     9,     1,     2,     1,
     1,     1,     1,     1,     1,     1,     0,     0,     1,     2,
     1,     4,     3,     0,     2,     1,     4,     3,     6,     2,
     3,     1,     1,     4,     2,     0,     1,     1,     1

};

public static final int yydefact[] = {
     0,
     0,     0,     0,     0,     9,     7,     0,    49,    48,     1,
    43,    42,     0,     2,    36,     0,     3,    11,    34,     4,
     5,     9,     6,     7,     0,     0,     0,     0,     0,     0,
     0,    22,    23,    24,    20,    21,     0,     0,     0,    13,
     0,    34,    10,     8,    46,     0,     0,     0,     0,    38,
    40,    25,    26,    27,    14,    12,     0,     0,    33,    35,
    47,    45,    44,    41,     0,    37,     0,    18,    15,    16,
     0,     0,    28,    29,    31,    19,    39,     0,     0,    30,
     0,     0,    32,     0,     0,    17,     0,     0,     0

};

public static final int yydefgoto[] = {
    87,
    23,    21,    24,    37,    69,    38,    39,    54,    67,    79,
    73,    74,    22,    41,    42,    40,    45,    46,    62,    11,
    18

};

public static final int yypact[] = {
    15,
     4,    13,    46,     6,     6,    46,    45,-32768,-32768,-32768,
-32768,-32768,    37,-32768,-32768,    62,-32768,-32768,    13,-32768,
-32768,     6,-32768,    46,     4,     4,    47,    50,     4,     8,
    46,-32768,-32768,-32768,-32768,-32768,    51,    46,    46,-32768,
    52,    13,-32768,-32768,     4,    55,     4,    24,    56,-32768,
-32768,-32768,-32768,-32768,-32768,-32768,    46,    46,-32768,-32768,
-32768,-32768,-32768,-32768,    57,-32768,    14,-32768,    46,-32768,
    58,    59,    14,-32768,-32768,-32768,-32768,    45,    60,-32768,
    72,    75,-32768,    62,    76,-32768,    63,    79,-32768

};

public static final int yypgoto[] = {
-32768,
    61,    64,     0,    -3,-32768,-32768,-32768,-32768,-32768,-32768,
-32768,     9,    80,    48,    85,    -8,     1,   -25,-32768,   -59,
    -1

};

public static final int yytable[] = {
    12,
    15,    10,    17,    51,    28,    25,     7,    75,    19,     8,
     9,    29,    78,    75,    29,    13,    72,    15,     8,    61,
     9,    52,    53,    12,    12,    49,    47,    12,    26,     8,
    55,     1,     2,     3,     4,     5,     6,    57,    58,    65,
    15,    26,     8,    12,    27,    12,    29,    64,    16,    48,
     8,     8,     8,    50,    56,    59,    68,    70,    63,    66,
    71,    77,    88,    82,    30,     9,    26,     8,    76,    31,
    32,    33,    34,    35,    36,    83,    81,    84,    89,    86,
    85,    80,    29,    20,    44,    43,    14,     0,     0,    60

};

public static final int yycheck[] = {
     1,
     2,     1,     3,    29,    13,     7,     3,    67,     3,     6,
     7,    13,    72,    73,    16,     3,     3,    19,     6,    45,
     7,    14,    15,    25,    26,    27,    26,    29,     5,     6,
    31,    17,    18,    19,    20,    21,    22,    38,    39,    48,
    42,     5,     6,    45,     8,    47,    48,    47,     3,     3,
     6,     6,     6,     4,     4,     4,    57,    58,     4,     4,
     4,     4,     0,     4,     3,     7,     5,     6,    69,     8,
     9,    10,    11,    12,    13,     4,    78,     3,     0,     4,
    84,    73,    84,     4,    24,    22,     2,    -1,    -1,    42

};



// SUFFIX



/** 
** This variable contains the last Object that has been parsed.
*/
public JavaAgent.resource.cdl.Parsable parseResult = null;

/** 
** This constructor simplifies contructing a FOPL parser for a String.
** The given String is the String to be parsed. If a fresh set of global
** Variables should be used for this parse then <tt>Variable.newVars()</tt> 
** should be called before this constructor. Using this constructor will 
** automatically invoke parsing and the result will be stored in the staic
** variable <tt>parseResult</tt> of this class.
** @param FOPLString the String to be parsed
** @exception Exception A number of exceptions can occur during parsing.
*/
public YYparse(String FOPLString) throws IOException, Exception {
  this(new YYlex(new ByteArrayInputStream(
      (FOPLString + ' ').getBytes())));
  yyparse();
}

/** 
** This constructor simplifies contructing a FOPL parser for an InputStream.
** The given InputStream is the String to be parsed. If a fresh set of global
** Variables should be used for this parse then <tt>Variable.newVars()</tt> 
** should be called before this constructor. Using this constructor will 
** automatically invoke parsing and the result will be stored in the staic
** variable <tt>parseResult</tt> of this class.
** @param FOPLIStream the InputStream from which to parse
** @exception Exception A number of exceptions can occur during parsing or
** reading from the Stream.
*/
public YYparse(InputStream FOPLIStream) throws IOException, Exception {
  this(new YYlex(FOPLIStream));
  yyparse();
}

private void yyverror(String s) throws ParseException {
  String errMsg = "FOPL parse error: line " + (yyloc.lineno()+1) + " ; " + 
      yyerror_verbose(s);
  throw new ParseException(errMsg);
}
  
static private Symbol EqualSy = Symbol.get("=");


}; /*class*/
