src/parser/smt2/Smt2.g

   1 /* *******************                                                        */
   2 /*! \file Smt2.g
   3  ** \verbatim
   4  ** Original author: cconway
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): taking
   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 SMT-LIB v2 input language.
  15  **
  16  ** Parser for SMT-LIB v2 input language.
  17  **/
  18
  19 grammar Smt2;
  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 smt2_input.cpp !
  31   k = 2;
  32 }/* options */
  33
  34 @header {
  35 /**
  36  ** This file is part of the CVC4 prototype.
  37  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  38  ** Courant Institute of Mathematical Sciences
  39  ** New York University
  40  ** See the file COPYING in the top-level source directory for licensing
  41  ** information.
  42  **/
  43 }/* @header */
  44
  45 @lexer::includes {
  46
  47 /** This suppresses warnings about the redefinition of token symbols between
  48   * different parsers. The redefinitions should be harmless as long as no
  49   * client: (a) #include's the lexer headers for two grammars AND (b) uses the
  50   * token symbol definitions.
  51   */
  52 #pragma GCC system_header
  53
  54 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
  55 /* This improves performance by ~10 percent on big inputs.
  56  * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
  57  * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
  58  * Otherwise, we have to let the lexer detect the encoding at runtime.
  59  */
  60 #  define ANTLR3_INLINE_INPUT_ASCII
  61 #  define ANTLR3_INLINE_INPUT_8BIT
  62 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
  63
  64 #include "parser/antlr_tracing.h"
  65
  66 }/* @lexer::includes */
  67
  68 @lexer::postinclude {
  69 #include <stdint.h>
  70
  71 #include "parser/smt2/smt2.h"
  72 #include "parser/antlr_input.h"
  73
  74 using namespace CVC4;
  75 using namespace CVC4::parser;
  76
  77 #undef PARSER_STATE
  78 #define PARSER_STATE ((Smt2*)LEXER->super)
  79 }/* @lexer::postinclude */
  80
  81 @parser::includes {
  82 #include "expr/command.h"
  83 #include "parser/parser.h"
  84 #include "parser/antlr_tracing.h"
  85
  86 namespace CVC4 {
  87   class Expr;
  88
  89   namespace parser {
  90     namespace smt2 {
  91       /**
  92        * Just exists to provide the uintptr_t constructor that ANTLR
  93        * requires.
  94        */
  95       struct myExpr : public CVC4::Expr {
  96         myExpr() : CVC4::Expr() {}
  97         myExpr(void*) : CVC4::Expr() {}
  98         myExpr(const Expr& e) : CVC4::Expr(e) {}
  99         myExpr(const myExpr& e) : CVC4::Expr(e) {}
 100       };/* struct myExpr */
 101     }/* CVC4::parser::smt2 namespace */
 102   }/* CVC4::parser namespace */
 103 }/* CVC4 namespace */
 104
 105 }/* @parser::includes */
 106
 107 @parser::postinclude {
 108
 109 #include "expr/expr.h"
 110 #include "expr/kind.h"
 111 #include "expr/type.h"
 112 #include "parser/antlr_input.h"
 113 #include "parser/parser.h"
 114 #include "parser/smt2/smt2.h"
 115 #include "util/integer.h"
 116 #include "util/output.h"
 117 #include "util/rational.h"
 118 #include "util/hash.h"
 119 #include <vector>
 120 #include <set>
 121 #include <string>
 122 #include <sstream>
 123
 124 using namespace CVC4;
 125 using namespace CVC4::parser;
 126
 127 /* These need to be macros so they can refer to the PARSER macro, which will be defined
 128  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
 129 #undef PARSER_STATE
 130 #define PARSER_STATE ((Smt2*)PARSER->super)
 131 #undef EXPR_MANAGER
 132 #define EXPR_MANAGER PARSER_STATE->getExprManager()
 133 #undef MK_EXPR
 134 #define MK_EXPR EXPR_MANAGER->mkExpr
 135 #undef MK_CONST
 136 #define MK_CONST EXPR_MANAGER->mkConst
 137 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
 138
 139 }/* parser::postinclude */
 140
 141 /**
 142  * Parses an expression.
 143  * @return the parsed expression, or the Null Expr if we've reached the end of the input
 144  */
 145 parseExpr returns [CVC4::parser::smt2::myExpr expr]
 146 @declarations {
 147   Expr expr2;
 148 }
 149   : term[expr, expr2]
 150   | EOF
 151   ;
 152
 153 /**
 154  * Parses a command
 155  * @return the parsed command, or NULL if we've reached the end of the input
 156  */
 157 parseCommand returns [CVC4::Command* cmd = NULL]
 158   : LPAREN_TOK c = command RPAREN_TOK { $cmd = c; }
 159   | EOF { $cmd = 0; }
 160   ;
 161
 162 /**
 163  * Parse the internal portion of the command, ignoring the surrounding parentheses.
 164  */
 165 command returns [CVC4::Command* cmd = NULL]
 166 @declarations {
 167   std::string name;
 168   std::vector<std::string> names;
 169   Expr expr, expr2;
 170   Type t;
 171   std::vector<Expr> terms;
 172   std::vector<Type> sorts;
 173   std::vector<std::pair<std::string, Type> > sortedVarNames;
 174   SExpr sexpr;
 175 }
 176   : /* set the logic */
 177     SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
 178     { Debug("parser") << "set logic: '" << name << "'" << std::endl;
 179       if( PARSER_STATE->logicIsSet() ) {
 180         PARSER_STATE->parseError("Only one set-logic is allowed.");
 181       }
 182       PARSER_STATE->setLogic(name);
 183       $cmd = new SetBenchmarkLogicCommand(name); }
 184   | SET_INFO_TOK KEYWORD symbolicExpr[sexpr]
 185     { name = AntlrInput::tokenText($KEYWORD);
 186       PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
 187       cmd = new SetInfoCommand(name.c_str() + 1, sexpr); }
 188   | /* get-info */
 189     GET_INFO_TOK KEYWORD
 190     { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); }
 191   | /* set-option */
 192     SET_OPTION_TOK KEYWORD symbolicExpr[sexpr]
 193     { name = AntlrInput::tokenText($KEYWORD);
 194       PARSER_STATE->setOption(name.c_str() + 1, sexpr);
 195       cmd = new SetOptionCommand(name.c_str() + 1, sexpr); }
 196   | /* get-option */
 197     GET_OPTION_TOK KEYWORD
 198     { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); }
 199   | /* sort declaration */
 200     DECLARE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 201     symbol[name,CHECK_UNDECLARED,SYM_SORT]
 202     { PARSER_STATE->checkUserSymbol(name); }
 203     n=INTEGER_LITERAL
 204     { Debug("parser") << "declare sort: '" << name
 205                       << "' arity=" << n << std::endl;
 206       unsigned arity = AntlrInput::tokenToUnsigned(n);
 207       if(arity == 0) {
 208         Type type = PARSER_STATE->mkSort(name);
 209         $cmd = new DeclareTypeCommand(name, 0, type);
 210       } else {
 211         Type type = PARSER_STATE->mkSortConstructor(name, arity);
 212         $cmd = new DeclareTypeCommand(name, arity, type);
 213       }
 214     }
 215   | /* sort definition */
 216     DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 217     symbol[name,CHECK_UNDECLARED,SYM_SORT]
 218     { PARSER_STATE->checkUserSymbol(name); }
 219     LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
 220     {
 221       PARSER_STATE->pushScope();
 222       for(std::vector<std::string>::const_iterator i = names.begin(),
 223             iend = names.end();
 224           i != iend;
 225           ++i) {
 226         sorts.push_back(PARSER_STATE->mkSort(*i));
 227       }
 228     }
 229     sortSymbol[t,CHECK_DECLARED]
 230     { PARSER_STATE->popScope();
 231       // Do NOT call mkSort, since that creates a new sort!
 232       // This name is not its own distinct sort, it's an alias.
 233       PARSER_STATE->defineParameterizedType(name, sorts, t);
 234       $cmd = new DefineTypeCommand(name, sorts, t);
 235     }
 236   | /* function declaration */
 237     DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 238     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 239     { PARSER_STATE->checkUserSymbol(name); }
 240     LPAREN_TOK sortList[sorts] RPAREN_TOK
 241     sortSymbol[t,CHECK_DECLARED]
 242     { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
 243       if( sorts.size() > 0 ) {
 244         t = EXPR_MANAGER->mkFunctionType(sorts, t);
 245       }
 246       Expr func = PARSER_STATE->mkVar(name, t);
 247       $cmd = new DeclareFunctionCommand(name, func, t); }
 248   | /* function definition */
 249     DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 250     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 251     { PARSER_STATE->checkUserSymbol(name); }
 252     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
 253     sortSymbol[t,CHECK_DECLARED]
 254     { /* add variables to parser state before parsing term */
 255       Debug("parser") << "define fun: '" << name << "'" << std::endl;
 256       if( sortedVarNames.size() > 0 ) {
 257         std::vector<CVC4::Type> sorts;
 258         sorts.reserve(sortedVarNames.size());
 259         for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 260               sortedVarNames.begin(), iend = sortedVarNames.end();
 261             i != iend;
 262             ++i) {
 263           sorts.push_back((*i).second);
 264         }
 265         t = EXPR_MANAGER->mkFunctionType(sorts, t);
 266       }
 267       PARSER_STATE->pushScope();
 268       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 269             sortedVarNames.begin(), iend = sortedVarNames.end();
 270           i != iend;
 271           ++i) {
 272         terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
 273       }
 274     }
 275     term[expr, expr2]
 276     { PARSER_STATE->popScope();
 277       // declare the name down here (while parsing term, signature
 278       // must not be extended with the name itself; no recursion
 279       // permitted)
 280       Expr func = PARSER_STATE->mkFunction(name, t);
 281       $cmd = new DefineFunctionCommand(name, func, terms, expr);
 282     }
 283   | /* value query */
 284     GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 285     LPAREN_TOK termList[terms,expr] RPAREN_TOK
 286     { $cmd = new GetValueCommand(terms); }
 287   | /* get-assignment */
 288     GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 289     { cmd = new GetAssignmentCommand; }
 290   | /* assertion */
 291     ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 292     term[expr, expr2]
 293     { cmd = new AssertCommand(expr); }
 294   | /* checksat */
 295     CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 296     { cmd = new CheckSatCommand(MK_CONST(bool(true))); }
 297   | /* get-assertions */
 298     GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 299     { cmd = new GetAssertionsCommand; }
 300   | /* get-proof */
 301     GET_PROOF_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 302     { cmd = new GetProofCommand; }
 303   | /* get-unsat-core */
 304     GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 305     { cmd = new GetUnsatCoreCommand; }
 306   | /* push */
 307     PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 308     ( k=INTEGER_LITERAL
 309       { unsigned n = AntlrInput::tokenToUnsigned(k);
 310         if(n == 0) {
 311           cmd = new EmptyCommand;
 312         } else if(n == 1) {
 313           cmd = new PushCommand;
 314         } else {
 315           CommandSequence* seq = new CommandSequence;
 316           do {
 317             seq->addCommand(new PushCommand);
 318           } while(--n > 0);
 319           cmd = seq;
 320         }
 321       }
 322     | { if(PARSER_STATE->strictModeEnabled()) {
 323           PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to PUSH.  Maybe you want (push 1)?");
 324         } else {
 325           cmd = new PushCommand;
 326         }
 327       } )
 328   | POP_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 329     ( k=INTEGER_LITERAL
 330       { unsigned n = AntlrInput::tokenToUnsigned(k);
 331         if(n == 0) {
 332           cmd = new EmptyCommand;
 333         } else if(n == 1) {
 334           cmd = new PopCommand;
 335         } else {
 336           CommandSequence* seq = new CommandSequence;
 337           do {
 338             seq->addCommand(new PopCommand);
 339           } while(--n > 0);
 340           cmd = seq;
 341         }
 342       }
 343     | { if(PARSER_STATE->strictModeEnabled()) {
 344           PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to POP.  Maybe you want (pop 1)?");
 345         } else {
 346           cmd = new PopCommand;
 347         }
 348       } )
 349   | EXIT_TOK
 350     { cmd = new QuitCommand; }
 351
 352     /* CVC4-extended SMT-LIBv2 commands */
 353   | extendedCommand[cmd]
 354     { if(PARSER_STATE->strictModeEnabled()) {
 355         PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode.");
 356       }
 357     }
 358   ;
 359
 360 extendedCommand[CVC4::Command*& cmd]
 361 @declarations {
 362   std::vector<CVC4::Datatype> dts;
 363   Type t;
 364   Expr e, e2;
 365   SExpr sexpr;
 366   std::string name;
 367   std::vector<std::string> names;
 368   std::vector<Type> sorts;
 369 }
 370     /* Extended SMT-LIBv2 set of commands syntax, not permitted in
 371      * --smtlib2 compliance mode. */
 372   : DECLARE_DATATYPES_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 373     { /* open a scope to keep the UnresolvedTypes contained */
 374       PARSER_STATE->pushScope(); }
 375     LPAREN_TOK RPAREN_TOK  //TODO: parametric datatypes
 376     LPAREN_TOK ( LPAREN_TOK datatypeDef[dts] RPAREN_TOK )+ RPAREN_TOK
 377     { PARSER_STATE->popScope();
 378       cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
 379   | /* get model */
 380     GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 381     { cmd = new GetModelCommand; }
 382   | ECHO_TOK
 383     ( simpleSymbolicExpr[sexpr]
 384       { std::stringstream ss;
 385         ss << sexpr;
 386         cmd = new EchoCommand(ss.str());
 387       }
 388     | { cmd = new EchoCommand(); }
 389     )
 390   | rewriterulesCommand[cmd]
 391   ;
 392
 393 rewriterulesCommand[CVC4::Command*& cmd]
 394 @declarations {
 395   std::vector<std::pair<std::string, Type> > sortedVarNames;
 396   std::vector<Expr> args, guards, heads, triggers;
 397   Expr head, body, expr, expr2, bvl;
 398   Kind kind;
 399 }
 400   : /* rewrite rules */
 401     REWRITE_RULE_TOK
 402     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
 403     {
 404       kind = CVC4::kind::RR_REWRITE;
 405       PARSER_STATE->pushScope();
 406       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 407             sortedVarNames.begin(), iend = sortedVarNames.end();
 408           i != iend;
 409           ++i) {
 410         args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
 411       }
 412       bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
 413     }
 414     LPAREN_TOK (termList[guards,expr])? RPAREN_TOK
 415     term[head, expr2] term[body, expr2]
 416     LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK
 417     {
 418       args.clear();
 419       args.push_back(head);
 420       args.push_back(body);
 421       /* triggers */
 422       if( !triggers.empty() ){
 423         expr2 = MK_EXPR(kind::INST_PATTERN_LIST, triggers);
 424         args.push_back(expr2);
 425       };
 426       expr = MK_EXPR(kind, args);
 427       args.clear();
 428       args.push_back(bvl);
 429       /* guards */
 430       switch( guards.size() ){
 431       case 0:
 432         args.push_back(MK_CONST(bool(true))); break;
 433       case 1:
 434         args.push_back(guards[0]); break;
 435       default:
 436         expr2 = MK_EXPR(kind::AND, guards);
 437         args.push_back(expr2); break;
 438       };
 439       args.push_back(expr);
 440       expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
 441       cmd = new AssertCommand(expr); }
 442     /* propagation rule */
 443   | rewritePropaKind[kind]
 444     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
 445     {
 446       PARSER_STATE->pushScope();
 447       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 448             sortedVarNames.begin(), iend = sortedVarNames.end();
 449           i != iend;
 450           ++i) {
 451         args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
 452       }
 453       bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
 454     }
 455     LPAREN_TOK (termList[guards,expr])? RPAREN_TOK
 456     LPAREN_TOK (termList[heads,expr])? RPAREN_TOK
 457     term[body, expr2]
 458     LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK
 459     {
 460       args.clear();
 461       /* heads */
 462       switch( heads.size() ){
 463       case 0:
 464         args.push_back(MK_CONST(bool(true))); break;
 465       case 1:
 466         args.push_back(heads[0]); break;
 467       default:
 468         expr2 = MK_EXPR(kind::AND, heads);
 469         args.push_back(expr2); break;
 470       };
 471       args.push_back(body);
 472       /* triggers */
 473       if( !triggers.empty() ){
 474         expr2 = MK_EXPR(kind::INST_PATTERN_LIST, triggers);
 475         args.push_back(expr2);
 476       };
 477       expr = MK_EXPR(kind, args);
 478       args.clear();
 479       args.push_back(bvl);
 480       /* guards */
 481       switch( guards.size() ){
 482       case 0:
 483         args.push_back(MK_CONST(bool(true))); break;
 484       case 1:
 485         args.push_back(guards[0]); break;
 486       default:
 487         expr2 = MK_EXPR(kind::AND, guards);
 488         args.push_back(expr2); break;
 489       };
 490       args.push_back(expr);
 491       expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
 492       cmd = new AssertCommand(expr); }
 493   ;
 494
 495 rewritePropaKind[CVC4::Kind& kind]
 496   :
 497   REDUCTION_RULE_TOK    { $kind = CVC4::kind::RR_REDUCTION; }
 498   | PROPAGATION_RULE_TOK  { $kind = CVC4::kind::RR_DEDUCTION; }
 499   ;
 500
 501 pattern[CVC4::Expr& expr]
 502 @declarations {
 503   std::vector<Expr> patexpr;
 504 }
 505   : LPAREN_TOK termList[patexpr,expr] RPAREN_TOK
 506     {
 507       expr = MK_EXPR(kind::INST_PATTERN, patexpr);
 508       //std::cout << "parsed pattern expr " << retExpr << std::endl;
 509     }
 510   ;
 511
 512 simpleSymbolicExpr[CVC4::SExpr& sexpr]
 513 @declarations {
 514   CVC4::Kind k;
 515   std::string s;
 516 }
 517   : INTEGER_LITERAL
 518     { sexpr = SExpr(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
 519   | DECIMAL_LITERAL
 520     { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
 521   | str[s]
 522     { sexpr = SExpr(s); }
 523   | symbol[s,CHECK_NONE,SYM_SORT]
 524     { sexpr = SExpr(s); }
 525   | builtinOp[k]
 526     { std::stringstream ss;
 527       ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k);
 528       sexpr = SExpr(ss.str());
 529     }
 530   | KEYWORD
 531     { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
 532   ;
 533
 534 symbolicExpr[CVC4::SExpr& sexpr]
 535 @declarations {
 536   std::vector<SExpr> children;
 537 }
 538   : simpleSymbolicExpr[sexpr]
 539   | LPAREN_TOK
 540     (symbolicExpr[sexpr] { children.push_back(sexpr); } )*
 541         RPAREN_TOK
 542     { sexpr = SExpr(children); }
 543   ;
 544
 545 /**
 546  * Matches a term.
 547  * @return the expression representing the formula
 548  */
 549 term[CVC4::Expr& expr, CVC4::Expr& expr2]
 550 @init {
 551   Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
 552   Kind kind;
 553   Expr op;
 554   std::string name;
 555   std::vector<Expr> args;
 556   SExpr sexpr;
 557   std::vector< std::pair<std::string, Type> > sortedVarNames;
 558   Expr f, f2;
 559   std::string attr;
 560   Expr attexpr;
 561   std::vector<Expr> patexprs;
 562   std::hash_set<std::string, StringHashFunction> names;
 563   std::vector< std::pair<std::string, Expr> > binders;
 564 }
 565   : /* a built-in operator application */
 566     LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
 567     {
 568       if( kind == CVC4::kind::EQUAL &&
 569           args.size() > 0 &&
 570           args[0].getType() == EXPR_MANAGER->booleanType() ) {
 571         /* Use IFF for boolean equalities. */
 572         kind = CVC4::kind::IFF;
 573       }
 574
 575       if( !PARSER_STATE->strictModeEnabled() &&
 576           (kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
 577           args.size() == 1) {
 578         /* Unary AND/OR can be replaced with the argument.
 579                It just so happens expr should already by the only argument. */
 580         Assert( expr == args[0] );
 581       } else if( CVC4::kind::isAssociative(kind) &&
 582                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
 583         /* Special treatment for associative operators with lots of children */
 584         expr = EXPR_MANAGER->mkAssociative(kind,args);
 585       } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) {
 586         expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
 587       } else {
 588         PARSER_STATE->checkOperator(kind, args.size());
 589         expr = MK_EXPR(kind, args);
 590       }
 591     }
 592   | LPAREN_TOK quantOp[kind]
 593     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
 594     {
 595       PARSER_STATE->pushScope();
 596       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 597             sortedVarNames.begin(), iend = sortedVarNames.end();
 598           i != iend;
 599           ++i) {
 600         args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
 601       }
 602       Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
 603       args.clear();
 604       args.push_back(bvl);
 605     }
 606     term[f, f2] RPAREN_TOK
 607     {
 608       PARSER_STATE->popScope();
 609       switch(f.getKind()) {
 610       case CVC4::kind::RR_REWRITE:
 611       case CVC4::kind::RR_REDUCTION:
 612       case CVC4::kind::RR_DEDUCTION:
 613         if(kind == CVC4::kind::EXISTS) {
 614           PARSER_STATE->parseError("Use Exists instead of Forall for a rewrite rule.");
 615         }
 616         args.push_back(f2); // guards
 617         args.push_back(f); // rule
 618         expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
 619         break;
 620       default:
 621         args.push_back(f);
 622         if(! f2.isNull()){
 623           args.push_back(f2);
 624         }
 625         expr = MK_EXPR(kind, args);
 626       }
 627     }
 628   | /* A non-built-in function application */
 629     LPAREN_TOK
 630     functionName[name, CHECK_DECLARED]
 631     { PARSER_STATE->checkFunctionLike(name);
 632       const bool isDefinedFunction =
 633         PARSER_STATE->isDefinedFunction(name);
 634       if(isDefinedFunction) {
 635         expr = PARSER_STATE->getFunction(name);
 636         kind = CVC4::kind::APPLY;
 637       } else {
 638         expr = PARSER_STATE->getVariable(name);
 639         Type t = expr.getType();
 640         if(t.isConstructor()) {
 641           kind = CVC4::kind::APPLY_CONSTRUCTOR;
 642         } else if(t.isSelector()) {
 643           kind = CVC4::kind::APPLY_SELECTOR;
 644         } else if(t.isTester()) {
 645           kind = CVC4::kind::APPLY_TESTER;
 646         } else {
 647           kind = CVC4::kind::APPLY_UF;
 648         }
 649       }
 650       args.push_back(expr);
 651     }
 652     termList[args,expr] RPAREN_TOK
 653     { Debug("parser") << "args has size " << args.size() << std::endl << "expr is " << expr << std::endl;
 654       for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
 655         Debug("parser") << "++ " << *i << std::endl;
 656       expr = MK_EXPR(kind, args); }
 657
 658   | /* An indexed function application */
 659     LPAREN_TOK indexedFunctionName[op] termList[args,expr] RPAREN_TOK
 660     { expr = MK_EXPR(op, args); }
 661
 662   | /* a let binding */
 663     LPAREN_TOK LET_TOK LPAREN_TOK
 664     { PARSER_STATE->pushScope(); }
 665     ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] term[expr, f2] RPAREN_TOK
 666       // this is a parallel let, so we have to save up all the contributions
 667       // of the let and define them only later on
 668       { if(names.count(name) == 1) {
 669           std::stringstream ss;
 670           ss << "warning: symbol `" << name << "' bound multiple times by let; the last binding will be used, shadowing earlier ones";
 671           PARSER_STATE->warning(ss.str());
 672         } else {
 673           names.insert(name);
 674         }
 675         binders.push_back(std::make_pair(name, expr)); } )+
 676     { // now implement these bindings
 677       for(std::vector< std::pair<std::string, Expr> >::iterator i = binders.begin(); i != binders.end(); ++i) {
 678         PARSER_STATE->defineVar((*i).first, (*i).second);
 679       }
 680     }
 681     RPAREN_TOK
 682     term[expr, f2]
 683     RPAREN_TOK
 684     { PARSER_STATE->popScope(); }
 685
 686     /* a variable */
 687   | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
 688     { const bool isDefinedFunction =
 689         PARSER_STATE->isDefinedFunction(name);
 690       if(isDefinedFunction) {
 691         expr = MK_EXPR(CVC4::kind::APPLY,
 692                        PARSER_STATE->getFunction(name));
 693       } else {
 694         expr = PARSER_STATE->getVariable(name);
 695         Type t = PARSER_STATE->getType(name);
 696         if(t.isConstructor() && ConstructorType(t).getArity() == 0) {
 697           // don't require parentheses, immediately turn it into an apply
 698           expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
 699         }
 700       }
 701     }
 702
 703     /* attributed expressions */
 704   | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
 705     ( attribute[expr, attexpr,attr]
 706       { if( attr == ":pattern" && ! attexpr.isNull()) {
 707           patexprs.push_back( attexpr );
 708         }
 709       }
 710     )+ RPAREN_TOK
 711     {
 712       if(attr == ":rewrite-rule") {
 713         Expr guard;
 714         Expr body;
 715         if(expr[1].getKind() == kind::IMPLIES ||
 716            expr[1].getKind() == kind::IFF ||
 717            expr[1].getKind() == kind::EQUAL) {
 718           guard = expr[0];
 719           body = expr[1];
 720         } else {
 721           guard = MK_CONST(bool(true));
 722           body = expr;
 723         }
 724         expr2 = guard;
 725         args.push_back(body[0]);
 726         args.push_back(body[1]);
 727         if(!f2.isNull()) {
 728           args.push_back(f2);
 729         }
 730
 731         if     ( body.getKind()==kind::IMPLIES )    kind = kind::RR_DEDUCTION;
 732         else if( body.getKind()==kind::IFF )        kind = kind::RR_REDUCTION;
 733         else if( body.getKind()==kind::EQUAL )      kind = kind::RR_REWRITE;
 734         else PARSER_STATE->parseError("Error parsing rewrite rule.");
 735
 736         expr = MK_EXPR( kind, args );
 737       } else if(! patexprs.empty()) {
 738         if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){
 739           for( size_t i=0; i<f2.getNumChildren(); i++ ){
 740             patexprs.push_back( f2[i] );
 741           }
 742         }
 743         expr2 = MK_EXPR(kind::INST_PATTERN_LIST, patexprs);
 744       }else{
 745         expr2 = f2;
 746       }
 747     }
 748     /* constants */
 749   | INTEGER_LITERAL
 750     { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
 751
 752   | DECIMAL_LITERAL
 753     { // FIXME: This doesn't work because an SMT rational is not a
 754       // valid GMP rational string
 755       expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
 756
 757   | LPAREN_TOK INDEX_TOK bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL RPAREN_TOK
 758     { if(AntlrInput::tokenText($bvLit).find("bv") == 0) {
 759         expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) );
 760       } else {
 761         PARSER_STATE->parseError("Unexpected symbol `" + AntlrInput::tokenText($bvLit) + "'");
 762       }
 763     }
 764
 765   | HEX_LITERAL
 766     { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
 767       std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
 768       expr = MK_CONST( BitVector(hexString, 16) ); }
 769
 770   | BINARY_LITERAL
 771     { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
 772       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
 773       expr = MK_CONST( BitVector(binString, 2) ); }
 774
 775     // NOTE: Theory constants go here
 776   ;
 777
 778 /**
 779  * Read attribute
 780  */
 781 attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
 782 @init {
 783   SExpr sexpr;
 784   Expr patexpr;
 785   std::vector<Expr> patexprs;
 786   Expr e2;
 787 }
 788 : KEYWORD
 789   {
 790     attr = AntlrInput::tokenText($KEYWORD);
 791     //EXPR_MANAGER->setNamedAttribute( expr, attr );
 792     if( attr==":rewrite-rule" ){
 793       //do nothing
 794     } else if( attr==":axiom" || attr==":conjecture" ){
 795       std::string attr_name = attr;
 796       attr_name.erase( attr_name.begin() );
 797       Command* c = new SetUserAttributeCommand( attr_name, expr );
 798       PARSER_STATE->preemptCommand(c);
 799     } else {
 800       std::stringstream ss;
 801       ss << "Attribute `" << attr << "' not supported";
 802       PARSER_STATE->parseError(ss.str());
 803     }
 804   }
 805   | ATTRIBUTE_PATTERN_TOK LPAREN_TOK ( term[patexpr, e2] { patexprs.push_back( patexpr ); }  )+ RPAREN_TOK
 806     {
 807       attr = std::string(":pattern");
 808       retExpr = MK_EXPR(kind::INST_PATTERN, patexprs);
 809     }
 810   | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
 811     {
 812       attr = std::string(":named");
 813       std::string name = sexpr.getValue();
 814       // FIXME ensure expr is a closed subterm
 815       // check that sexpr is a fresh function symbol
 816       PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
 817       // define it
 818       Expr func = PARSER_STATE->mkFunction(name, expr.getType());
 819       // bind name to expr with define-fun
 820       Command* c =
 821         new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
 822       PARSER_STATE->preemptCommand(c);
 823     }
 824   ;
 825
 826 /**
 827  * Matches a bit-vector operator (the ones parametrized by numbers)
 828  */
 829 indexedFunctionName[CVC4::Expr& op]
 830   : LPAREN_TOK INDEX_TOK
 831     ( 'extract' n1=INTEGER_LITERAL n2=INTEGER_LITERAL
 832       { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1),
 833                                        AntlrInput::tokenToUnsigned($n2))); }
 834     | 'repeat' n=INTEGER_LITERAL
 835       { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
 836     | 'zero_extend' n=INTEGER_LITERAL
 837       { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
 838     | 'sign_extend' n=INTEGER_LITERAL
 839       { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); }
 840     | 'rotate_left' n=INTEGER_LITERAL
 841       { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
 842     | 'rotate_right' n=INTEGER_LITERAL
 843       { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
 844     | badIndexedFunctionName
 845    )
 846     RPAREN_TOK
 847   ;
 848
 849 /**
 850  * Matches an erroneous indexed function name (and args) for better
 851  * error reporting.
 852  */
 853 badIndexedFunctionName
 854 @declarations {
 855   std::string name;
 856 }
 857   : symbol[name,CHECK_NONE,SYM_VARIABLE] INTEGER_LITERAL+
 858       { PARSER_STATE->parseError(std::string("Unknown indexed function `") + name + "'"); }
 859   ;
 860
 861 /**
 862  * Matches a sequence of terms and puts them into the formulas
 863  * vector.
 864  * @param formulas the vector to fill with terms
 865  * @param expr an Expr reference for the elements of the sequence
 866  */
 867 /* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
 868  * time through this rule. */
 869 termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
 870 @declarations {
 871   Expr expr2;
 872 }
 873   : ( term[expr, expr2] { formulas.push_back(expr); } )+
 874   ;
 875
 876 /**
 877  * Matches a string, and strips off the quotes.
 878  */
 879 str[std::string& s]
 880   : STRING_LITERAL
 881     { s = AntlrInput::tokenText($STRING_LITERAL);
 882       /* strip off the quotes */
 883       s = s.substr(1, s.size() - 2);
 884     }
 885   ;
 886
 887 /**
 888  * Matches a builtin operator symbol and sets kind to its associated Expr kind.
 889  */
 890 builtinOp[CVC4::Kind& kind]
 891 @init {
 892   Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
 893 }
 894   : NOT_TOK      { $kind = CVC4::kind::NOT;     }
 895   | IMPLIES_TOK  { $kind = CVC4::kind::IMPLIES; }
 896   | AND_TOK      { $kind = CVC4::kind::AND;     }
 897   | OR_TOK       { $kind = CVC4::kind::OR;      }
 898   | XOR_TOK      { $kind = CVC4::kind::XOR;     }
 899   | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
 900   | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
 901   | ITE_TOK      { $kind = CVC4::kind::ITE; }
 902   | GREATER_THAN_TOK
 903                  { $kind = CVC4::kind::GT; }
 904   | GREATER_THAN_EQUAL_TOK
 905                  { $kind = CVC4::kind::GEQ; }
 906   | LESS_THAN_EQUAL_TOK
 907                  { $kind = CVC4::kind::LEQ; }
 908   | LESS_THAN_TOK
 909                  { $kind = CVC4::kind::LT; }
 910   | PLUS_TOK     { $kind = CVC4::kind::PLUS; }
 911   | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
 912   | STAR_TOK     { $kind = CVC4::kind::MULT; }
 913   | DIV_TOK      { $kind = CVC4::kind::DIVISION; }
 914   | INTS_DIV_TOK      { $kind = CVC4::kind::INTS_DIVISION; }
 915   | INTS_MOD_TOK      { $kind = CVC4::kind::INTS_MODULUS; }
 916
 917   | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
 918   | STORE_TOK    { $kind = CVC4::kind::STORE; }
 919
 920   | CONCAT_TOK   { $kind = CVC4::kind::BITVECTOR_CONCAT; }
 921   | BVNOT_TOK   { $kind = CVC4::kind::BITVECTOR_NOT; }
 922   | BVAND_TOK   { $kind = CVC4::kind::BITVECTOR_AND; }
 923   | BVOR_TOK   { $kind = CVC4::kind::BITVECTOR_OR; }
 924   | BVNEG_TOK   { $kind = CVC4::kind::BITVECTOR_NEG; }
 925   | BVADD_TOK   { $kind = CVC4::kind::BITVECTOR_PLUS; }
 926   | BVMUL_TOK   { $kind = CVC4::kind::BITVECTOR_MULT; }
 927   | BVUDIV_TOK   { $kind = CVC4::kind::BITVECTOR_UDIV; }
 928   | BVUREM_TOK   { $kind = CVC4::kind::BITVECTOR_UREM; }
 929   | BVSHL_TOK     { $kind = CVC4::kind::BITVECTOR_SHL; }
 930   | BVLSHR_TOK     { $kind = CVC4::kind::BITVECTOR_LSHR; }
 931   | BVULT_TOK     { $kind = CVC4::kind::BITVECTOR_ULT; }
 932   | BVNAND_TOK     { $kind = CVC4::kind::BITVECTOR_NAND; }
 933   | BVNOR_TOK     { $kind = CVC4::kind::BITVECTOR_NOR; }
 934   | BVXOR_TOK     { $kind = CVC4::kind::BITVECTOR_XOR; }
 935   | BVXNOR_TOK     { $kind = CVC4::kind::BITVECTOR_XNOR; }
 936   | BVCOMP_TOK     { $kind = CVC4::kind::BITVECTOR_COMP; }
 937   | BVSUB_TOK     { $kind = CVC4::kind::BITVECTOR_SUB; }
 938   | BVSDIV_TOK     { $kind = CVC4::kind::BITVECTOR_SDIV; }
 939   | BVSREM_TOK     { $kind = CVC4::kind::BITVECTOR_SREM; }
 940   | BVSMOD_TOK     { $kind = CVC4::kind::BITVECTOR_SMOD; }
 941   | BVASHR_TOK     { $kind = CVC4::kind::BITVECTOR_ASHR; }
 942   | BVULE_TOK     { $kind = CVC4::kind::BITVECTOR_ULE; }
 943   | BVUGT_TOK     { $kind = CVC4::kind::BITVECTOR_UGT; }
 944   | BVUGE_TOK     { $kind = CVC4::kind::BITVECTOR_UGE; }
 945   | BVSLT_TOK     { $kind = CVC4::kind::BITVECTOR_SLT; }
 946   | BVSLE_TOK     { $kind = CVC4::kind::BITVECTOR_SLE; }
 947   | BVSGT_TOK     { $kind = CVC4::kind::BITVECTOR_SGT; }
 948   | BVSGE_TOK     { $kind = CVC4::kind::BITVECTOR_SGE; }
 949
 950   // NOTE: Theory operators go here
 951   ;
 952
 953 quantOp[CVC4::Kind& kind]
 954 @init {
 955   Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
 956 }
 957   : EXISTS_TOK      { $kind = CVC4::kind::EXISTS; }
 958   | FORALL_TOK    { $kind = CVC4::kind::FORALL; }
 959   ;
 960
 961 /**
 962  * Matches a (possibly undeclared) function symbol (returning the string)
 963  * @param check what kind of check to do with the symbol
 964  */
 965 functionName[std::string& name, CVC4::parser::DeclarationCheck check]
 966   : symbol[name,check,SYM_VARIABLE]
 967   ;
 968
 969 /**
 970  * Matches an previously declared function symbol (returning an Expr)
 971  */
 972 functionSymbol[CVC4::Expr& fun]
 973 @declarations {
 974         std::string name;
 975 }
 976   : functionName[name,CHECK_DECLARED]
 977     { PARSER_STATE->checkFunctionLike(name);
 978       fun = PARSER_STATE->getVariable(name); }
 979   ;
 980
 981 /**
 982  * Matches a sequence of sort symbols and fills them into the given
 983  * vector.
 984  */
 985 sortList[std::vector<CVC4::Type>& sorts]
 986 @declarations {
 987   Type t;
 988 }
 989   : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
 990   ;
 991
 992 nonemptySortList[std::vector<CVC4::Type>& sorts]
 993 @declarations {
 994   Type t;
 995 }
 996   : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+
 997   ;
 998
 999 /**
1000  * Matches a sequence of (variable,sort) symbol pairs and fills them
1001  * into the given vector.
1002  */
1003 sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars]
1004 @declarations {
1005   std::string name;
1006   Type t;
1007 }
1008   : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] RPAREN_TOK
1009       { sortedVars.push_back(make_pair(name, t)); }
1010     )*
1011   ;
1012
1013 /**
1014  * Matches the sort symbol, which can be an arbitrary symbol.
1015  * @param check the check to perform on the name
1016  */
1017 sortName[std::string& name, CVC4::parser::DeclarationCheck check]
1018   : symbol[name,check,SYM_SORT]
1019   ;
1020
1021 sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
1022 @declarations {
1023   std::string name;
1024   std::vector<CVC4::Type> args;
1025   std::vector<uint64_t> numerals;
1026 }
1027   : sortName[name,CHECK_NONE]
1028         {
1029           if( check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT) ){
1030             t = PARSER_STATE->getSort(name);
1031           }else{
1032             t = PARSER_STATE->mkUnresolvedType(name);
1033           }
1034         }
1035   | LPAREN_TOK INDEX_TOK symbol[name,CHECK_NONE,SYM_SORT] nonemptyNumeralList[numerals] RPAREN_TOK
1036     {
1037       if( name == "BitVec" ) {
1038         if( numerals.size() != 1 ) {
1039           PARSER_STATE->parseError("Illegal bitvector type.");
1040         }
1041         t = EXPR_MANAGER->mkBitVectorType(numerals.front());
1042       } else {
1043         Unhandled(name);
1044       }
1045     }
1046   | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
1047     {
1048       if( name == "Array" ) {
1049         if( args.size() != 2 ) {
1050           PARSER_STATE->parseError("Illegal array type.");
1051         }
1052         t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
1053       } else {
1054         t = PARSER_STATE->getSort(name, args);
1055       }
1056     }
1057   ;
1058
1059 /**
1060  * Matches a list of symbols, with check and type arguments as for the
1061  * symbol[] rule below.
1062  */
1063 symbolList[std::vector<std::string>& names,
1064            CVC4::parser::DeclarationCheck check,
1065            CVC4::parser::SymbolType type]
1066 @declarations {
1067   std::string id;
1068 }
1069   : ( symbol[id,check,type] { names.push_back(id); } )*
1070   ;
1071
1072 /**
1073  * Matches an symbol and sets the string reference parameter id.
1074  * @param id string to hold the symbol
1075  * @param check what kinds of check to do on the symbol
1076  * @param type the intended namespace for the symbol
1077  */
1078 symbol[std::string& id,
1079        CVC4::parser::DeclarationCheck check,
1080        CVC4::parser::SymbolType type]
1081   : SIMPLE_SYMBOL
1082     { id = AntlrInput::tokenText($SIMPLE_SYMBOL);
1083       PARSER_STATE->checkDeclaration(id, check, type);
1084     }
1085   | QUOTED_SYMBOL
1086     { id = AntlrInput::tokenText($QUOTED_SYMBOL);
1087       /* strip off the quotes */
1088       id = id.substr(1, id.size() - 2);
1089       PARSER_STATE->checkDeclaration(id, check, type);
1090     }
1091   ;
1092
1093 /**
1094  * Matches a nonempty list of numerals.
1095  * @param numerals the (empty) vector to house the numerals.
1096  */
1097 nonemptyNumeralList[std::vector<uint64_t>& numerals]
1098   : ( INTEGER_LITERAL
1099       { numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
1100     )+
1101   ;
1102
1103 /**
1104  * Parses a datatype definition
1105  */
1106 datatypeDef[std::vector<CVC4::Datatype>& datatypes]
1107 @init {
1108   std::string id, id2;
1109   Type t;
1110   std::vector< Type > params;
1111 }
1112     /* This really needs to be CHECK_NONE, or mutually-recursive
1113      * datatypes won't work, because this type will already be
1114      * "defined" as an unresolved type; don't worry, we check
1115      * below. */
1116   : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
1117     ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
1118         t = PARSER_STATE->mkSort(id2);
1119         params.push_back( t );
1120       }
1121       ( symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
1122         t = PARSER_STATE->mkSort(id2);
1123         params.push_back( t ); }
1124       )* ']'
1125     )?
1126     { datatypes.push_back(Datatype(id,params));
1127       if(!PARSER_STATE->isUnresolvedType(id)) {
1128         // if not unresolved, must be undeclared
1129         PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
1130       }
1131     }
1132     ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+
1133     { PARSER_STATE->popScope(); }
1134   ;
1135
1136 /**
1137  * Parses a constructor defintion for type
1138  */
1139 constructorDef[CVC4::Datatype& type]
1140 @init {
1141   std::string id;
1142   CVC4::DatatypeConstructor* ctor = NULL;
1143 }
1144   : symbol[id,CHECK_UNDECLARED,SYM_SORT]
1145     { // make the tester
1146       std::string testerId("is_");
1147       testerId.append(id);
1148       PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
1149       ctor = new CVC4::DatatypeConstructor(id, testerId);
1150     }
1151     ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
1152     { // make the constructor
1153       type.addConstructor(*ctor);
1154       Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
1155       delete ctor;
1156     }
1157   ;
1158
1159 selector[CVC4::DatatypeConstructor& ctor]
1160 @init {
1161   std::string id;
1162   Type t, t2;
1163 }
1164   : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t,CHECK_NONE]
1165     { ctor.addArg(id, t);
1166       Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
1167     }
1168   ;
1169
1170 // Base SMT-LIB tokens
1171 ASSERT_TOK : 'assert';
1172 CHECKSAT_TOK : 'check-sat';
1173 DECLARE_FUN_TOK : 'declare-fun';
1174 DECLARE_SORT_TOK : 'declare-sort';
1175 DEFINE_FUN_TOK : 'define-fun';
1176 DEFINE_SORT_TOK : 'define-sort';
1177 GET_VALUE_TOK : 'get-value';
1178 GET_ASSIGNMENT_TOK : 'get-assignment';
1179 GET_ASSERTIONS_TOK : 'get-assertions';
1180 GET_PROOF_TOK : 'get-proof';
1181 GET_UNSAT_CORE_TOK : 'get-unsat-core';
1182 EXIT_TOK : 'exit';
1183 ITE_TOK : 'ite';
1184 LET_TOK : 'let';
1185 ATTRIBUTE_TOK : '!';
1186 LPAREN_TOK : '(';
1187 RPAREN_TOK : ')';
1188 INDEX_TOK : '_';
1189 SET_LOGIC_TOK : 'set-logic';
1190 SET_INFO_TOK : 'set-info';
1191 GET_INFO_TOK : 'get-info';
1192 SET_OPTION_TOK : 'set-option';
1193 GET_OPTION_TOK : 'get-option';
1194 PUSH_TOK : 'push';
1195 POP_TOK : 'pop';
1196
1197 // extended commands
1198 DECLARE_DATATYPES_TOK : 'declare-datatypes';
1199 GET_MODEL_TOK : 'get-model';
1200 ECHO_TOK : 'echo';
1201 REWRITE_RULE_TOK : 'assert-rewrite';
1202 REDUCTION_RULE_TOK : 'assert-reduction';
1203 PROPAGATION_RULE_TOK : 'assert-propagation';
1204
1205 // attributes
1206 ATTRIBUTE_PATTERN_TOK : ':pattern';
1207 ATTRIBUTE_NAMED_TOK : ':named';
1208
1209 // operators (NOTE: theory symbols go here)
1210 AMPERSAND_TOK     : '&';
1211 AND_TOK           : 'and';
1212 AT_TOK            : '@';
1213 DISTINCT_TOK      : 'distinct';
1214 DIV_TOK           : '/';
1215 EQUAL_TOK         : '=';
1216 EXISTS_TOK        : 'exists';
1217 FORALL_TOK        : 'forall';
1218 GREATER_THAN_TOK  : '>';
1219 GREATER_THAN_EQUAL_TOK  : '>=';
1220 IMPLIES_TOK       : '=>';
1221 LESS_THAN_TOK     : '<';
1222 LESS_THAN_EQUAL_TOK     : '<=';
1223 MINUS_TOK         : '-';
1224 NOT_TOK           : 'not';
1225 OR_TOK            : 'or';
1226 // PERCENT_TOK       : '%';
1227 PLUS_TOK          : '+';
1228 POUND_TOK         : '#';
1229 SELECT_TOK        : 'select';
1230 STAR_TOK          : '*';
1231 STORE_TOK         : 'store';
1232 // TILDE_TOK         : '~';
1233 XOR_TOK           : 'xor';
1234
1235 INTS_DIV_TOK : 'div';
1236 INTS_MOD_TOK : 'mod';
1237
1238 CONCAT_TOK : 'concat';
1239 BVNOT_TOK : 'bvnot';
1240 BVAND_TOK : 'bvand';
1241 BVOR_TOK : 'bvor';
1242 BVNEG_TOK : 'bvneg';
1243 BVADD_TOK : 'bvadd';
1244 BVMUL_TOK : 'bvmul';
1245 BVUDIV_TOK : 'bvudiv';
1246 BVUREM_TOK : 'bvurem';
1247 BVSHL_TOK : 'bvshl';
1248 BVLSHR_TOK : 'bvlshr';
1249 BVULT_TOK : 'bvult';
1250 BVNAND_TOK : 'bvnand';
1251 BVNOR_TOK : 'bvnor';
1252 BVXOR_TOK : 'bvxor';
1253 BVXNOR_TOK : 'bvxnor';
1254 BVCOMP_TOK : 'bvcomp';
1255 BVSUB_TOK : 'bvsub';
1256 BVSDIV_TOK : 'bvsdiv';
1257 BVSREM_TOK : 'bvsrem';
1258 BVSMOD_TOK : 'bvsmod';
1259 BVASHR_TOK : 'bvashr';
1260 BVULE_TOK : 'bvule';
1261 BVUGT_TOK : 'bvugt';
1262 BVUGE_TOK : 'bvuge';
1263 BVSLT_TOK : 'bvslt';
1264 BVSLE_TOK : 'bvsle';
1265 BVSGT_TOK : 'bvsgt';
1266 BVSGE_TOK : 'bvsge';
1267
1268 /**
1269  * A sequence of printable ASCII characters (except backslash) that starts
1270  * and ends with | and does not otherwise contain |.
1271  *
1272  * You shouldn't generally use this in parser rules, as the |quoting|
1273  * will be part of the token text.  Use the symbol[] parser rule instead.
1274  */
1275 QUOTED_SYMBOL
1276   : '|' ~('|' | '\\')* '|'
1277   ;
1278
1279 /**
1280  * Matches a keyword from the input. A keyword is a simple symbol prefixed
1281  * with a colon.
1282  */
1283 KEYWORD
1284   : ':' (ALPHA | DIGIT | SYMBOL_CHAR)+
1285   ;
1286
1287 /**
1288  * Matches a "simple" symbol: a non-empty sequence of letters, digits and
1289  * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
1290  * digit, and is not the special reserved symbols '!' or '_'.
1291  */
1292 SIMPLE_SYMBOL
1293   : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)+
1294   | ALPHA
1295   | SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
1296   ;
1297
1298 /**
1299  * Matches and skips whitespace in the input.
1300  */
1301 WHITESPACE
1302   : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }
1303   ;
1304
1305 /**
1306  * Matches an integer constant from the input (non-empty sequence of
1307  * digits, with no leading zeroes).
1308  */
1309 INTEGER_LITERAL
1310   : NUMERAL
1311   ;
1312
1313 /**
1314  * Match an integer constant. In non-strict mode, this is any sequence
1315  * of digits. In strict mode, non-zero integers can't have leading
1316  * zeroes.
1317  */
1318 fragment NUMERAL
1319 @init {
1320   char *start = (char*) GETCHARINDEX();
1321 }
1322   : DIGIT+
1323     { Debug("parser-extra") << "NUMERAL: "
1324        << (uintptr_t)start << ".." << GETCHARINDEX()
1325        << " strict? " << (bool)(PARSER_STATE->strictModeEnabled())
1326        << " ^0? " << (bool)(*start == '0')
1327        << " len>1? " << (bool)(start < (char*)(GETCHARINDEX() - 1))
1328        << std::endl; }
1329     { !PARSER_STATE->strictModeEnabled() ||
1330       *start != '0' ||
1331       start == (char*)(GETCHARINDEX() - 1) }?
1332   ;
1333
1334 /**
1335  * Matches a decimal constant from the input.
1336  */
1337 DECIMAL_LITERAL
1338   : NUMERAL '.' DIGIT+
1339   ;
1340
1341 /**
1342  * Matches a hexadecimal constant.
1343  */
1344 HEX_LITERAL
1345   : '#x' HEX_DIGIT+
1346   ;
1347
1348 /**
1349  * Matches a binary constant.
1350  */
1351 BINARY_LITERAL
1352   : '#b' ('0' | '1')+
1353   ;
1354
1355
1356 /**
1357  * Matches a double quoted string literal.  Escaping is supported, and
1358  * escape character '\' has to be escaped.
1359  *
1360  * You shouldn't generally use this in parser rules, as the quotes
1361  * will be part of the token text.  Use the str[] parser rule instead.
1362  */
1363 STRING_LITERAL
1364   : '"' (ESCAPE | ~('"'|'\\'))* '"'
1365   ;
1366
1367 /**
1368  * Matches the comments and ignores them
1369  */
1370 COMMENT
1371   : ';' (~('\n' | '\r'))* { SKIP(); }
1372   ;
1373
1374 /**
1375  * Matches any letter ('a'-'z' and 'A'-'Z').
1376  */
1377 fragment
1378 ALPHA
1379   : 'a'..'z'
1380   | 'A'..'Z'
1381   ;
1382
1383 /**
1384  * Matches the digits (0-9)
1385  */
1386 fragment DIGIT : '0'..'9';
1387
1388 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
1389
1390 /**
1391  * Matches the characters that may appear as a one-character "symbol"
1392  * (which excludes _ and !, which are reserved words in SMT-LIBv2).
1393  */
1394 fragment SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
1395   : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '.' | '$' | '~'
1396   | '&' | '^' | '<' | '>' | '@'
1397   ;
1398
1399 /**
1400  * Matches the characters that may appear in a "symbol" (i.e., an identifier)
1401  */
1402 fragment SYMBOL_CHAR
1403   : SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE | '_' | '!'
1404   ;
1405
1406 /**
1407  * Matches an allowed escaped character.
1408  */
1409 fragment ESCAPE : '\\' ('"' | '\\');