src/parser/cvc/Cvc.g

   1 /* *******************                                                        */
   2 /*! \file Cvc.g
   3  ** \verbatim
   4  ** Original author: Christopher L. Conway
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): Tim King, Andrew Reynolds, Dejan Jovanovic
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Parser for CVC presentation input language
  13  **
  14  ** Parser for CVC presentation input language.
  15  **/
  16
  17 grammar Cvc;
  18
  19 options {
  20   // C output for antlr
  21   language = 'C';
  22
  23   // Skip the default error handling, just break with exceptions
  24   // defaultErrorHandler = false;
  25
  26   // Only lookahead of <= k requested (disable for LL* parsing)
  27   // Note that CVC4's BoundedTokenBuffer requires a fixed k !
  28   // If you change this k, change it also in cvc_input.cpp !
  29   k = 3;
  30 }/* options */
  31
  32 tokens {
  33   /* commands */
  34
  35   ASSERT_TOK = 'ASSERT';
  36   QUERY_TOK = 'QUERY';
  37   CHECKSAT_TOK = 'CHECKSAT';
  38   OPTION_TOK = 'OPTION';
  39   PUSH_TOK = 'PUSH';
  40   POP_TOK = 'POP';
  41   POPTO_TOK = 'POPTO';
  42   PUSH_SCOPE_TOK = 'PUSH_SCOPE';
  43   POP_SCOPE_TOK = 'POP_SCOPE';
  44   POPTO_SCOPE_TOK = 'POPTO_SCOPE';
  45   RESET_TOK = 'RESET';
  46   DATATYPE_TOK = 'DATATYPE';
  47   END_TOK = 'END';
  48   CONTEXT_TOK = 'CONTEXT';
  49   FORGET_TOK = 'FORGET';
  50   GET_TYPE_TOK = 'GET_TYPE';
  51   CHECK_TYPE_TOK = 'CHECK_TYPE';
  52   GET_CHILD_TOK = 'GET_CHILD';
  53   GET_OP_TOK = 'GET_OP';
  54   GET_VALUE_TOK = 'GET_VALUE';
  55   SUBSTITUTE_TOK = 'SUBSTITUTE';
  56   DBG_TOK = 'DBG';
  57   TRACE_TOK = 'TRACE';
  58   UNTRACE_TOK = 'UNTRACE';
  59   HELP_TOK = 'HELP';
  60   TRANSFORM_TOK = 'TRANSFORM';
  61   PRINT_TOK = 'PRINT';
  62   PRINT_TYPE_TOK = 'PRINT_TYPE';
  63   CALL_TOK = 'CALL';
  64   ECHO_TOK = 'ECHO';
  65   EXIT_TOK = 'EXIT';
  66   INCLUDE_TOK = 'INCLUDE';
  67   DUMP_PROOF_TOK = 'DUMP_PROOF';
  68   DUMP_ASSUMPTIONS_TOK = 'DUMP_ASSUMPTIONS';
  69   DUMP_SIG_TOK = 'DUMP_SIG';
  70   DUMP_TCC_TOK = 'DUMP_TCC';
  71   DUMP_TCC_ASSUMPTIONS_TOK = 'DUMP_TCC_ASSUMPTIONS';
  72   DUMP_TCC_PROOF_TOK = 'DUMP_TCC_PROOF';
  73   DUMP_CLOSURE_TOK = 'DUMP_CLOSURE';
  74   DUMP_CLOSURE_PROOF_TOK = 'DUMP_CLOSURE_PROOF';
  75   WHERE_TOK = 'WHERE';
  76   ASSERTIONS_TOK = 'ASSERTIONS';
  77   ASSUMPTIONS_TOK = 'ASSUMPTIONS';
  78   COUNTEREXAMPLE_TOK = 'COUNTEREXAMPLE';
  79   COUNTERMODEL_TOK = 'COUNTERMODEL';
  80   ARITH_VAR_ORDER_TOK = 'ARITH_VAR_ORDER';
  81
  82   /* operators */
  83
  84   AND_TOK = 'AND';
  85   BOOLEAN_TOK = 'BOOLEAN';
  86   ELSEIF_TOK = 'ELSIF';
  87   ELSE_TOK = 'ELSE';
  88   ENDIF_TOK = 'ENDIF';
  89   FALSE_TOK = 'FALSE';
  90   IF_TOK = 'IF';
  91   IN_TOK = 'IN';
  92   INT_TOK = 'INT';
  93   LET_TOK = 'LET';
  94   NOT_TOK = 'NOT';
  95   OR_TOK = 'OR';
  96   REAL_TOK = 'REAL';
  97   THEN_TOK = 'THEN';
  98   TRUE_TOK = 'TRUE';
  99   TYPE_TOK = 'TYPE';
 100   XOR_TOK = 'XOR';
 101
 102   ARRAY_TOK = 'ARRAY';
 103   OF_TOK = 'OF';
 104   WITH_TOK = 'WITH';
 105
 106   SUBTYPE_TOK = 'SUBTYPE';
 107
 108   FORALL_TOK = 'FORALL';
 109   EXISTS_TOK = 'EXISTS';
 110   PATTERN_TOK = 'PATTERN';
 111
 112   LAMBDA = 'LAMBDA';
 113
 114   // Symbols
 115
 116   COLON = ':';
 117   COMMA = ',';
 118   LPAREN = '(';
 119   RPAREN = ')';
 120   LBRACE = '{';
 121   RBRACE = '}';
 122   LBRACKET = '[';
 123   RBRACKET = ']';
 124   SEMICOLON = ';';
 125   BAR = '|';
 126   UNDERSCORE = '_';
 127
 128   SQHASH = '[#';
 129   HASHSQ = '#]';
 130   PARENHASH = '(#';
 131   HASHPAREN = '#)';
 132
 133   // Operators
 134
 135   ARROW_TOK = '->';
 136   DIV_TOK = '/';
 137   EQUAL_TOK = '=';
 138   DISEQUAL_TOK = '/=';
 139   EXP_TOK = '^';
 140   GT_TOK = '>';
 141   GEQ_TOK = '>=';
 142   IFF_TOK = '<=>';
 143   IMPLIES_TOK = '=>';
 144   LT_TOK = '<';
 145   LEQ_TOK = '<=';
 146   MINUS_TOK = '-';
 147   PLUS_TOK = '+';
 148   STAR_TOK = '*';
 149   ASSIGN_TOK = ':=';
 150   MOD_TOK = 'MOD';
 151   INTDIV_TOK = 'DIV';
 152   FLOOR_TOK = 'FLOOR';
 153   DISTINCT_TOK = 'DISTINCT';
 154
 155   // Bitvectors
 156
 157   BITVECTOR_TOK = 'BITVECTOR';
 158   LEFTSHIFT_TOK = '<<';
 159   RIGHTSHIFT_TOK = '>>';
 160   BVPLUS_TOK = 'BVPLUS';
 161   BVSUB_TOK = 'BVSUB';
 162   BVUDIV_TOK = 'BVUDIV';
 163   BVSDIV_TOK = 'BVSDIV';
 164   BVUREM_TOK = 'BVUREM';
 165   BVSREM_TOK = 'BVSREM';
 166   BVSMOD_TOK = 'BVSMOD';
 167   BVSHL_TOK = 'BVSHL';
 168   BVASHR_TOK = 'BVASHR';
 169   BVLSHR_TOK = 'BVLSHR';
 170   BVUMINUS_TOK = 'BVUMINUS';
 171   BVMULT_TOK = 'BVMULT';
 172   BVNEG_TOK = '~';
 173   BVAND_TOK = '&';
 174   BVXOR_TOK = 'BVXOR';
 175   BVNAND_TOK = 'BVNAND';
 176   BVNOR_TOK = 'BVNOR';
 177   BVCOMP_TOK = 'BVCOMP';
 178   BVXNOR_TOK = 'BVXNOR';
 179   CONCAT_TOK = '@';
 180   //BVTOINT_TOK = 'BVTOINT';
 181   //INTTOBV_TOK = 'INTTOBV';
 182   //BOOLEXTRACT_TOK = 'BOOLEXTRACT';
 183   //IS_INTEGER_TOK = 'IS_INTEGER';
 184   BVLT_TOK = 'BVLT';
 185   BVGT_TOK = 'BVGT';
 186   BVLE_TOK = 'BVLE';
 187   BVGE_TOK = 'BVGE';
 188   SX_TOK = 'SX';
 189   BVZEROEXTEND_TOK = 'BVZEROEXTEND';
 190   BVREPEAT_TOK = 'BVREPEAT';
 191   BVROTL_TOK = 'BVROTL';
 192   BVROTR_TOK = 'BVROTR';
 193   BVSLT_TOK = 'BVSLT';
 194   BVSGT_TOK = 'BVSGT';
 195   BVSLE_TOK = 'BVSLE';
 196   BVSGE_TOK = 'BVSGE';
 197
 198   // these are parsed by special NUMBER_OR_RANGEOP rule, below
 199   DECIMAL_LITERAL;
 200   INTEGER_LITERAL;
 201   DOT;
 202   DOTDOT;
 203 }/* tokens */
 204
 205 @parser::members {
 206
 207 // Idea and code guidance from Sam Harwell,
 208 // http://www.antlr.org/wiki/display/ANTLR3/Operator+precedence+parser
 209
 210 bool isRightToLeft(int type) {
 211   // return true here for any operators that are right-to-left associative
 212   switch(type) {
 213   case IMPLIES_TOK: return true;
 214   default: return false;
 215   }
 216 }/* isRightToLeft() */
 217
 218 int getOperatorPrecedence(int type) {
 219   switch(type) {
 220   case BITVECTOR_TOK: return 1;
 221   //case DOT:
 222   case LPAREN:
 223   case LBRACE: return 2;
 224   case LBRACKET: return 3;
 225   case ARROW_TOK: return 4;
 226   //case IS_INTEGER_TOK: return 5;
 227   case BVSLT_TOK:
 228   case BVSLE_TOK:
 229   case BVSGT_TOK:
 230   case BVSGE_TOK: return 6;
 231   case BVLT_TOK:
 232   case BVLE_TOK:
 233   case BVGT_TOK:
 234   case BVGE_TOK: return 7;
 235   case LEFTSHIFT_TOK:
 236   case RIGHTSHIFT_TOK: return 8;
 237   case SX_TOK:
 238   case BVZEROEXTEND_TOK:
 239   case BVREPEAT_TOK:
 240   case BVROTL_TOK:
 241   case BVROTR_TOK: return 9;
 242   case BVUDIV_TOK:
 243   case BVSDIV_TOK:
 244   case BVUREM_TOK:
 245   case BVSREM_TOK:
 246   case BVSMOD_TOK:
 247   case BVSHL_TOK:
 248   case BVASHR_TOK:
 249   case BVLSHR_TOK: return 10;
 250   case BVUMINUS_TOK:
 251   case BVPLUS_TOK:
 252   case BVSUB_TOK: return 11;
 253   case BVNEG_TOK: return 12;
 254   case BVXNOR_TOK: return 13;
 255   case BVNOR_TOK:
 256   case BVCOMP_TOK: return 14;
 257   case BVNAND_TOK: return 15;
 258   case BVXOR_TOK: return 16;
 259   case BVAND_TOK: return 17;
 260   case BAR: return 18;
 261   case CONCAT_TOK: return 19;
 262 //case UMINUS_TOK: return 20;
 263   case WITH_TOK: return 21;
 264   case EXP_TOK: return 22;
 265   case STAR_TOK:
 266   case INTDIV_TOK:
 267   case DIV_TOK:
 268   case MOD_TOK: return 23;
 269   case PLUS_TOK:
 270   case MINUS_TOK: return 24;
 271   case LEQ_TOK:
 272   case LT_TOK:
 273   case GEQ_TOK:
 274   case GT_TOK: return 25;
 275   case EQUAL_TOK:
 276   case DISEQUAL_TOK: return 26;
 277   case NOT_TOK: return 27;
 278   case AND_TOK: return 28;
 279   case OR_TOK:
 280   case XOR_TOK: return 29;
 281   case IMPLIES_TOK: return 30;// right-to-left
 282   case IFF_TOK: return 31;
 283   case FORALL_TOK:
 284   case EXISTS_TOK: return 32;
 285   case ASSIGN_TOK:
 286   case IN_TOK: return 33;
 287
 288   default:
 289     std::stringstream ss;
 290     ss << "internal error: no entry in precedence table for operator " << CvcParserTokenNames[type];
 291     throw ParserException(ss.str());
 292   }
 293 }/* getOperatorPrecedence() */
 294
 295 Kind getOperatorKind(int type, bool& negate) {
 296   negate = false;
 297
 298   switch(type) {
 299     // booleanBinop
 300   case IFF_TOK: return kind::IFF;
 301   case IMPLIES_TOK: return kind::IMPLIES;
 302   case OR_TOK: return kind::OR;
 303   case XOR_TOK: return kind::XOR;
 304   case AND_TOK: return kind::AND;
 305
 306     // comparisonBinop
 307   case EQUAL_TOK: return kind::EQUAL;
 308   case DISEQUAL_TOK: negate = true; return kind::EQUAL;
 309   case GT_TOK: return kind::GT;
 310   case GEQ_TOK: return kind::GEQ;
 311   case LT_TOK: return kind::LT;
 312   case LEQ_TOK: return kind::LEQ;
 313
 314     // arithmeticBinop
 315   case PLUS_TOK: return kind::PLUS;
 316   case MINUS_TOK: return kind::MINUS;
 317   case STAR_TOK: return kind::MULT;
 318   case INTDIV_TOK: return kind::INTS_DIVISION;
 319   case MOD_TOK: return kind::INTS_MODULUS;
 320   case DIV_TOK: return kind::DIVISION;
 321   case EXP_TOK: return kind::POW;
 322
 323     // bvBinop
 324   case CONCAT_TOK: return kind::BITVECTOR_CONCAT;
 325   case BAR: return kind::BITVECTOR_OR;
 326   case BVAND_TOK: return kind::BITVECTOR_AND;
 327   }
 328
 329   std::stringstream ss;
 330   ss << "internal error: no entry in operator-kind table for operator " << CvcParserTokenNames[type];
 331   throw ParserException(ss.str());
 332
 333 }/* getOperatorKind() */
 334
 335 unsigned findPivot(const std::vector<unsigned>& operators,
 336                    unsigned startIndex, unsigned stopIndex) {
 337   unsigned pivot = startIndex;
 338   unsigned pivotRank = getOperatorPrecedence(operators[pivot]);
 339   /*Debug("prec") << "initial pivot at " << pivot
 340                 << "(" << CvcParserTokenNames[operators[pivot]] << ") "
 341                 << "level " << pivotRank << std::endl;*/
 342   for(unsigned i = startIndex + 1; i <= stopIndex; ++i) {
 343     unsigned current = getOperatorPrecedence(operators[i]);
 344     bool rtl = isRightToLeft(operators[i]);
 345     if(current > pivotRank || (current == pivotRank && !rtl)) {
 346       /*Debug("prec") << "new pivot at " << i
 347                     << "(" << CvcParserTokenNames[operators[i]] << ") "
 348                     << "level " << current << " rtl == " << rtl << std::endl;*/
 349       pivot = i;
 350       pivotRank = current;
 351     }
 352   }
 353   return pivot;
 354 }/* findPivot() */
 355
 356 Expr createPrecedenceTree(Parser* parser, ExprManager* em,
 357                           const std::vector<CVC4::Expr>& expressions,
 358                           const std::vector<unsigned>& operators,
 359                           unsigned startIndex, unsigned stopIndex) {
 360   assert(expressions.size() == operators.size() + 1);
 361   assert(startIndex < expressions.size());
 362   assert(stopIndex < expressions.size());
 363   assert(startIndex <= stopIndex);
 364
 365   if(stopIndex == startIndex) {
 366     return expressions[startIndex];
 367   }
 368
 369   unsigned pivot = findPivot(operators, startIndex, stopIndex - 1);
 370   //Debug("prec") << "pivot[" << startIndex << "," << stopIndex - 1 << "] at " << pivot << std::endl;
 371   bool negate;
 372   Kind k = getOperatorKind(operators[pivot], negate);
 373   Expr lhs = createPrecedenceTree(parser, em, expressions, operators, startIndex, pivot);
 374   Expr rhs = createPrecedenceTree(parser, em, expressions, operators, pivot + 1, stopIndex);
 375   if(k == kind::EQUAL && lhs.getType().isBoolean()) {
 376     if(parser->strictModeEnabled()) {
 377       WarningOnce() << "Warning: in strict parsing mode, will not convert BOOL = BOOL to BOOL <=> BOOL" << std::endl;
 378     } else {
 379       k = kind::IFF;
 380     }
 381   }
 382   Expr e = em->mkExpr(k, lhs, rhs);
 383   return negate ? em->mkExpr(kind::NOT, e) : e;
 384 }/* createPrecedenceTree() recursive variant */
 385
 386 Expr createPrecedenceTree(Parser* parser, ExprManager* em,
 387                           const std::vector<CVC4::Expr>& expressions,
 388                           const std::vector<unsigned>& operators) {
 389   if(Debug.isOn("prec") && operators.size() > 1) {
 390     for(unsigned i = 0; i < expressions.size(); ++i) {
 391       Debug("prec") << expressions[i];
 392       if(operators.size() > i) {
 393         Debug("prec") << ' ' << CvcParserTokenNames[operators[i]] << ' ';
 394       }
 395     }
 396     Debug("prec") << std::endl;
 397   }
 398
 399   Expr e = createPrecedenceTree(parser, em, expressions, operators, 0, expressions.size() - 1);
 400   if(Debug.isOn("prec") && operators.size() > 1) {
 401     Expr::setlanguage::Scope ls(Debug("prec"), language::output::LANG_AST);
 402     Debug("prec") << "=> " << e << std::endl;
 403   }
 404   return e;
 405 }/* createPrecedenceTree() base variant */
 406
 407 /** Add n NOTs to the front of e and return the result. */
 408 Expr addNots(ExprManager* em, size_t n, Expr e) {
 409   while(n-- > 0) {
 410     e = em->mkExpr(kind::NOT, e);
 411   }
 412   return e;
 413 }/* addNots() */
 414
 415 }/* @parser::members */
 416
 417 @header {
 418 /**
 419  ** This file is part of CVC4.
 420  ** Copyright (c) 2009-2013  New York University and The University of Iowa
 421  ** See the file COPYING in the top-level source directory for licensing
 422  ** information.
 423  **/
 424 }/* @header */
 425
 426 @lexer::includes {
 427
 428 /** This suppresses warnings about the redefinition of token symbols between different
 429   * parsers. The redefinitions should be harmless as long as no client: (a) #include's
 430   * the lexer headers for two grammars AND (b) uses the token symbol definitions. */
 431 #pragma GCC system_header
 432
 433 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
 434 /* This improves performance by ~10 percent on big inputs.
 435  * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
 436  * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
 437  * Otherwise, we have to let the lexer detect the encoding at runtime.
 438  */
 439 #  define ANTLR3_INLINE_INPUT_ASCII
 440 #  define ANTLR3_INLINE_INPUT_8BIT
 441 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 442
 443 #include "parser/antlr_tracing.h"
 444 #include "util/integer.h"
 445 #include "parser/antlr_input.h"
 446 #include "parser/parser.h"
 447
 448 }/* @lexer::includes */
 449
 450 @parser::includes {
 451
 452 #include <stdint.h>
 453 #include <cassert>
 454 #include "expr/command.h"
 455 #include "parser/parser.h"
 456 #include "util/subrange_bound.h"
 457 #include "parser/antlr_tracing.h"
 458
 459 namespace CVC4 {
 460   class Expr;
 461
 462   namespace parser {
 463     namespace cvc {
 464       /**
 465        * This class is just here to get around an unfortunate bit of Antlr.
 466        * We use strings below as return values from rules, which require
 467        * them to be constructible by a void*.  So we derive the string
 468        * class to provide just such a conversion.
 469        */
 470       class myString : public std::string {
 471       public:
 472         myString(const std::string& s) : std::string(s) {}
 473         myString(void*) : std::string() {}
 474         myString() : std::string() {}
 475       };/* class myString */
 476
 477       /**
 478        * Just exists to give us the void* construction that
 479        * ANTLR requires.
 480        */
 481       class mySubrangeBound : public CVC4::SubrangeBound {
 482       public:
 483         mySubrangeBound() : CVC4::SubrangeBound() {}
 484         mySubrangeBound(void*) : CVC4::SubrangeBound() {}
 485         mySubrangeBound(const Integer& i) : CVC4::SubrangeBound(i) {}
 486         mySubrangeBound(const SubrangeBound& b) : CVC4::SubrangeBound(b) {}
 487       };/* class mySubrangeBound */
 488
 489       /**
 490        * Just exists to give us the void* construction that
 491        * ANTLR requires.
 492        */
 493       struct myExpr : public CVC4::Expr {
 494         myExpr() : CVC4::Expr() {}
 495         myExpr(void*) : CVC4::Expr() {}
 496         myExpr(const Expr& e) : CVC4::Expr(e) {}
 497         myExpr(const myExpr& e) : CVC4::Expr(e) {}
 498       };/* struct myExpr */
 499
 500     }/* CVC4::parser::cvc namespace */
 501   }/* CVC4::parser namespace */
 502 }/* CVC4 namespace */
 503
 504 }/* @parser::includes */
 505
 506 @parser::postinclude {
 507
 508 #include "expr/expr.h"
 509 #include "expr/kind.h"
 510 #include "expr/type.h"
 511 #include "parser/antlr_input.h"
 512 #include "parser/parser.h"
 513 #include "util/output.h"
 514
 515 #include <vector>
 516 #include <string>
 517 #include <sstream>
 518
 519 #define REPEAT_COMMAND(k, CommandCtor)                      \
 520   ({                                                        \
 521     unsigned __k = (k);                                     \
 522     (__k <= 1)                                              \
 523       ? (Command*) new CommandCtor                          \
 524       : ({                                                  \
 525           CommandSequence* __seq = new CommandSequence();   \
 526           while(__k-- > 0) {                                \
 527             __seq->addCommand(new CommandCtor);             \
 528           }                                                 \
 529           (Command*) __seq;                                 \
 530         });                                                 \
 531   })
 532
 533 using namespace CVC4;
 534 using namespace CVC4::parser;
 535
 536 /* These need to be macros so they can refer to the PARSER macro, which will be defined
 537  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
 538 #undef PARSER_STATE
 539 #define PARSER_STATE ((Parser*)PARSER->super)
 540 #undef EXPR_MANAGER
 541 #define EXPR_MANAGER PARSER_STATE->getExprManager()
 542 #undef MK_EXPR
 543 #define MK_EXPR EXPR_MANAGER->mkExpr
 544 #undef MK_CONST
 545 #define MK_CONST EXPR_MANAGER->mkConst
 546 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
 547
 548 #define ENSURE_BV_SIZE(k, f)                                   \
 549 {                                                              \
 550   unsigned size = BitVectorType(f.getType()).getSize();        \
 551   if(k > size) {                                               \
 552     f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k - size)), f);   \
 553   } else if (k < size) {                                       \
 554     f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f);      \
 555   }                                                            \
 556 }
 557
 558 }/* @parser::postinclude */
 559
 560 /**
 561  * Parses an expression.
 562  * @return the parsed expression
 563  */
 564 parseExpr returns [CVC4::Expr expr = CVC4::Expr()]
 565   : formula[expr]
 566   | EOF
 567   ;
 568
 569 /**
 570  * Parses a command (the whole benchmark)
 571  * @return the command of the benchmark
 572  */
 573 parseCommand returns [CVC4::Command* cmd = NULL]
 574   : c=command { $cmd = c; }
 575   | LPAREN IDENTIFIER
 576     { std::string s = AntlrInput::tokenText($IDENTIFIER);
 577       if(s == "benchmark") {
 578         PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv1 format detected.  Use --lang smt1 for SMT-LIBv1 support.");
 579       } else if(s == "set" || s == "get" || s == "declare" ||
 580                 s == "define" || s == "assert") {
 581         PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIB format detected.  Use --lang smt for SMT-LIB support.");
 582       } else {
 583         PARSER_STATE->parseError("A CVC4 presentation language command cannot begin with a parenthesis; expected command name.");
 584       }
 585     }
 586   | EOF { $cmd = NULL; }
 587   ;
 588
 589 /**
 590  * Matches a command of the input. If a declaration, it will return an empty
 591  * command.
 592  */
 593 command returns [CVC4::Command* cmd = NULL]
 594   : ( mainCommand[cmd] SEMICOLON
 595     | SEMICOLON
 596     | LET_TOK { PARSER_STATE->pushScope(); }
 597       typeOrVarLetDecl[CHECK_DECLARED] ( COMMA typeOrVarLetDecl[CHECK_DECLARED] )*
 598       IN_TOK c=command
 599       { $cmd = c;
 600         PARSER_STATE->popScope();
 601       }
 602     )
 603     { if($cmd == NULL) {
 604         cmd = new EmptyCommand();
 605       }
 606     }
 607   ;
 608
 609 typeOrVarLetDecl[CVC4::parser::DeclarationCheck check]
 610 options { backtrack = true; }
 611   : letDecl | typeLetDecl[check]
 612   ;
 613
 614 mainCommand[CVC4::Command*& cmd]
 615 @init {
 616   Expr f;
 617   SExpr sexpr;
 618   std::string id;
 619   Type t;
 620   std::vector<CVC4::Datatype> dts;
 621   Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl;
 622   std::string s;
 623 }
 624     /* our bread & butter */
 625   : ASSERT_TOK formula[f] { cmd = new AssertCommand(f); }
 626
 627   | QUERY_TOK formula[f] { cmd = new QueryCommand(f); }
 628   | CHECKSAT_TOK formula[f]? { cmd = f.isNull() ? new CheckSatCommand() : new CheckSatCommand(f); }
 629
 630     /* options */
 631   | OPTION_TOK
 632     ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
 633     ( symbolicExpr[sexpr]
 634       { if(s == "logic") {
 635           cmd = new SetBenchmarkLogicCommand(sexpr.getValue());
 636         } else {
 637           cmd = new SetOptionCommand(s, sexpr);
 638         }
 639       }
 640     | TRUE_TOK { cmd = new SetOptionCommand(s, SExpr("true")); }
 641     | FALSE_TOK { cmd = new SetOptionCommand(s, SExpr("false")); }
 642     | { cmd = new SetOptionCommand(s, SExpr("true")); }
 643     )
 644
 645     /* push / pop */
 646   | PUSH_TOK ( k=numeral { cmd = REPEAT_COMMAND(k, PushCommand()); }
 647                | { cmd = new PushCommand(); } )
 648   | POP_TOK ( k=numeral { cmd = REPEAT_COMMAND(k, PopCommand()); }
 649               | { cmd = new PopCommand(); } )
 650   | POPTO_TOK k=numeral?
 651     { UNSUPPORTED("POPTO command"); }
 652
 653     /* push / pop scopes */
 654   | PUSH_SCOPE_TOK k=numeral?
 655     { UNSUPPORTED("PUSH_SCOPE command"); }
 656   | POP_SCOPE_TOK k=numeral?
 657     { UNSUPPORTED("POP_SCOPE command"); }
 658   | POPTO_SCOPE_TOK k=numeral?
 659     { UNSUPPORTED("POPTO_SCOPE command"); }
 660
 661   | RESET_TOK
 662     { UNSUPPORTED("RESET command"); }
 663
 664     // Datatypes can be mututally-recursive if they're in the same
 665     // definition block, separated by a comma.  So we parse everything
 666     // and then ask the ExprManager to resolve everything in one go.
 667   | DATATYPE_TOK
 668     { /* open a scope to keep the UnresolvedTypes contained */
 669       PARSER_STATE->pushScope(); }
 670     datatypeDef[dts]
 671     ( COMMA datatypeDef[dts] )*
 672     END_TOK
 673     { PARSER_STATE->popScope();
 674       cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
 675
 676   | CONTEXT_TOK
 677     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
 678       { UNSUPPORTED("CONTEXT command"); }
 679     | { UNSUPPORTED("CONTEXT command"); }
 680     )
 681
 682   | FORGET_TOK identifier[id,CHECK_NONE,SYM_VARIABLE]
 683     { UNSUPPORTED("FORGET command"); }
 684
 685   | GET_TYPE_TOK formula[f]
 686     { UNSUPPORTED("GET_TYPE command"); }
 687
 688   | CHECK_TYPE_TOK formula[f] COLON type[t,CHECK_DECLARED]
 689     { UNSUPPORTED("CHECK_TYPE command"); }
 690
 691   | GET_CHILD_TOK formula[f] k=numeral
 692     { UNSUPPORTED("GET_CHILD command"); }
 693
 694   | GET_OP_TOK formula[f]
 695     { UNSUPPORTED("GET_OP command"); }
 696
 697   | GET_VALUE_TOK formula[f]
 698     { cmd = new GetValueCommand(f); }
 699
 700   | SUBSTITUTE_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED] EQUAL_TOK
 701     formula[f] LBRACKET identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[f] RBRACKET
 702     { UNSUPPORTED("SUBSTITUTE command"); }
 703
 704     /* Like the --debug command line option, DBG turns on both tracing
 705      * and debugging. */
 706   | DBG_TOK
 707     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
 708       { Debug.on(s); Trace.on(s); }
 709     | { Message() << "Please specify what to debug." << std::endl; }
 710     )
 711
 712   | TRACE_TOK
 713     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
 714       { Trace.on(s); }
 715     | { Message() << "Please specify something to trace." << std::endl; }
 716     )
 717   | UNTRACE_TOK
 718     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
 719       { Trace.off(s); }
 720     | { Message() << "Please specify something to untrace." << std::endl; }
 721     )
 722
 723   | HELP_TOK
 724     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
 725       { Message() << "No help available for `" << s << "'." << std::endl; }
 726     | { Message() << "Please use --help at the command line for help." << std::endl; }
 727     )
 728
 729   | TRANSFORM_TOK formula[f]
 730     { cmd = new SimplifyCommand(f); }
 731
 732   | PRINT_TOK formula[f]
 733     { UNSUPPORTED("PRINT command"); }
 734   | PRINT_TYPE_TOK type[t,CHECK_DECLARED]
 735     { UNSUPPORTED("PRINT_TYPE command"); }
 736
 737   | CALL_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] formula[f]
 738     { UNSUPPORTED("CALL command"); }
 739
 740   | ECHO_TOK
 741     ( simpleSymbolicExpr[sexpr]
 742       { cmd = new EchoCommand(sexpr.getValue()); }
 743     | { cmd = new EchoCommand(); }
 744     )
 745
 746   | EXIT_TOK
 747     { cmd = new QuitCommand(); }
 748
 749   | INCLUDE_TOK
 750     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
 751       { UNSUPPORTED("INCLUDE command"); }
 752     | { PARSER_STATE->parseError("No filename given to INCLUDE command"); }
 753     )
 754
 755   | DUMP_PROOF_TOK
 756     { cmd = new GetProofCommand(); }
 757
 758   | ( DUMP_ASSUMPTIONS_TOK
 759     | DUMP_SIG_TOK
 760     | DUMP_TCC_TOK
 761     | DUMP_TCC_ASSUMPTIONS_TOK
 762     | DUMP_TCC_PROOF_TOK
 763     | DUMP_CLOSURE_TOK
 764     | DUMP_CLOSURE_PROOF_TOK
 765     ) { UNSUPPORTED("DUMP* command"); }
 766
 767     /* these are all synonyms */
 768   | ( WHERE_TOK | ASSERTIONS_TOK | ASSUMPTIONS_TOK )
 769     { cmd = new GetAssertionsCommand(); }
 770
 771   | COUNTEREXAMPLE_TOK
 772     { cmd = new GetModelCommand; }
 773   | COUNTERMODEL_TOK
 774     { cmd = new GetModelCommand; }
 775
 776   | ARITH_VAR_ORDER_TOK LPAREN formula[f] ( COMMA formula[f] )* RPAREN
 777     { UNSUPPORTED("ARITH_VAR_ORDER command"); }
 778
 779   | toplevelDeclaration[cmd]
 780   ;
 781
 782 simpleSymbolicExpr[CVC4::SExpr& sexpr]
 783 @declarations {
 784   std::string s;
 785   CVC4::Rational r;
 786 }
 787   : INTEGER_LITERAL
 788     { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
 789   | MINUS_TOK INTEGER_LITERAL
 790     { sexpr = SExpr(-Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
 791   | DECIMAL_LITERAL
 792     { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
 793   | HEX_LITERAL
 794     { sexpr = SExpr(AntlrInput::tokenText($HEX_LITERAL)); }
 795   | BINARY_LITERAL
 796     { sexpr = SExpr(AntlrInput::tokenText($BINARY_LITERAL)); }
 797   | str[s]
 798     { sexpr = SExpr(s); }
 799   | IDENTIFIER
 800     { sexpr = SExpr(AntlrInput::tokenText($IDENTIFIER)); }
 801   ;
 802
 803 symbolicExpr[CVC4::SExpr& sexpr]
 804 @declarations {
 805   std::vector<SExpr> children;
 806 }
 807   : simpleSymbolicExpr[sexpr]
 808   | LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN
 809     { sexpr = SExpr(children); }
 810   ;
 811
 812 /**
 813  * Match a top-level declaration.
 814  */
 815 toplevelDeclaration[CVC4::Command*& cmd]
 816 @init {
 817   std::vector<std::string> ids;
 818   Type t;
 819   Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl;
 820 }
 821   : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON
 822     ( declareVariables[cmd,t,ids,true]
 823     | declareTypes[cmd,ids] )
 824   ;
 825
 826 /**
 827  * A bound variable declaration.
 828  */
 829 boundVarDecl[std::vector<std::string>& ids, CVC4::Type& t]
 830   : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[*(Command**)NULL,t,ids,false]
 831   ;
 832
 833 /**
 834  * A series of bound variable declarations.
 835  */
 836 boundVarDecls
 837 @init {
 838   std::vector<std::string> ids;
 839   Type t;
 840 }
 841   : boundVarDecl[ids,t] ( COMMA boundVarDecl[ids,t] )*
 842   ;
 843
 844 boundVarDeclsReturn[std::vector<CVC4::Expr>& terms,
 845                     std::vector<CVC4::Type>& types]
 846 @init {
 847   std::vector<std::string> ids;
 848   Type t;
 849   terms.clear();
 850   types.clear();
 851 }
 852   : boundVarDeclReturn[terms,types] ( COMMA boundVarDeclReturn[terms,types] )*
 853   ;
 854
 855 boundVarDeclReturn[std::vector<CVC4::Expr>& terms,
 856                    std::vector<CVC4::Type>& types]
 857 @init {
 858   std::vector<std::string> ids;
 859   Type t;
 860   // NOTE: do not clear the vectors here!
 861 }
 862   : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED]
 863     { const std::vector<Expr>& vars = PARSER_STATE->mkBoundVars(ids, t);
 864       terms.insert(terms.end(), vars.begin(), vars.end());
 865       for(unsigned i = 0; i < vars.size(); ++i) {
 866         types.push_back(t);
 867       }
 868     }
 869   ;
 870
 871 /**
 872  * Match the right-hand-side of a type declaration.  Unlike
 873  * declareVariables[] below, don't need to return the Type, since it's
 874  * always the KindType (the type of types).  Also don't need toplevel
 875  * because type declarations are always top-level, except for
 876  * type-lets, which don't use this rule.
 877  */
 878 declareTypes[CVC4::Command*& cmd, const std::vector<std::string>& idList]
 879 @init {
 880   Type t;
 881 }
 882     /* A sort declaration (e.g., "T : TYPE") */
 883   : TYPE_TOK
 884     { DeclarationSequence* seq = new DeclarationSequence();
 885       for(std::vector<std::string>::const_iterator i = idList.begin();
 886           i != idList.end();
 887           ++i) {
 888         // Don't allow a type variable to clash with a previously
 889         // declared type variable, however a type variable and a
 890         // non-type variable can clash unambiguously.  Break from CVC3
 891         // behavior here.
 892         PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT);
 893         Type sort = PARSER_STATE->mkSort(*i);
 894         Command* decl = new DeclareTypeCommand(*i, 0, sort);
 895         seq->addCommand(decl);
 896       }
 897       cmd = seq;
 898     }
 899
 900     /* A type alias "T : TYPE = foo..." */
 901   | TYPE_TOK EQUAL_TOK type[t,CHECK_DECLARED]
 902     { for(std::vector<std::string>::const_iterator i = idList.begin();
 903           i != idList.end();
 904           ++i) {
 905         PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT);
 906         PARSER_STATE->defineType(*i, t);
 907       }
 908     }
 909   ;
 910
 911 /**
 912  * Match the right-hand side of a variable declaration.  Returns the
 913  * type.  Some IDs might have been declared previously, and are not
 914  * re-declared if topLevel is true (CVC allows re-declaration if the
 915  * types are compatible---if they aren't compatible, an error is
 916  * thrown).  Also if topLevel is true, variable definitions are
 917  * permitted and "cmd" is output.  If topLevel is false, bound vars
 918  * are created
 919  */
 920 declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::string>& idList, bool topLevel]
 921 @init {
 922   Expr f;
 923   Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
 924 }
 925     /* A variable declaration (or definition) */
 926   : type[t,CHECK_DECLARED] ( EQUAL_TOK formula[f] )?
 927     { DeclarationSequence* seq = NULL;
 928       if(topLevel) {
 929         cmd = seq = new DeclarationSequence();
 930       }
 931       if(f.isNull()) {
 932         Debug("parser") << "working on " << idList.front() << " : " << t << std::endl;
 933         // CVC language allows redeclaration of variables if types are the same
 934         for(std::vector<std::string>::const_iterator i = idList.begin(),
 935               i_end = idList.end();
 936             i != i_end;
 937             ++i) {
 938           if(PARSER_STATE->isDeclared(*i, SYM_VARIABLE)) {
 939             Type oldType = PARSER_STATE->getType(*i);
 940             Debug("parser") << "  " << *i << " was declared previously "
 941                             << "with type " << oldType << std::endl;
 942             if(oldType != t) {
 943               std::stringstream ss;
 944               ss << Expr::setlanguage(language::output::LANG_CVC4)
 945                  << "incompatible type for `" << *i << "':" << std::endl
 946                  << "  old type: " << oldType << std::endl
 947                  << "  new type: " << t << std::endl;
 948               PARSER_STATE->parseError(ss.str());
 949             } else {
 950               Debug("parser") << "  types " << t << " and " << oldType
 951                               << " are compatible" << std::endl;
 952             }
 953           } else {
 954             Debug("parser") << "  " << *i << " not declared" << std::endl;
 955             if(topLevel) {
 956               Expr func = PARSER_STATE->mkVar(*i, t, ExprManager::VAR_FLAG_GLOBAL);
 957               Command* decl = new DeclareFunctionCommand(*i, func, t);
 958               seq->addCommand(decl);
 959             } else {
 960               PARSER_STATE->mkBoundVar(*i, t);
 961             }
 962           }
 963         }
 964       } else {
 965         // f is not null-- meaning this is a definition not a declaration
 966         if(!topLevel) {
 967           // must be top-level; doesn't make sense to write something
 968           // like e.g. FORALL(x:INT = 4): [...]
 969           PARSER_STATE->parseError("cannot construct a definition here; maybe you want a LET");
 970         }
 971         assert(!idList.empty());
 972         for(std::vector<std::string>::const_iterator i = idList.begin(),
 973               i_end = idList.end();
 974             i != i_end;
 975             ++i) {
 976           Debug("parser") << "making " << *i << " : " << t << " = " << f << std::endl;
 977           PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
 978           Expr func = EXPR_MANAGER->mkVar(*i, t, ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
 979           PARSER_STATE->defineFunction(*i, f);
 980           Command* decl = new DefineFunctionCommand(*i, func, f);
 981           seq->addCommand(decl);
 982         }
 983       }
 984     }
 985   ;
 986
 987 /**
 988  * Matches a list of identifiers separated by a comma and puts them in the
 989  * given list.
 990  * @param idList the list to fill with identifiers.
 991  * @param check what kinds of check to perform on the symbols
 992  */
 993 identifierList[std::vector<std::string>& idList,
 994                CVC4::parser::DeclarationCheck check,
 995                CVC4::parser::SymbolType type]
 996 @init {
 997   std::string id;
 998   idList.clear();
 999 }
1000   : identifier[id,check,type] { idList.push_back(id); }
1001     ( COMMA identifier[id,check,type] { idList.push_back(id); } )*
1002   ;
1003
1004 /**
1005  * Matches an identifier and returns a string.
1006  */
1007 identifier[std::string& id,
1008            CVC4::parser::DeclarationCheck check,
1009            CVC4::parser::SymbolType type]
1010   : IDENTIFIER
1011     { id = AntlrInput::tokenText($IDENTIFIER);
1012       PARSER_STATE->checkDeclaration(id, check, type); }
1013   ;
1014
1015 /**
1016  * Match the type in a declaration and do the declaration binding.  If
1017  * "check" is CHECK_NONE, then identifiers occurring in the type need
1018  * not exist!  They are created as "unresolved" types and linked up in
1019  * a type-substitution pass.  Right now, only datatype definitions are
1020  * supported in this way (since type names can occur without any
1021  * forward-declaration in CVC language datatype definitions, we have
1022  * to create types for them on-the-fly).  Before passing CHECK_NONE
1023  * you really should have a clear idea of WHY you need to parse that
1024  * way; then you should trace through Parser::mkMutualDatatypeType()
1025  * to figure out just what you're in for.
1026  */
1027 type[CVC4::Type& t,
1028      CVC4::parser::DeclarationCheck check]
1029 @init {
1030   Type t2;
1031   bool lhs;
1032   std::vector<Type> args;
1033 }
1034     /* a type, possibly a function */
1035   : restrictedTypePossiblyFunctionLHS[t,check,lhs]
1036     { if(lhs) {
1037         assert(t.isTuple());
1038         args = TupleType(t).getTypes();
1039       } else {
1040         args.push_back(t);
1041       }
1042     }
1043     ( ARROW_TOK type[t2,check] { args.push_back(t2); } )?
1044     { if(t2.isNull()) {
1045         if(lhs) {
1046           PARSER_STATE->parseError("improperly-placed type list; expected `->' after to define a function; or else maybe these parentheses were meant to be square brackets, to define a tuple type?");
1047         }
1048       } else {
1049         t = EXPR_MANAGER->mkFunctionType(args);
1050       }
1051     }
1052
1053     /* type-lets: typeLetDecl defines the types, we just manage the
1054      * scopes here.  NOTE that LET in the CVC language is always
1055      * sequential! */
1056   | LET_TOK { PARSER_STATE->pushScope(); }
1057     typeLetDecl[check] ( COMMA typeLetDecl[check] )* IN_TOK type[t,check]
1058     { PARSER_STATE->popScope(); }
1059   ;
1060
1061 // A restrictedType is one that is not a "bare" function type (it can
1062 // be enclosed in parentheses) and is not a type list.  To support the
1063 // syntax
1064 //
1065 //   f : (nat, nat) -> nat;
1066 //
1067 // we have to permit restrictedTypes to be type lists (as on the LHS
1068 // there).  The "type" rule above uses restictedTypePossiblyFunctionLHS
1069 // directly in order to implement that; this rule allows a type list to
1070 // parse but then issues an error.
1071 restrictedType[CVC4::Type& t,
1072                CVC4::parser::DeclarationCheck check]
1073 @init {
1074   bool lhs;
1075 }
1076   : restrictedTypePossiblyFunctionLHS[t,check,lhs]
1077     { if(lhs) { PARSER_STATE->parseError("improperly-placed type list; maybe these parentheses were meant to be square brackets, to define a tuple type?"); } }
1078   ;
1079
1080 /**
1081  * lhs is set to "true" on output if we have a list of types, so an
1082  * ARROW must follow.  An ARROW can always follow; lhs means it MUST.
1083  */
1084 restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
1085                                   CVC4::parser::DeclarationCheck check,
1086                                   bool& lhs]
1087 @init {
1088   Type t2;
1089   Expr f, f2;
1090   std::string id;
1091   std::vector<Type> types;
1092   std::vector< std::pair<std::string, Type> > typeIds;
1093   //SymbolTable* symtab;
1094   Parser* parser;
1095   lhs = false;
1096 }
1097     /* named types */
1098   : identifier[id,check,SYM_SORT]
1099     parameterization[check,types]?
1100     {
1101       if(check == CHECK_DECLARED ||
1102          PARSER_STATE->isDeclared(id, SYM_SORT)) {
1103         Debug("parser-param") << "param: getSort " << id << " " << types.size() << " " << PARSER_STATE->getArity( id )
1104                               << " " << PARSER_STATE->isDeclared(id, SYM_SORT) << std::endl;
1105         if(types.size() != PARSER_STATE->getArity(id)) {
1106           std::stringstream ss;
1107           ss << "incorrect arity for symbol `" << id << "': expected "
1108              << PARSER_STATE->getArity( id ) << " type arguments, got "
1109              << types.size();
1110           PARSER_STATE->parseError(ss.str());
1111         }
1112         if(types.size() > 0) {
1113           t = PARSER_STATE->getSort(id, types);
1114         }else{
1115           t = PARSER_STATE->getSort(id);
1116         }
1117       } else {
1118         if(types.empty()) {
1119           t = PARSER_STATE->mkUnresolvedType(id);
1120           Debug("parser-param") << "param: make unres type " << id << std::endl;
1121         }else{
1122           t = PARSER_STATE->mkUnresolvedTypeConstructor(id,types);
1123           t = SortConstructorType(t).instantiate( types );
1124           Debug("parser-param") << "param: make unres param type " << id << " " << types.size() << " "
1125                                 << PARSER_STATE->getArity( id ) << std::endl;
1126         }
1127       }
1128     }
1129
1130     /* array types */
1131   | ARRAY_TOK restrictedType[t,check] OF_TOK restrictedType[t2,check]
1132     { t = EXPR_MANAGER->mkArrayType(t, t2); }
1133
1134     /* subtypes */
1135   | SUBTYPE_TOK LPAREN
1136     /* A bit tricky: this LAMBDA expression cannot refer to constants
1137      * declared in the outer context.  What follows isn't quite right,
1138      * though, since type aliases and function definitions should be
1139      * retained in the set of current declarations. */
1140     { /*symtab = PARSER_STATE->getSymbolTable();
1141       PARSER_STATE->useDeclarationsFrom(new SymbolTable());*/ }
1142     formula[f] ( COMMA formula[f2] )? RPAREN
1143     { /*SymbolTable* old = PARSER_STATE->getSymbolTable();
1144       PARSER_STATE->useDeclarationsFrom(symtab);
1145       delete old;*/
1146       PARSER_STATE->unimplementedFeature("predicate subtyping not supported in this release");
1147       /*t = f2.isNull() ?
1148         EXPR_MANAGER->mkPredicateSubtype(f) :
1149         EXPR_MANAGER->mkPredicateSubtype(f, f2);
1150       */
1151     }
1152
1153     /* subrange types */
1154   | LBRACKET k1=bound DOTDOT k2=bound RBRACKET
1155     { if(k1.hasBound() && k2.hasBound() &&
1156          k1.getBound() > k2.getBound()) {
1157         std::stringstream ss;
1158         ss << "Subrange [" << k1.getBound() << ".." << k2.getBound()
1159            << "] inappropriate: range must be nonempty!";
1160         PARSER_STATE->parseError(ss.str());
1161       }
1162       t = EXPR_MANAGER->mkSubrangeType(SubrangeBounds(k1, k2));
1163     }
1164
1165     /* tuple types / old-style function types */
1166   | LBRACKET ( type[t,check] { types.push_back(t); }
1167     ( COMMA type[t,check] { types.push_back(t); } )* )? RBRACKET
1168     { if(types.size() == 1 && types.front().isFunction()) {
1169         // old style function syntax [ T -> U ]
1170         PARSER_STATE->parseError("old-style function type syntax not supported anymore; please use the new syntax");
1171       } else {
1172         // tuple type [ T, U, V... ]
1173         t = EXPR_MANAGER->mkTupleType(types);
1174       }
1175     }
1176
1177     /* record types */
1178   | SQHASH ( identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); }
1179     ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } )* )? HASHSQ
1180     { t = EXPR_MANAGER->mkRecordType(typeIds); }
1181
1182     /* bitvector types */
1183   | BITVECTOR_TOK LPAREN k=numeral RPAREN
1184     { if(k == 0) {
1185         PARSER_STATE->parseError("Illegal bitvector size: 0");
1186       }
1187       t = EXPR_MANAGER->mkBitVectorType(k);
1188     }
1189
1190     /* basic types */
1191   | BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); }
1192   | REAL_TOK { t = EXPR_MANAGER->realType(); }
1193   | INT_TOK { t = EXPR_MANAGER->integerType(); }
1194
1195     /* Parenthesized general type, or the lhs of an ARROW (a list of
1196      * types).  These two things are combined to avoid conflicts in
1197      * parsing. */
1198   | LPAREN type[t,check] { types.push_back(t); }
1199     ( COMMA type[t,check] { lhs = true; types.push_back(t); } )* RPAREN
1200     { if(lhs) { t = EXPR_MANAGER->mkTupleType(types); }
1201       // if !lhs, t is already set up correctly, nothing to do..
1202     }
1203   ;
1204
1205 parameterization[CVC4::parser::DeclarationCheck check,
1206                  std::vector<CVC4::Type>& params]
1207 @init {
1208   Type t;
1209 }
1210   : LBRACKET restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); }
1211     ( COMMA restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); } )* RBRACKET
1212   ;
1213
1214 bound returns [CVC4::parser::cvc::mySubrangeBound bound]
1215   : UNDERSCORE { $bound = SubrangeBound(); }
1216   | k=integer { $bound = SubrangeBound(k.getNumerator()); }
1217 ;
1218
1219 typeLetDecl[CVC4::parser::DeclarationCheck check]
1220 @init {
1221   Type t;
1222   std::string id;
1223 }
1224   : identifier[id,CHECK_NONE,SYM_SORT] (COLON TYPE_TOK)? EQUAL_TOK restrictedType[t,check]
1225     { PARSER_STATE->defineType(id, t); }
1226   ;
1227
1228 /**
1229  * Matches a CVC4 expression.  Formulas and terms are not really
1230  * distinguished during parsing; please ignore the naming of the
1231  * grammar rules.
1232  *
1233  * @return the expression representing the formula/term
1234  */
1235 formula[CVC4::Expr& f]
1236 @init {
1237   Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
1238   Expr f2;
1239   std::vector<CVC4::Expr> expressions;
1240   std::vector<unsigned> operators;
1241   unsigned op;
1242 }
1243   : n=nots
1244     ( prefixFormula[f]
1245       { f = addNots(EXPR_MANAGER, n, f); }
1246     | comparison[f]
1247       { f = addNots(EXPR_MANAGER, n, f);
1248         expressions.push_back(f);
1249       }
1250       morecomparisons[expressions,operators]?
1251       { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
1252     )
1253   ;
1254
1255 morecomparisons[std::vector<CVC4::Expr>& expressions,
1256                 std::vector<unsigned>& operators] returns [size_t i = 0]
1257 @init {
1258   unsigned op;
1259   Expr f;
1260   $i = expressions.size();
1261 }
1262   : booleanBinop[op] { operators.push_back(op); }
1263     n=nots
1264     ( prefixFormula[f]
1265       { expressions.push_back(addNots(EXPR_MANAGER, n, f)); }
1266     | comparison[f]
1267       { f = addNots(EXPR_MANAGER, n, f);
1268         expressions.push_back(f);
1269       }
1270       morecomparisons[expressions,operators]?
1271     )
1272   ;
1273
1274 /** Matches 0 or more NOTs. */
1275 nots returns [size_t n = 0]
1276   : ( NOT_TOK { ++$n; } )*
1277   ;
1278
1279 prefixFormula[CVC4::Expr& f]
1280 @init {
1281   std::vector<std::string> ids;
1282   std::vector<Expr> terms;
1283   std::vector<Type> types;
1284   std::vector<Expr> bvs;
1285   Type t;
1286   Kind k;
1287   Expr ipl;
1288 }
1289     /* quantifiers */
1290   : ( FORALL_TOK { k = kind::FORALL; } | EXISTS_TOK { k = kind::EXISTS; } )
1291     { PARSER_STATE->pushScope(); } LPAREN
1292     boundVarDecl[ids,t]
1293     { for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) {
1294         bvs.push_back(PARSER_STATE->mkBoundVar(*i, t));
1295       }
1296       ids.clear();
1297     }
1298     ( COMMA boundVarDecl[ids,t]
1299       {
1300         for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) {
1301           bvs.push_back(PARSER_STATE->mkBoundVar(*i, t));
1302         }
1303         ids.clear();
1304       }
1305     )* RPAREN {
1306       terms.push_back( EXPR_MANAGER->mkExpr( kind::BOUND_VAR_LIST, bvs ) ); }
1307     COLON instantiationPatterns[ipl]? formula[f]
1308     { PARSER_STATE->popScope();
1309       terms.push_back(f);
1310       if(! ipl.isNull()) {
1311         terms.push_back(ipl);
1312       }
1313       f = MK_EXPR(k, terms);
1314     }
1315
1316    /* lets: letDecl defines the variables and functionss, we just
1317      * manage the scopes here.  NOTE that LET in the CVC language is
1318      * always sequential! */
1319   | LET_TOK { PARSER_STATE->pushScope(); }
1320     letDecl ( COMMA letDecl )*
1321     IN_TOK formula[f] { PARSER_STATE->popScope(); }
1322
1323    /* lambda */
1324   | LAMBDA { PARSER_STATE->pushScope(); } LPAREN
1325     boundVarDeclsReturn[terms,types]
1326     RPAREN COLON formula[f]
1327     { PARSER_STATE->popScope();
1328       Type t = EXPR_MANAGER->mkFunctionType(types, f.getType());
1329       std::string name = "lambda";
1330       Expr func = PARSER_STATE->mkAnonymousFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
1331       Command* cmd = new DefineFunctionCommand(name, func, terms, f);
1332       PARSER_STATE->preemptCommand(cmd);
1333       f = func;
1334     }
1335
1336     /* array literals */
1337   | ARRAY_TOK { PARSER_STATE->pushScope(); } LPAREN
1338     boundVarDecl[ids,t] RPAREN COLON formula[f]
1339     { PARSER_STATE->popScope();
1340       UNSUPPORTED("array literals not supported yet");
1341       f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType()), ExprManager::VAR_FLAG_GLOBAL);
1342     }
1343   ;
1344
1345 instantiationPatterns[ CVC4::Expr& expr ]
1346 @init {
1347   std::vector<Expr> args;
1348   Expr f;
1349   std::vector<Expr> patterns;
1350 }
1351   : ( PATTERN_TOK LPAREN formula[f] { args.push_back( f ); } (COMMA formula[f] { args.push_back( f ); } )* RPAREN COLON
1352       { patterns.push_back( EXPR_MANAGER->mkExpr( kind::INST_PATTERN, args ) );
1353         args.clear();
1354       } )+
1355     { if(! patterns.empty()) {
1356        expr = EXPR_MANAGER->mkExpr( kind::INST_PATTERN_LIST, patterns );
1357        }
1358     }
1359   ;
1360
1361 /**
1362  * Matches (and defines) a single LET declaration.
1363  */
1364 letDecl
1365 @init {
1366   Expr e;
1367   std::string name;
1368 }
1369   : identifier[name,CHECK_NONE,SYM_VARIABLE] EQUAL_TOK formula[e]
1370     { Debug("parser") << Expr::setlanguage(language::output::LANG_CVC4) << e.getType() << std::endl;
1371       PARSER_STATE->defineVar(name, e);
1372       Debug("parser") << "LET[" << PARSER_STATE->scopeLevel() << "]: "
1373                       << name << std::endl
1374                       << " ==>" << " " << e << std::endl;
1375     }
1376   ;
1377
1378 booleanBinop[unsigned& op]
1379 @init {
1380   op = LT(1)->getType(LT(1));
1381 }
1382   : IFF_TOK
1383   | IMPLIES_TOK
1384   | OR_TOK
1385   | XOR_TOK
1386   | AND_TOK
1387   ;
1388
1389 comparison[CVC4::Expr& f]
1390 @init {
1391   std::vector<CVC4::Expr> expressions;
1392   std::vector<unsigned> operators;
1393   unsigned op;
1394 }
1395   : term[f] { expressions.push_back(f); }
1396     ( comparisonBinop[op] term[f]
1397       { operators.push_back(op); expressions.push_back(f); } )*
1398     { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
1399   ;
1400
1401 comparisonBinop[unsigned& op]
1402 @init {
1403   op = LT(1)->getType(LT(1));
1404 }
1405   : EQUAL_TOK
1406   | DISEQUAL_TOK
1407   | GT_TOK
1408   | GEQ_TOK
1409   | LT_TOK
1410   | LEQ_TOK
1411   ;
1412
1413 term[CVC4::Expr& f]
1414 @init {
1415   std::vector<CVC4::Expr> expressions;
1416   std::vector<unsigned> operators;
1417   unsigned op;
1418   Type t;
1419 }
1420   : storeTerm[f] { expressions.push_back(f); }
1421     ( arithmeticBinop[op] storeTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
1422     { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
1423   ;
1424
1425 arithmeticBinop[unsigned& op]
1426 @init {
1427   op = LT(1)->getType(LT(1));
1428 }
1429   : PLUS_TOK
1430   | MINUS_TOK
1431   | STAR_TOK
1432   | INTDIV_TOK
1433   | MOD_TOK
1434   | DIV_TOK
1435   | EXP_TOK
1436   ;
1437
1438 /** Parses an array/tuple/record assignment term. */
1439 storeTerm[CVC4::Expr& f]
1440   : uminusTerm[f]
1441     ( WITH_TOK
1442       ( arrayStore[f] ( COMMA arrayStore[f] )*
1443       | DOT ( tupleStore[f] ( COMMA DOT tupleStore[f] )*
1444             | recordStore[f] ( COMMA DOT recordStore[f] )* ) )
1445     | /* nothing */
1446     )
1447   ;
1448
1449 /**
1450  * Parses just part of the array assignment (and constructs
1451  * the store terms).
1452  */
1453 arrayStore[CVC4::Expr& f]
1454 @init {
1455   Expr f2, f3;
1456   std::vector<Expr> dims;
1457 }
1458   : ( LBRACKET formula[f2] { dims.push_back(f2); } RBRACKET )+
1459     ASSIGN_TOK uminusTerm[f3]
1460     { assert(dims.size() >= 1);
1461       // these loops are a bit complicated; they're only used for the
1462       // multidimensional ...WITH [a][b] :=... syntax
1463       for(unsigned i = 0; i < dims.size() - 1; ++i) {
1464         f = MK_EXPR(CVC4::kind::SELECT, f, dims[i]);
1465       }
1466       // a[i][j][k] := v  turns into
1467       // store(a, i, store(a[i], j, store(a[i][j], k, v)))
1468       for(unsigned i = dims.size() - 1; i > 0; --i) {
1469         f3 = MK_EXPR(CVC4::kind::STORE, f, dims[i], f3);
1470         // strip off one layer of the select
1471         f = f[0];
1472       }
1473
1474       // outermost wrapping
1475       f = MK_EXPR(CVC4::kind::STORE, f, dims[0], f3);
1476     }
1477   ;
1478
1479 /**
1480  * Parses just part of the tuple assignment (and constructs
1481  * the store terms).
1482  */
1483 tupleStore[CVC4::Expr& f]
1484 @init {
1485   Expr f2;
1486 }
1487   : k=numeral ASSIGN_TOK uminusTerm[f2]
1488     {
1489       Type t = f.getType();
1490       if(! t.isTuple()) {
1491         PARSER_STATE->parseError("tuple-update applied to non-tuple");
1492       }
1493       size_t length = TupleType(t).getLength();
1494       if(k >= length) {
1495         std::stringstream ss;
1496         ss << "tuple is of length " << length << "; cannot update index " << k;
1497         PARSER_STATE->parseError(ss.str());
1498       }
1499       f = MK_EXPR(MK_CONST(TupleUpdate(k)), f, f2);
1500     }
1501   ;
1502
1503 /**
1504  * Parses just part of the record assignment (and constructs
1505  * the store terms).
1506  */
1507 recordStore[CVC4::Expr& f]
1508 @init {
1509   std::string id;
1510   Expr f2;
1511 }
1512   : identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK uminusTerm[f2]
1513     {
1514       Type t = f.getType();
1515       if(! t.isRecord()) {
1516         PARSER_STATE->parseError("record-update applied to non-record");
1517       }
1518       const Record& rec = RecordType(t).getRecord();
1519       Record::const_iterator fld = rec.find(id);
1520       if(fld == rec.end()) {
1521         PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
1522       }
1523       f = MK_EXPR(MK_CONST(RecordUpdate(id)), f, f2);
1524     }
1525   ;
1526
1527 /** Parses a unary minus term. */
1528 uminusTerm[CVC4::Expr& f]
1529 @init {
1530   unsigned minusCount = 0;
1531 }
1532     /* Unary minus */
1533   : (MINUS_TOK { ++minusCount; })+ bvBinaryOpTerm[f]
1534     { while(minusCount > 0) { --minusCount; f = MK_EXPR(CVC4::kind::UMINUS, f); } }
1535   | bvBinaryOpTerm[f]
1536   ;
1537
1538 /** Parses bitvectors.  Starts with binary operators @, &, and |. */
1539 bvBinaryOpTerm[CVC4::Expr& f]
1540 @init {
1541   std::vector<CVC4::Expr> expressions;
1542   std::vector<unsigned> operators;
1543   unsigned op;
1544 }
1545   : bvNegTerm[f] { expressions.push_back(f); }
1546     ( bvBinop[op] bvNegTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
1547     { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
1548   ;
1549 bvBinop[unsigned& op]
1550 @init {
1551   op = LT(1)->getType(LT(1));
1552 }
1553   : CONCAT_TOK
1554   | BAR // bitwise OR
1555   | BVAND_TOK
1556   ;
1557
1558 bvNegTerm[CVC4::Expr& f]
1559     /* BV neg */
1560   : BVNEG_TOK bvNegTerm[f]
1561     { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
1562   | postfixTerm[f]
1563   ;
1564
1565 /**
1566  * Parses an array select / bitvector extract / bitvector shift /
1567  * function or constructor application.  These are all parsed the same
1568  * way because they are all effectively post-fix operators and can
1569  * continue piling onto an expression.  Array selects and bitvector
1570  * extracts even share similar syntax with their use of [ square
1571  * brackets ], so we left-factor as much out as possible to make ANTLR
1572  * happy.
1573  */
1574 postfixTerm[CVC4::Expr& f]
1575 @init {
1576   Expr f2;
1577   bool extract = false, left = false;
1578   std::vector<Expr> args;
1579   std::string id;
1580   Type t;
1581 }
1582   : ( bvTerm[f]
1583     ( /* array select / bitvector extract */
1584       LBRACKET
1585         ( formula[f2] { extract = false; }
1586         | k1=numeral COLON k2=numeral { extract = true; } )
1587       RBRACKET
1588       { if(extract) {
1589           /* bitvector extract */
1590           f = MK_EXPR(MK_CONST(BitVectorExtract(k1, k2)), f);
1591         } else {
1592           /* array select */
1593           f = MK_EXPR(CVC4::kind::SELECT, f, f2);
1594         }
1595       }
1596
1597       /* left- or right-shift */
1598     | ( LEFTSHIFT_TOK { left = true; }
1599       | RIGHTSHIFT_TOK { left = false; } ) k=numeral
1600       { // Defined in:
1601         // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit
1602         if(left) {
1603           f = MK_EXPR(kind::BITVECTOR_CONCAT, f, MK_CONST(BitVector(k)));
1604         } else {
1605           unsigned n = BitVectorType(f.getType()).getSize();
1606           f = MK_EXPR(kind::BITVECTOR_CONCAT, MK_CONST(BitVector(k)),
1607                       MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f));
1608         }
1609       }
1610
1611       /* function/constructor application */
1612     | LPAREN { args.push_back(f); }
1613       formula[f] { args.push_back(f); }
1614       ( COMMA formula[f] { args.push_back(f); } )* RPAREN
1615       // TODO: check arity
1616       { Type t = args.front().getType();
1617         Debug("parser") << "type is " << t << std::endl;
1618         Debug("parser") << "expr is " << args.front() << std::endl;
1619         if(PARSER_STATE->isDefinedFunction(args.front())) {
1620           f = MK_EXPR(CVC4::kind::APPLY, args);
1621         } else if(t.isFunction()) {
1622           f = MK_EXPR(CVC4::kind::APPLY_UF, args);
1623         } else if(t.isConstructor()) {
1624           f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
1625         } else if(t.isSelector()) {
1626           f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args);
1627         } else if(t.isTester()) {
1628           f = MK_EXPR(CVC4::kind::APPLY_TESTER, args);
1629         } else {
1630           PARSER_STATE->parseError("internal error: unhandled function application kind");
1631         }
1632       }
1633
1634       /* record / tuple select */
1635     | DOT
1636       ( identifier[id,CHECK_NONE,SYM_VARIABLE]
1637         { Type t = f.getType();
1638           if(! t.isRecord()) {
1639             PARSER_STATE->parseError("record-select applied to non-record");
1640           }
1641           const Record& rec = RecordType(t).getRecord();
1642           Record::const_iterator fld = rec.find(id);
1643           if(fld == rec.end()) {
1644             PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
1645           }
1646           f = MK_EXPR(MK_CONST(RecordSelect(id)), f);
1647         }
1648       | k=numeral
1649         { Type t = f.getType();
1650           if(! t.isTuple()) {
1651             PARSER_STATE->parseError("tuple-select applied to non-tuple");
1652           }
1653           size_t length = TupleType(t).getLength();
1654           if(k >= length) {
1655             std::stringstream ss;
1656             ss << "tuple is of length " << length << "; cannot access index " << k;
1657             PARSER_STATE->parseError(ss.str());
1658           }
1659           f = MK_EXPR(MK_CONST(TupleSelect(k)), f);
1660         }
1661       )
1662     )*
1663     | FLOOR_TOK LPAREN formula[f] RPAREN
1664       { f = MK_EXPR(CVC4::kind::TO_INTEGER, f); }
1665     | DISTINCT_TOK LPAREN
1666       formula[f] { args.push_back(f); }
1667       ( COMMA formula[f] { args.push_back(f); } )* RPAREN
1668       { f = (args.size() == 1) ? MK_CONST(bool(true)) : MK_EXPR(CVC4::kind::DISTINCT, args); }
1669     )
1670     ( typeAscription[f, t]
1671       { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) {
1672           std::vector<CVC4::Expr> v;
1673           Expr e = f.getOperator();
1674           const DatatypeConstructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)];
1675           v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
1676                                MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator() ));
1677           v.insert(v.end(), f.begin(), f.end());
1678           f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
1679         } else {
1680           if(f.getType() != t) {
1681             PARSER_STATE->parseError("Type ascription not satisfied.");
1682           }
1683         }
1684       }
1685     )?
1686   ;
1687
1688 bvTerm[CVC4::Expr& f]
1689 @init {
1690   Expr f2;
1691   std::vector<Expr> args;
1692 }
1693     /* BV xor */
1694   : BVXOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1695     { f = MK_EXPR(CVC4::kind::BITVECTOR_XOR, f, f2); }
1696   | BVNAND_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1697     { f = MK_EXPR(CVC4::kind::BITVECTOR_NAND, f, f2); }
1698   | BVNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1699     { f = MK_EXPR(CVC4::kind::BITVECTOR_NOR, f, f2); }
1700   | BVCOMP_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1701     { f = MK_EXPR(CVC4::kind::BITVECTOR_COMP, f, f2); }
1702   | BVXNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1703     { f = MK_EXPR(CVC4::kind::BITVECTOR_XNOR, f, f2); }
1704
1705     /* BV unary minus */
1706   | BVUMINUS_TOK LPAREN formula[f] RPAREN
1707     { f = MK_EXPR(CVC4::kind::BITVECTOR_NEG, f); }
1708     /* BV addition */
1709   | BVPLUS_TOK LPAREN k=numeral COMMA formula[f] { args.push_back(f); }
1710     ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN
1711     {
1712       if (k <= 0) {
1713         PARSER_STATE->parseError("BVPLUS(k,_,_) must have k > 0");
1714       }
1715       for (unsigned i = 0; i < args.size(); ++ i) {
1716         ENSURE_BV_SIZE(k, args[i]);
1717       }
1718       f = MK_EXPR(CVC4::kind::BITVECTOR_PLUS, args);
1719     }
1720     /* BV subtraction */
1721   | BVSUB_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN
1722     {
1723       if (k <= 0) {
1724         PARSER_STATE->parseError("BVSUB(k,_,_) must have k > 0");
1725       }
1726       ENSURE_BV_SIZE(k, f);
1727       ENSURE_BV_SIZE(k, f2);
1728       f = MK_EXPR(CVC4::kind::BITVECTOR_SUB, f, f2);
1729     }
1730     /* BV multiplication */
1731   | BVMULT_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN
1732     {
1733       if (k <= 0) {
1734         PARSER_STATE->parseError("BVMULT(k,_,_) must have k > 0");
1735       }
1736       ENSURE_BV_SIZE(k, f);
1737       ENSURE_BV_SIZE(k, f2);
1738       f = MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2);
1739     }
1740     /* BV unsigned division */
1741   | BVUDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1742     { f = MK_EXPR(CVC4::kind::BITVECTOR_UDIV, f, f2); }
1743     /* BV signed division */
1744   | BVSDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1745     { f = MK_EXPR(CVC4::kind::BITVECTOR_SDIV, f, f2); }
1746     /* BV unsigned remainder */
1747   | BVUREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1748     { f = MK_EXPR(CVC4::kind::BITVECTOR_UREM, f, f2); }
1749     /* BV signed remainder */
1750   | BVSREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1751     { f = MK_EXPR(CVC4::kind::BITVECTOR_SREM, f, f2); }
1752     /* BV signed modulo */
1753   | BVSMOD_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1754     { f = MK_EXPR(CVC4::kind::BITVECTOR_SMOD, f, f2); }
1755     /* BV left shift */
1756   | BVSHL_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1757     { f = MK_EXPR(CVC4::kind::BITVECTOR_SHL, f, f2); }
1758     /* BV arithmetic right shift */
1759   | BVASHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1760     { f = MK_EXPR(CVC4::kind::BITVECTOR_ASHR, f, f2); }
1761     /* BV logical left shift */
1762   | BVLSHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1763     { f = MK_EXPR(CVC4::kind::BITVECTOR_LSHR, f, f2); }
1764     /* BV sign extension */
1765   | SX_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1766     { unsigned n = BitVectorType(f.getType()).getSize();
1767       // Sign extension in TheoryBitVector is defined as in SMT-LIB
1768       // which is different than in the CVC language
1769       // SX(BITVECTOR(k), n) in CVC language extends to n bits
1770       // In SMT-LIB, such a thing expands to k + n bits
1771       f = MK_EXPR(MK_CONST(BitVectorSignExtend(k - n)), f); }
1772     /* BV zero extension */
1773   | BVZEROEXTEND_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1774     { unsigned n = BitVectorType(f.getType()).getSize();
1775       // Zero extension in TheoryBitVector is defined as in SMT-LIB
1776       // which is the same as in CVC3, but different than SX!
1777       // SX(BITVECTOR(k), n) in CVC language extends to n bits
1778       // BVZEROEXTEND(BITVECTOR(k), n) in CVC language extends to k + n bits
1779       f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f); }
1780     /* BV repeat operation */
1781   | BVREPEAT_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1782     { f = MK_EXPR(MK_CONST(BitVectorRepeat(k)), f); }
1783     /* BV rotate right */
1784   | BVROTR_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1785     { f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); }
1786     /* BV rotate left */
1787   | BVROTL_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1788     { f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); }
1789
1790     /* BV comparisons */
1791   | BVLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1792     { f = MK_EXPR(CVC4::kind::BITVECTOR_ULT, f, f2); }
1793   | BVLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1794     { f = MK_EXPR(CVC4::kind::BITVECTOR_ULE, f, f2); }
1795   | BVGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1796     { f = MK_EXPR(CVC4::kind::BITVECTOR_UGT, f, f2); }
1797   | BVGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1798     { f = MK_EXPR(CVC4::kind::BITVECTOR_UGE, f, f2); }
1799   | BVSLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1800     { f = MK_EXPR(CVC4::kind::BITVECTOR_SLT, f, f2); }
1801   | BVSLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1802     { f = MK_EXPR(CVC4::kind::BITVECTOR_SLE, f, f2); }
1803   | BVSGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1804     { f = MK_EXPR(CVC4::kind::BITVECTOR_SGT, f, f2); }
1805   | BVSGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1806     { f = MK_EXPR(CVC4::kind::BITVECTOR_SGE, f, f2); }
1807
1808   /*
1809   | IS_INTEGER_TOK LPAREN formula[f] RPAREN
1810     { f = MK_EXPR(CVC4::kind::BITVECTOR_IS_INTEGER, f); }
1811   */
1812
1813   | simpleTerm[f]
1814   ;
1815
1816 /** Parses a simple term. */
1817 simpleTerm[CVC4::Expr& f]
1818 @init {
1819   std::string name;
1820   std::vector<Expr> args;
1821   std::vector<std::string> names;
1822   Expr e;
1823   Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
1824   Type t;
1825 }
1826     /* if-then-else */
1827   : iteTerm[f]
1828
1829     /* parenthesized sub-formula / tuple literals */
1830   | LPAREN formula[f] { args.push_back(f); }
1831     ( COMMA formula[f] { args.push_back(f); } )* RPAREN
1832     { if(args.size() > 1) {
1833         /* If args has elements, we must be a tuple literal.
1834          * Otherwise, f is already the sub-formula, and
1835          * there's nothing to do */
1836         std::vector<Type> types;
1837         for(std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); ++i) {
1838           types.push_back((*i).getType());
1839         }
1840         TupleType t = EXPR_MANAGER->mkTupleType(types);
1841         f = MK_EXPR(kind::TUPLE, args);
1842       }
1843     }
1844
1845     /* empty tuple literal */
1846   | LPAREN RPAREN
1847     { f = MK_EXPR(kind::TUPLE, std::vector<Expr>()); }
1848     /* empty record literal */
1849   | PARENHASH HASHPAREN
1850     { RecordType t = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >());
1851       f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), std::vector<Expr>());
1852     }
1853
1854     /* boolean literals */
1855   | TRUE_TOK  { f = MK_CONST(bool(true)); }
1856   | FALSE_TOK { f = MK_CONST(bool(false)); }
1857     /* arithmetic literals */
1858     /* syntactic predicate: never match INTEGER.DIGIT as an integer and a dot!
1859      * This is a rational constant!  Otherwise the parser interprets it as a tuple
1860      * selector! */
1861   | DECIMAL_LITERAL { f = MK_CONST(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
1862   | INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
1863     /* bitvector literals */
1864   | HEX_LITERAL
1865     { assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 );
1866       std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4);
1867       f = MK_CONST( BitVector(hexString, 16) ); }
1868   | BINARY_LITERAL
1869     { assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 );
1870       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4);
1871       f = MK_CONST( BitVector(binString, 2) ); }
1872     /* record literals */
1873   | PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); }
1874     ( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN
1875     { std::vector< std::pair<std::string, Type> > typeIds;
1876       assert(names.size() == args.size());
1877       for(unsigned i = 0; i < names.size(); ++i) {
1878         typeIds.push_back(std::make_pair(names[i], args[i].getType()));
1879       }
1880       RecordType t = EXPR_MANAGER->mkRecordType(typeIds);
1881       f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), args);
1882     }
1883
1884     /* variable / zero-ary constructor application */
1885   | identifier[name,CHECK_DECLARED,SYM_VARIABLE]
1886     /* ascriptions will be required for parameterized zero-ary constructors */
1887     { f = PARSER_STATE->getVariable(name); }
1888     { // datatypes: zero-ary constructors
1889       Type t2 = PARSER_STATE->getType(name);
1890       if(t2.isConstructor() && ConstructorType(t2).getArity() == 0) {
1891         // don't require parentheses, immediately turn it into an apply
1892         f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, f);
1893       }
1894     }
1895   ;
1896
1897 /**
1898  * Matches (and performs) a type ascription.
1899  * The f arg is the term to check (it is an input-only argument).
1900  */
1901 typeAscription[const CVC4::Expr& f, CVC4::Type& t]
1902 @init {
1903 }
1904   : COLON COLON type[t,CHECK_DECLARED]
1905   ;
1906
1907 /**
1908  * Matches an entry in a record literal.
1909  */
1910 recordEntry[std::string& name, CVC4::Expr& ex]
1911   : identifier[name,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[ex]
1912   ;
1913
1914 /**
1915  * Parses an ITE term.
1916  */
1917 iteTerm[CVC4::Expr& f]
1918 @init {
1919   std::vector<Expr> args;
1920   Debug("parser-extra") << "ite: " << AntlrInput::tokenText(LT(1)) << std::endl;
1921 }
1922   : IF_TOK formula[f] { args.push_back(f); }
1923     THEN_TOK formula[f] { args.push_back(f); }
1924     iteElseTerm[f] { args.push_back(f); }
1925     ENDIF_TOK
1926     { f = MK_EXPR(CVC4::kind::ITE, args); }
1927   ;
1928
1929 /**
1930  * Parses the else part of the ITE, i.e. ELSE f, or ELSIF b THEN f1 ...
1931  */
1932 iteElseTerm[CVC4::Expr& f]
1933 @init {
1934   std::vector<Expr> args;
1935   Debug("parser-extra") << "else: " << AntlrInput::tokenText(LT(1)) << std::endl;
1936 }
1937   : ELSE_TOK formula[f]
1938   | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); }
1939     THEN_TOK iteThen = formula[f] { args.push_back(f); }
1940     iteElse = iteElseTerm[f] { args.push_back(f); }
1941     { f = MK_EXPR(CVC4::kind::ITE, args); }
1942   ;
1943
1944 /**
1945  * Parses a datatype definition
1946  */
1947 datatypeDef[std::vector<CVC4::Datatype>& datatypes]
1948 @init {
1949   std::string id, id2;
1950   Type t;
1951   std::vector< Type > params;
1952 }
1953     /* This really needs to be CHECK_NONE, or mutually-recursive
1954      * datatypes won't work, because this type will already be
1955      * "defined" as an unresolved type; don't worry, we check
1956      * below. */
1957   : identifier[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
1958     ( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] {
1959         t = PARSER_STATE->mkSort(id2, ExprManager::SORT_FLAG_PLACEHOLDER);
1960         params.push_back( t );
1961       }
1962       ( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] {
1963         t = PARSER_STATE->mkSort(id2, ExprManager::SORT_FLAG_PLACEHOLDER);
1964         params.push_back( t ); }
1965       )* RBRACKET
1966     )?
1967     { datatypes.push_back(Datatype(id, params));
1968       if(!PARSER_STATE->isUnresolvedType(id)) {
1969         // if not unresolved, must be undeclared
1970         PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
1971       }
1972     }
1973     EQUAL_TOK constructorDef[datatypes.back()]
1974     ( BAR constructorDef[datatypes.back()] )*
1975     { PARSER_STATE->popScope(); }
1976   ;
1977
1978 /**
1979  * Parses a constructor defintion for type
1980  */
1981 constructorDef[CVC4::Datatype& type]
1982 @init {
1983   std::string id;
1984   CVC4::DatatypeConstructor* ctor = NULL;
1985 }
1986   : identifier[id,CHECK_UNDECLARED,SYM_SORT]
1987     { // make the tester
1988       std::string testerId("is_");
1989       testerId.append(id);
1990       PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
1991       ctor = new CVC4::DatatypeConstructor(id, testerId);
1992     }
1993     ( LPAREN
1994       selector[*ctor]
1995       ( COMMA selector[*ctor] )*
1996       RPAREN
1997     )?
1998     { // make the constructor
1999       type.addConstructor(*ctor);
2000       Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
2001       delete ctor;
2002     }
2003   ;
2004
2005 selector[CVC4::DatatypeConstructor& ctor]
2006 @init {
2007   std::string id;
2008   Type t, t2;
2009 }
2010   : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON type[t,CHECK_NONE]
2011     { ctor.addArg(id, t);
2012       Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
2013     }
2014   ;
2015
2016 /**
2017  * Matches an identifier from the input. An identifier is a sequence of letters,
2018  * digits and "_", "'", "." symbols, starting with a letter.
2019  */
2020 IDENTIFIER : (ALPHA | '_') (ALPHA | DIGIT | '_' | '\'' | '\\' | '?' | '$' | '~')*;
2021
2022 /**
2023  * Same as an integer literal converted to an unsigned int, but
2024  * slightly more convenient AND works around a strange ANTLR bug (?)
2025  * in the BVPLUS/BVMINUS/BVMULT rules where $INTEGER_LITERAL was
2026  * returning a reference to the wrong token?!
2027  */
2028 numeral returns [unsigned k = 0]
2029   : INTEGER_LITERAL
2030     { $k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); }
2031   ;
2032
2033 /**
2034  * Similar to numeral but for arbitrary-precision, signed integer.
2035  */
2036 integer returns [CVC4::Rational k = 0]
2037   : INTEGER_LITERAL
2038     { $k = AntlrInput::tokenToInteger($INTEGER_LITERAL); }
2039   | MINUS_TOK INTEGER_LITERAL
2040     { $k = -AntlrInput::tokenToInteger($INTEGER_LITERAL); }
2041   ;
2042
2043 /**
2044  * Similar to numeral but for strings.
2045  */
2046 str[std::string& s]
2047   : STRING_LITERAL
2048     { s = AntlrInput::tokenText($STRING_LITERAL);
2049       /* strip off the quotes */
2050       s = s.substr(1, s.size() - 2);
2051     }
2052   ;
2053
2054 /**
2055  * Matches a hexadecimal constant.
2056  */
2057 HEX_LITERAL
2058   : '0hex' HEX_DIGIT+
2059   ;
2060
2061 /**
2062  * Matches a binary constant.
2063  */
2064 BINARY_LITERAL
2065   : '0bin' ('0' | '1')+
2066   ;
2067
2068 /**
2069  * Matches a double quoted string literal. Escaping is supported, and
2070  * escape character '\' has to be escaped.
2071  */
2072 STRING_LITERAL: '"' (ESCAPE | ~('"'|'\\'))* '"';
2073
2074 /**
2075  * Matches any letter ('a'-'z' and 'A'-'Z').
2076  */
2077 fragment ALPHA : 'a'..'z' | 'A'..'Z';
2078
2079 /**
2080  * Matches the decimal digits (0-9)
2081  */
2082 fragment DIGIT : '0'..'9';
2083
2084 // This rule adapted from http://www.antlr.org/wiki/pages/viewpage.action?pageId=13828121
2085 // which reportedly comes from Tapestry (http://tapestry.apache.org/tapestry5/)
2086 //
2087 // Special rule that uses parsing tricks to identify numbers and ranges; it's all about
2088 // the dot ('.').
2089 // Recognizes:
2090 // '.' as DOT
2091 // '..' as DOTDOT
2092 // INTEGER_LITERAL (digit+)
2093 // DECIMAL_LITERAL (digit* . digit+)
2094 // Has to watch out for embedded rangeop (i.e. "1..10" is not "1." and ".10").
2095 //
2096 // This doesn't ever generate the NUMBER_OR_RANGEOP token, it
2097 // manipulates the $type inside to return the right token.
2098 NUMBER_OR_RANGEOP
2099   : DIGIT+
2100     (
2101       { LA(2) != '.' }? => '.' DIGIT* { $type = DECIMAL_LITERAL; }
2102       | { $type = INTEGER_LITERAL; }
2103     )
2104   | '.'
2105     ( '.' {$type = DOTDOT; }
2106     | {$type = DOT; }
2107     )
2108   ;
2109
2110 // these empty fragments remove "no lexer rule corresponding to token" warnings
2111 fragment INTEGER_LITERAL:;
2112 fragment DECIMAL_LITERAL:;
2113 fragment DOT:;
2114 fragment DOTDOT:;
2115
2116 /**
2117  * Matches the hexidecimal digits (0-9, a-f, A-F)
2118  */
2119 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
2120
2121 /**
2122  * Matches and skips whitespace in the input and ignores it.
2123  */
2124 WHITESPACE : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); };
2125
2126 /**
2127  * Matches the comments and ignores them
2128  */
2129 COMMENT : '%' (~('\n' | '\r'))* { SKIP(); };
2130
2131 /**
2132  * Matches an allowed escaped character.
2133  */
2134 fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');