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

  FileName    [smt.y]

  PackageName [smt]

  Synopsis    [Yacc for formula parser.]

  SeeAlso     [smt.h]
 
  Author      [Hyondeuk Kim]

  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado

  All rights reserved.

  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions
  are met:

  Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

  Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

  Neither the name of the University of Colorado nor the names of its
  contributors may be used to endorse or promote products derived from
  this software without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  POSSIBILITY OF SUCH DAMAGE.]

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

#ifdef HAVE_LIBGMP
 
#include <stdlib.h>
#include "smt.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

#ifndef yytext
#define yytext SmtYytext
#endif

  //static char rcsid[] UNUSED = "$Id: smt.y,v 1.6 2009-04-13 11:07:58 hhkim Exp $";

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

#include "smtLex.c"

%}

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

%union {
  smtFml_t *fml;	
  char *str;
}

%type <fml> benchmark bench_name bench_attributes bench_attribute status sort_symbs sort_symb_decls fun_symb_decls fun_symb_decl pred_symb_decls pred_symb_decl an_formulas an_formula quant_vars quant_var quant_symb connective an_atom prop_atom an_terms an_term basic_term annotations annotation
%type <str> user_value sort_symb_decl sort_symb pred_symb fun_symb attribute fvar var logic_name

%token TRUE_TOK
%token FALSE_TOK
%token ITE_TOK
%token NOT_TOK
%token IMPLIES_TOK
%token IF_THEN_ELSE_TOK
%token AND_TOK
%token OR_TOK
%token XOR_TOK
%token IFF_TOK
%token EXISTS_TOK
%token FORALL_TOK
%token LET_TOK
%token FLET_TOK
%token NOTES_TOK
%token SORTS_TOK
%token FUNS_TOK
%token PREDS_TOK
%token EXTENSIONS_TOK
%token DEFINITION_TOK
%token AXIOMS_TOK
%token LOGIC_TOK
%token COLON_TOK
%token LPAREN_TOK
%token RPAREN_TOK
%token SAT_TOK
%token UNSAT_TOK
%token UNKNOWN_TOK
%token ASSUMPTION_TOK
%token FORMULA_TOK
%token STATUS_TOK
%token BENCHMARK_TOK
%token EXTRASORTS_TOK
%token EXTRAFUNS_TOK
%token EXTRAPREDS_TOK
%token LANGUAGE_TOK
%token DOLLAR_TOK
%token EQUALS_TOK
%token DISTINCT_TOK
%token SEMICOLON_TOK
%token EOF_TOK
%token NUMERAL_TOK 
%token VAR_TOK 
%token SYM_TOK 
%token STRING_TOK 
%token AR_SYMB  
%token USER_VAL_TOK

/* precedence is specified here from lowest to highest */

%nonassoc FORMULA_TOK
%nonassoc LPAREN_TOK RPAREN_TOK
%nonassoc OR_TOK XOR_TOK
%nonassoc AND_TOK
%nonassoc ITE_TOK IF_THEN_ELSE_TOK IMPLIES_TOK IFF_TOK FLET_TOK LET_TOK
%nonassoc AR_SYMB EQUALS_TOK DISTINCT_TOK
%nonassoc VAR_TOK NUMERAL_TOK SYM_TOK TRUE_TOK FALSE_TOK
%nonassoc NOT_TOK EXISTS_TOK FORALL_TOK

%%

/*---------------------------------------------------------------------------*/
/*      Grammar rules                                                        */
/*---------------------------------------------------------------------------*/

benchmark:
LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK
{

};

bench_name:
SYM_TOK 
{ 

};

bench_attributes:
bench_attribute bench_attributes {/*$1::$2*/}
| bench_attribute {/*[$1]*/};

