%{/*********************                                         -*- C++ -*-  */
/** smtlib.ypp
 ** This file is part of the CVC4 prototype.
 ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
 ** Courant Institute of Mathematical Sciences
 ** New York University
 ** See the file COPYING in the top-level source directory for licensing
 ** information.
 **
 ** This file contains the bison code for the parser that reads in CVC
 ** commands in SMT-LIB language.
 **/

#include "cvc4.h"
#include "parser_state.h"

// Exported shared data
namespace CVC4 {
namespace parser {
  extern ParserState* _global_parser_state;
}
}

using namespace std;
using namespace CVC4;
using namespace CVC4::parser;

// Suppress the bogus warning suppression in bison (it generates compile error)
#undef __GNUC_MINOR__

/** stuff that lives in smtlib_scanner.lpp */
extern int smtliblex(void);

/** Error call */ 
int smtliberror(const char *s) { return _global_parser_state->parseError(s); }

#define YYLTYPE_IS_TRIVIAL 1
#define YYMAXDEPTH 10485760

%}

%union {

  std::string *p_string;
  std::vector<std::string> *p_string_vector;

  CVC4::Expr *p_expression;
  std::vector<CVC4::Expr> *p_expression_vector;

  CVC4::Command *p_command;
  CVC4::CommandSequence *p_command_sequence;

  CVC4::parser::ParserState::BenchmarkStatus d_bench_status;
  
  CVC4::Kind d_kind;
  
};

%token <p_string> NUMERAL_TOK
%token <p_string> SYM_TOK
%token <p_string> STRING_TOK
%token <p_string> USER_VAL_TOK

%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 LET_TOK
%token FLET_TOK
%token NOTES_TOK
%token LOGIC_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 DISTINCT_TOK
%token COLON_TOK
%token LBRACKET_TOK
%token RBRACKET_TOK
%token LPAREN_TOK
%token RPAREN_TOK
%token DOLLAR_TOK
%token QUESTION_TOK

%token EOF_TOK

%type <p_string> bench_name logic_name pred_symb attribute user_value  
%type <d_bench_status> status
%type <p_expression> an_formula an_atom prop_atom
%type <p_expression_vector> an_formulas;
%type <d_kind> connective;
%type <p_command> bench_attribute
%type <p_command_sequence> bench_attributes  

%start benchmark
 
%%

benchmark:
    LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK {
      _global_parser_state->setBenchmarkName(*$3);
      _global_parser_state->setCommand($4);
    }    
  | EOF_TOK { _global_parser_state->setCommand(new EmptyCommand()); }
; 

bench_name: SYM_TOK;

bench_attributes:
    bench_attribute                   { $$ = new CommandSequence($1); }
  | bench_attributes bench_attribute  { $$ = $1; $$->addCommand($2);  }
;
 
bench_attribute:
    COLON_TOK FORMULA_TOK an_formula  { $$ = new CheckSatCommand(*$3); delete $3; }  
  | COLON_TOK STATUS_TOK status       { $$ = new EmptyCommand(); _global_parser_state->setBenchmarkStatus($3); } 
  | COLON_TOK LOGIC_TOK logic_name    { $$ = new EmptyCommand(); _global_parser_state->setBenchmarkLogic(*$3); delete $3; } 
  | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK { $$ = new EmptyCommand(); }
  | annotation { $$ = new EmptyCommand(); }
;  
 
logic_name: SYM_TOK;

status: 
    SAT_TOK     { $$ = ParserState::SATISFIABLE;   }
  | UNSAT_TOK   { $$ = ParserState::UNSATISFIABLE; }
  | UNKNOWN_TOK { $$ = ParserState::UNKNOWN;       }
;

pred_symb_decls:
    pred_symb_decl
  | pred_symb_decls pred_symb_decl
;

pred_symb_decl:
    LPAREN_TOK pred_sig annotations RPAREN_TOK
  | LPAREN_TOK pred_sig RPAREN_TOK
;

pred_sig:
  pred_symb { _global_parser_state->declareNewPredicate(*$1); delete $1; } 
;

an_formulas:
    an_formula             { $$ = new vector<Expr>; $$->push_back(*$1); delete $1; }
  | an_formulas an_formula { $$ = $1;               $$->push_back(*$2); delete $2; }
;

an_formula:
    an_atom
  | LPAREN_TOK connective an_formulas RPAREN_TOK { $$ = _global_parser_state->newExpression($2, *$3); delete $3; } 
;

connective:
    NOT_TOK                  { $$ = NOT;     }
  | IMPLIES_TOK              { $$ = IMPLIES; }
  | IF_THEN_ELSE_TOK         { $$ = ITE;     }
  | AND_TOK                  { $$ = AND;     }
  | OR_TOK                   { $$ = OR;      } 
  | XOR_TOK                  { $$ = XOR;     }
  | IFF_TOK                  { $$ = IFF;     }
;

an_atom: prop_atom;

prop_atom:
    TRUE_TOK     { $$ = _global_parser_state->getNewTrue();                         }
  | FALSE_TOK    { $$ = _global_parser_state->getNewFalse();                        }
  | pred_symb    { $$ = _global_parser_state->getNewVariableByName(*$1); delete $1; }
;  

annotations:
    annotation
  | annotations annotation
  ;
  
annotation:
    attribute                 { delete $1; }                
  | attribute user_value      { delete $1; delete $2; }
  ;

user_value: USER_VAL_TOK;

pred_symb: SYM_TOK;

attribute: 
    COLON_TOK SYM_TOK { $$ = $2; }
  ;

%%