src/parser/cvc/Cvc.g

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