bench_attribute:
COLON_TOK ASSUMPTION_TOK an_formula 
{

}
| COLON_TOK FORMULA_TOK an_formula 
{
  /* root fml is the subfml */ 
  gvar->fml = (smtFml_t *) ((smtFml_t *) $3)->subfmlArr->space[0];
}
| COLON_TOK STATUS_TOK status 
{

}
| COLON_TOK LOGIC_TOK logic_name 
{
  if ( !strcmp($3, "QF_IDL") ) {
    gvar->flag |= IDL_MASK;
    gvar->epsilon = 1;
    gvar->epsilonless = 0;
  } else if ( !strcmp($3, "QF_RDL") ) {
    gvar->flag |= RDL_MASK;  
    gvar->epsilon = 0.00001;
    gvar->epsilonless = 0.000001;
  } else if ( !strcmp($3, "QF_LIA") ) {
    gvar->flag |= LIA_MASK;
    gvar->epsilon = 1;
    gvar->epsilonless = 0;
  } else if ( !strcmp($3, "QF_LRA") ) {
    gvar->flag |= LRA_MASK;
    gvar->epsilon = 0.00001;
    gvar->epsilonless = 0.000001;
  } else {
    gvar->flag |= UNKNOWN_MASK;
    smt_print_unknown();
    exit(0);
  }
  
  free($3);  
}
| COLON_TOK EXTRASORTS_TOK LPAREN_TOK sort_symb_decls RPAREN_TOK {/*EXTRASORTS($4)*/}
| COLON_TOK EXTRAFUNS_TOK LPAREN_TOK fun_symb_decls RPAREN_TOK 
{
}
| COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK 
{
}
| COLON_TOK NOTES_TOK STRING_TOK {/*NOTES($3)*/}
| annotation {/*ANNOTATION($1)*/};

logic_name:
SYM_TOK {
  $$ = util_strsav(yytext); 
};

status:
SAT_TOK {
  /*SAT*/ 
  gvar->status = 1;
}
| UNSAT_TOK {
  /*UNSAT*/ 
  gvar->status = 0;
}
| UNKNOWN_TOK {
  /*UNKNOWN*/ 
  gvar->status = 2;
};

sort_symbs:
sort_symbs sort_symb
{ 

}
| sort_symb 
{ 

};

sort_symb_decls:
sort_symb_decls sort_symb_decl
{ 

}
| sort_symb_decl 
{ 
  $$ = (smtFml_t *) $1;
};

fun_symb_decls:
fun_symb_decls fun_symb_decl 
{
  gvar->tfml = (smtFml_t *) $2->subfmlArr->space[0];
  $1->subfmlArr = sat_array_insert($1->subfmlArr, (long) gvar->tfml);   

  $$ = $1;
}
| fun_symb_decl 
{ 
  $$ = (smtFml_t *) $1;
};

fun_symb_decl:
LPAREN_TOK fun_symb sort_symbs sort_symb annotations RPAREN_TOK
{

}
| LPAREN_TOK fun_symb sort_symbs sort_symb RPAREN_TOK
{

}
| LPAREN_TOK fun_symb sort_symb annotations RPAREN_TOK
{

} 
| LPAREN_TOK fun_symb sort_symb RPAREN_TOK
{
  /* fun_symb: ex: extrafuns(numerical var) */
  if (!st_lookup(gvar->fun_table, $2, (char **) &(gvar->tfml))) {
    /* new fun_symb */
    gvar->tfml = smt_create_function_symbol($2);
    st_insert(gvar->fun_table, $2, (char *) gvar->tfml);
    gvar->nvar = smt_create_numerical_variable($2, gvar->tfml);
    gvar->nvarArr = sat_array_insert(gvar->nvarArr, (long) gvar->nvar);
  } else {
    free($2);
  }

  free($3);

  $$ = gvar->tfml;
};

pred_symb_decls:
pred_symb_decls pred_symb_decl 
{
  gvar->tfml = (smtFml_t *) $2->subfmlArr->space[0];
  $1->subfmlArr = sat_array_insert($1->subfmlArr, (long) gvar->tfml);  

  $$ = $1;
}
| pred_symb_decl 
{
  $$ = $1;
};

pred_symb_decl:
LPAREN_TOK pred_symb sort_symbs annotations RPAREN_TOK
{

}
| LPAREN_TOK pred_symb annotations RPAREN_TOK
{

}
| LPAREN_TOK pred_symb sort_symbs RPAREN_TOK
{

}
| LPAREN_TOK pred_symb RPAREN_TOK
{
  /* pred_symb: ex: extrapreds(boolean var) */
  if (!st_lookup(gvar->pred_table, $2, (char **)&(gvar->tfml))) {
    /* new pred_symb */
    gvar->tfml = smt_create_predicate_symbol($2);
    st_insert(gvar->pred_table, $2, (char *) gvar->tfml);
    gvar->bvar = smt_create_bool_variable($2, gvar->tfml);
    gvar->bvarArr = sat_array_insert(gvar->bvarArr, (long) gvar->bvar);
  } else {
    free($2);
  }

  $$ = gvar->tfml;
};

