%{
/**CFile*****************************************************************

  FileName    [ctlp.y]

  PackageName [ctlp]

  Synopsis    [Yacc for CTL formula parser.]

  SeeAlso     [ctlp.h]

  Author      [Gary York, Ramin Hojati, Tom Shiple, Yuji Kukimoto
	       Jae-Young Jang, In-Ho Moon]

  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
  All rights reserved.

  Permission is hereby granted, without written agreement and without license
  or royalty fees, to use, copy, modify, and distribute this software and its
  documentation for any purpose, provided that the above copyright notice and
  the following two paragraphs appear in all copies of this software.

  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

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

#include "ctlpInt.h"

/*
 * The following is a workaround for a bug in bison, which generates code
 * that uses alloca().  Their lengthy sequence of #ifdefs for defining
 * alloca() does the wrong thing for HPUX (it should do what is defined below)
 */
#ifdef __hpux
#  include <alloca.h>
#endif

static char rcsid[] UNUSED = "$Id: ctlp.y,v 1.20 2010/04/09 23:30:23 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#include "ctlpLex.c"

%}

/*---------------------------------------------------------------------------*/
/*      Grammar declarations                                                 */
/*---------------------------------------------------------------------------*/

%union {
  Ctlp_Formula_t *sf;	/* state formula */
  char *str;
}

%type <sf> error stateformula formula
%type <str> name name_vector name_union name_or macro ax_mult ex_mult

/* %token YYERROR_VERBOSE */

%token TOK_DEFINE
%token TOK_MACRO
%token TOK_ID
%token TOK_ID2
%token TOK_ID_VECTOR
%token TOK_ID_UNION
%token TOK_COMMA
%token TOK_EQIV
%token TOK_FORALL
%token TOK_EXISTS
%token TOK_UNTIL
%token TOK_FORALL_NEXT
%token TOK_FORALL_EVENTUALLY
%token TOK_FORALL_GLOBALLY
%token TOK_EXISTS_NEXT
%token TOK_EXISTS_EVENTUALLY
%token TOK_EXISTS_GLOBALLY
%token TOK_FORALL_NEXT_MULT
%token TOK_EXISTS_NEXT_MULT
%token TOK_THEN
%token TOK_EQ
%token TOK_XOR
%token TOK_AND
%token TOK_OR
%token TOK_NOT
%token TOK_ASSIGN
%token TOK_TRUE
%token TOK_FALSE

/* precedence is specified here from lowest to highest */
%nonassoc TOK_UNTIL
%left TOK_THEN
%left TOK_EQ
%left TOK_XOR
%left TOK_OR
%left TOK_AND
%nonassoc TOK_FORALL_NEXT TOK_FORALL_EVENTUALLY TOK_FORALL_GLOBALLY TOK_EXISTS_NEXT TOK_EXISTS_EVENTUALLY TOK_EXISTS_GLOBALLY
%nonassoc TOK_NOT

%%

/*---------------------------------------------------------------------------*/
/*      Grammar rules                                                        */
/*---------------------------------------------------------------------------*/
formulas     : /* nothing */
	     | formulas formula
	     ;

formula : stateformula ';'
	       { CtlpFormulaAddToGlobalArray($1);
		       $$ = $1;
	   /*
	    * The formula is echoed by the lexical analyzer to stdout.
	    * Here we are just printing the line number after it.
	    */
	   CtlpGlobalFormula = NIL(Ctlp_Formula_t);
	 }
       | TOK_DEFINE name stateformula
	 { if (!CtlpFormulaAddToTable($2, $3, CtlpMacroTable)){
	     CtlpYyerror("** ctl error : MACRO ERROR");
			 (void) fprintf(vis_stderr, "Macro \"%s\" is already in table.\n\n",$2);
	     Ctlp_FormulaFree(CtlpGlobalFormula);
	     $$ = NULL;
	   }else{
	     $$ = $3;
	   }
	   CtlpGlobalFormula = NIL(Ctlp_Formula_t);
	 }
	     | error ';'
	       { $$ = NULL;
	   /*
	    * Error was detected reading the formula. Garbage collect
	    * and print error message.
	    */
		       Ctlp_FormulaFree(CtlpGlobalFormula);
		       (void) fprintf(vis_stderr, "** ctl error : Invalid CTL formula, line %d\n\n", CtlpYylineno);
	   CtlpGlobalFormula = NIL(Ctlp_Formula_t);
	 }
	     ;

