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 /* This improves performance by ~10 percent on big inputs.
  55  * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
  56  * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
  57  * Otherwise, we have to let the lexer detect the encoding at runtime.
  58  */
  59 #define ANTLR3_INLINE_INPUT_ASCII
  60
  61 #include "parser/antlr_tracing.h"
  62
  63 }/* @lexer::includes */
  64
  65 @lexer::postinclude {
  66 #include <stdint.h>
  67
  68 #include "parser/smt2/smt2.h"
  69 #include "parser/antlr_input.h"
  70
  71 using namespace CVC4;
  72 using namespace CVC4::parser;
  73
  74 #undef PARSER_STATE
  75 #define PARSER_STATE ((Smt2*)LEXER->super)
  76 }/* @lexer::postinclude */
  77
  78 @parser::includes {
  79 #include "expr/command.h"
  80 #include "parser/parser.h"
  81 #include "parser/antlr_tracing.h"
  82
  83 namespace CVC4 {
  84   class Expr;
  85
  86   namespace parser {
  87     namespace smt2 {
  88       /**
  89        * Just exists to provide the uintptr_t constructor that ANTLR
  90        * requires.
  91        */
  92       struct myExpr : public CVC4::Expr {
  93         myExpr() : CVC4::Expr() {}
  94         myExpr(void*) : CVC4::Expr() {}
  95         myExpr(const Expr& e) : CVC4::Expr(e) {}
  96         myExpr(const myExpr& e) : CVC4::Expr(e) {}
  97       };/* struct myExpr */
  98     }/* CVC4::parser::smt2 namespace */
  99   }/* CVC4::parser namespace */
 100 }/* CVC4 namespace */
 101
 102 }/* @parser::includes */
 103
 104 @parser::postinclude {
 105
 106 #include "expr/expr.h"
 107 #include "expr/kind.h"
 108 #include "expr/type.h"
 109 #include "parser/antlr_input.h"
 110 #include "parser/parser.h"
 111 #include "parser/smt2/smt2.h"
 112 #include "util/integer.h"
 113 #include "util/output.h"
 114 #include "util/rational.h"
 115 #include <vector>
 116
 117 using namespace CVC4;
 118 using namespace CVC4::parser;
 119
 120 /* These need to be macros so they can refer to the PARSER macro, which will be defined
 121  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
 122 #undef PARSER_STATE
 123 #define PARSER_STATE ((Smt2*)PARSER->super)
 124 #undef EXPR_MANAGER
 125 #define EXPR_MANAGER PARSER_STATE->getExprManager()
 126 #undef MK_EXPR
 127 #define MK_EXPR EXPR_MANAGER->mkExpr
 128 #undef MK_CONST
 129 #define MK_CONST EXPR_MANAGER->mkConst
 130 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
 131
 132 }/* parser::postinclude */
 133
 134 /**
 135  * Parses an expression.
 136  * @return the parsed expression, or the Null Expr if we've reached the end of the input
 137  */
 138 parseExpr returns [CVC4::parser::smt2::myExpr expr]
 139   : term[expr]
 140   | EOF
 141   ;
 142
 143 /**
 144  * Parses a command
 145  * @return the parsed command, or NULL if we've reached the end of the input
 146  */
 147 parseCommand returns [CVC4::Command* cmd = NULL]
 148   : LPAREN_TOK c = command RPAREN_TOK { $cmd = c; }
 149   | EOF { $cmd = 0; }
 150   ;
 151
 152 /**
 153  * Parse the internal portion of the command, ignoring the surrounding parentheses.
 154  */
 155 command returns [CVC4::Command* cmd = NULL]
 156 @declarations {
 157   std::string name;
 158   std::vector<std::string> names;
 159   Expr expr;
 160   Type t;
 161   std::vector<Expr> terms;
 162   std::vector<Type> sorts;
 163   std::vector<std::pair<std::string, Type> > sortedVarNames;
 164   SExpr sexpr;
 165 }
 166   : /* set the logic */
 167     SET_LOGIC_TOK SYMBOL
 168     { name = AntlrInput::tokenText($SYMBOL);
 169       Debug("parser") << "set logic: '" << name << "'" << std::endl;
 170       if( PARSER_STATE->strictModeEnabled() && PARSER_STATE->logicIsSet() ) {
 171         PARSER_STATE->parseError("Only one set-logic is allowed.");
 172       }
 173       PARSER_STATE->setLogic(name);
 174       $cmd = new SetBenchmarkLogicCommand(name); }
 175   | SET_INFO_TOK KEYWORD symbolicExpr[sexpr]
 176     { name = AntlrInput::tokenText($KEYWORD);
 177       PARSER_STATE->setInfo(name,sexpr);
 178       cmd = new SetInfoCommand(name,sexpr); }
 179   | /* get-info */
 180     GET_INFO_TOK KEYWORD
 181     { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD)); }
 182   | /* set-option */
 183     SET_OPTION_TOK KEYWORD symbolicExpr[sexpr]
 184     { name = AntlrInput::tokenText($KEYWORD);
 185       PARSER_STATE->setOption(name,sexpr);
 186       cmd = new SetOptionCommand(name,sexpr); }
 187   | /* get-option */
 188     GET_OPTION_TOK KEYWORD
 189     { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD)); }
 190   | /* sort declaration */
 191     DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL
 192     { Debug("parser") << "declare sort: '" << name
 193                       << "' arity=" << n << std::endl;
 194       PARSER_STATE->checkThatLogicIsSet();
 195       unsigned arity = AntlrInput::tokenToUnsigned(n);
 196       if(arity == 0) {
 197         Type type = PARSER_STATE->mkSort(name);
 198         $cmd = new DeclareTypeCommand(name, 0, type);
 199       } else {
 200         Type type = PARSER_STATE->mkSortConstructor(name, arity);
 201         $cmd = new DeclareTypeCommand(name, arity, type);
 202       }
 203     }
 204   | /* sort definition */
 205     DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT]
 206     LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
 207     {
 208       PARSER_STATE->checkThatLogicIsSet();
 209       PARSER_STATE->pushScope();
 210       for(std::vector<std::string>::const_iterator i = names.begin(),
 211             iend = names.end();
 212           i != iend;
 213           ++i) {
 214         sorts.push_back(PARSER_STATE->mkSort(*i));
 215       }
 216     }
 217     sortSymbol[t,CHECK_DECLARED]
 218     { PARSER_STATE->popScope();
 219       // Do NOT call mkSort, since that creates a new sort!
 220       // This name is not its own distinct sort, it's an alias.
 221       PARSER_STATE->defineParameterizedType(name, sorts, t);
 222       $cmd = new DefineTypeCommand(name, sorts, t);
 223     }
 224   | /* function declaration */
 225     DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 226     LPAREN_TOK sortList[sorts] RPAREN_TOK
 227     sortSymbol[t,CHECK_DECLARED]
 228     { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
 229       PARSER_STATE->checkThatLogicIsSet();
 230       if( sorts.size() > 0 ) {
 231         t = EXPR_MANAGER->mkFunctionType(sorts, t);
 232       }
 233       PARSER_STATE->mkVar(name, t);
 234       $cmd = new DeclareFunctionCommand(name, t); }
 235   | /* function definition */
 236     DEFINE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 237     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
 238     sortSymbol[t,CHECK_DECLARED]
 239     { /* add variables to parser state before parsing term */
 240       Debug("parser") << "define fun: '" << name << "'" << std::endl;
 241       PARSER_STATE->checkThatLogicIsSet();
 242       if( sortedVarNames.size() > 0 ) {
 243         std::vector<CVC4::Type> sorts;
 244         sorts.reserve(sortedVarNames.size());
 245         for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 246               sortedVarNames.begin(), iend = sortedVarNames.end();
 247             i != iend;
 248             ++i) {
 249           sorts.push_back((*i).second);
 250         }
 251         t = EXPR_MANAGER->mkFunctionType(sorts, t);
 252       }
 253       PARSER_STATE->pushScope();
 254       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 255             sortedVarNames.begin(), iend = sortedVarNames.end();
 256           i != iend;
 257           ++i) {
 258         terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
 259       }
 260     }
 261     term[expr]
 262     { PARSER_STATE->popScope();
 263       // declare the name down here (while parsing term, signature
 264       // must not be extended with the name itself; no recursion
 265       // permitted)
 266       Expr func = PARSER_STATE->mkFunction(name, t);
 267       $cmd = new DefineFunctionCommand(name, func, terms, expr);
 268     }
 269   | /* value query */
 270     GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK
 271     { PARSER_STATE->checkThatLogicIsSet();
 272       if(terms.size() == 1) {
 273         $cmd = new GetValueCommand(terms[0]);
 274       } else {
 275         CommandSequence* seq = new CommandSequence();
 276         for(std::vector<Expr>::const_iterator i = terms.begin(),
 277               iend = terms.end();
 278             i != iend;
 279             ++i) {
 280           seq->addCommand(new GetValueCommand(*i));
 281         }
 282         $cmd = seq;
 283       }
 284     }
 285   | /* get-assignment */
 286     GET_ASSIGNMENT_TOK
 287     { PARSER_STATE->checkThatLogicIsSet();
 288       cmd = new GetAssignmentCommand; }
 289   | /* assertion */
 290     ASSERT_TOK term[expr]
 291     { PARSER_STATE->checkThatLogicIsSet();
 292       cmd = new AssertCommand(expr); }
 293   | /* checksat */
 294     CHECKSAT_TOK
 295     { PARSER_STATE->checkThatLogicIsSet();
 296       cmd = new CheckSatCommand(MK_CONST(bool(true))); }
 297   | /* get-assertions */
 298     GET_ASSERTIONS_TOK
 299     { PARSER_STATE->checkThatLogicIsSet();
 300       cmd = new GetAssertionsCommand; }
 301   | /* get-proof */
 302     GET_PROOF_TOK
 303     { PARSER_STATE->checkThatLogicIsSet();
 304       cmd = new GetProofCommand; }
 305   | /* get-unsat-core */
 306     GET_UNSAT_CORE_TOK
 307     { PARSER_STATE->checkThatLogicIsSet();
 308       UNSUPPORTED("unsat cores not yet supported"); }
 309   | /* push */
 310     PUSH_TOK
 311     { PARSER_STATE->checkThatLogicIsSet(); }
 312     ( k=INTEGER_LITERAL
 313       { unsigned n = AntlrInput::tokenToUnsigned(k);
 314         if(n == 0) {
 315           cmd = new EmptyCommand;
 316         } else if(n == 1) {
 317           cmd = new PushCommand;
 318         } else {
 319           CommandSequence* seq = new CommandSequence;
 320           do {
 321             seq->addCommand(new PushCommand);
 322           } while(--n > 0);
 323           cmd = seq;
 324         }
 325       }
 326     | { if(PARSER_STATE->strictModeEnabled()) {
 327           PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to PUSH.  Maybe you want (push 1)?");
 328         } else {
 329           cmd = new PushCommand;
 330         }
 331       } )
 332   | POP_TOK
 333     { PARSER_STATE->checkThatLogicIsSet(); }
 334     ( k=INTEGER_LITERAL
 335       { unsigned n = AntlrInput::tokenToUnsigned(k);
 336         if(n == 0) {
 337           cmd = new EmptyCommand;
 338         } else if(n == 1) {
 339           cmd = new PopCommand;
 340         } else {
 341           CommandSequence* seq = new CommandSequence;
 342           do {
 343             seq->addCommand(new PopCommand);
 344           } while(--n > 0);
 345           cmd = seq;
 346         }
 347       }
 348     | { if(PARSER_STATE->strictModeEnabled()) {
 349           PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to POP.  Maybe you want (pop 1)?");
 350         } else {
 351           cmd = new PopCommand;
 352         }
 353       } )
 354   | EXIT_TOK
 355     { cmd = new QuitCommand; }
 356
 357     /* CVC4-extended SMT-LIBv2 commands */
 358   | extendedCommand[cmd]
 359     { PARSER_STATE->checkThatLogicIsSet();
 360       if(PARSER_STATE->strictModeEnabled()) {
 361         PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode.");
 362       }
 363     }
 364   ;
 365
 366 extendedCommand[CVC4::Command*& cmd]
 367 @declarations {
 368   std::vector<CVC4::Datatype> dts;
 369   Type t;
 370   Expr e;
 371   SExpr sexpr;
 372   std::string name;
 373   std::vector<std::string> names;
 374   std::vector<Type> sorts;
 375 }
 376     /* Extended SMT-LIBv2 set of commands syntax, not permitted in
 377      * --smtlib2 compliance mode. */
 378   : DECLARE_DATATYPES_TOK
 379     { /* open a scope to keep the UnresolvedTypes contained */
 380       PARSER_STATE->pushScope(); }
 381     LPAREN_TOK ( LPAREN_TOK datatypeDef[dts] RPAREN_TOK )+ RPAREN_TOK
 382     { PARSER_STATE->popScope();
 383       cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
 384   | ECHO_TOK
 385     ( simpleSymbolicExpr[sexpr]
 386       { std::stringstream ss;
 387         ss << sexpr;
 388         cmd = new EchoCommand(ss.str());
 389       }
 390     | { cmd = new EchoCommand(); }
 391     )
 392   ;
 393
 394 simpleSymbolicExpr[CVC4::SExpr& sexpr]
 395 @declarations {
 396   CVC4::Kind k;
 397   std::string s;
 398 }
 399   : INTEGER_LITERAL
 400     { sexpr = SExpr(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
 401   | DECIMAL_LITERAL
 402     { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
 403   | str[s]
 404     { sexpr = SExpr(s); }
 405   | SYMBOL
 406     { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); }
 407   | builtinOp[k]
 408     { std::stringstream ss;
 409       ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k);
 410       sexpr = SExpr(ss.str());
 411     }
 412   | KEYWORD
 413     { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
 414   ;
 415
 416 symbolicExpr[CVC4::SExpr& sexpr]
 417 @declarations {
 418   std::vector<SExpr> children;
 419 }
 420   : simpleSymbolicExpr[sexpr]
 421   | LPAREN_TOK
 422     (symbolicExpr[sexpr] { children.push_back(sexpr); } )*
 423         RPAREN_TOK
 424     { sexpr = SExpr(children); }
 425   ;
 426
 427 /**
 428  * Matches a term.
 429  * @return the expression representing the formula
 430  */
 431 term[CVC4::Expr& expr]
 432 @init {
 433   Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
 434   Kind kind;
 435   Expr op;
 436   std::string name;
 437   std::vector<Expr> args;
 438   SExpr sexpr;
 439 }
 440   : /* a built-in operator application */
 441     LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
 442     {
 443       if( kind == CVC4::kind::EQUAL &&
 444           args.size() > 0 &&
 445           args[0].getType() == EXPR_MANAGER->booleanType() ) {
 446         /* Use IFF for boolean equalities. */
 447         kind = CVC4::kind::IFF;
 448       }
 449
 450       if( !PARSER_STATE->strictModeEnabled() &&
 451           (kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
 452           args.size() == 1) {
 453         /* Unary AND/OR can be replaced with the argument.
 454                It just so happens expr should already by the only argument. */
 455         Assert( expr == args[0] );
 456       } else if( CVC4::kind::isAssociative(kind) &&
 457                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
 458         /* Special treatment for associative operators with lots of children */
 459         expr = EXPR_MANAGER->mkAssociative(kind,args);
 460       } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) {
 461         expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
 462       } else {
 463         PARSER_STATE->checkOperator(kind, args.size());
 464         expr = MK_EXPR(kind, args);
 465       }
 466     }
 467
 468   | /* A non-built-in function application */
 469     LPAREN_TOK
 470     functionName[name,CHECK_DECLARED]
 471     { PARSER_STATE->checkFunctionLike(name);
 472       const bool isDefinedFunction =
 473         PARSER_STATE->isDefinedFunction(name);
 474       if(isDefinedFunction) {
 475         expr = PARSER_STATE->getFunction(name);
 476         kind = CVC4::kind::APPLY;
 477       } else {
 478         expr = PARSER_STATE->getVariable(name);
 479         Type t = expr.getType();
 480         if( t.isConstructor() ){
 481           kind = CVC4::kind::APPLY_CONSTRUCTOR;
 482         }else if( t.isSelector() ){
 483           kind = CVC4::kind::APPLY_SELECTOR;
 484         }else if( t.isTester() ){
 485           kind = CVC4::kind::APPLY_TESTER;
 486         }else{
 487           kind = CVC4::kind::APPLY_UF;
 488         }
 489       }
 490       args.push_back(expr);
 491     }
 492     termList[args,expr] RPAREN_TOK
 493     { Debug("parser") << "args has size " << args.size() << std::endl << "expr is " << expr << std::endl;
 494       for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
 495         Debug("parser") << "++ " << *i << std::endl;
 496       expr = MK_EXPR(kind, args); }
 497
 498   | /* An indexed function application */
 499     LPAREN_TOK indexedFunctionName[op] termList[args,expr] RPAREN_TOK
 500     { expr = MK_EXPR(op, args); }
 501
 502   | /* a let binding */
 503     LPAREN_TOK LET_TOK LPAREN_TOK
 504     { PARSER_STATE->pushScope(); }
 505     ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[expr] RPAREN_TOK
 506       { PARSER_STATE->defineVar(name,expr); } )+
 507     RPAREN_TOK
 508     term[expr]
 509     RPAREN_TOK
 510     { PARSER_STATE->popScope(); }
 511
 512     /* a variable */
 513   | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
 514     { const bool isDefinedFunction =
 515         PARSER_STATE->isDefinedFunction(name);
 516       if(isDefinedFunction) {
 517         expr = MK_EXPR(CVC4::kind::APPLY,
 518                        PARSER_STATE->getFunction(name));
 519       } else {
 520         expr = PARSER_STATE->getVariable(name);
 521         Type t = PARSER_STATE->getType(name);
 522         if(t.isConstructor() && ConstructorType(t).getArity() == 0) {
 523           // don't require parentheses, immediately turn it into an apply
 524           expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
 525         }
 526       }
 527     }
 528
 529     /* attributed expressions */
 530   | LPAREN_TOK ATTRIBUTE_TOK term[expr] KEYWORD symbolicExpr[sexpr] RPAREN_TOK
 531     { std::string attr = AntlrInput::tokenText($KEYWORD);
 532       if(attr == ":named") {
 533         name = sexpr.getValue();
 534         // FIXME ensure expr is a closed subterm
 535         // check that sexpr is a fresh function symbol
 536         PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
 537         // define it
 538         Expr func = PARSER_STATE->mkFunction(name, expr.getType());
 539         // bind name to expr with define-fun
 540         Command* c =
 541           new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
 542         PARSER_STATE->preemptCommand(c);
 543       } else {
 544         std::stringstream ss;
 545         ss << "Attribute `" << attr << "' not supported";
 546         PARSER_STATE->parseError(ss.str());
 547       }
 548     }
 549
 550     /* constants */
 551   | INTEGER_LITERAL
 552     { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
 553
 554   | DECIMAL_LITERAL
 555     { // FIXME: This doesn't work because an SMT rational is not a
 556       // valid GMP rational string
 557       expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
 558
 559   | LPAREN_TOK INDEX_TOK bvLit=SYMBOL size=INTEGER_LITERAL RPAREN_TOK
 560     { if(AntlrInput::tokenText($bvLit).find("bv") == 0) {
 561         expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) );
 562       } else {
 563         PARSER_STATE->parseError("Unexpected symbol `" + AntlrInput::tokenText($bvLit) + "'");
 564       }
 565     }
 566
 567   | HEX_LITERAL
 568     { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
 569       std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
 570       expr = MK_CONST( BitVector(hexString, 16) ); }
 571
 572   | BINARY_LITERAL
 573     { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
 574       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
 575       expr = MK_CONST( BitVector(binString, 2) ); }
 576
 577     // NOTE: Theory constants go here
 578   ;
 579
 580 /**
 581  * Matches a bit-vector operator (the ones parametrized by numbers)
 582  */
 583 indexedFunctionName[CVC4::Expr& op]
 584   : LPAREN_TOK INDEX_TOK
 585     ( 'extract' n1=INTEGER_LITERAL n2=INTEGER_LITERAL
 586       { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1),
 587                                        AntlrInput::tokenToUnsigned($n2))); }
 588     | 'repeat' n=INTEGER_LITERAL
 589       { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
 590     | 'zero_extend' n=INTEGER_LITERAL
 591       { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
 592     | 'sign_extend' n=INTEGER_LITERAL
 593       { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); }
 594     | 'rotate_left' n=INTEGER_LITERAL
 595       { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
 596     | 'rotate_right' n=INTEGER_LITERAL
 597       { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
 598     | badIndexedFunctionName
 599    )
 600     RPAREN_TOK
 601   ;
 602
 603 /**
 604  * Matches an erroneous indexed function name (and args) for better
 605  * error reporting.
 606  */
 607 badIndexedFunctionName
 608 @declarations {
 609   std::string name;
 610 }
 611   : symbol[name,CHECK_NONE,SYM_VARIABLE] INTEGER_LITERAL+
 612       { PARSER_STATE->parseError(std::string("Unknown indexed function `") + name + "'"); }
 613   ;
 614
 615 /**
 616  * Matches a sequence of terms and puts them into the formulas
 617  * vector.
 618  * @param formulas the vector to fill with terms
 619  * @param expr an Expr reference for the elements of the sequence
 620  */
 621 /* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
 622  * time through this rule. */
 623 termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
 624   : ( term[expr] { formulas.push_back(expr); } )+
 625   ;
 626
 627 /**
 628  * Matches a string, and strips off the quotes.
 629  */
 630 str[std::string& s]
 631   : STRING_LITERAL
 632     { s = AntlrInput::tokenText($STRING_LITERAL);
 633       /* strip off the quotes */
 634       s = s.substr(1, s.size() - 2);
 635     }
 636   ;
 637
 638 /**
 639 * Matches a builtin operator symbol and sets kind to its associated Expr kind.
 640 */
 641 builtinOp[CVC4::Kind& kind]
 642 @init {
 643   Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
 644 }
 645   : NOT_TOK      { $kind = CVC4::kind::NOT;     }
 646   | IMPLIES_TOK  { $kind = CVC4::kind::IMPLIES; }
 647   | AND_TOK      { $kind = CVC4::kind::AND;     }
 648   | OR_TOK       { $kind = CVC4::kind::OR;      }
 649   | XOR_TOK      { $kind = CVC4::kind::XOR;     }
 650   | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
 651   | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
 652   | ITE_TOK      { $kind = CVC4::kind::ITE; }
 653   | GREATER_THAN_TOK
 654                  { $kind = CVC4::kind::GT; }
 655   | GREATER_THAN_EQUAL_TOK
 656                  { $kind = CVC4::kind::GEQ; }
 657   | LESS_THAN_EQUAL_TOK
 658                  { $kind = CVC4::kind::LEQ; }
 659   | LESS_THAN_TOK
 660                  { $kind = CVC4::kind::LT; }
 661   | PLUS_TOK     { $kind = CVC4::kind::PLUS; }
 662   | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
 663   | STAR_TOK     { $kind = CVC4::kind::MULT; }
 664   | DIV_TOK      { $kind = CVC4::kind::DIVISION; }
 665   | INTS_DIV_TOK      { $kind = CVC4::kind::INTS_DIVISION; }
 666   | INTS_MOD_TOK      { $kind = CVC4::kind::INTS_MODULUS; }
 667
 668   | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
 669   | STORE_TOK    { $kind = CVC4::kind::STORE; }
 670
 671   | CONCAT_TOK   { $kind = CVC4::kind::BITVECTOR_CONCAT; }
 672   | BVNOT_TOK   { $kind = CVC4::kind::BITVECTOR_NOT; }
 673   | BVAND_TOK   { $kind = CVC4::kind::BITVECTOR_AND; }
 674   | BVOR_TOK   { $kind = CVC4::kind::BITVECTOR_OR; }
 675   | BVNEG_TOK   { $kind = CVC4::kind::BITVECTOR_NEG; }
 676   | BVADD_TOK   { $kind = CVC4::kind::BITVECTOR_PLUS; }
 677   | BVMUL_TOK   { $kind = CVC4::kind::BITVECTOR_MULT; }
 678   | BVUDIV_TOK   { $kind = CVC4::kind::BITVECTOR_UDIV; }
 679   | BVUREM_TOK   { $kind = CVC4::kind::BITVECTOR_UREM; }
 680   | BVSHL_TOK     { $kind = CVC4::kind::BITVECTOR_SHL; }
 681   | BVLSHR_TOK     { $kind = CVC4::kind::BITVECTOR_LSHR; }
 682   | BVULT_TOK     { $kind = CVC4::kind::BITVECTOR_ULT; }
 683   | BVNAND_TOK     { $kind = CVC4::kind::BITVECTOR_NAND; }
 684   | BVNOR_TOK     { $kind = CVC4::kind::BITVECTOR_NOR; }
 685   | BVXOR_TOK     { $kind = CVC4::kind::BITVECTOR_XOR; }
 686   | BVXNOR_TOK     { $kind = CVC4::kind::BITVECTOR_XNOR; }
 687   | BVCOMP_TOK     { $kind = CVC4::kind::BITVECTOR_COMP; }
 688   | BVSUB_TOK     { $kind = CVC4::kind::BITVECTOR_SUB; }
 689   | BVSDIV_TOK     { $kind = CVC4::kind::BITVECTOR_SDIV; }
 690   | BVSREM_TOK     { $kind = CVC4::kind::BITVECTOR_SREM; }
 691   | BVSMOD_TOK     { $kind = CVC4::kind::BITVECTOR_SMOD; }
 692   | BVASHR_TOK     { $kind = CVC4::kind::BITVECTOR_ASHR; }
 693   | BVULE_TOK     { $kind = CVC4::kind::BITVECTOR_ULE; }
 694   | BVUGT_TOK     { $kind = CVC4::kind::BITVECTOR_UGT; }
 695   | BVUGE_TOK     { $kind = CVC4::kind::BITVECTOR_UGE; }
 696   | BVSLT_TOK     { $kind = CVC4::kind::BITVECTOR_SLT; }
 697   | BVSLE_TOK     { $kind = CVC4::kind::BITVECTOR_SLE; }
 698   | BVSGT_TOK     { $kind = CVC4::kind::BITVECTOR_SGT; }
 699   | BVSGE_TOK     { $kind = CVC4::kind::BITVECTOR_SGE; }
 700
 701   // NOTE: Theory operators go here
 702   ;
 703
 704 /**
 705  * Matches a (possibly undeclared) function symbol (returning the string)
 706  * @param check what kind of check to do with the symbol
 707  */
 708 functionName[std::string& name, CVC4::parser::DeclarationCheck check]
 709   : symbol[name,check,SYM_VARIABLE]
 710   ;
 711
 712 /**
 713  * Matches an previously declared function symbol (returning an Expr)
 714  */
 715 functionSymbol[CVC4::Expr& fun]
 716 @declarations {
 717         std::string name;
 718 }
 719   : functionName[name,CHECK_DECLARED]
 720     { PARSER_STATE->checkFunctionLike(name);
 721       fun = PARSER_STATE->getVariable(name); }
 722   ;
 723
 724 /**
 725  * Matches a sequence of sort symbols and fills them into the given
 726  * vector.
 727  */
 728 sortList[std::vector<CVC4::Type>& sorts]
 729 @declarations {
 730   Type t;
 731 }
 732   : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
 733   ;
 734
 735 nonemptySortList[std::vector<CVC4::Type>& sorts]
 736 @declarations {
 737   Type t;
 738 }
 739   : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+
 740   ;
 741
 742 /**
 743  * Matches a sequence of (variable,sort) symbol pairs and fills them
 744  * into the given vector.
 745  */
 746 sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars]
 747 @declarations {
 748   std::string name;
 749   Type t;
 750 }
 751   : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] RPAREN_TOK
 752       { sortedVars.push_back(make_pair(name, t)); }
 753     )*
 754   ;
 755
 756 /**
 757  * Matches the sort symbol, which can be an arbitrary symbol.
 758  * @param check the check to perform on the name
 759  */
 760 sortName[std::string& name, CVC4::parser::DeclarationCheck check]
 761   : symbol[name,check,SYM_SORT]
 762   ;
 763
 764 sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
 765 @declarations {
 766   std::string name;
 767   std::vector<CVC4::Type> args;
 768   std::vector<uint64_t> numerals;
 769 }
 770   : sortName[name,CHECK_NONE]
 771         {
 772           if( check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT) ){
 773             t = PARSER_STATE->getSort(name);
 774           }else{
 775             t = PARSER_STATE->mkUnresolvedType(name);
 776           }
 777         }
 778   | LPAREN_TOK INDEX_TOK symbol[name,CHECK_NONE,SYM_SORT] nonemptyNumeralList[numerals] RPAREN_TOK
 779     {
 780       if( name == "BitVec" ) {
 781         if( numerals.size() != 1 ) {
 782           PARSER_STATE->parseError("Illegal bitvector type.");
 783         }
 784         t = EXPR_MANAGER->mkBitVectorType(numerals.front());
 785       } else {
 786         Unhandled(name);
 787       }
 788     }
 789   | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
 790     {
 791       if( name == "Array" ) {
 792         if( args.size() != 2 ) {
 793           PARSER_STATE->parseError("Illegal array type.");
 794         }
 795         t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
 796       } else {
 797         t = PARSER_STATE->getSort(name, args);
 798       }
 799     }
 800   ;
 801
 802 /**
 803  * Matches a list of symbols, with check and type arguments as for the
 804  * symbol[] rule below.
 805  */
 806 symbolList[std::vector<std::string>& names,
 807            CVC4::parser::DeclarationCheck check,
 808            CVC4::parser::SymbolType type]
 809 @declarations {
 810   std::string id;
 811 }
 812   : ( symbol[id,check,type] { names.push_back(id); } )*
 813   ;
 814
 815 /**
 816  * Matches an symbol and sets the string reference parameter id.
 817  * @param id string to hold the symbol
 818  * @param check what kinds of check to do on the symbol
 819  * @param type the intended namespace for the symbol
 820  */
 821 symbol[std::string& id,
 822        CVC4::parser::DeclarationCheck check,
 823        CVC4::parser::SymbolType type]
 824   : SYMBOL
 825     { id = AntlrInput::tokenText($SYMBOL);
 826       Debug("parser") << "symbol: " << id
 827                       << " check? " << check
 828                       << " type? " << type << std::endl;
 829       PARSER_STATE->checkDeclaration(id, check, type); }
 830   ;
 831
 832 /**
 833  * Matches a nonempty list of numerals.
 834  * @param numerals the (empty) vector to house the numerals.
 835  */
 836 nonemptyNumeralList[std::vector<uint64_t>& numerals]
 837   : ( INTEGER_LITERAL
 838       { numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
 839     )+
 840   ;
 841
 842 /**
 843  * Parses a datatype definition
 844  */
 845 datatypeDef[std::vector<CVC4::Datatype>& datatypes]
 846 @init {
 847   std::string id, id2;
 848   Type t;
 849   std::vector< Type > params;
 850 }
 851     /* This really needs to be CHECK_NONE, or mutually-recursive
 852      * datatypes won't work, because this type will already be
 853      * "defined" as an unresolved type; don't worry, we check
 854      * below. */
 855   : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
 856     ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
 857         t = PARSER_STATE->mkSort(id2);
 858         params.push_back( t );
 859       }
 860       ( symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
 861         t = PARSER_STATE->mkSort(id2);
 862         params.push_back( t ); }
 863       )* ']'
 864     )?
 865     { datatypes.push_back(Datatype(id,params));
 866       if(!PARSER_STATE->isUnresolvedType(id)) {
 867         // if not unresolved, must be undeclared
 868         PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
 869       }
 870     }
 871     ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+
 872     { PARSER_STATE->popScope(); }
 873   ;
 874
 875 /**
 876  * Parses a constructor defintion for type
 877  */
 878 constructorDef[CVC4::Datatype& type]
 879 @init {
 880   std::string id;
 881   CVC4::DatatypeConstructor* ctor = NULL;
 882 }
 883   : symbol[id,CHECK_UNDECLARED,SYM_SORT]
 884     { // make the tester
 885       std::string testerId("is_");
 886       testerId.append(id);
 887       PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
 888       ctor = new CVC4::DatatypeConstructor(id, testerId);
 889     }
 890     ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
 891     { // make the constructor
 892       type.addConstructor(*ctor);
 893       Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
 894       delete ctor;
 895     }
 896   ;
 897
 898 selector[CVC4::DatatypeConstructor& ctor]
 899 @init {
 900   std::string id;
 901   Type t, t2;
 902 }
 903   : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t,CHECK_NONE]
 904     { ctor.addArg(id, t);
 905       Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
 906     }
 907   ;
 908
 909 // Base SMT-LIB tokens
 910 ASSERT_TOK : 'assert';
 911 CHECKSAT_TOK : 'check-sat';
 912 DECLARE_FUN_TOK : 'declare-fun';
 913 DECLARE_SORT_TOK : 'declare-sort';
 914 DEFINE_FUN_TOK : 'define-fun';
 915 DEFINE_SORT_TOK : 'define-sort';
 916 GET_VALUE_TOK : 'get-value';
 917 GET_ASSIGNMENT_TOK : 'get-assignment';
 918 GET_ASSERTIONS_TOK : 'get-assertions';
 919 GET_PROOF_TOK : 'get-proof';
 920 GET_UNSAT_CORE_TOK : 'get-unsat-core';
 921 EXIT_TOK : 'exit';
 922 ITE_TOK : 'ite';
 923 LET_TOK : 'let';
 924 ATTRIBUTE_TOK : '!';
 925 LPAREN_TOK : '(';
 926 RPAREN_TOK : ')';
 927 INDEX_TOK : '_';
 928 SET_LOGIC_TOK : 'set-logic';
 929 SET_INFO_TOK : 'set-info';
 930 GET_INFO_TOK : 'get-info';
 931 SET_OPTION_TOK : 'set-option';
 932 GET_OPTION_TOK : 'get-option';
 933 PUSH_TOK : 'push';
 934 POP_TOK : 'pop';
 935
 936 // extended commands
 937 DECLARE_DATATYPES_TOK : 'declare-datatypes';
 938 ECHO_TOK : 'echo';
 939
 940 // operators (NOTE: theory symbols go here)
 941 AMPERSAND_TOK     : '&';
 942 AND_TOK           : 'and';
 943 AT_TOK            : '@';
 944 DISTINCT_TOK      : 'distinct';
 945 DIV_TOK           : '/';
 946 EQUAL_TOK         : '=';
 947 EXISTS_TOK        : 'exists';
 948 FORALL_TOK        : 'forall';
 949 GREATER_THAN_TOK  : '>';
 950 GREATER_THAN_EQUAL_TOK  : '>=';
 951 IMPLIES_TOK       : '=>';
 952 LESS_THAN_TOK     : '<';
 953 LESS_THAN_EQUAL_TOK     : '<=';
 954 MINUS_TOK         : '-';
 955 NOT_TOK           : 'not';
 956 OR_TOK            : 'or';
 957 // PERCENT_TOK       : '%';
 958 PLUS_TOK          : '+';
 959 POUND_TOK         : '#';
 960 SELECT_TOK        : 'select';
 961 STAR_TOK          : '*';
 962 STORE_TOK         : 'store';
 963 // TILDE_TOK         : '~';
 964 XOR_TOK           : 'xor';
 965
 966 INTS_DIV_TOK : 'div';
 967 INTS_MOD_TOK : 'mod';
 968
 969 CONCAT_TOK : 'concat';
 970 BVNOT_TOK : 'bvnot';
 971 BVAND_TOK : 'bvand';
 972 BVOR_TOK : 'bvor';
 973 BVNEG_TOK : 'bvneg';
 974 BVADD_TOK : 'bvadd';
 975 BVMUL_TOK : 'bvmul';
 976 BVUDIV_TOK : 'bvudiv';
 977 BVUREM_TOK : 'bvurem';
 978 BVSHL_TOK : 'bvshl';
 979 BVLSHR_TOK : 'bvlshr';
 980 BVULT_TOK : 'bvult';
 981 BVNAND_TOK : 'bvnand';
 982 BVNOR_TOK : 'bvnor';
 983 BVXOR_TOK : 'bvxor';
 984 BVXNOR_TOK : 'bvxnor';
 985 BVCOMP_TOK : 'bvcomp';
 986 BVSUB_TOK : 'bvsub';
 987 BVSDIV_TOK : 'bvsdiv';
 988 BVSREM_TOK : 'bvsrem';
 989 BVSMOD_TOK : 'bvsmod';
 990 BVASHR_TOK : 'bvashr';
 991 BVULE_TOK : 'bvule';
 992 BVUGT_TOK : 'bvugt';
 993 BVUGE_TOK : 'bvuge';
 994 BVSLT_TOK : 'bvslt';
 995 BVSLE_TOK : 'bvsle';
 996 BVSGT_TOK : 'bvsgt';
 997 BVSGE_TOK : 'bvsge';
 998
 999 /**
1000  * Matches a symbol from the input. A symbol is a "simple" symbol or a
1001  * sequence of printable ASCII characters that starts and ends with | and
1002  * does not otherwise contain |.
1003  */
1004 SYMBOL
1005   : SIMPLE_SYMBOL
1006   | '|' ~('|')+ '|'
1007   ;
1008
1009 /**
1010  * Matches a keyword from the input. A keyword is a simple symbol prefixed
1011  * with a colon.
1012  */
1013 KEYWORD
1014   : ':' SIMPLE_SYMBOL
1015   ;
1016
1017 /** Matches a "simple" symbol: a non-empty sequence of letters, digits and
1018  * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
1019  * digit, and is not the special reserved symbol '_'.
1020  */
1021 fragment SIMPLE_SYMBOL
1022   : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)+
1023   | ALPHA
1024   | SYMBOL_CHAR_NOUNDERSCORE
1025   ;
1026
1027 /**
1028  * Matches and skips whitespace in the input.
1029  */
1030 WHITESPACE
1031   : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }
1032   ;
1033
1034 /**
1035  * Matches an integer constant from the input (non-empty sequence of
1036  * digits, with no leading zeroes).
1037  */
1038 INTEGER_LITERAL
1039   : NUMERAL
1040   ;
1041
1042 /**
1043  * Match an integer constant. In non-strict mode, this is any sequence
1044  * of digits. In strict mode, non-zero integers can't have leading
1045  * zeroes.
1046  */
1047 fragment NUMERAL
1048 @init {
1049   char *start = (char*) GETCHARINDEX();
1050 }
1051   : DIGIT+
1052     { Debug("parser-extra") << "NUMERAL: "
1053        << (uintptr_t)start << ".." << GETCHARINDEX()
1054        << " strict? " << (bool)(PARSER_STATE->strictModeEnabled())
1055        << " ^0? " << (bool)(*start == '0')
1056        << " len>1? " << (bool)(start < (char*)(GETCHARINDEX() - 1))
1057        << std::endl; }
1058     { !PARSER_STATE->strictModeEnabled() ||
1059       *start != '0' ||
1060       start == (char*)(GETCHARINDEX() - 1) }?
1061   ;
1062
1063 /**
1064  * Matches a decimal constant from the input.
1065  */
1066 DECIMAL_LITERAL
1067   : NUMERAL '.' DIGIT+
1068   ;
1069
1070 /**
1071  * Matches a hexadecimal constant.
1072  */
1073 HEX_LITERAL
1074   : '#x' HEX_DIGIT+
1075   ;
1076
1077 /**
1078  * Matches a binary constant.
1079  */
1080 BINARY_LITERAL
1081   : '#b' ('0' | '1')+
1082   ;
1083
1084
1085 /**
1086  * Matches a double quoted string literal. Escaping is supported, and
1087  * escape character '\' has to be escaped.
1088  */
1089 STRING_LITERAL
1090   : '"' (ESCAPE | ~('"'|'\\'))* '"'
1091   ;
1092
1093 /**
1094  * Matches the comments and ignores them
1095  */
1096 COMMENT
1097   : ';' (~('\n' | '\r'))* { SKIP(); }
1098   ;
1099
1100 /**
1101  * Matches any letter ('a'-'z' and 'A'-'Z').
1102  */
1103 fragment
1104 ALPHA
1105   : 'a'..'z'
1106   | 'A'..'Z'
1107   ;
1108
1109 /**
1110  * Matches the digits (0-9)
1111  */
1112 fragment DIGIT : '0'..'9';
1113
1114 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
1115
1116 /**
1117  * Matches the characters that may appear in a "symbol" (i.e., an identifier)
1118  */
1119 fragment SYMBOL_CHAR_NOUNDERSCORE
1120   : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '~'
1121   | '&' | '^' | '<' | '>' | '@'
1122   ;
1123
1124 fragment SYMBOL_CHAR
1125   : SYMBOL_CHAR_NOUNDERSCORE | '_'
1126   ;
1127
1128 /**
1129  * Matches an allowed escaped character.
1130  */
1131 fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');