an_formulas:
an_formulas an_formula 
{
  /* add an_formula to an_formulas */
  gvar->tfml = (smtFml_t *) $2->subfmlArr->space[0];
  $1->subfmlArr = sat_array_insert($1->subfmlArr, (long) gvar->tfml);

  $$ = $1;
}
| an_formula 
{
  $$ = $1;
};

an_formula:
an_atom 
{
  $$ = $1;
}
| LPAREN_TOK connective an_formulas annotations RPAREN_TOK
{

}
| LPAREN_TOK connective an_formulas RPAREN_TOK
{
  gvar->tfml = (smtFml_t *) $3;
  gvar->tfml->type = (smtFmlType_t) $2;
  smt_increase_subfml_ins(gvar->tfml);

  $$ = smt_create_returning_formula(gvar->tfml);
}
| LPAREN_TOK quant_symb quant_vars an_formula annotations RPAREN_TOK
{

}
| LPAREN_TOK quant_symb quant_vars an_formula RPAREN_TOK
{

}
| LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula annotations RPAREN_TOK
{

}
| LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula RPAREN_TOK
{
  /* replace var in formula with a term */
  gvar->tfml = (smtFml_t *) $5->subfmlArr->space[0];
  smt_duplicate_formula((smtFml_t *) $4, gvar->tfml);  

  $$ = $7;
}
| LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula annotations RPAREN_TOK
{

}
| LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula RPAREN_TOK
{
  /* replace var in formula with a formula */
  gvar->tfml = (smtFml_t *) $5->subfmlArr->space[0];
  smt_duplicate_formula((smtFml_t *) $4, gvar->tfml); 

  if (smt_is_atom_formula((smtFml_t *) $4)) 
    gvar->avfmlArr = sat_array_insert(gvar->avfmlArr, (long) $4);

  $$ = $7;
};

var:
VAR_TOK
{
  /* ?<var_tok>: 
     term variable for let */
  gvar->str = util_strsav(yytext);

  if (st_lookup(gvar->term_var_table, gvar->str,
		(char **)&(gvar->tfml))) {
    free(gvar->str);
  } else {
    gvar->tfml = smt_create_term_variable(gvar->str);
    st_insert(gvar->term_var_table, gvar->str, (char *) gvar->tfml);
  }

  $$ = (char *) gvar->tfml;
};

quant_vars:
quant_vars quant_var 
{

}
| quant_var 
{

};

quant_var: 
LPAREN_TOK var sort_symb RPAREN_TOK
{
  
};

quant_symb:
EXISTS_TOK { /*EXISTS*/ }
| FORALL_TOK { /*FORALL*/ };

connective:
NOT_TOK 
{ 
  $$ = (smtFml_t *) NOT_c;
}
| IMPLIES_TOK 
{ 
  $$ = (smtFml_t *) IMP_c;
}
| IF_THEN_ELSE_TOK 
{ 
  $$ = (smtFml_t *) ITE_c;
}
| AND_TOK 
{ 
  $$ = (smtFml_t *) AND_c;
}
| OR_TOK 
{ 
  $$ = (smtFml_t *) OR_c;
}
| XOR_TOK 
{ 
  $$ = (smtFml_t *) XOR_c;
}
| IFF_TOK 
{ 
  $$ = (smtFml_t *) IFF_c;
};