stateformula : '(' stateformula ')'
       { $$ = $2;
	 CtlpGlobalFormula= $$;}
     | TOK_EXISTS '(' stateformula TOK_UNTIL stateformula ')'
       { $$ = Ctlp_FormulaCreate(Ctlp_EU_c, $3, $5);
	 CtlpGlobalFormula= $$; }
     | TOK_EXISTS_NEXT stateformula
       { $$ = Ctlp_FormulaCreate(Ctlp_EX_c, $2, NIL(Ctlp_Formula_t));
	 CtlpGlobalFormula= $$;}
     | ex_mult '(' stateformula ')'
       { $$ = Ctlp_FormulaCreateEXMult($1, $3);
	 if ($$ == NIL(Ctlp_Formula_t)){
	    CtlpYyerror("** ctl error : MULTIPLE EX ERROR");
	    (void) fprintf(vis_stderr,"Error during parsing line %d.\n\n", CtlpYylineno);
	    Ctlp_FormulaFree(CtlpGlobalFormula);
	 }
	 FREE($1);
	 CtlpGlobalFormula= $$;
       }
     | TOK_EXISTS_EVENTUALLY stateformula
       { $$ = Ctlp_FormulaCreate(Ctlp_EF_c, $2, NIL(Ctlp_Formula_t));
	 CtlpGlobalFormula= $$; }
     | TOK_EXISTS_GLOBALLY stateformula
       { $$ = Ctlp_FormulaCreate(Ctlp_EG_c, $2, NIL(Ctlp_Formula_t));
	 CtlpGlobalFormula= $$;}
     | TOK_FORALL '(' stateformula TOK_UNTIL stateformula ')'
       { $$ = Ctlp_FormulaCreate(Ctlp_AU_c, $3, $5);
	 CtlpGlobalFormula= $$; }
     | TOK_FORALL_NEXT stateformula
       { $$ = Ctlp_FormulaCreate(Ctlp_AX_c, $2, NIL(Ctlp_Formula_t));
	 CtlpGlobalFormula= $$; }
     | ax_mult '(' stateformula ')'
       { $$ = Ctlp_FormulaCreateAXMult($1, $3);
	 if ($$ == NIL(Ctlp_Formula_t)){
	    CtlpYyerror("** ctl error : MULTIPLE AX ERROR");
	    (void) fprintf(vis_stderr,"Error during parsing line %d.\n\n", CtlpYylineno);
	    Ctlp_FormulaFree(CtlpGlobalFormula);
	 }
	 FREE($1);
	 CtlpGlobalFormula= $$;
       }
     | TOK_FORALL_EVENTUALLY stateformula
       { $$ = Ctlp_FormulaCreate(Ctlp_AF_c, $2, NIL(Ctlp_Formula_t));
	 CtlpGlobalFormula= $$; }
     | TOK_FORALL_GLOBALLY stateformula
       { $$ = Ctlp_FormulaCreate(Ctlp_AG_c, $2, NIL(Ctlp_Formula_t));
	 CtlpGlobalFormula= $$; }
     | stateformula TOK_AND stateformula
       { $$ = Ctlp_FormulaCreate(Ctlp_AND_c, $1, $3);
	 CtlpGlobalFormula= $$; }
     | stateformula TOK_OR stateformula
       { $$ = Ctlp_FormulaCreate(Ctlp_OR_c, $1, $3);
	 CtlpGlobalFormula= $$; }
     | TOK_NOT stateformula
       { $$ = Ctlp_FormulaCreate(Ctlp_NOT_c, $2, NIL(Ctlp_Formula_t));
	 CtlpGlobalFormula= $$; }
     | stateformula TOK_THEN stateformula
       { $$ = Ctlp_FormulaCreate(Ctlp_THEN_c, $1, $3);
	 CtlpGlobalFormula= $$; }
     | stateformula TOK_EQ stateformula
       { $$ = Ctlp_FormulaCreate(Ctlp_EQ_c, $1, $3);
	 CtlpGlobalFormula= $$; }
     | stateformula TOK_XOR stateformula
       { $$ = Ctlp_FormulaCreate(Ctlp_XOR_c, $1, $3);
	 CtlpGlobalFormula= $$; }
     | name TOK_ASSIGN name
       { $$ = Ctlp_FormulaCreate(Ctlp_ID_c, $1, $3);
	 CtlpGlobalFormula= $$; }
     | name TOK_ASSIGN name_union
       { $$ = Ctlp_FormulaCreateOr($1, $3);
	 FREE($1);
	 FREE($3);
	 CtlpGlobalFormula= $$; }
     | name_vector TOK_ASSIGN name
       { $$ = Ctlp_FormulaCreateVectorAnd($1, $3);
	 if ($$ == NIL(Ctlp_Formula_t)){
	    CtlpYyerror("** ctl error : Matching ERROR");
	    (void) fprintf(vis_stderr,"LHS token is not matched to RHS token, line %d.\n\n", CtlpYylineno);
	    Ctlp_FormulaFree(CtlpGlobalFormula);
	 }
	 FREE($1);
	 FREE($3);
	 CtlpGlobalFormula= $$;
       }
     | name_vector TOK_ASSIGN name_union
       { $$ = Ctlp_FormulaCreateVectorOr($1, $3);
	 if ($$ == NIL(Ctlp_Formula_t)){
	    CtlpYyerror("** ctl error : Matching ERROR");
	    (void) fprintf(vis_stderr,"LHS token is not matched to RHS token, line %d\n\n", CtlpYylineno);
	    Ctlp_FormulaFree(CtlpGlobalFormula);
	 }
	 FREE($1);
	 FREE($3);
	 CtlpGlobalFormula= $$; }
     | name TOK_EQIV name
       { $$ = Ctlp_FormulaCreateEquiv($1, $3);
	 if ($$ == NIL(Ctlp_Formula_t)){
	    CtlpYyerror("** ctl error : Matching ERROR");
	    (void) fprintf(vis_stderr,"LHS token is not matched to RHS token, line %d.\n\n", CtlpYylineno);
	    Ctlp_FormulaFree(CtlpGlobalFormula);
	 }
	 FREE($1);
	 FREE($3);
	 CtlpGlobalFormula= $$;
       }
     | name_vector TOK_EQIV name_vector
       { $$ = Ctlp_FormulaCreateVectorEquiv($1, $3);
	 FREE($1);
	 FREE($3);
	 CtlpGlobalFormula= $$; }
     | name TOK_ASSIGN TOK_FORALL
       { $$ = Ctlp_FormulaCreate(Ctlp_ID_c, $1, util_strsav("A"));
	 CtlpGlobalFormula= $$; }
     | name TOK_ASSIGN TOK_EXISTS
       { $$ = Ctlp_FormulaCreate(Ctlp_ID_c, $1, util_strsav("E"));
	 CtlpGlobalFormula= $$; }
     | name TOK_ASSIGN TOK_UNTIL
       { $$ = Ctlp_FormulaCreate(Ctlp_ID_c, $1, util_strsav("U"));
	 CtlpGlobalFormula= $$; }
     | TOK_FORALL TOK_ASSIGN name
       { $$ = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav("A"), $3);
	 CtlpGlobalFormula= $$; }
     | TOK_EXISTS TOK_ASSIGN name
       { $$ = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav("E"), $3);
	 CtlpGlobalFormula= $$; }
     | TOK_UNTIL TOK_ASSIGN name
       { $$ = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav("U"), $3);
	 CtlpGlobalFormula= $$; }
     | TOK_TRUE
       { $$ = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(Ctlp_Formula_t), NIL(Ctlp_Formula_t));
	 CtlpGlobalFormula= $$; }
     | TOK_FALSE
       { $$ = Ctlp_FormulaCreate(Ctlp_FALSE_c, NIL(Ctlp_Formula_t), NIL(Ctlp_Formula_t));
	 CtlpGlobalFormula= $$; }
     | macro
       { $$ = CtlpFormulaFindInTable($1, CtlpMacroTable);
	 if ($$ == NIL(Ctlp_Formula_t)){
	    CtlpYyerror("** ctl error : Macro Error");
	    (void) fprintf(vis_stderr,"Macro \"%s\" is not defined.\n\n",$1);
	 }
	 FREE($1);
	 CtlpGlobalFormula= $$;
       };

name:  TOK_ID
       { $$ = util_strsav(CtlpYytext); }
     | TOK_ID2
       { (void) CtlpChangeBracket(CtlpYytext);
	 $$ = util_strsav(CtlpYytext); };

name_vector: TOK_ID_VECTOR
       { $$ = util_strsav(CtlpYytext); };

name_union: '{' name_or '}'
       { $$ = $2; };

name_or: name
       { $$ = $1; }
      |  name_or TOK_COMMA name
       { $$ = util_strcat3($1,",",$3);
	 FREE($1);
	 FREE($3);
       }
      ;

macro: TOK_MACRO name
       { $$ = $2; } ;

ax_mult: TOK_FORALL_NEXT_MULT
       { $$ = util_strsav(CtlpYytext); } ;
ex_mult: TOK_EXISTS_NEXT_MULT
       { $$ = util_strsav(CtlpYytext); } ;
%%