/********************* -*- 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"). **/ %{ #include "vc.h" #include "parser_exception.h" #include "parser_state.h" //#include "rational.h" // Exported shared data namespace CVC4 { extern ParserState* parserState; } // Define shortcuts for various things #define TMP CVC4::parserState #define EXPR CVC4::parserState->expr #define VC (CVC4::parserState->vc) #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::parserState->fileName << ":" << CVC4::parserState->lineNum << ": " << s; return CVC4::parserState->error(ss.str()); } namespace CVC4 { // File-static auxiliary funcion to wrap accessors upto the index i // (not inclusive) around "e". Used to rebuild the UPDATE expressions. static Expr wrapAccessors(const Expr& e, const std::vector& accessors, const int i) { DebugAssert((int)accessors.size() >= i, "wrapAccessors: too few accessors"); Expr res(e); for(int j=0; jlistExpr(acc, res); break; case RAW_LIST: DebugAssert(acc.arity() == 2 && acc[0].getKind() == ID, "PL.y: wrong number of arguments in the accessor of WITH: " +acc.toString()); res = VC->listExpr(acc[0], res, acc[1]); break; default: DebugAssert(false, "PL.y: Bad accessor in WITH: "+acc.toString()); } } return res; } // Convert a complex WITH statement into a bunch of nested simple UPDATEs // Updator "e1 WITH accessors := e2" is represented as // (e1 (accessor1 accessor2 ... ) e2), where the accessors are: // (READ idx) // ID (datatype constructor's argument) // (RECORD_SELECT ID) // and (TUPLE_SELECT num). // We rebuild this into nested RECORD_UPDATE, WRITE, // TUPLE_UPDATE, and DATATYPE_UPDATE expressions. For example: // // e WITH [idx] car.f := newVal is transformed into // e WITH [idx] := (e[idx] WITH car := (car(e[idx]) WITH .f := newVal)) // which is represented as // (WRITE e idx // (DATATYPE_UPDATE (READ e idx) car // (RECORD_UPDATE (car (READ e idx)) f newVal))). // Here "car" and "f" are identifiers (ID "car") and (ID "f"). static Expr PLprocessUpdate(const CVC4::Expr& e, const CVC4::Expr& update) { TRACE("parser verbose", "PLprocessUpdate(", e, ") {"); DebugAssert(update.arity() == 2,"PL.y: Bad WITH statement: " +update.toString()); // Rebuild accessors: resolve ID in (READ (ID "name")) and leave // the rest alone TRACE("parser verbose", "PLprocessUpdate: update[0] = ", update[0], ""); std::vector acc; for(Expr::iterator i=update[0].begin(), iend=update[0].end(); i!=iend; ++i) { TRACE("parser verbose", "*i = ", *i, ""); acc.push_back(*i); } TRACE("parser verbose", "acc.size() = ", acc.size(), ""); TRACE("parser verbose", "accessors = ", VC->listExpr(acc), ""); // 'res' serves as the accumulator of updators; initially it is // newVal (which is update[1]). We run through accessors in reverse // order, wrapping this accumulator with the corresponding // updators. Expr res(update[1]); // Rebuilding the original expression "e" // The main loop for(int i=acc.size()-1; i>=0; i--) { Expr ac(acc[i]); // The current accessor TRACE("parser verbose", "ac["+int2string(i)+"] = ", ac, ""); // "e" with all preceding accessors Expr tmp(wrapAccessors(e, acc, i)); TRACE("parser verbose", "tmp = ", tmp, ""); switch(ac.getKind()) { case ID: // Datatype update res = VC->listExpr("_DATATYPE_UPDATE", tmp, ac, res); break; case RAW_LIST: { const std::string& kind = ac[0][0].getString(); if(kind == "_READ") // Array update res = VC->listExpr("_WRITE", tmp, ac[1], res); else if(kind == "_RECORD_SELECT") // Record update res = VC->listExpr("_RECORD_UPDATE", tmp, ac[1], res); else if(kind == "_TUPLE_SELECT") // Tuple element res = VC->listExpr("_TUPLE_UPDATE", tmp, ac[1], res); else DebugAssert(false, "PL.y: Bad accessor in WITH: "+ac.toString()); break; } default: DebugAssert(false, "PL.y: Bad accessor in WITH: "+ac.toString()); } } TRACE("parser verbose", "PLprocessUpdate => ", res, " }"); return res; } // Process a vector of simultaneous updates (from a single WITH) static Expr PLprocessUpdates(const CVC4::Expr& e, const std::vector& updates, size_t idx=0) { // Processed all the updates if(idx >= updates.size()) return e; return PLprocessUpdates(PLprocessUpdate(e, updates[idx]), updates, idx+1); } } // end of namespace CVC4 #define YYLTYPE_IS_TRIVIAL 1 #define YYMAXDEPTH 10485760 /* Prefer YYERROR_VERBOSE over %error-verbose to avoid errors in older bison */ #define YYERROR_VERBOSE 1 %} %union { std::string *str; CVC4::Expr *node; std::vector *vec; int kind; }; %start cmd /* 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 FieldDecls TypeList IDs reverseIDs SingleDataTypes Constructors %type LetDecls TypeLetDecls BoundVarDecls ElseRest VarDecls %type Exprs AndExpr OrExpr Pattern Patterns %type RecordEntries UpdatePosition Updates %type Type /* IndexType */ TypeNotIdentifier TypeDef %type DataType SingleDataType Constructor %type FunctionType RecordType Real Int BitvectorType %type FieldDecl TupleType %type ArrayType ScalarType SubType BasicType SubrangeType %type LeftBound RightBound %type Expr Conditional UpdatePositionNode Update Lambda %type QuantExpr ArrayLiteral RecordLiteral RecordEntry TupleLiteral %type LetDecl LetExpr LetDeclsNode %type TypeLetDecl TypeLetExpr TypeLetDeclsNode %type BoundVarDecl BoundVarDeclNode VarDecl %type ConstDecl TypeDecl %type Identifier StringLiteral Numeral Binary Hex %type Assert Query Help Dbg Trace Option %type Transform Print Call Echo DumpCommand %type Include Where Push Pop PopTo %type Context Forget Get_Child Get_Op Get_Type Check_Type Substitute %type other_cmd %type Arith_Var_Order %token ID_TOK STRINGLIT_TOK NUMERAL_TOK HEX_TOK BINARY_TOK %% cmd : TypeDecl ';' { EXPR = *$1; delete $1; YYACCEPT; } | ConstDecl ';' { EXPR = *$1; delete $1; YYACCEPT; } | other_cmd ';' { EXPR = *$1; delete $1; YYACCEPT; } | ';' { EXPR = CVC4::Expr(); YYACCEPT; } | DONE_TOK { TMP->done = true; EXPR = CVC4::Expr(); YYACCEPT; } ; other_cmd : Assert { $$ = $1; } | Query { $$ = $1; } | Dbg { $$ = $1; } | Trace { $$ = $1; } | Option { $$ = $1; } | Help { $$ = $1; } | Transform { $$ = $1; } | Print { $$ = $1; } | Call { $$ = $1; } | Echo { $$ = $1; } | Include { $$ = $1; } | DumpCommand { $$ = $1; } | Where { $$ = $1; } | Push { $$ = $1; } | Pop { $$ = $1; } | PopTo { $$ = $1; } | Context { $$ = $1; } | Substitute { $$ = $1; } | Get_Child { $$ = $1; } | Get_Op { $$ = $1; } | Get_Type { $$ = $1; } | Check_Type { $$ = $1; } | Forget { $$ = $1; } | Arith_Var_Order { $$ = $1; } ; Arith_Var_Order : ARITH_VAR_ORDER_TOK '(' Exprs ')' { $$ = new CVC4::Expr(VC->listExpr("_ARITH_VAR_ORDER", *$3)); delete $3; } ; Assert : ASSERT_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_ASSERT", *$2)); delete $2; } ; Query : QUERY_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_QUERY", *$2)); delete $2; } | CHECKSAT_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_CHECKSAT", *$2)); delete $2; } | CHECKSAT_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_CHECKSAT"))); } | CONTINUE_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_CONTINUE"))); } | RESTART_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_RESTART", *$2)); delete $2; } ; Dbg : DBG_TOK StringLiteral { $$ = new CVC4::Expr(VC->listExpr("_DBG", *$2)); delete $2; } | DBG_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DBG"))); } ; Trace : TRACE_TOK StringLiteral { $$ = new CVC4::Expr(VC->listExpr("_TRACE", *$2)); delete $2; } | UNTRACE_TOK StringLiteral { $$ = new CVC4::Expr(VC->listExpr("_UNTRACE", *$2)); delete $2; } ; Option : OPTION_TOK StringLiteral Numeral { $$ = new CVC4::Expr(VC->listExpr("_OPTION", *$2, *$3)); delete $2; delete $3; } | OPTION_TOK StringLiteral MINUS_TOK Numeral { CVC4::Rational value= -$4->getRational(); CVC4::Expr e = CVC4::Expr(VC->ratExpr(value.toString())); $$ = new CVC4::Expr(VC->listExpr("_OPTION", *$2, e)); delete $2; delete $4; } | OPTION_TOK StringLiteral StringLiteral { $$ = new CVC4::Expr(VC->listExpr("_OPTION", *$2, *$3)); delete $2; delete $3; } ; Help : HELP_TOK StringLiteral { $$ = new CVC4::Expr(VC->listExpr("_HELP", *$2)); delete $2; } | HELP_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_HELP"))); } ; Transform : TRANSFORM_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_TRANSFORM", *$2)); delete $2; } ; Print : PRINT_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_PRINT", *$2)); delete $2; } | PRINT_TYPE_TOK Type { $$ = new CVC4::Expr(VC->listExpr("_PRINT", *$2)); delete $2; } ; Call : CALL_TOK Identifier Expr { $$ = new CVC4::Expr(VC->listExpr("_CALL", *$2, *$3)); delete $2; delete $3; } ; Echo : ECHO_TOK StringLiteral { $$ = new CVC4::Expr(VC->listExpr("_ECHO", *$2)); delete $2; } | ECHO_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_ECHO"))); } ; Include : INCLUDE_TOK StringLiteral { $$ = new CVC4::Expr(VC->listExpr("_INCLUDE", *$2)); delete $2; } ; DumpCommand : DUMP_PROOF_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_PROOF"))); } | DUMP_ASSUMPTIONS_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_ASSUMPTIONS"))); } | DUMP_SIG_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_SIG"))); } | DUMP_TCC_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_TCC"))); } | DUMP_TCC_ASSUMPTIONS_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_TCC_ASSUMPTIONS"))); } | DUMP_TCC_PROOF_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_TCC_PROOF"))); } | DUMP_CLOSURE_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_CLOSURE"))); } | DUMP_CLOSURE_PROOF_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_CLOSURE_PROOF"))); } ; Where : WHERE_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_WHERE"))); } | ASSERTIONS_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_ASSERTIONS"))); } | ASSUMPTIONS_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_ASSUMPTIONS"))); } | COUNTEREXAMPLE_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_COUNTEREXAMPLE"))); } | COUNTERMODEL_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_COUNTERMODEL"))); } ; Push : PUSH_TOK Numeral { $$ = new CVC4::Expr(VC->listExpr("_PUSH", *$2)); delete $2; } | PUSH_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_PUSH"))); } | PUSH_SCOPE_TOK Numeral { $$ = new CVC4::Expr(VC->listExpr("_PUSH_SCOPE", *$2)); delete $2; } | PUSH_SCOPE_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_PUSH_SCOPE"))); } ; Pop : POP_TOK Numeral { $$ = new CVC4::Expr(VC->listExpr("_POP", *$2)); delete $2; } | POP_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POP"))); } | POP_SCOPE_TOK Numeral { $$ = new CVC4::Expr(VC->listExpr("_POP_SCOPE", *$2)); delete $2; } | POP_SCOPE_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POP_SCOPE"))); } ; PopTo : POPTO_TOK Numeral { $$ = new CVC4::Expr(VC->listExpr("_POPTO", *$2)); delete $2; } | POPTO_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POPTO"))); } | POPTO_SCOPE_TOK Numeral { $$ = new CVC4::Expr(VC->listExpr("_POPTO_SCOPE", *$2)); delete $2; } | POPTO_SCOPE_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POPTO_SCOPE"))); } | RESET_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_RESET"))); } ; Context : CONTEXT_TOK StringLiteral { $$ = new CVC4::Expr(VC->listExpr("_CONTEXT", *$2)); delete $2; } | CONTEXT_TOK { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_CONTEXT"))); } ; Forget : FORGET_TOK Identifier { $$ = new CVC4::Expr(VC->listExpr("_FORGET", *$2)); delete $2; } ; Get_Type : GET_TYPE_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_GET_TYPE", *$2)); delete $2; } ; Check_Type : CHECK_TYPE_TOK Expr ':' Type { $$ = new CVC4::Expr(VC->listExpr("_CHECK_TYPE",*$2, *$4)); delete $2; delete $4; } ; Get_Child : GET_CHILD_TOK Expr Numeral { $$ = new CVC4::Expr(VC->listExpr("_GET_CHILD", *$2, *$3)); delete $2; delete $3; } ; Get_Op : GET_OP_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_GET_CHILD", *$2)); delete $2; } ; Substitute : SUBSTITUTE_TOK Identifier ':' Type '=' Expr '[' Identifier ASSIGN_TOK Expr ']' { std::vector tmp; tmp.push_back(*$2); tmp.push_back(*$4); tmp.push_back(*$6); tmp.push_back(*$8); tmp.push_back(*$10); $$ = new CVC4::Expr(VC->listExpr("_SUBSTITUTE", tmp)); delete $2; delete $4; delete $6; delete $8; delete $10; } ; Identifier : ID_TOK { $$ = new CVC4::Expr(VC->idExpr(*$1)); delete $1; } ; StringLiteral : STRINGLIT_TOK { $$ = new CVC4::Expr(VC->stringExpr(*$1)); delete $1; } ; Numeral : NUMERAL_TOK { $$ = new CVC4::Expr(VC->ratExpr((*$1))); delete $1; } ; Binary : BINARY_TOK { $$ = new CVC4::Expr (VC->listExpr("_BVCONST", VC->stringExpr(*$1))); delete $1; } ; Hex : HEX_TOK { $$ = new CVC4::Expr (VC->listExpr("_BVCONST", VC->stringExpr(*$1), VC->ratExpr(16))); delete $1; } ; /* Grammar for Types */ Type : Identifier { $$ = $1; } | TypeNotIdentifier { $$ = $1; } ; TypeNotIdentifier: ArrayType { $$ = $1; } | FunctionType { $$ = $1; } | BasicType { $$ = $1; } | SubrangeType { $$ = $1; } | TupleType { $$ = $1; } | RecordType { $$ = $1; } | TypeLetExpr { $$ = $1; } | BitvectorType {$$ = $1;} | SubType { $$ = $1; } | '(' Type ')' { $$ = $2; } ; TypeDef : Type { $$ = $1; } | ScalarType { $$ = $1; } ; DataType : DATATYPE_TOK SingleDataTypes END_TOK { $$ = new CVC4::Expr( VC->listExpr("_TYPEDEF", VC->listExpr("_DATATYPE", *$2))); delete $2; } ; SingleDataTypes : SingleDataType { $$ = new std::vector; $$->push_back(*$1); delete $1; } | SingleDataTypes ',' SingleDataType { $1->push_back(*$3); $$ = $1; delete $3; } ; SingleDataType : Identifier '=' Constructors { $$ = new CVC4::Expr(VC->listExpr(*$1, VC->listExpr(*$3))); delete $1; delete $3; } ; Constructors : Constructor { $$ = new std::vector; $$->push_back(*$1); delete $1; } | Constructors MID_TOK Constructor { $1->push_back(*$3); $$ = $1; delete $3; } ; Constructor : Identifier { $$ = new CVC4::Expr(VC->listExpr(*$1)); delete $1; } | Identifier '(' VarDecls ')' { CVC4::Expr tmp = VC->listExpr(*$3); $$ = new CVC4::Expr(VC->listExpr(*$1, tmp)); delete $1; delete $3; } ; VarDecls : VarDecl { $$ = new std::vector; $$->push_back(*$1); delete $1; } | VarDecls ',' VarDecl { $1->push_back(*$3); $$ = $1; delete $3; } ; VarDecl : Identifier ':' Type { $$ = new CVC4::Expr(VC->listExpr(*$1, *$3)); delete $1; delete $3; } ; FunctionType : '[' Type ARROW_TOK Type ']' { // Old style functions $$ = new CVC4::Expr(VC->listExpr("_OLD_ARROW", *$2, *$4)); delete $2; delete $4; } | Type ARROW_TOK Type { std::vector temp; temp.push_back(*$1); temp.push_back(*$3); $$ = new CVC4::Expr(VC->listExpr("_ARROW", temp)); delete $1; delete $3; } | '(' TypeList ')' ARROW_TOK Type { $2->push_back(*$5); $$ = new CVC4::Expr(VC->listExpr("_ARROW", *$2)); delete $2; delete $5; } ; RecordType : SQHASH_TOK FieldDecls HASHSQ_TOK { $$ = new CVC4::Expr(VC->listExpr(*$2)); delete $2; } ; FieldDecls : FieldDecl { $$ = new std::vector; $$->push_back(VC->idExpr("_RECORD_TYPE")); $$->push_back(*$1); delete $1; } | FieldDecls ',' FieldDecl { $1->push_back(*$3); $$ = $1; delete $3; } ; FieldDecl : Identifier ':' Type { $$ = new CVC4::Expr(VC->listExpr(*$1, *$3)); delete $1; delete $3; } ; TupleType : '[' TypeList ']' { $$ = new CVC4::Expr(VC->listExpr("_TUPLE_TYPE", *$2)); delete $2; } ; TypeList : Type ',' Type { $$ = new std::vector; $$->push_back(*$1); $$->push_back(*$3); delete $1; delete $3; } | TypeList ',' Type { $1->push_back(*$3); $$ = $1; delete $3; } ; /* IndexType : SubrangeType { $$ = $1; } */ /* | Real /\* WART: maybe change to INTEGER when we */ /* get that working? *\/ */ /* | Int */ /* { $$ = $1; } */ /* | Identifier { $$ = $1; } */ /* ; */ ArrayType : ARRAY_TOK Type OF_TOK Type { $$ = new CVC4::Expr(VC->listExpr("_ARRAY", *$2, *$4)); delete $2; delete $4; } ; ScalarType : '{' IDs '}' { std::vector::iterator theIter = $2->begin(); $2->insert(theIter, VC->idExpr("_SCALARTYPE")); $$ = new CVC4::Expr(VC->listExpr(*$2)); delete $2; } ; SubType : SUBTYPE_TOK '(' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_SUBTYPE", *$3)); delete $3; } | SUBTYPE_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_SUBTYPE", *$3, *$5)); delete $3; delete $5; } ; BasicType : BOOLEAN_TOK { $$ = new CVC4::Expr(VC->idExpr("_BOOLEAN")); } | Real | Int ; BitvectorType : BITVECTOR_TOK '(' Numeral ')' { $$ = new CVC4::Expr(VC->listExpr("_BITVECTOR", *$3)); delete $3; } ; Real : REAL_TOK { $$ = new CVC4::Expr(VC->idExpr("_REAL")); } ; Int : INT_TOK { $$ = new CVC4::Expr(VC->idExpr("_INT")); } ; SubrangeType : '[' LeftBound DOTDOT_TOK RightBound ']' { $$ = new CVC4::Expr(VC->listExpr("_SUBRANGE", *$2, *$4)); delete $2; delete $4; } ; LeftBound : '_' { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_NEGINF"))); } | Numeral { $$ = $1; } | MINUS_TOK Numeral { CVC4::Rational value= -$2->getRational(); $$ = new CVC4::Expr(VC->ratExpr(value.toString())); delete $2; } ; RightBound : '_' { $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POSINF"))); } | Numeral { $$ = $1; } | MINUS_TOK Numeral { CVC4::Rational value= -$2->getRational(); $$ = new CVC4::Expr(VC->ratExpr(value.toString())); delete $2; } ; /* right recursive to eliminate a conflict. Reverses order? */ reverseIDs : Identifier { $$ = new std::vector; $$->push_back(*$1); delete $1; } | Identifier ',' reverseIDs { $3->push_back(*$1); $$ = $3; delete $1; } ; IDs : reverseIDs { $$ = new std::vector($1->rbegin(), $1->rend()); delete $1; } ; /* Grammar for exprs */ Expr : Identifier { $$ = $1; } | Numeral { $$ = $1; } | Binary { $$ = $1; } | Hex { $$ = $1; } | Expr '(' Exprs ')' { std::vector tmp; tmp.push_back(*$1); tmp.insert(tmp.end(), $3->begin(), $3->end()); $$ = new CVC4::Expr(VC->listExpr(tmp)); delete $1; delete $3; } | SIMULATE_TOK '(' Exprs ')' { $$ = new CVC4::Expr(VC->listExpr("_SIMULATE", *$3)); delete $3; } | Expr '[' Expr ']' { $$ = new CVC4::Expr(VC->listExpr("_READ", *$1, *$3)); delete $1; delete $3; } | Expr '.' Identifier { $$ = new CVC4::Expr(VC->listExpr("_RECORD_SELECT", *$1, *$3)); delete $1; delete $3; } | Expr '.' Numeral { $$ = new CVC4::Expr(VC->listExpr("_TUPLE_SELECT", *$1, *$3)); delete $1; delete $3; } | Expr WITH_TOK Updates { $$ = new CVC4::Expr(CVC4::PLprocessUpdates(*$1, *$3)); delete $1; delete $3; } | Lambda { $$ = $1; } | QuantExpr { $$ = $1; } | LetExpr { $$ = $1; } | ArrayLiteral { $$ = $1; } | RecordLiteral { $$ = $1; } | TupleLiteral { $$ = $1; } | Conditional { $$ = $1; } | TRUELIT_TOK { $$ = new CVC4::Expr(VC->idExpr("_TRUE_EXPR")); } | FALSELIT_TOK { $$ = new CVC4::Expr(VC->idExpr("_FALSE_EXPR")); } | MINUS_TOK Expr %prec UMINUS_TOK { if ($2->isRational()) { CVC4::Rational value= -$2->getRational(); $$= new CVC4::Expr(VC->ratExpr(value.toString())); } else $$ = new CVC4::Expr(VC->listExpr("_UMINUS", *$2)); delete $2; } | NOT_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_NOT", *$2)); delete $2; } | IS_INTEGER_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_IS_INTEGER", *$2)); delete $2; } | TCC_TOK '(' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_TCC", *$3)); delete $3; } | Expr '=' Expr { $$ = new CVC4::Expr(VC->listExpr("_EQ", *$1, *$3)); delete $1; delete $3; } | Expr NEQ_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_NEQ", *$1, *$3)); delete $1; delete $3; } | Expr XOR_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_XOR", *$1, *$3)); delete $1; delete $3; } | OrExpr %prec OR_TOK { $$ = new CVC4::Expr(VC->listExpr("_OR", *$1)); delete $1; } | AndExpr %prec AND_TOK { $$ = new CVC4::Expr(VC->listExpr("_AND", *$1)); delete $1; } | Expr IMPLIES_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_IMPLIES", *$1, *$3)); delete $1; delete $3; } | Expr IFF_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_IFF", *$1, *$3)); delete $1; delete $3; } | Expr PLUS_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_PLUS", *$1, *$3)); delete $1; delete $3; } | Expr MINUS_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_MINUS", *$1, *$3)); delete $1; delete $3; } | Expr MULT_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_TRANS_CLOSURE", *$1, *$4, *$6)); delete $1; delete $4; delete $6; } | Expr MULT_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_MULT", *$1, *$3)); delete $1; delete $3; } | Expr POW_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_POW", *$3, *$1)); delete $1; delete $3; } | Expr DIV_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_DIVIDE", *$1, *$3)); delete $1; delete $3; } // | Expr INTDIV_TOK Expr // { // $$ = new CVC4::Expr(VC->listExpr("_INTDIV", *$1, *$3)); // delete $1; // delete $3; // } // | Expr MOD_TOK Expr // { // $$ = new CVC4::Expr(VC->listExpr("_MOD", *$1, *$3)); // delete $1; // delete $3; // } | Expr GT_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_GT", *$1, *$3)); delete $1; delete $3; } | Expr GE_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_GE", *$1, *$3)); delete $1; delete $3; } | FLOOR_TOK '(' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_FLOOR", *$3)); delete $3; } | Expr LT_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_LT", *$1, *$3)); delete $1; delete $3; } | Expr LE_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_LE", *$1, *$3)); delete $1; delete $3; } | '(' Expr ')' { $$ = $2; } | BVNEG_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_BVNEG", *$2)); delete $2; } | Expr '[' NUMERAL_TOK ':' NUMERAL_TOK ']' { $$ = new CVC4::Expr (VC->listExpr("_EXTRACT", VC->ratExpr(*$3), VC->ratExpr(*$5), *$1)); delete $1; delete $3; delete $5; } | Expr BVAND_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_BVAND", *$1, *$3)); delete $1; delete $3; } | Expr MID_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_BVOR", *$1, *$3)); delete $1; delete $3; } | Expr LEFTSHIFT_TOK NUMERAL_TOK { $$ = new CVC4::Expr (VC->listExpr("_LEFTSHIFT", *$1, VC->ratExpr(*$3))); delete $1; delete $3; } | Expr RIGHTSHIFT_TOK NUMERAL_TOK { $$ = new CVC4::Expr (VC->listExpr("_RIGHTSHIFT", *$1, VC->ratExpr(*$3))); delete $1; delete $3; } | BVXOR_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVXOR", *$3, *$5)); delete $3; delete $5; } | BVNAND_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVNAND", *$3, *$5)); delete $3; delete $5; } | BVNOR_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVNOR", *$3, *$5)); delete $3; delete $5; } | BVCOMP_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVCOMP", *$3, *$5)); delete $3; delete $5; } | BVXNOR_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVXNOR", *$3, *$5)); delete $3; delete $5; } | SX_TOK '(' Expr ',' NUMERAL_TOK ')' { $$ = new CVC4::Expr(VC->listExpr("_SX",*$3,VC->ratExpr(*$5))); delete $3; delete $5; } | BVZEROEXTEND_TOK '(' Expr ',' NUMERAL_TOK ')' { $$ = new CVC4::Expr(VC->listExpr("_BVZEROEXTEND",VC->ratExpr(*$5),*$3)); delete $3; delete $5; } | BVREPEAT_TOK '(' Expr ',' NUMERAL_TOK ')' { $$ = new CVC4::Expr(VC->listExpr("_BVREPEAT",VC->ratExpr(*$5),*$3)); delete $3; delete $5; } | BVROTL_TOK '(' Expr ',' NUMERAL_TOK ')' { $$ = new CVC4::Expr(VC->listExpr("_BVROTL",VC->ratExpr(*$5),*$3)); delete $3; delete $5; } | BVROTR_TOK '(' Expr ',' NUMERAL_TOK ')' { $$ = new CVC4::Expr(VC->listExpr("_BVROTR",VC->ratExpr(*$5),*$3)); delete $3; delete $5; } | BVLT_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVLT", *$3, *$5)); delete $3; delete $5; } | BVGT_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVGT", *$3, *$5)); delete $3; delete $5; } | BVLE_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVLE", *$3, *$5)); delete $3; delete $5; } | BVGE_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVGE", *$3, *$5)); delete $3; delete $5; } | BVSLT_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVSLT", *$3, *$5)); delete $3; delete $5; } | BVSGT_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVSGT", *$3, *$5)); delete $3; delete $5; } | BVSLE_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVSLE", *$3, *$5)); delete $3; delete $5; } | BVSGE_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVSGE", *$3, *$5)); delete $3; delete $5; } | Expr CONCAT_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_CONCAT", *$1, *$3)); delete $1; delete $3; } | INTTOBV_TOK '(' Expr ',' NUMERAL_TOK ',' NUMERAL_TOK ')' { $$ = new CVC4::Expr (VC->listExpr("_INTTOBV", *$3, VC->ratExpr(*$5), VC->ratExpr(*$7))); delete $3; delete $5; delete $7; } | BVTOINT_TOK '(' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVTOINT", *$3)); delete $3; } | BOOLEXTRACT_TOK '(' Expr ',' NUMERAL_TOK ')' { //FIXME: this function is not to be exposed //to the user counterexamples containing //this function can be translated into //BV-EXTRACT and comparison with 0 or 1 $$ = new CVC4::Expr(VC->listExpr("_BOOLEXTRACT", *$3, VC->ratExpr(*$5))); delete $3; delete $5; } | BVPLUS_TOK '(' NUMERAL_TOK ',' Exprs ')' { std::vector k; k.push_back(VC->ratExpr(*$3)); k.insert(k.end(), $5->begin(), $5->end()); $$ = new CVC4::Expr(VC->listExpr("_BVPLUS", k)); delete $3; delete $5; } | BVSUB_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' { $$ = new CVC4::Expr (VC->listExpr("_BVSUB", VC->ratExpr(*$3), *$5, *$7)); delete $3; delete $5; delete $7; } | BVUDIV_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr (VC->listExpr("_BVUDIV", *$3, *$5)); delete $3; delete $5; } | BVSDIV_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr (VC->listExpr("_BVSDIV", *$3, *$5)); delete $3; delete $5; } | BVUREM_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr (VC->listExpr("_BVUREM", *$3, *$5)); delete $3; delete $5; } | BVSREM_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr (VC->listExpr("_BVSREM", *$3, *$5)); delete $3; delete $5; } | BVSMOD_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr (VC->listExpr("_BVSMOD", *$3, *$5)); delete $3; delete $5; } | BVSHL_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr (VC->listExpr("_BVSHL", *$3, *$5)); delete $3; delete $5; } | BVASHR_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr (VC->listExpr("_BVASHR", *$3, *$5)); delete $3; delete $5; } | BVLSHR_TOK '(' Expr ',' Expr ')' { $$ = new CVC4::Expr (VC->listExpr("_BVLSHR", *$3, *$5)); delete $3; delete $5; } | BVUMINUS_TOK '(' Expr ')' { $$ = new CVC4::Expr(VC->listExpr("_BVUMINUS", *$3)); delete $3; } | BVMULT_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' { $$ = new CVC4::Expr (VC->listExpr("_BVMULT", VC->ratExpr(*$3), *$5, *$7)); delete $3; delete $5; delete $7; } | DISTINCT_TOK '(' Exprs ')' { $$ = new CVC4::Expr(VC->listExpr("_DISTINCT", *$3)); delete $3; } ; AndExpr : AndExpr AND_TOK Expr { $1->push_back(*$3); $$ = $1; delete $3; } | Expr AND_TOK Expr { $$ = new std::vector; $$->push_back(*$1); $$->push_back(*$3); delete $1; delete $3; } ; OrExpr : OrExpr OR_TOK Expr { $1->push_back(*$3); $$ = $1; delete $3; } | Expr OR_TOK Expr { $$ = new std::vector; $$->push_back(*$1); $$->push_back(*$3); delete $1; delete $3; } ; Conditional : IF_TOK Expr THEN_TOK Expr ElseRest { $5->push_back(VC->listExpr(*$2, *$4)); $5->push_back(VC->idExpr("_COND")); /* at this point, the list for ElseRest is in reverse order from what it should be. */ std::vector tmp; tmp.insert(tmp.end(), $5->rbegin(), $5->rend()); $$ = new CVC4::Expr(VC->listExpr(tmp)); delete $2; delete $4; delete $5; } ; ElseRest : ELSE_TOK Expr ENDIF_TOK { $$ = new std::vector; $$->push_back(VC->listExpr("_ELSE",*$2)); delete $2; } | ELSIF_TOK Expr THEN_TOK Expr ElseRest { /* NOTE that we're getting the list built up in the reverse order here. We'll fix things when we produce a Conditional. */ $5->push_back(VC->listExpr(*$2, *$4)); $$ = $5; delete $2; delete $4; } ; Exprs : Expr { $$ = new std::vector; $$->push_back(*$1); delete $1; } | Exprs ',' Expr { $1->push_back(*$3); $$ = $1; delete $3; } ; Pattern : PATTERN_TOK '(' Exprs ')' ':' { $$ = $3; } Patterns : Pattern { $$ = new std::vector; $$->push_back(VC->listExpr(*$1)); delete $1; } | Patterns Pattern { $1->push_back(VC->listExpr(*$2)); $$ = $1; delete $2; } ; Update : UpdatePositionNode ASSIGN_TOK Expr { $$ = new CVC4::Expr(VC->listExpr(*$1, *$3)); delete $1; delete $3; } ; Updates : Update { $$ = new std::vector; $$->push_back(*$1); delete $1; } | Updates ',' Update { $$->push_back(*$3); delete $3; } ; UpdatePositionNode : UpdatePosition { $$ = new CVC4::Expr(VC->listExpr(*$1)); delete $1; } ; UpdatePosition : '[' Expr ']' { $$ = new std::vector; $$->push_back(VC->listExpr("_READ", *$2)); delete $2; } | Identifier { $$ = new std::vector; $$->push_back(*$1); delete $1; } | '.' Identifier { $$ = new std::vector; $$->push_back(VC->listExpr("_RECORD_SELECT", *$2)); delete $2; } | '.' Numeral { $$ = new std::vector; $$->push_back(VC->listExpr("_TUPLE_SELECT", *$2)); delete $2; } | UpdatePosition '[' Expr ']' { $1->push_back(VC->listExpr("_READ", *$3)); $$ = $1; delete $3; } | UpdatePosition Identifier { $1->push_back(*$2); $$ = $1; delete $2; } | UpdatePosition '.' Identifier { $1->push_back(VC->listExpr("_RECORD_SELECT",*$3)); $$ = $1; delete $3; } | UpdatePosition '.' Numeral { $1->push_back(VC->listExpr("_TUPLE_SELECT", *$3)); $$ = $1; delete $3; } ; Lambda : LAMBDA_TOK '(' BoundVarDecls ')' ':' Expr %prec ASSIGN_TOK { $$ = new CVC4::Expr(VC->listExpr("_LAMBDA", VC->listExpr(*$3), (*$6))); delete $3; delete $6; } ; QuantExpr : FORALL_TOK '(' BoundVarDecls ')' ':' Expr %prec FORALL_TOK { $$ = new CVC4::Expr(VC->listExpr("_FORALL", VC->listExpr(*$3), *$6)); delete $3; delete $6; } | FORALL_TOK '(' BoundVarDecls ')' ':' Patterns Expr %prec FORALL_TOK { $$ = new CVC4::Expr(VC->listExpr("_FORALL", VC->listExpr(*$3), *$7, VC->listExpr(*$6))); delete $3; delete $6; delete $7; } | EXISTS_TOK '(' BoundVarDecls ')' ':' Expr %prec EXISTS_TOK { $$ = new CVC4::Expr(VC->listExpr("_EXISTS", VC->listExpr(*$3), (*$6))); delete $3; delete $6; } ; | EXISTS_TOK '(' BoundVarDecls ')' ':' Patterns Expr %prec EXISTS_TOK { $$ = new CVC4::Expr(VC->listExpr("_EXISTS", VC->listExpr(*$3), *$7, VC->listExpr(*$6))); delete $3; delete $6; delete $7; } ArrayLiteral : ARRAY_TOK '(' BoundVarDecl ')' ':' Expr %prec ASSIGN_TOK { $$ = new CVC4::Expr (VC->listExpr("_ARRAY_LITERAL", *$3, *$6)); delete $3; delete $6; } ; RecordLiteral : PARENHASH_TOK RecordEntries HASHPAREN_TOK { $2->insert($2->begin(), VC->idExpr("_RECORD")); $$ = new CVC4::Expr(VC->listExpr(*$2)); delete $2; } ; RecordEntries : RecordEntry { $$ = new std::vector; $$->push_back(*$1); delete $1; } | RecordEntries ',' RecordEntry { $1->push_back(*$3); $$ = $1; delete $3; } ; RecordEntry : Identifier ASSIGN_TOK Expr { $$ = new CVC4::Expr(VC->listExpr(*$1, *$3)); delete $1; delete $3; } ; TupleLiteral : '(' Exprs ',' Expr ')' { $2->push_back(*$4); $2->insert($2->begin(),VC->idExpr("_TUPLE")); $$ = new CVC4::Expr(VC->listExpr(*$2)); delete $2; delete $4; } ; LetDeclsNode : LetDecls { $$ = new CVC4::Expr(VC->listExpr(*$1)); delete $1; } ; LetDecls : LetDecl { $$ = new std::vector; $$->push_back(*$1); delete $1; } | LetDecls ',' LetDecl { $1->push_back(*$3); $$ = $1; delete $3; } ; LetDecl : Identifier '=' Expr { $$ = new CVC4::Expr(VC->listExpr(*$1,*$3)); delete $1; delete $3; } | Identifier ':' Type '=' Expr { $$ = new CVC4::Expr(VC->listExpr(*$1,*$5)); delete $1; delete $3; delete $5; } ; LetExpr : LET_TOK LetDeclsNode IN_TOK Expr { $$ = new CVC4::Expr(VC->listExpr("_LET", *$2, *$4)); delete $2; delete $4; } ; TypeLetDeclsNode : TypeLetDecls { $$ = new CVC4::Expr(VC->listExpr(*$1)); delete $1; } ; TypeLetDecls : TypeLetDecl { $$ = new std::vector; $$->push_back(*$1); delete $1; } | TypeLetDecls ',' TypeLetDecl { $1->push_back(*$3); $$ = $1; delete $3; } ; TypeLetDecl : Identifier '=' Type { $$ = new CVC4::Expr(VC->listExpr(*$1, *$3)); delete $1; delete $3; } | Identifier ':' TYPE_TOK '=' Type { $$ = new CVC4::Expr(VC->listExpr(*$1,*$5)); delete $1; delete $5; } ; TypeLetExpr : LET_TOK TypeLetDeclsNode IN_TOK Type { $$ = new CVC4::Expr(VC->listExpr("_LET", *$2, *$4)); delete $2; delete $4; } ; BoundVarDecl : IDs ':' Type { $1->push_back(*$3); delete $3; $$ = new CVC4::Expr(VC->listExpr(*$1)); delete $1; } ; BoundVarDecls : BoundVarDecl { $$ = new std::vector; $$->push_back(*$1); delete $1; } | BoundVarDecls ',' BoundVarDecl { $1->push_back(*$3); $$ = $1; delete $3; } ; BoundVarDeclNode: BoundVarDecls { $$ = new CVC4::Expr(VC->listExpr(*$1)); delete $1; } ; ConstDecl : Identifier ':' Type '=' Expr { $$ = new CVC4::Expr(VC->listExpr("_CONST", *$1, *$3, *$5)); delete $1; delete $3; delete $5; } | Identifier ':' Type { $$ =new CVC4::Expr (VC->listExpr("_CONST", VC->listExpr(*$1), *$3)); delete $1; delete $3; } | Identifier '(' BoundVarDeclNode ')' ':' Type '=' Expr { std::vector tmp; tmp.push_back(VC->idExpr("_DEFUN")); tmp.push_back(*$1); tmp.push_back(*$3); tmp.push_back(*$6); tmp.push_back(*$8); $$ = new CVC4::Expr(VC->listExpr(tmp)); delete $1; delete $3; delete $6; delete $8; } | Identifier '(' BoundVarDeclNode ')' ':' Type { std::vector tmp; tmp.push_back(VC->idExpr("_DEFUN")); tmp.push_back(*$1); tmp.push_back(*$3); tmp.push_back(*$6); $$ = new CVC4::Expr(VC->listExpr(tmp)); delete $1; delete $3; delete $6; } | Identifier ',' IDs ':' Type { $3->insert($3->begin(), *$1); $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$3), *$5)); delete $1; delete $3; delete $5; } ; TypeDecl : DataType { $$ = $1; } | Identifier ':' TYPE_TOK '=' TypeDef { $$ = new CVC4::Expr(VC->listExpr("_TYPEDEF", *$1, *$5)); delete $1; delete $5; } | Identifier ':' TYPE_TOK { $$ =new CVC4::Expr(VC->listExpr("_TYPE", *$1)); delete $1; } | Identifier ',' IDs ':' TYPE_TOK { std::vector tmp; tmp.push_back(*$1); tmp.insert(tmp.end(), $3->begin(), $3->end()); $$ = new CVC4::Expr(VC->listExpr("_TYPE", tmp)); delete $1; delete $3; } ; %%