an_atom:
prop_atom 
{  
  $$ = $1; 
}
| LPAREN_TOK prop_atom annotations RPAREN_TOK 
{

}
| LPAREN_TOK pred_symb an_terms annotations RPAREN_TOK
{

}
| LPAREN_TOK pred_symb an_terms RPAREN_TOK
{
  /* atom: pred_symb(ex: <, >, ...) terms */
  gvar->tfml = $3;
  gvar->tfml->type = smt_get_ar_symbol($2);
  smt_increase_subfml_ins(gvar->tfml);

  gvar->avfmlArr = sat_array_insert(gvar->avfmlArr, (long) gvar->tfml);

  free($2);

  /* create returning formula */
  $$ = smt_create_returning_formula(gvar->tfml);
}
| LPAREN_TOK EQUALS_TOK an_terms an_term annotations RPAREN_TOK
{

}
| LPAREN_TOK EQUALS_TOK an_terms an_term RPAREN_TOK
{
  /* equality atom: = terms */
  gvar->tfml = (smtFml_t *) $4->subfmlArr->space[0];
  $3->type = EQ_c;
  $3->subfmlArr = sat_array_insert($3->subfmlArr, (long) gvar->tfml);
  gvar->tfml = $3;
  smt_increase_subfml_ins(gvar->tfml);
  
  gvar->avfmlArr = sat_array_insert(gvar->avfmlArr, (long) gvar->tfml);

  /* create returning formula */
  $$ = smt_create_returning_formula(gvar->tfml);
}
| LPAREN_TOK DISTINCT_TOK an_terms an_term annotations RPAREN_TOK
{

}
| LPAREN_TOK DISTINCT_TOK an_terms an_term RPAREN_TOK
{
  /* disequality atom: != terms */
  gvar->tfml = (smtFml_t *) $4->subfmlArr->space[0];
  $3->type = NEQ_c;
  $3->subfmlArr = sat_array_insert($3->subfmlArr, (long) gvar->tfml);
  gvar->tfml = $3;
  gvar->avfmlArr = sat_array_insert(gvar->avfmlArr, (long) gvar->tfml);
  
  /* create returning formula */
  $$ = smt_create_returning_formula(gvar->tfml);
};

prop_atom:
TRUE_TOK
{
  gvar->str = util_strsav(yytext);
  
  if (st_lookup(gvar->pred_table, gvar->str, (char **)&(gvar->tfml))) {
    free(gvar->str);
  } else {
    gvar->tfml = smt_create_constant_predicate_symbol(gvar->str, 1);
    st_insert(gvar->pred_table, gvar->str, (char *) gvar->tfml);
  }
  
  /* create returning formula */
  $$ = smt_create_returning_formula(gvar->tfml);
}
| FALSE_TOK
{
  gvar->str = util_strsav(yytext);
  
  if (st_lookup(gvar->pred_table, gvar->str, 
		(char **)&(gvar->tfml))) {
    free(gvar->str);
  } else {
    gvar->tfml = smt_create_constant_predicate_symbol(gvar->str, 0);
    st_insert(gvar->pred_table, gvar->str, (char *) gvar->tfml);
  }

  /* create returning formula */
  $$ = smt_create_returning_formula(gvar->tfml);
}
| fvar
{ 
  gvar->tfml = (smtFml_t *) $1;
    
  /* create returning formula */
  $$ = smt_create_returning_formula(gvar->tfml);
}
| pred_symb 
{
  if (st_lookup(gvar->pred_table, $1, (char **)&(gvar->tfml))) {
    free($1);
  } else {
    gvar->tfml = smt_create_predicate_symbol($1);
    st_insert(gvar->pred_table, $1, (char *) gvar->tfml);
    gvar->bvar = smt_create_bool_variable($1, gvar->tfml);
    gvar->bvarArr = sat_array_insert(gvar->bvarArr, (long) gvar->bvar);
  }
  
  /* create returning formula */
  $$ = smt_create_returning_formula(gvar->tfml);
};

an_terms:
an_terms an_term 
{
  gvar->tfml = (smtFml_t *) $2->subfmlArr->space[0];
  assert(gvar->tfml->type!=NONE_c);
  $1->subfmlArr = sat_array_insert($1->subfmlArr, (long) gvar->tfml);

  $$ = $1;
}
| an_term 
{ 
  $$ = $1;
};

