diff options
Diffstat (limited to 'src/parser/pl.ypp')
| -rw-r--r-- | src/parser/pl.ypp | 388 |
1 files changed, 0 insertions, 388 deletions
diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp deleted file mode 100644 index f0bc21942..000000000 --- a/src/parser/pl.ypp +++ /dev/null @@ -1,388 +0,0 @@ -%{/******************* -*- C++ -*- */ -/** pl.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 the presentation language (hence "PL"). - **/ - -#define YYDEBUG 1 - -#include <list> -#include <vector> -#include <string> -#include <ostream> -#include <sstream> - -#include "smt/smt_engine.h" -#include "parser/parser_exception.h" -#include "parser/parser_state.h" -#include "expr/expr.h" -#include "expr/expr_builder.h" -#include "expr/expr_manager.h" -#include "util/command.h" -//#include "rational.h" - -// Exported shared data -namespace CVC4 { - namespace parser { - extern ParserState* _global_parser_state;; - }/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -// Define shortcuts for various things -// #define TMP CVC4::parser::_global_parser_state -// #define EXPR CVC4::parser::_global_parser_state->expr -#define SMT_ENGINE (CVC4::parser::_global_parser_state->getSmtEngine()) -#define EXPR_MANAGER (CVC4::parser::_global_parser_state->getExpressionManager()) -// #define RAT(args) CVC4::newRational args - -// Suppress the bogus warning suppression in bison (it generates -// compile error) -#undef __GNUC_MINOR__ - -/* stuff that lives in PL.lex */ -extern int PLlex(void); - -int PLerror(const char *s) { - std::ostringstream ss; - ss << CVC4::parser::_global_parser_state->getFileName() << ":" - << CVC4::parser::_global_parser_state->getLineNumber() << ": " << s; - CVC4::parser::_global_parser_state->parseError(ss.str()); - return 0;// dead code; error() above throws an exception -} - -// make the entry point public -int CVC4_PUBLIC PLparse(void *YYPARSE_PARAM); - -#define YYLTYPE_IS_TRIVIAL 1 -#define YYMAXDEPTH 10485760 -/* Prefer YYERROR_VERBOSE over %error-verbose to avoid errors in older bison */ -#define YYERROR_VERBOSE 1 - -using namespace CVC4; - -%} - -%union { - std::string *str; - CVC4::Expr *expr; - CVC4::Command *cmd; - std::vector<CVC4::Expr> *vec; - std::list<std::string> *strlst; - int kind; -}; - - -%start cmd - // %start Query - -/* strings are for better error messages. - "_TOK" is so macros don't conflict with kind names */ - -%token DISTINCT_TOK "DISTINCT" -%token AND_TOK "AND" -%token ARRAY_TOK "ARRAY" -%token BOOLEAN_TOK "BOOLEAN" -%token DATATYPE_TOK "DATATYPE" -%token ELSE_TOK "ELSE" -%token ELSIF_TOK "ELSIF" -%token END_TOK "END" -%token ENDIF_TOK "ENDIF" -%token EXISTS_TOK "EXISTS" -%token FALSELIT_TOK "FALSE" -%token FORALL_TOK "FORALL" -%token IN_TOK "IN" -%token IF_TOK "IF" -%token LAMBDA_TOK "LAMBDA" -%token SIMULATE_TOK "SIMULATE" -%token LET_TOK "LET" -%token NOT_TOK "NOT" -%token IS_INTEGER_TOK "IS_INTEGER" -%token OF_TOK "OF" -%token OR_TOK "OR" -%token REAL_TOK "REAL" -%token INT_TOK "INT" -%token SUBTYPE_TOK "SUBTYPE" -%token BITVECTOR_TOK "BITVECTOR" -%token THEN_TOK "THEN" -%token TRUELIT_TOK "TRUE" -%token TYPE_TOK "TYPE" -%token WITH_TOK "WITH" -%token XOR_TOK "XOR" -%token TCC_TOK "TCC" -%token PATTERN_TOK "PATTERN" -%token '_' -%token DONE_TOK - -%token DOTDOT_TOK ".." -%token ASSIGN_TOK ":=" -%token NEQ_TOK "/=" -%token IMPLIES_TOK "=>" -%token IFF_TOK "<=>" -%token PLUS_TOK "+" -%token MINUS_TOK "-" -%token MULT_TOK "*" -%token POW_TOK "^" -%token DIV_TOK "/" -%token MOD_TOK "MOD" -%token INTDIV_TOK "DIV" -%token LT_TOK "<" -%token LE_TOK "<=" -%token GT_TOK ">" -%token GE_TOK ">=" -%token FLOOR_TOK "FLOOR" -%token LEFTSHIFT_TOK "<<" -%token RIGHTSHIFT_TOK ">>" -%token BVPLUS_TOK "BVPLUS" -%token BVSUB_TOK "BVSUB" -%token BVUDIV_TOK "BVUDIV" -%token BVSDIV_TOK "BVSDIV" -%token BVUREM_TOK "BVUREM" -%token BVSREM_TOK "BVSREM" -%token BVSMOD_TOK "BVSMOD" -%token BVSHL_TOK "BVSHL" -%token BVASHR_TOK "BVASHR" -%token BVLSHR_TOK "BVLSHR" -%token BVUMINUS_TOK "BVUMINUS" -%token BVMULT_TOK "BVMULT" -%token SQHASH_TOK "[#" -%token HASHSQ_TOK "#]" -%token PARENHASH_TOK "(#" -%token HASHPAREN_TOK "#)" -%token ARROW_TOK "->" -%token BVNEG_TOK "~" -%token BVAND_TOK "&" -%token MID_TOK "|" -%token BVXOR_TOK "BVXOR" -%token BVNAND_TOK "BVNAND" -%token BVNOR_TOK "BVNOR" -%token BVCOMP_TOK "BVCOMP" -%token BVXNOR_TOK "BVXNOR" -%token CONCAT_TOK "@" -%token BVTOINT_TOK "BVTOINT" -%token INTTOBV_TOK "INTTOBV" -%token BOOLEXTRACT_TOK "BOOLEXTRACT" -%token BVLT_TOK "BVLT" -%token BVGT_TOK "BVGT" -%token BVLE_TOK "BVLE" -%token BVGE_TOK "BVGE" -%token SX_TOK "SX" -%token BVZEROEXTEND_TOK "BVZEROEXTEND" -%token BVREPEAT_TOK "BVREPEAT" -%token BVROTL_TOK "BVROTL" -%token BVROTR_TOK "BVROTR" -%token BVSLT_TOK "BVSLT" -%token BVSGT_TOK "BVSGT" -%token BVSLE_TOK "BVSLE" -%token BVSGE_TOK "BVSGE" - - -/* commands given in prefix syntax */ -%token ARITH_VAR_ORDER_TOK "ARITH_VAR_ORDER" -%token ASSERT_TOK "ASSERT" -%token QUERY_TOK "QUERY" -%token CHECKSAT_TOK "CHECKSAT" -%token CONTINUE_TOK "CONTINUE" -%token RESTART_TOK "RESTART" -%token HELP_TOK "HELP" -%token DBG_TOK "DBG" -%token TRACE_TOK "TRACE" -%token UNTRACE_TOK "UNTRACE" -%token OPTION_TOK "OPTION" -%token TRANSFORM_TOK "TRANSFORM" -%token PRINT_TOK "PRINT" -%token PRINT_TYPE_TOK "PRINT_TYPE" -%token CALL_TOK "CALL" -%token ECHO_TOK "ECHO" -%token INCLUDE_TOK "INCLUDE" -%token DUMP_PROOF_TOK "DUMP_PROOF" -%token DUMP_ASSUMPTIONS_TOK "DUMP_ASSUMPTIONS" -%token DUMP_SIG_TOK "DUMP_SIG" -%token DUMP_TCC_TOK "DUMP_TCC" -%token DUMP_TCC_ASSUMPTIONS_TOK "DUMP_TCC_ASSUMPTIONS" -%token DUMP_TCC_PROOF_TOK "DUMP_TCC_PROOF" -%token DUMP_CLOSURE_TOK "DUMP_CLOSURE" -%token DUMP_CLOSURE_PROOF_TOK "DUMP_CLOSURE_PROOF" -%token WHERE_TOK "WHERE" -%token ASSERTIONS_TOK "ASSERTIONS" -%token ASSUMPTIONS_TOK "ASSUMPTIONS" -%token COUNTEREXAMPLE_TOK "COUNTEREXAMPLE" -%token COUNTERMODEL_TOK "COUNTERMODEL" -%token PUSH_TOK "PUSH" -%token POP_TOK "POP" -%token POPTO_TOK "POPTO" -%token PUSH_SCOPE_TOK "PUSH_SCOPE" -%token POP_SCOPE_TOK "POP_SCOPE" -%token POPTO_SCOPE_TOK "POPTO_SCOPE" -%token RESET_TOK "RESET" -%token CONTEXT_TOK "CONTEXT" -%token FORGET_TOK "FORGET" -%token GET_TYPE_TOK "GET_TYPE" -%token CHECK_TYPE_TOK "CHECK_TYPE" -%token GET_CHILD_TOK "GET_CHILD" -%token GET_OP_TOK "GET_OP" -%token SUBSTITUTE_TOK "SUBSTITUTE" - -%nonassoc ASSIGN_TOK IN_TOK -%nonassoc FORALL_TOK EXISTS_TOK -%left IFF_TOK -%right IMPLIES_TOK -%left OR_TOK XOR_TOK -%left AND_TOK -%left NOT_TOK - -%nonassoc '=' NEQ_TOK -%nonassoc LE_TOK LT_TOK GE_TOK GT_TOK FLOOR_TOK -%left PLUS_TOK MINUS_TOK -%left MULT_TOK INTDIV_TOK DIV_TOK MOD_TOK -%left POW_TOK -%left WITH_TOK -%left UMINUS_TOK -%left CONCAT_TOK -%left MID_TOK -%left BVAND_TOK -%left BVXOR_TOK -%left BVNAND_TOK -%left BVNOR_TOK BVCOMP_TOK -%left BVXNOR_TOK -%left BVNEG_TOK -%left BVUMINUS_TOK BVPLUS_TOK BVSUB_TOK -%left BVUDIV_TOK BVSDIV_TOK BVUREM_TOK BVSREM_TOK BVSMOD_TOK BVSHL_TOK BVASHR_TOK BVLSHR_TOK -%left SX_TOK BVZEROEXTEND_TOK BVREPEAT_TOK BVROTL_TOK BVROTR_TOK -%left LEFTSHIFT_TOK RIGHTSHIFT_TOK -%nonassoc BVLT_TOK BVLE_TOK BVGT_TOK BVGE_TOK -%nonassoc BVSLT_TOK BVSLE_TOK BVSGT_TOK BVSGE_TOK -%right IS_INTEGER_TOK -%left ARROW_TOK - -%nonassoc '[' -%nonassoc '{' '.' '(' -%nonassoc BITVECTOR_TOK - -// %type <vec> FieldDecls TypeList IDs reverseIDs SingleDataTypes Constructors -// %type <vec> LetDecls TypeLetDecls BoundVarDecls ElseRest VarDecls -// %type <vec> Exprs AndExpr OrExpr Pattern Patterns -// %type <vec> RecordEntries UpdatePosition Updates - -// %type <node> Type /* IndexType */ TypeNotIdentifier TypeDef -// %type <node> DataType SingleDataType Constructor -// %type <node> FunctionType RecordType Real Int BitvectorType -// %type <node> FieldDecl TupleType -// %type <node> ArrayType ScalarType SubType BasicType SubrangeType -// %type <node> LeftBound RightBound -%type <expr> Expr // Conditional UpdatePositionNode Update Lambda -// %type <node> QuantExpr ArrayLiteral RecordLiteral RecordEntry TupleLiteral -// %type <node> LetDecl LetExpr LetDeclsNode -// %type <node> TypeLetDecl TypeLetExpr TypeLetDeclsNode -// %type <node> BoundVarDecl BoundVarDeclNode VarDecl -// %type <node> ConstDecl TypeDecl -%type <strlst> IdentifierList // StringLiteral Numeral Binary Hex -%type <str> Identifier // Type - -%type <cmd> cmd /// Assert Query Help Dbg Trace Option -// %type <node> Transform Print Call Echo DumpCommand -// %type <node> Include Where Push Pop PopTo -// %type <node> Context Forget Get_Child Get_Op Get_Type Check_Type Substitute -// %type <node> other_cmd -// %type <node> Arith_Var_Order - -%token <str> ID_TOK STRINGLIT_TOK NUMERAL_TOK HEX_TOK BINARY_TOK - -%% - -cmd: - ASSERT_TOK Expr { - $$ = new AssertCommand(*$2); - CVC4::parser::_global_parser_state->setCommand($$); - delete $2; - } - | QUERY_TOK Expr { - $$ = new QueryCommand(*$2); - CVC4::parser::_global_parser_state->setCommand($$); - delete $2; - } - | CHECKSAT_TOK Expr { - $$ = new CheckSatCommand(*$2); - CVC4::parser::_global_parser_state->setCommand($$); - delete $2; - } - | CHECKSAT_TOK { - $$ = new CheckSatCommand(); - CVC4::parser::_global_parser_state->setCommand($$); - } - | IdentifierList ':' Type { // variable/constant declaration - // FIXME: assuming Type is BOOLEAN - for(std::list<std::string>::iterator i = $1->begin(); i != $1->end(); ++i) - CVC4::parser::_global_parser_state->declareNewPredicate(*i); - delete $1; - CVC4::parser::_global_parser_state->setCommand(new EmptyCommand()); - } - | DONE_TOK { - CVC4::parser::_global_parser_state->setCommand(new EmptyCommand()); - CVC4::parser::_global_parser_state->setDone(); - YYACCEPT; - } - -Expr: - Identifier { - $$ = CVC4::parser::_global_parser_state->getNewVariableByName(*$1); - delete $1; - } - | TRUELIT_TOK { - $$ = new Expr(EXPR_MANAGER->mkExpr(TRUE)); - } - | FALSELIT_TOK { - $$ = new Expr(EXPR_MANAGER->mkExpr(FALSE)); - } - | Expr OR_TOK Expr { - $$ = new Expr(EXPR_MANAGER->mkExpr(OR, *$1, *$3)); - delete $1; - delete $3; - } - | Expr AND_TOK Expr { - $$ = new Expr(EXPR_MANAGER->mkExpr(AND, *$1, *$3)); - delete $1; - delete $3; - } - | Expr IMPLIES_TOK Expr { - $$ = new Expr(EXPR_MANAGER->mkExpr(IMPLIES, *$1, *$3)); - delete $1; - delete $3; - } - | Expr IFF_TOK Expr { - $$ = new Expr(EXPR_MANAGER->mkExpr(IFF, *$1, *$3)); - delete $1; - delete $3; - } - | NOT_TOK Expr { - $$ = new Expr(EXPR_MANAGER->mkExpr(NOT, *$2)); - delete $2; - } ; - -IdentifierList: - Identifier { - $$ = new std::list<std::string>; - $$->push_front(*$1); - delete $1; - } - | Identifier ',' IdentifierList { - $3->push_front(*$1); - $$ = $3; - delete $1; - } - -Identifier: - ID_TOK { - $$ = $1; - } - -Type: - BOOLEAN_TOK - -%% |