an_term:
basic_term 
{
  $$ = $1;
}
| LPAREN_TOK basic_term annotations RPAREN_TOK 
{

}
| LPAREN_TOK fun_symb an_terms annotations RPAREN_TOK
{

}
| LPAREN_TOK fun_symb an_terms RPAREN_TOK
{
  /* funtion symbol(ex: +, -, *, /, ...  term */
  gvar->tfml = $3;
  gvar->tfml->type = smt_get_ar_symbol($2);
  smt_increase_subfml_ins(gvar->tfml);
  free($2);

  /* create returning formula */
  $$ = smt_create_returning_formula(gvar->tfml);
}
| LPAREN_TOK ITE_TOK an_formula an_term an_term annotations RPAREN_TOK
{

}
| LPAREN_TOK ITE_TOK an_formula an_term an_term RPAREN_TOK
{
  gvar->flag |= TERM_ITE_MASK;

  gvar->tfml = (smtFml_t *) $4->subfmlArr->space[0];
  $3->subfmlArr = sat_array_insert($3->subfmlArr, (long) gvar->tfml);
  gvar->tfml = (smtFml_t *) $5->subfmlArr->space[0];
  $3->subfmlArr = sat_array_insert($3->subfmlArr, (long) gvar->tfml);
  $3->type = ITE_c;

  /* create returning formula */
  gvar->tfml = (smtFml_t *) $3;
  smt_increase_subfml_ins(gvar->tfml);
  $$ = smt_create_returning_formula(gvar->tfml);
};

basic_term:
var 
{
  gvar->tfml = (smtFml_t *) $1;

  /* create returning formula */
  $$ = smt_create_returning_formula(gvar->tfml);
}
| NUMERAL_TOK 
{
  /* constant */
  gvar->str = util_strsav(yytext);

  if (st_lookup(gvar->num_table, gvar->str, (char **)&(gvar->tfml))) {
    free(gvar->str);
  } else {
    gvar->tfml = smt_create_constant_formula(gvar->str);
    st_insert(gvar->num_table, gvar->str, (char *) gvar->tfml);
  }

  /* create returning formula */
  $$ = smt_create_returning_formula(gvar->tfml);
}
| fun_symb 
{
  if (st_lookup(gvar->fun_table, $1, (char **)&(gvar->tfml))) {
    free($1);
  } else {
    if (gvar->flag & IDL_MASK || gvar->flag & LIA_MASK)
      gvar->tfml = smt_create_function_symbol($1);
    else if (gvar->flag & RDL_MASK || gvar->flag & LRA_MASK)
      gvar->tfml = smt_create_function_symbol($1);
  }
  
  /* create returning formula */
  $$ = smt_create_returning_formula(gvar->tfml);
};

annotations:
annotation annotations 
{ 

}
| annotation 
{
  $$ = $1;
};

annotation:
attribute 
{
  $$ = (smtFml_t *) $1; 
}
| attribute user_value 
{

};

user_value:
USER_VAL_TOK {};

sort_symb_decl:
SYM_TOK 
{
  $$ = util_strsav(yytext);
};

sort_symb:
SYM_TOK 
{ 
  $$ = util_strsav(yytext);
};

pred_symb:
SYM_TOK 
{ /* returns the name of the pred_symb : predicate */ 
  $$ = util_strsav(yytext);
}
| AR_SYMB 
{ /* returns arith symbol: ex: <, >, =, ... */
  $$ = util_strsav(yytext);
};

fun_symb:
SYM_TOK
{ /* returns the name of the fun_symb : numerical variable */ 
  gvar->str = util_strsav(yytext);
  assert(gvar->str);
  $$ = gvar->str;
}
| AR_SYMB 
{ /* returns arith symbol: ex: +, -, *, /, ... */ 
  gvar->str = util_strsav(yytext); 
  assert(gvar->str);
  $$ = gvar->str;
};
   
attribute:
COLON_TOK SYM_TOK
{
  
};

fvar: 
DOLLAR_TOK SYM_TOK 
{ 
  gvar->str = util_strsav(yytext); 

  /* $<simple_identifier>: 
     intermediate variable that substitutes propostional atom */
  if (st_lookup(gvar->fml_var_table, gvar->str, 
		(char **)&(gvar->tfml))) {
    free(gvar->str);
  } else {
    gvar->tfml = smt_create_fml_variable(gvar->str);
    st_insert(gvar->fml_var_table, gvar->str, (char *) gvar->tfml);
  }

  $$ = (char *) gvar->tfml;   
};

%%
 
#endif