src/parser/smt2/Smt2.g

   1 /* *******************                                                        */
   2 /*! \file Smt2.g
   3  ** \verbatim
   4  ** Original author: Christopher L. Conway
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): Dejan Jovanovic, Kshitij Bansal, Tianyi Liang, Francois Bobot, Andrew Reynolds
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Parser for SMT-LIB v2 input language
  13  **
  14  ** Parser for SMT-LIB v2 input language.
  15  **/
  16
  17 grammar Smt2;
  18
  19 options {
  20   // C output for antlr
  21   language = 'C';
  22
  23   // Skip the default error handling, just break with exceptions
  24   // defaultErrorHandler = false;
  25
  26   // Only lookahead of <= k requested (disable for LL* parsing)
  27   // Note that CVC4's BoundedTokenBuffer requires a fixed k !
  28   // If you change this k, change it also in smt2_input.cpp !
  29   k = 2;
  30 }/* options */
  31
  32 @header {
  33 /**
  34  ** This file is part of CVC4.
  35  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  36  ** See the file COPYING in the top-level source directory for licensing
  37  ** information.
  38  **/
  39 }/* @header */
  40
  41 @lexer::includes {
  42
  43 /** This suppresses warnings about the redefinition of token symbols between
  44   * different parsers. The redefinitions should be harmless as long as no
  45   * client: (a) #include's the lexer headers for two grammars AND (b) uses the
  46   * token symbol definitions.
  47   */
  48 #pragma GCC system_header
  49
  50 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
  51 /* This improves performance by ~10 percent on big inputs.
  52  * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
  53  * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
  54  * Otherwise, we have to let the lexer detect the encoding at runtime.
  55  */
  56 #  define ANTLR3_INLINE_INPUT_ASCII
  57 #  define ANTLR3_INLINE_INPUT_8BIT
  58 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
  59
  60 #include "parser/antlr_tracing.h"
  61
  62 }/* @lexer::includes */
  63
  64 @lexer::postinclude {
  65 #include <stdint.h>
  66
  67 #include "parser/smt2/smt2.h"
  68 #include "parser/antlr_input.h"
  69
  70 using namespace CVC4;
  71 using namespace CVC4::parser;
  72
  73 #undef PARSER_STATE
  74 #define PARSER_STATE ((Smt2*)LEXER->super)
  75 }/* @lexer::postinclude */
  76
  77 @parser::includes {
  78 #include "expr/command.h"
  79 #include "parser/parser.h"
  80 #include "parser/antlr_tracing.h"
  81
  82 namespace CVC4 {
  83   class Expr;
  84
  85   namespace parser {
  86     namespace smt2 {
  87       /**
  88        * Just exists to provide the uintptr_t constructor that ANTLR
  89        * requires.
  90        */
  91       struct myExpr : public CVC4::Expr {
  92         myExpr() : CVC4::Expr() {}
  93         myExpr(void*) : CVC4::Expr() {}
  94         myExpr(const Expr& e) : CVC4::Expr(e) {}
  95         myExpr(const myExpr& e) : CVC4::Expr(e) {}
  96       };/* struct myExpr */
  97     }/* CVC4::parser::smt2 namespace */
  98   }/* CVC4::parser namespace */
  99 }/* CVC4 namespace */
 100
 101 }/* @parser::includes */
 102
 103 @parser::postinclude {
 104
 105 #include "expr/expr.h"
 106 #include "expr/kind.h"
 107 #include "expr/type.h"
 108 #include "parser/antlr_input.h"
 109 #include "parser/parser.h"
 110 #include "parser/smt2/smt2.h"
 111 #include "util/integer.h"
 112 #include "util/output.h"
 113 #include "util/rational.h"
 114 #include "util/hash.h"
 115 #include "util/floatingpoint.h"
 116 #include <vector>
 117 #include <set>
 118 #include <string>
 119 #include <sstream>
 120 // \todo Review the need for this header
 121 #include "math.h"
 122
 123 using namespace CVC4;
 124 using namespace CVC4::parser;
 125
 126 /* These need to be macros so they can refer to the PARSER macro, which
 127  * will be defined by ANTLR *after* this section. (If they were functions,
 128  * 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 static bool isClosed(const Expr& e, std::set<Expr>& free, std::hash_set<Expr, ExprHashFunction>& closedCache) {
 140   if(closedCache.find(e) != closedCache.end()) {
 141     return true;
 142   }
 143
 144   if(e.getKind() == kind::FORALL || e.getKind() == kind::EXISTS || e.getKind() == kind::LAMBDA) {
 145     isClosed(e[1], free, closedCache);
 146     for(Expr::const_iterator i = e[0].begin(); i != e[0].end(); ++i) {
 147       free.erase(*i);
 148     }
 149   } else if(e.getKind() == kind::BOUND_VARIABLE) {
 150     free.insert(e);
 151     return false;
 152   } else {
 153     if(e.hasOperator()) {
 154       isClosed(e.getOperator(), free, closedCache);
 155     }
 156     for(Expr::const_iterator i = e.begin(); i != e.end(); ++i) {
 157       isClosed(*i, free, closedCache);
 158     }
 159   }
 160
 161   if(free.empty()) {
 162     closedCache.insert(e);
 163     return true;
 164   } else {
 165     return false;
 166   }
 167 }
 168
 169 static inline bool isClosed(const Expr& e, std::set<Expr>& free) {
 170   std::hash_set<Expr, ExprHashFunction> cache;
 171   return isClosed(e, free, cache);
 172 }
 173
 174 }/* parser::postinclude */
 175
 176 /**
 177  * Parses an expression.
 178  * @return the parsed expression, or the Null Expr if we've reached the
 179  * end of the input
 180  */
 181 parseExpr returns [CVC4::parser::smt2::myExpr expr]
 182 @declarations {
 183   Expr expr2;
 184 }
 185   : term[expr, expr2]
 186   | EOF
 187   ;
 188
 189 /**
 190  * Parses a command
 191  * @return the parsed command, or NULL if we've reached the end of the input
 192  */
 193 parseCommand returns [CVC4::Command* cmd = NULL]
 194 @declarations {
 195   std::string name;
 196 }
 197   : LPAREN_TOK c = command RPAREN_TOK { $cmd = c; }
 198
 199     /* This extended command has to be in the outermost production so that
 200      * the RPAREN_TOK is properly eaten and we are in a good state to read
 201      * the included file's tokens. */
 202   | LPAREN_TOK INCLUDE_TOK str[name,true] RPAREN_TOK
 203     { if(!PARSER_STATE->canIncludeFile()) {
 204         PARSER_STATE->parseError("include-file feature was disabled for this run.");
 205       }
 206       if(PARSER_STATE->strictModeEnabled()) {
 207         PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode.");
 208       }
 209       PARSER_STATE->includeFile(name);
 210       // The command of the included file will be produced at the next parseCommand() call
 211       cmd = new EmptyCommand("include::" + name);
 212     }
 213
 214   | EOF { $cmd = 0; }
 215   ;
 216
 217 /**
 218  * Parse the internal portion of the command, ignoring the surrounding
 219  * parentheses.
 220  */
 221 command returns [CVC4::Command* cmd = NULL]
 222 @declarations {
 223   std::string name;
 224   std::vector<std::string> names;
 225   Expr expr, expr2;
 226   Type t;
 227   std::vector<Expr> terms;
 228   std::vector<Type> sorts;
 229   std::vector<std::pair<std::string, Type> > sortedVarNames;
 230 }
 231   : /* set the logic */
 232     SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
 233     { Debug("parser") << "set logic: '" << name << "'" << std::endl;
 234       if( PARSER_STATE->logicIsSet() ) {
 235         PARSER_STATE->parseError("Only one set-logic is allowed.");
 236       }
 237       PARSER_STATE->setLogic(name);
 238       $cmd = new SetBenchmarkLogicCommand(name); }
 239   | /* set-info */
 240     SET_INFO_TOK metaInfoInternal[cmd]
 241   | /* get-info */
 242     GET_INFO_TOK KEYWORD
 243     { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); }
 244   | /* set-option */
 245     SET_OPTION_TOK setOptionInternal[cmd]
 246   | /* get-option */
 247     GET_OPTION_TOK KEYWORD
 248     { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); }
 249   | /* sort declaration */
 250     DECLARE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 251     { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) &&
 252          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) &&
 253          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) &&
 254          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) {
 255         PARSER_STATE->parseError(std::string("Free sort symbols not allowed in ") + PARSER_STATE->getLogic().getLogicString());
 256       }
 257     }
 258     symbol[name,CHECK_UNDECLARED,SYM_SORT]
 259     { PARSER_STATE->checkUserSymbol(name); }
 260     n=INTEGER_LITERAL
 261     { Debug("parser") << "declare sort: '" << name
 262                       << "' arity=" << n << std::endl;
 263       unsigned arity = AntlrInput::tokenToUnsigned(n);
 264       if(arity == 0) {
 265         Type type = PARSER_STATE->mkSort(name);
 266         $cmd = new DeclareTypeCommand(name, 0, type);
 267       } else {
 268         Type type = PARSER_STATE->mkSortConstructor(name, arity);
 269         $cmd = new DeclareTypeCommand(name, arity, type);
 270       }
 271     }
 272   | /* sort definition */
 273     DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 274     symbol[name,CHECK_UNDECLARED,SYM_SORT]
 275     { PARSER_STATE->checkUserSymbol(name); }
 276     LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
 277     { PARSER_STATE->pushScope(true);
 278       for(std::vector<std::string>::const_iterator i = names.begin(),
 279             iend = names.end();
 280           i != iend;
 281           ++i) {
 282         sorts.push_back(PARSER_STATE->mkSort(*i));
 283       }
 284     }
 285     sortSymbol[t,CHECK_DECLARED]
 286     { PARSER_STATE->popScope();
 287       // Do NOT call mkSort, since that creates a new sort!
 288       // This name is not its own distinct sort, it's an alias.
 289       PARSER_STATE->defineParameterizedType(name, sorts, t);
 290       $cmd = new DefineTypeCommand(name, sorts, t);
 291     }
 292   | /* function declaration */
 293     DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 294     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 295     { PARSER_STATE->checkUserSymbol(name); }
 296     LPAREN_TOK sortList[sorts] RPAREN_TOK
 297     sortSymbol[t,CHECK_DECLARED]
 298     { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
 299       if( sorts.size() > 0 ) {
 300         if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
 301           PARSER_STATE->parseError(std::string("Functions (of non-zero arity) cannot be declared in logic ") + PARSER_STATE->getLogic().getLogicString());
 302         }
 303         t = EXPR_MANAGER->mkFunctionType(sorts, t);
 304       }
 305       Expr func = PARSER_STATE->mkVar(name, t);
 306       $cmd = new DeclareFunctionCommand(name, func, t); }
 307   | /* function definition */
 308     DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 309     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 310     { PARSER_STATE->checkUserSymbol(name); }
 311     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
 312     sortSymbol[t,CHECK_DECLARED]
 313     { /* add variables to parser state before parsing term */
 314       Debug("parser") << "define fun: '" << name << "'" << std::endl;
 315       if( sortedVarNames.size() > 0 ) {
 316         std::vector<CVC4::Type> sorts;
 317         sorts.reserve(sortedVarNames.size());
 318         for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 319               sortedVarNames.begin(), iend = sortedVarNames.end();
 320             i != iend;
 321             ++i) {
 322           sorts.push_back((*i).second);
 323         }
 324         t = EXPR_MANAGER->mkFunctionType(sorts, t);
 325       }
 326       PARSER_STATE->pushScope(true);
 327       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 328             sortedVarNames.begin(), iend = sortedVarNames.end();
 329           i != iend;
 330           ++i) {
 331         terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
 332       }
 333     }
 334     term[expr, expr2]
 335     { PARSER_STATE->popScope();
 336       // declare the name down here (while parsing term, signature
 337       // must not be extended with the name itself; no recursion
 338       // permitted)
 339       Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
 340       $cmd = new DefineFunctionCommand(name, func, terms, expr);
 341     }
 342   | /* value query */
 343     GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 344     ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
 345       { $cmd = new GetValueCommand(terms); }
 346     | ~LPAREN_TOK
 347       { PARSER_STATE->parseError("The get-value command expects a list of terms.  Perhaps you forgot a pair of parentheses?"); } )
 348   | /* get-assignment */
 349     GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 350     { cmd = new GetAssignmentCommand(); }
 351   | /* assertion */
 352     ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 353     { PARSER_STATE->clearLastNamedTerm(); }
 354     term[expr, expr2]
 355     { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr;
 356       cmd = new AssertCommand(expr, inUnsatCore);
 357       if(inUnsatCore) {
 358         PARSER_STATE->registerUnsatCoreName(PARSER_STATE->lastNamedTerm());
 359       }
 360     }
 361   | /* check-sat */
 362     CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 363     ( term[expr, expr2]
 364       { if(PARSER_STATE->strictModeEnabled()) {
 365           PARSER_STATE->parseError("Extended commands (such as check-sat with an argument) are not permitted while operating in strict compliance mode.");
 366         }
 367       }
 368     | { expr = MK_CONST(bool(true)); } )
 369     { cmd = new CheckSatCommand(expr); }
 370   | /* get-assertions */
 371     GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 372     { cmd = new GetAssertionsCommand(); }
 373   | /* get-proof */
 374     GET_PROOF_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 375     { cmd = new GetProofCommand(); }
 376   | /* get-unsat-core */
 377     GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 378     { cmd = new GetUnsatCoreCommand(PARSER_STATE->getUnsatCoreNames()); }
 379   | /* push */
 380     PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 381     ( k=INTEGER_LITERAL
 382       { unsigned n = AntlrInput::tokenToUnsigned(k);
 383         if(n == 0) {
 384           cmd = new EmptyCommand();
 385         } else if(n == 1) {
 386           PARSER_STATE->pushScope();
 387           PARSER_STATE->pushUnsatCoreNameScope();
 388           cmd = new PushCommand();
 389         } else {
 390           CommandSequence* seq = new CommandSequence();
 391           do {
 392             PARSER_STATE->pushScope();
 393             PARSER_STATE->pushUnsatCoreNameScope();
 394             Command* c = new PushCommand();
 395             c->setMuted(n > 1);
 396             seq->addCommand(c);
 397           } while(--n > 0);
 398           cmd = seq;
 399         }
 400       }
 401     | { if(PARSER_STATE->strictModeEnabled()) {
 402           PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to PUSH.  Maybe you want (push 1)?");
 403         } else {
 404           PARSER_STATE->pushScope();
 405           PARSER_STATE->pushUnsatCoreNameScope();
 406           cmd = new PushCommand();
 407         }
 408       } )
 409   | POP_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 410     ( k=INTEGER_LITERAL
 411       { unsigned n = AntlrInput::tokenToUnsigned(k);
 412         if(n > PARSER_STATE->scopeLevel()) {
 413           PARSER_STATE->parseError("Attempted to pop above the top stack frame.");
 414         }
 415         if(n == 0) {
 416           cmd = new EmptyCommand();
 417         } else if(n == 1) {
 418           PARSER_STATE->popUnsatCoreNameScope();
 419           PARSER_STATE->popScope();
 420           cmd = new PopCommand();
 421         } else {
 422           CommandSequence* seq = new CommandSequence();
 423           do {
 424             PARSER_STATE->popUnsatCoreNameScope();
 425             PARSER_STATE->popScope();
 426             Command* c = new PopCommand();
 427             c->setMuted(n > 1);
 428             seq->addCommand(c);
 429           } while(--n > 0);
 430           cmd = seq;
 431         }
 432       }
 433     | { if(PARSER_STATE->strictModeEnabled()) {
 434           PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to POP.  Maybe you want (pop 1)?");
 435         } else {
 436           PARSER_STATE->popUnsatCoreNameScope();
 437           PARSER_STATE->popScope();
 438           cmd = new PopCommand();
 439         }
 440       } )
 441
 442     /* exit */
 443   | EXIT_TOK
 444     { cmd = new QuitCommand(); }
 445
 446     /* New SMT-LIB 2.5 command set */
 447   | smt25Command[cmd]
 448     { if(PARSER_STATE->v2_0() && PARSER_STATE->strictModeEnabled()) {
 449         PARSER_STATE->parseError("SMT-LIB 2.5 commands are not permitted while operating in strict compliance mode and in SMT-LIB 2.0 mode.");
 450       }
 451     }
 452
 453     /* CVC4-extended SMT-LIB commands */
 454   | extendedCommand[cmd]
 455     { if(PARSER_STATE->strictModeEnabled()) {
 456         PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode.");
 457       }
 458     }
 459
 460     /* error handling */
 461   | SIMPLE_SYMBOL
 462     { std::string id = AntlrInput::tokenText($SIMPLE_SYMBOL);
 463       if(id == "benchmark") {
 464         PARSER_STATE->parseError("In SMT-LIBv2 mode, but got something that looks like SMT-LIBv1.  Use --lang smt1 for SMT-LIBv1.");
 465       } else {
 466         PARSER_STATE->parseError("expected SMT-LIBv2 command, got `" + id + "'.");
 467       }
 468     }
 469   ;
 470
 471 // Separate this into its own rule (can be invoked by set-info or meta-info)
 472 metaInfoInternal[CVC4::Command*& cmd]
 473 @declarations {
 474   std::string name;
 475   SExpr sexpr;
 476 }
 477   : KEYWORD symbolicExpr[sexpr]
 478     { name = AntlrInput::tokenText($KEYWORD);
 479       if(name == ":cvc4-logic" || name == ":cvc4_logic") {
 480         PARSER_STATE->setLogic(sexpr.getValue());
 481       } else if(name == ":smt-lib-version") {
 482         // if we don't recognize the revision name, just keep the current mode
 483         if( (sexpr.isRational() && sexpr.getRationalValue() == Rational(2)) ||
 484             sexpr.getValue() == "2" ||
 485             sexpr.getValue() == "2.0" ) {
 486           PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_0);
 487         } else if( (sexpr.isRational() && sexpr.getRationalValue() == Rational(5, 2)) ||
 488                    sexpr.getValue() == "2.5" ) {
 489           PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_5);
 490         }
 491       }
 492       PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
 493       cmd = new SetInfoCommand(name.c_str() + 1, sexpr);
 494     }
 495   ;
 496
 497 setOptionInternal[CVC4::Command*& cmd]
 498 @init {
 499   std::string name;
 500   SExpr sexpr;
 501 }
 502   : keyword[name] symbolicExpr[sexpr]
 503     { PARSER_STATE->setOption(name.c_str() + 1, sexpr);
 504       cmd = new SetOptionCommand(name.c_str() + 1, sexpr);
 505       // Ugly that this changes the state of the parser; but
 506       // global-declarations affects parsing, so we can't hold off
 507       // on this until some SmtEngine eventually (if ever) executes it.
 508       if(name == ":global-declarations") {
 509         PARSER_STATE->setGlobalDeclarations(sexpr.getValue() == "true");
 510       }
 511     }
 512   ;
 513
 514 smt25Command[CVC4::Command*& cmd]
 515 @declarations {
 516   std::string name;
 517   Expr expr, expr2;
 518   std::vector<std::pair<std::string, Type> > sortedVarNames;
 519   SExpr sexpr;
 520   Type t;
 521 }
 522     /* meta-info */
 523   : META_INFO_TOK metaInfoInternal[cmd]
 524
 525     /* declare-const */
 526   | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 527     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 528     { PARSER_STATE->checkUserSymbol(name); }
 529     sortSymbol[t,CHECK_DECLARED]
 530     { Expr c = PARSER_STATE->mkVar(name, t);
 531       $cmd = new DeclareFunctionCommand(name, c, t); }
 532
 533     /* get model */
 534   | GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 535     { cmd = new GetModelCommand(); }
 536
 537     /* echo */
 538   | ECHO_TOK
 539     ( simpleSymbolicExpr[sexpr]
 540       { std::stringstream ss;
 541         ss << sexpr;
 542         cmd = new EchoCommand(ss.str());
 543       }
 544     | { cmd = new EchoCommand(); }
 545     )
 546
 547     /* reset: reset everything, returning solver to initial state.
 548      * Logic and options must be set again. */
 549   | RESET_TOK
 550     { cmd = new ResetCommand();
 551       PARSER_STATE->reset();
 552     }
 553     /* reset-assertions: reset assertions, assertion stack, declarations,
 554      * etc., but the logic and options remain as they were. */
 555   | RESET_ASSERTIONS_TOK
 556     { cmd = new ResetAssertionsCommand();
 557       PARSER_STATE->resetAssertions();
 558     }
 559
 560   | /* recursive function definition */
 561     DEFINE_FUN_REC_TOK { PARSER_STATE->checkThatLogicIsSet(); } LPAREN_TOK
 562     { PARSER_STATE->pushScope(true); }
 563     ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 564       { PARSER_STATE->checkUserSymbol(name); }
 565       LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
 566       sortSymbol[t,CHECK_DECLARED]
 567       { /* add variables to parser state before parsing term */
 568         Debug("parser") << "define fun rec: '" << name << "'" << std::endl;
 569           if( sortedVarNames.size() > 0 ) {
 570           std::vector<CVC4::Type> sorts;
 571           sorts.reserve(sortedVarNames.size());
 572           for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 573                 sortedVarNames.begin(), iend = sortedVarNames.end();
 574               i != iend;
 575               ++i) {
 576             sorts.push_back((*i).second);
 577           }
 578           t = EXPR_MANAGER->mkFunctionType(sorts, t);
 579         }
 580         PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
 581         PARSER_STATE->pushScope(true);
 582         for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 583               sortedVarNames.begin(), iend = sortedVarNames.end();
 584             i != iend;
 585             ++i) {
 586           PARSER_STATE->mkBoundVar((*i).first, (*i).second);
 587         }
 588       }
 589       term[expr, expr2]
 590       { PARSER_STATE->popScope(); }
 591       RPAREN_TOK )+ RPAREN_TOK
 592       { PARSER_STATE->popScope(); }
 593
 594   // CHECK_SAT_ASSUMING still being discussed
 595   // GET_UNSAT_ASSUMPTIONS
 596   ;
 597
 598 extendedCommand[CVC4::Command*& cmd]
 599 @declarations {
 600   std::vector<CVC4::Datatype> dts;
 601   Expr e, e2;
 602   Type t;
 603   std::string name;
 604   std::vector<std::string> names;
 605   std::vector<Expr> terms;
 606   std::vector<Type> sorts;
 607   std::vector<std::pair<std::string, Type> > sortedVarNames;
 608 }
 609     /* Extended SMT-LIB set of commands syntax, not permitted in
 610      * --smtlib2 compliance mode. */
 611   : DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
 612   | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
 613   | rewriterulesCommand[cmd]
 614
 615     /* Support some of Z3's extended SMT-LIB commands */
 616
 617   | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 618     { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) &&
 619          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) &&
 620          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) &&
 621          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) {
 622         PARSER_STATE->parseError(std::string("Free sort symbols not allowed in ") + PARSER_STATE->getLogic().getLogicString());
 623       }
 624     }
 625     { $cmd = new CommandSequence(); }
 626     LPAREN_TOK
 627     ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
 628       { PARSER_STATE->checkUserSymbol(name);
 629         Type type = PARSER_STATE->mkSort(name);
 630         static_cast<CommandSequence*>($cmd)->addCommand(new DeclareTypeCommand(name, 0, type));
 631       }
 632     )+
 633     RPAREN_TOK
 634
 635   | DECLARE_FUNS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 636     { $cmd = new CommandSequence(); }
 637     LPAREN_TOK
 638     ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 639       { PARSER_STATE->checkUserSymbol(name); }
 640       nonemptySortList[sorts] RPAREN_TOK
 641       { Type t;
 642         if(sorts.size() > 1) {
 643           if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
 644             PARSER_STATE->parseError(std::string("Functions (of non-zero arity) cannot be declared in logic ") + PARSER_STATE->getLogic().getLogicString());
 645           }
 646           t = EXPR_MANAGER->mkFunctionType(sorts);
 647         } else {
 648           t = sorts[0];
 649         }
 650         Expr func = PARSER_STATE->mkVar(name, t);
 651         static_cast<CommandSequence*>($cmd)->addCommand(new DeclareFunctionCommand(name, func, t));
 652       }
 653     )+
 654     RPAREN_TOK
 655
 656   | DECLARE_PREDS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 657     { $cmd = new CommandSequence(); }
 658     LPAREN_TOK
 659     ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 660       { PARSER_STATE->checkUserSymbol(name); }
 661       sortList[sorts] RPAREN_TOK
 662       { Type t = EXPR_MANAGER->booleanType();
 663         if(sorts.size() > 0) {
 664           if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
 665             PARSER_STATE->parseError(std::string("Predicates (of non-zero arity) cannot be declared in logic ") + PARSER_STATE->getLogic().getLogicString());
 666           }
 667           t = EXPR_MANAGER->mkFunctionType(sorts, t);
 668         }
 669         Expr func = PARSER_STATE->mkVar(name, t);
 670         static_cast<CommandSequence*>($cmd)->addCommand(new DeclareFunctionCommand(name, func, t));
 671       }
 672     )+
 673     RPAREN_TOK
 674
 675   | DEFINE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 676     ( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 677       { PARSER_STATE->checkUserSymbol(name); }
 678       term[e,e2]
 679       { Expr func = PARSER_STATE->mkFunction(name, e.getType(), ExprManager::VAR_FLAG_DEFINED);
 680         $cmd = new DefineFunctionCommand(name, func, e);
 681       }
 682     | LPAREN_TOK
 683       symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 684       { PARSER_STATE->checkUserSymbol(name); }
 685       sortedVarList[sortedVarNames] RPAREN_TOK
 686       { /* add variables to parser state before parsing term */
 687         Debug("parser") << "define fun: '" << name << "'" << std::endl;
 688         PARSER_STATE->pushScope(true);
 689         for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 690               sortedVarNames.begin(), iend = sortedVarNames.end();
 691             i != iend;
 692             ++i) {
 693           terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
 694         }
 695       }
 696       term[e,e2]
 697       { PARSER_STATE->popScope();
 698         // declare the name down here (while parsing term, signature
 699         // must not be extended with the name itself; no recursion
 700         // permitted)
 701         Type t = e.getType();
 702         if( sortedVarNames.size() > 0 ) {
 703           std::vector<CVC4::Type> sorts;
 704           sorts.reserve(sortedVarNames.size());
 705           for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 706                 sortedVarNames.begin(), iend = sortedVarNames.end();
 707               i != iend;
 708               ++i) {
 709             sorts.push_back((*i).second);
 710           }
 711           t = EXPR_MANAGER->mkFunctionType(sorts, t);
 712         }
 713         Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
 714         $cmd = new DefineFunctionCommand(name, func, terms, e);
 715       }
 716     )
 717   | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 718     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 719     { PARSER_STATE->checkUserSymbol(name); }
 720     sortSymbol[t,CHECK_DECLARED]
 721     { /* add variables to parser state before parsing term */
 722       Debug("parser") << "define const: '" << name << "'" << std::endl;
 723       PARSER_STATE->pushScope(true);
 724       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 725             sortedVarNames.begin(), iend = sortedVarNames.end();
 726           i != iend;
 727           ++i) {
 728         terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
 729       }
 730     }
 731     term[e, e2]
 732     { PARSER_STATE->popScope();
 733       // declare the name down here (while parsing term, signature
 734       // must not be extended with the name itself; no recursion
 735       // permitted)
 736       Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
 737       $cmd = new DefineFunctionCommand(name, func, terms, e);
 738     }
 739
 740   | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 741     term[e,e2]
 742     { cmd = new SimplifyCommand(e); }
 743   ;
 744
 745
 746 datatypesDefCommand[bool isCo, CVC4::Command*& cmd]
 747 @declarations {
 748   std::vector<CVC4::Datatype> dts;
 749   std::string name;
 750   std::vector<Type> sorts;
 751 }
 752   : { PARSER_STATE->checkThatLogicIsSet();
 753     /* open a scope to keep the UnresolvedTypes contained */
 754     PARSER_STATE->pushScope(true); }
 755   LPAREN_TOK /* parametric sorts */
 756   ( symbol[name,CHECK_UNDECLARED,SYM_SORT] {
 757     sorts.push_back( PARSER_STATE->mkSort(name) ); }
 758   )*
 759   RPAREN_TOK
 760   LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
 761   { PARSER_STATE->popScope();
 762   cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
 763   ;
 764
 765 rewriterulesCommand[CVC4::Command*& cmd]
 766 @declarations {
 767   std::vector<std::pair<std::string, Type> > sortedVarNames;
 768   std::vector<Expr> args, guards, heads, triggers;
 769   Expr head, body, expr, expr2, bvl;
 770   Kind kind;
 771 }
 772   : /* rewrite rules */
 773     REWRITE_RULE_TOK
 774     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
 775     {
 776       kind = CVC4::kind::RR_REWRITE;
 777       PARSER_STATE->pushScope(true);
 778       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 779             sortedVarNames.begin(), iend = sortedVarNames.end();
 780           i != iend;
 781           ++i) {
 782         args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
 783       }
 784       bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
 785     }
 786     LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK
 787     LPAREN_TOK (termList[guards,expr])? RPAREN_TOK
 788     term[head, expr2] term[body, expr2]
 789     {
 790       args.clear();
 791       args.push_back(head);
 792       args.push_back(body);
 793       /* triggers */
 794       if( !triggers.empty() ){
 795         expr2 = MK_EXPR(kind::INST_PATTERN_LIST, triggers);
 796         args.push_back(expr2);
 797       };
 798       expr = MK_EXPR(kind, args);
 799       args.clear();
 800       args.push_back(bvl);
 801       /* guards */
 802       switch( guards.size() ){
 803       case 0:
 804         args.push_back(MK_CONST(bool(true))); break;
 805       case 1:
 806         args.push_back(guards[0]); break;
 807       default:
 808         expr2 = MK_EXPR(kind::AND, guards);
 809         args.push_back(expr2); break;
 810       };
 811       args.push_back(expr);
 812       expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
 813       cmd = new AssertCommand(expr, false); }
 814     /* propagation rule */
 815   | rewritePropaKind[kind]
 816     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
 817     {
 818       PARSER_STATE->pushScope(true);
 819       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 820             sortedVarNames.begin(), iend = sortedVarNames.end();
 821           i != iend;
 822           ++i) {
 823         args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
 824       }
 825       bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
 826     }
 827     LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK
 828     LPAREN_TOK (termList[guards,expr])? RPAREN_TOK
 829     LPAREN_TOK (termList[heads,expr])? RPAREN_TOK
 830     term[body, expr2]
 831     {
 832       args.clear();
 833       /* heads */
 834       switch( heads.size() ){
 835       case 0:
 836         args.push_back(MK_CONST(bool(true))); break;
 837       case 1:
 838         args.push_back(heads[0]); break;
 839       default:
 840         expr2 = MK_EXPR(kind::AND, heads);
 841         args.push_back(expr2); break;
 842       };
 843       args.push_back(body);
 844       /* triggers */
 845       if( !triggers.empty() ){
 846         expr2 = MK_EXPR(kind::INST_PATTERN_LIST, triggers);
 847         args.push_back(expr2);
 848       };
 849       expr = MK_EXPR(kind, args);
 850       args.clear();
 851       args.push_back(bvl);
 852       /* guards */
 853       switch( guards.size() ){
 854       case 0:
 855         args.push_back(MK_CONST(bool(true))); break;
 856       case 1:
 857         args.push_back(guards[0]); break;
 858       default:
 859         expr2 = MK_EXPR(kind::AND, guards);
 860         args.push_back(expr2); break;
 861       };
 862       args.push_back(expr);
 863       expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
 864       cmd = new AssertCommand(expr, false); }
 865   ;
 866
 867 rewritePropaKind[CVC4::Kind& kind]
 868   : REDUCTION_RULE_TOK    { $kind = CVC4::kind::RR_REDUCTION; }
 869   | PROPAGATION_RULE_TOK  { $kind = CVC4::kind::RR_DEDUCTION; }
 870   ;
 871
 872 pattern[CVC4::Expr& expr]
 873 @declarations {
 874   std::vector<Expr> patexpr;
 875 }
 876   : LPAREN_TOK termList[patexpr,expr] RPAREN_TOK
 877     {
 878       expr = MK_EXPR(kind::INST_PATTERN, patexpr);
 879     }
 880   ;
 881
 882 simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
 883 @declarations {
 884   CVC4::Kind k;
 885   std::string s;
 886   std::vector<unsigned int> s_vec;
 887 }
 888   : INTEGER_LITERAL
 889     { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
 890   | DECIMAL_LITERAL
 891     { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
 892   | HEX_LITERAL
 893     { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
 894       std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
 895       sexpr = Integer(hexString, 16);
 896     }
 897   | BINARY_LITERAL
 898     { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
 899       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
 900       sexpr = Integer(binString, 2);
 901     }
 902   | str[s,false]
 903     { sexpr = SExpr(s); }
 904 //  | LPAREN_TOK STRCST_TOK
 905 //      ( INTEGER_LITERAL {
 906 //          s_vec.push_back( atoi( AntlrInput::tokenText($INTEGER_LITERAL) ) + 65 );
 907 //        } )* RPAREN_TOK
 908 //   {
 909 //      sexpr = SExpr( MK_CONST( ::CVC4::String(s_vec) ) );
 910 //      }
 911   | symbol[s,CHECK_NONE,SYM_SORT]
 912     { sexpr = SExpr(SExpr::Keyword(s)); }
 913   | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK)
 914     { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); }
 915   | builtinOp[k]
 916     { std::stringstream ss;
 917       ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2_5) << EXPR_MANAGER->mkConst(k);
 918       sexpr = SExpr(ss.str());
 919     }
 920   ;
 921
 922 keyword[std::string& s]
 923   : KEYWORD
 924     { s = AntlrInput::tokenText($KEYWORD); }
 925   ;
 926
 927 simpleSymbolicExpr[CVC4::SExpr& sexpr]
 928   : simpleSymbolicExprNoKeyword[sexpr]
 929   | KEYWORD
 930     { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
 931   ;
 932
 933 symbolicExpr[CVC4::SExpr& sexpr]
 934 @declarations {
 935   std::vector<SExpr> children;
 936 }
 937   : simpleSymbolicExpr[sexpr]
 938   | LPAREN_TOK
 939     ( symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK
 940     { sexpr = SExpr(children); }
 941   ;
 942
 943 /**
 944  * Matches a term.
 945  * @return the expression representing the formula
 946  */
 947 term[CVC4::Expr& expr, CVC4::Expr& expr2]
 948 @init {
 949   Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
 950   Kind kind = kind::NULL_EXPR;
 951   Expr op;
 952   std::string name;
 953   std::vector<Expr> args;
 954   std::vector< std::pair<std::string, Type> > sortedVarNames;
 955   Expr f, f2, f3, f4;
 956   std::string attr;
 957   Expr attexpr;
 958   std::vector<Expr> patexprs;
 959   std::hash_set<std::string, StringHashFunction> names;
 960   std::vector< std::pair<std::string, Expr> > binders;
 961   Type type;
 962   std::string s;
 963   bool isBuiltinOperator = false;
 964 }
 965   : /* a built-in operator application */
 966     LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
 967     {
 968       if( kind == CVC4::kind::EQUAL &&
 969           args.size() > 0 &&
 970           args[0].getType() == EXPR_MANAGER->booleanType() ) {
 971         /* Use IFF for boolean equalities. */
 972         kind = CVC4::kind::IFF;
 973       }
 974
 975       if( !PARSER_STATE->strictModeEnabled() &&
 976           (kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
 977           args.size() == 1) {
 978         /* Unary AND/OR can be replaced with the argument.
 979          * It just so happens expr should already be the only argument. */
 980         assert( expr == args[0] );
 981       } else if( CVC4::kind::isAssociative(kind) &&
 982                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
 983         /* Special treatment for associative operators with lots of children */
 984         expr = EXPR_MANAGER->mkAssociative(kind, args);
 985       } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) {
 986         expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
 987       } else if( ( kind == CVC4::kind::XOR || kind == CVC4::kind::MINUS ) &&
 988                  args.size() > 2 ) {
 989         /* left-associative, but CVC4 internally only supports 2 args */
 990         expr = args[0];
 991         for(size_t i = 1; i < args.size(); ++i) {
 992           expr = MK_EXPR(kind, expr, args[i]);
 993         }
 994       } else if( kind == CVC4::kind::IMPLIES && args.size() > 2 ) {
 995         /* right-associative, but CVC4 internally only supports 2 args */
 996         expr = args[args.size() - 1];
 997         for(size_t i = args.size() - 1; i > 0;) {
 998           expr = MK_EXPR(kind, args[--i], expr);
 999         }
1000       } else if( ( kind == CVC4::kind::IFF || kind == CVC4::kind::EQUAL ||
1001                    kind == CVC4::kind::LT || kind == CVC4::kind::GT ||
1002                    kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) &&
1003                  args.size() > 2 ) {
1004         /* "chainable", but CVC4 internally only supports 2 args */
1005         expr = MK_EXPR(MK_CONST(Chain(kind)), args);
1006       } else if( PARSER_STATE->strictModeEnabled() && kind == CVC4::kind::ABS &&
1007                  args.size() == 1 && !args[0].getType().isInteger() ) {
1008         /* first, check that ABS is even defined in this logic */
1009         PARSER_STATE->checkOperator(kind, args.size());
1010         PARSER_STATE->parseError("abs can only be applied to Int, not Real, while in strict SMT-LIB compliance mode");
1011       } else {
1012         PARSER_STATE->checkOperator(kind, args.size());
1013         expr = MK_EXPR(kind, args);
1014       }
1015     }
1016   | LPAREN_TOK AS_TOK term[f, f2] sortSymbol[type, CHECK_DECLARED] RPAREN_TOK
1017     {
1018       if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) {
1019         std::vector<CVC4::Expr> v;
1020         Expr e = f.getOperator();
1021         const DatatypeConstructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)];
1022         v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
1023                              MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() ));
1024         v.insert(v.end(), f.begin(), f.end());
1025         expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
1026       } else if(f.getKind() == CVC4::kind::EMPTYSET) {
1027         Debug("parser") << "Empty set encountered: " << f << " "
1028                           << f2 << " " << type <<  std::endl;
1029         expr = MK_CONST( ::CVC4::EmptySet(type) );
1030       } else {
1031         if(f.getType() != type) {
1032           PARSER_STATE->parseError("Type ascription not satisfied.");
1033         }
1034       }
1035     }
1036   | LPAREN_TOK quantOp[kind]
1037     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1038     {
1039       PARSER_STATE->pushScope(true);
1040       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
1041             sortedVarNames.begin(), iend = sortedVarNames.end();
1042           i != iend;
1043           ++i) {
1044         args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
1045       }
1046       Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
1047       args.clear();
1048       args.push_back(bvl);
1049     }
1050     term[f, f2] RPAREN_TOK
1051     {
1052       PARSER_STATE->popScope();
1053       switch(f.getKind()) {
1054       case CVC4::kind::RR_REWRITE:
1055       case CVC4::kind::RR_REDUCTION:
1056       case CVC4::kind::RR_DEDUCTION:
1057         if(kind == CVC4::kind::EXISTS) {
1058           PARSER_STATE->parseError("Use Exists instead of Forall for a rewrite rule.");
1059         }
1060         args.push_back(f2); // guards
1061         args.push_back(f); // rule
1062         expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
1063         break;
1064       default:
1065         args.push_back(f);
1066         if(! f2.isNull()){
1067           args.push_back(f2);
1068         }
1069         expr = MK_EXPR(kind, args);
1070       }
1071     }
1072   | LPAREN_TOK functionName[name, CHECK_NONE]
1073     { isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
1074       if(isBuiltinOperator) {
1075         /* A built-in operator not already handled by the lexer */
1076         kind = PARSER_STATE->getOperatorKind(name);
1077       } else {
1078         /* A non-built-in function application */
1079         PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE);
1080         PARSER_STATE->checkFunctionLike(name);
1081         const bool isDefinedFunction =
1082           PARSER_STATE->isDefinedFunction(name);
1083         if(isDefinedFunction) {
1084           expr = PARSER_STATE->getFunction(name);
1085           kind = CVC4::kind::APPLY;
1086         } else {
1087           expr = PARSER_STATE->getVariable(name);
1088           Type t = expr.getType();
1089           if(t.isConstructor()) {
1090             kind = CVC4::kind::APPLY_CONSTRUCTOR;
1091           } else if(t.isSelector()) {
1092             kind = CVC4::kind::APPLY_SELECTOR;
1093           } else if(t.isTester()) {
1094             kind = CVC4::kind::APPLY_TESTER;
1095           } else {
1096             kind = CVC4::kind::APPLY_UF;
1097           }
1098         }
1099         args.push_back(expr);
1100       }
1101         }
1102     termList[args,expr] RPAREN_TOK
1103     { Debug("parser") << "args has size " << args.size() << std::endl << "expr is " << expr << std::endl;
1104       for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) {
1105         Debug("parser") << "++ " << *i << std::endl;
1106       }
1107       if(isBuiltinOperator) {
1108         PARSER_STATE->checkOperator(kind, args.size());
1109       }
1110       expr = MK_EXPR(kind, args); }
1111
1112   | LPAREN_TOK
1113     ( /* An indexed function application */
1114       indexedFunctionName[op] termList[args,expr] RPAREN_TOK
1115       { expr = MK_EXPR(op, args);
1116         PARSER_STATE->checkOperator(expr.getKind(), args.size());
1117       }
1118     | /* Array constant (in Z3 syntax) */
1119       LPAREN_TOK AS_TOK CONST_TOK sortSymbol[type, CHECK_DECLARED]
1120       RPAREN_TOK term[f, f2] RPAREN_TOK
1121       {
1122         if(!type.isArray()) {
1123           std::stringstream ss;
1124           ss << "expected array constant term, but cast is not of array type" << std::endl
1125              << "cast type: " << type;
1126           PARSER_STATE->parseError(ss.str());
1127         }
1128         if(!f.isConst()) {
1129           std::stringstream ss;
1130           ss << "expected constant term inside array constant, but found "
1131              << "nonconstant term:" << std::endl
1132              << "the term: " << f;
1133           PARSER_STATE->parseError(ss.str());
1134         }
1135         if(!ArrayType(type).getConstituentType().isComparableTo(f.getType())) {
1136           std::stringstream ss;
1137           ss << "type mismatch inside array constant term:" << std::endl
1138              << "array type:          " << type << std::endl
1139              << "expected const type: " << ArrayType(type).getConstituentType() << std::endl
1140              << "computed const type: " << f.getType();
1141           PARSER_STATE->parseError(ss.str());
1142         }
1143         expr = MK_CONST( ::CVC4::ArrayStoreAll(type, f) );
1144       }
1145     )
1146   | /* a let binding */
1147     LPAREN_TOK LET_TOK LPAREN_TOK
1148     { PARSER_STATE->pushScope(true); }
1149     ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] term[expr, f2] RPAREN_TOK
1150       // this is a parallel let, so we have to save up all the contributions
1151       // of the let and define them only later on
1152       { if(names.count(name) == 1) {
1153           std::stringstream ss;
1154           ss << "warning: symbol `" << name << "' bound multiple times by let; the last binding will be used, shadowing earlier ones";
1155           PARSER_STATE->warning(ss.str());
1156         } else {
1157           names.insert(name);
1158         }
1159         binders.push_back(std::make_pair(name, expr)); } )+
1160     { // now implement these bindings
1161       for(std::vector< std::pair<std::string, Expr> >::iterator i = binders.begin(); i != binders.end(); ++i) {
1162         PARSER_STATE->defineVar((*i).first, (*i).second);
1163       }
1164     }
1165     RPAREN_TOK
1166     term[expr, f2]
1167     RPAREN_TOK
1168     { PARSER_STATE->popScope(); }
1169
1170     /* a variable */
1171   | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
1172     { const bool isDefinedFunction =
1173         PARSER_STATE->isDefinedFunction(name);
1174       if(PARSER_STATE->isAbstractValue(name)) {
1175         expr = PARSER_STATE->mkAbstractValue(name);
1176       } else if(isDefinedFunction) {
1177         expr = MK_EXPR(CVC4::kind::APPLY,
1178                        PARSER_STATE->getFunction(name));
1179       } else {
1180         expr = PARSER_STATE->getVariable(name);
1181         Type t = PARSER_STATE->getType(name);
1182         if(t.isConstructor() && ConstructorType(t).getArity() == 0) {
1183           // don't require parentheses, immediately turn it into an apply
1184           expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
1185         }
1186       }
1187     }
1188
1189     /* attributed expressions */
1190   | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
1191     ( attribute[expr, attexpr, attr]
1192       { if( ! attexpr.isNull()) {
1193           patexprs.push_back( attexpr );
1194         }
1195       }
1196     )+ RPAREN_TOK
1197     {
1198       if(attr == ":rewrite-rule") {
1199         Expr guard;
1200         Expr body;
1201         if(expr[1].getKind() == kind::IMPLIES ||
1202            expr[1].getKind() == kind::IFF ||
1203            expr[1].getKind() == kind::EQUAL) {
1204           guard = expr[0];
1205           body = expr[1];
1206         } else {
1207           guard = MK_CONST(bool(true));
1208           body = expr;
1209         }
1210         expr2 = guard;
1211         args.push_back(body[0]);
1212         args.push_back(body[1]);
1213         if(!f2.isNull()) {
1214           args.push_back(f2);
1215         }
1216
1217         if     ( body.getKind()==kind::IMPLIES )    kind = kind::RR_DEDUCTION;
1218         else if( body.getKind()==kind::IFF )        kind = kind::RR_REDUCTION;
1219         else if( body.getKind()==kind::EQUAL )      kind = kind::RR_REWRITE;
1220         else PARSER_STATE->parseError("Error parsing rewrite rule.");
1221
1222         expr = MK_EXPR( kind, args );
1223       } else if(! patexprs.empty()) {
1224         if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){
1225           for( size_t i=0; i<f2.getNumChildren(); i++ ){
1226             if( f2[i].getKind()==kind::INST_PATTERN ){
1227               patexprs.push_back( f2[i] );
1228             }else{
1229               std::stringstream ss;
1230               ss << "warning: rewrite rules do not support " << f2[i] << " within instantiation pattern list";
1231               PARSER_STATE->warning(ss.str());
1232             }
1233           }
1234         }
1235         expr2 = MK_EXPR(kind::INST_PATTERN_LIST, patexprs);
1236       } else {
1237         expr2 = f2;
1238       }
1239     }
1240     /* constants */
1241   | INTEGER_LITERAL
1242     { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
1243
1244   | DECIMAL_LITERAL
1245     { // FIXME: This doesn't work because an SMT rational is not a
1246       // valid GMP rational string
1247       expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
1248
1249   | LPAREN_TOK INDEX_TOK
1250     ( bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL
1251       { if(AntlrInput::tokenText($bvLit).find("bv") == 0) {
1252            expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) );
1253         } else {
1254            PARSER_STATE->parseError("Unexpected symbol `" + AntlrInput::tokenText($bvLit) + "'");
1255         }
1256       }
1257     | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
1258       { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
1259                                       AntlrInput::tokenToUnsigned($sb),
1260                                       +INFINITY)); }
1261     | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
1262       { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
1263                                       AntlrInput::tokenToUnsigned($sb),
1264                                      -INFINITY)); }
1265     | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
1266       { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
1267                                       AntlrInput::tokenToUnsigned($sb),
1268                                       NAN)); }
1269     // NOTE: Theory parametric constants go here
1270
1271     )
1272     RPAREN_TOK
1273
1274   | HEX_LITERAL
1275     { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
1276       std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
1277       expr = MK_CONST( BitVector(hexString, 16) ); }
1278
1279   | BINARY_LITERAL
1280     { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
1281       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
1282       expr = MK_CONST( BitVector(binString, 2) ); }
1283
1284   | str[s,false]
1285     { expr = MK_CONST( ::CVC4::String(s) ); }
1286   | FP_RNE_TOK      { expr = MK_CONST(roundNearestTiesToEven); }
1287   | FP_RNA_TOK      { expr = MK_CONST(roundNearestTiesToAway); }
1288   | FP_RTP_TOK      { expr = MK_CONST(roundTowardPositive); }
1289   | FP_RTN_TOK      { expr = MK_CONST(roundTowardNegative); }
1290   | FP_RTZ_TOK      { expr = MK_CONST(roundTowardZero); }
1291   | FP_RNE_FULL_TOK { expr = MK_CONST(roundNearestTiesToEven); }
1292   | FP_RNA_FULL_TOK { expr = MK_CONST(roundNearestTiesToAway); }
1293   | FP_RTP_FULL_TOK { expr = MK_CONST(roundTowardPositive); }
1294   | FP_RTN_FULL_TOK { expr = MK_CONST(roundTowardNegative); }
1295   | FP_RTZ_FULL_TOK { expr = MK_CONST(roundTowardZero); }
1296
1297   | RENOSTR_TOK
1298     { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_EMPTY, nvec ); }
1299
1300   | REALLCHAR_TOK
1301     { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_SIGMA, nvec ); }
1302
1303   | EMPTYSET_TOK
1304     { expr = MK_CONST( ::CVC4::EmptySet(Type())); }
1305
1306     // NOTE: Theory constants go here
1307   ;
1308
1309 /**
1310  * Read attribute
1311  */
1312 attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
1313 @init {
1314   SExpr sexpr;
1315   Expr patexpr;
1316   std::vector<Expr> patexprs;
1317   Expr e2;
1318   bool hasValue = false;
1319 }
1320   : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )?
1321   {
1322     attr = AntlrInput::tokenText($KEYWORD);
1323     // EXPR_MANAGER->setNamedAttribute( expr, attr );
1324     if(attr == ":rewrite-rule") {
1325       if(hasValue) {
1326         std::stringstream ss;
1327         ss << "warning: Attribute " << attr << " does not take a value (ignoring)";
1328         PARSER_STATE->warning(ss.str());
1329       }
1330       // do nothing
1331     } else if(attr==":axiom" || attr==":conjecture" || attr==":fun-def" || attr==":sygus" || attr==":synthesis") {
1332       if(hasValue) {
1333         std::stringstream ss;
1334         ss << "warning: Attribute " << attr << " does not take a value (ignoring)";
1335         PARSER_STATE->warning(ss.str());
1336       }
1337       bool success = true;
1338       if( attr==":fun-def" ){
1339         if( ( expr.getKind()!=kind::EQUAL && expr.getKind()!=kind::IFF ) || expr[0].getKind()!=kind::APPLY_UF ){
1340           success = false;
1341         }else{
1342           FunctionType t = (FunctionType)expr[0].getOperator().getType();
1343           for( unsigned i=0; i<expr[0].getNumChildren(); i++ ){
1344             if( expr[0][i].getKind()!=kind::BOUND_VARIABLE || expr[0][i].getType()!=t.getArgTypes()[i] ){
1345               success = false;
1346               break;
1347             }else{
1348               for( unsigned j=0; j<i; j++ ){
1349                 if( expr[0][j]==expr[0][i] ){
1350                   success = false;
1351                   break;
1352                 }
1353               }
1354             }
1355           }
1356         }
1357         if( !success ){
1358           std::stringstream ss;
1359           ss << "warning: Function definition should be an equality whose LHS is an uninterpreted function applied to unique variables.";
1360           PARSER_STATE->warning(ss.str());
1361         }
1362       }
1363       if( success ){
1364         std::string attr_name = attr;
1365         attr_name.erase( attr_name.begin() );
1366         //will set the attribute on auxiliary var (preserves attribute on formula through rewriting)
1367         Type t = EXPR_MANAGER->booleanType();
1368         Expr avar = PARSER_STATE->mkVar(attr_name, t);
1369         retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
1370         Command* c = new SetUserAttributeCommand( attr_name, avar );
1371         c->setMuted(true);
1372         PARSER_STATE->preemptCommand(c);
1373       }
1374     } else {
1375       PARSER_STATE->attributeNotSupported(attr);
1376     }
1377   }
1378   | ATTRIBUTE_PATTERN_TOK LPAREN_TOK ( term[patexpr, e2] { patexprs.push_back( patexpr ); }  )+ RPAREN_TOK
1379     {
1380       attr = std::string(":pattern");
1381       retExpr = MK_EXPR(kind::INST_PATTERN, patexprs);
1382     }
1383   | ATTRIBUTE_NO_PATTERN_TOK term[patexpr, e2]
1384     {
1385       attr = std::string(":no-pattern");
1386       retExpr = MK_EXPR(kind::INST_NO_PATTERN, patexpr);
1387     }
1388   | tok=( ATTRIBUTE_INST_LEVEL | ATTRIBUTE_RR_PRIORITY ) INTEGER_LITERAL
1389     {
1390       Expr n = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) );
1391       std::vector<Expr> values;
1392       values.push_back( n );
1393       std::string attr_name(AntlrInput::tokenText($tok));
1394       attr_name.erase( attr_name.begin() );
1395       Type t = EXPR_MANAGER->booleanType();
1396       Expr avar = PARSER_STATE->mkVar(attr_name, t);
1397       retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
1398       Command* c = new SetUserAttributeCommand( attr_name, avar, values );
1399       c->setMuted(true);
1400       PARSER_STATE->preemptCommand(c);
1401     }
1402   | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
1403     {
1404       attr = std::string(":named");
1405       if(!sexpr.isKeyword()) {
1406         PARSER_STATE->parseError("improperly formed :named annotation");
1407       }
1408       std::string name = sexpr.getValue();
1409       PARSER_STATE->checkUserSymbol(name);
1410       // ensure expr is a closed subterm
1411       std::set<Expr> freeVars;
1412       if(!isClosed(expr, freeVars)) {
1413         assert(!freeVars.empty());
1414         std::stringstream ss;
1415         ss << ":named annotations can only name terms that are closed; this one contains free variables:";
1416         for(std::set<Expr>::const_iterator i = freeVars.begin(); i != freeVars.end(); ++i) {
1417           ss << " " << *i;
1418         }
1419         PARSER_STATE->parseError(ss.str());
1420       }
1421       // check that sexpr is a fresh function symbol, and reserve it
1422       PARSER_STATE->reserveSymbolAtAssertionLevel(name);
1423       // define it
1424       Expr func = PARSER_STATE->mkFunction(name, expr.getType());
1425       // remember the last term to have been given a :named attribute
1426       PARSER_STATE->setLastNamedTerm(expr, name);
1427       // bind name to expr with define-fun
1428       Command* c =
1429         new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
1430       c->setMuted(true);
1431       PARSER_STATE->preemptCommand(c);
1432     }
1433   ;
1434
1435 /**
1436  * Matches a bit-vector operator (the ones parametrized by numbers)
1437  */
1438 indexedFunctionName[CVC4::Expr& op]
1439   : LPAREN_TOK INDEX_TOK
1440     ( 'extract' n1=INTEGER_LITERAL n2=INTEGER_LITERAL
1441       { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1),
1442                                        AntlrInput::tokenToUnsigned($n2))); }
1443     | 'repeat' n=INTEGER_LITERAL
1444       { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
1445     | 'zero_extend' n=INTEGER_LITERAL
1446       { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
1447     | 'sign_extend' n=INTEGER_LITERAL
1448       { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); }
1449     | 'rotate_left' n=INTEGER_LITERAL
1450       { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
1451     | 'rotate_right' n=INTEGER_LITERAL
1452       { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
1453     | DIVISIBLE_TOK n=INTEGER_LITERAL
1454       { op = MK_CONST(Divisible(AntlrInput::tokenToUnsigned($n))); }
1455     | INT2BV_TOK n=INTEGER_LITERAL
1456       { op = MK_CONST(IntToBitVector(AntlrInput::tokenToUnsigned($n)));
1457         if(PARSER_STATE->strictModeEnabled()) {
1458           PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode");
1459         } }
1460     | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
1461       { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
1462                                     AntlrInput::tokenToUnsigned($sb),
1463                                     +INFINITY)); }
1464     | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
1465       { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
1466                                     AntlrInput::tokenToUnsigned($sb),
1467                                     -INFINITY)); }
1468     | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
1469       { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
1470                                     AntlrInput::tokenToUnsigned($sb),
1471                                     NAN)); }
1472     | FP_PZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
1473       { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
1474                                     AntlrInput::tokenToUnsigned($sb),
1475                                     +0.0)); }
1476     | FP_NZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
1477       { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
1478                                     AntlrInput::tokenToUnsigned($sb),
1479                                     -0.0)); }
1480     | FP_TO_FP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
1481       { op = MK_CONST(FloatingPointToFPGeneric(AntlrInput::tokenToUnsigned($eb),
1482                                                AntlrInput::tokenToUnsigned($sb))); }
1483     | FP_TO_FPBV_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
1484       { op = MK_CONST(FloatingPointToFPIEEEBitVector(AntlrInput::tokenToUnsigned($eb),
1485                                                      AntlrInput::tokenToUnsigned($sb))); }
1486     | FP_TO_FPFP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
1487       { op = MK_CONST(FloatingPointToFPFloatingPoint(AntlrInput::tokenToUnsigned($eb),
1488                                                      AntlrInput::tokenToUnsigned($sb))); }
1489     | FP_TO_FPR_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
1490       { op = MK_CONST(FloatingPointToFPReal(AntlrInput::tokenToUnsigned($eb),
1491                                             AntlrInput::tokenToUnsigned($sb))); }
1492     | FP_TO_FPS_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
1493       { op = MK_CONST(FloatingPointToFPSignedBitVector(AntlrInput::tokenToUnsigned($eb),
1494                                                        AntlrInput::tokenToUnsigned($sb))); }
1495     | FP_TO_FPU_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
1496       { op = MK_CONST(FloatingPointToFPUnsignedBitVector(AntlrInput::tokenToUnsigned($eb),
1497                                                          AntlrInput::tokenToUnsigned($sb))); }
1498     | FP_TO_UBV_TOK m=INTEGER_LITERAL
1499       { op = MK_CONST(FloatingPointToUBV(AntlrInput::tokenToUnsigned($m))); }
1500     | FP_TO_SBV_TOK m=INTEGER_LITERAL
1501       { op = MK_CONST(FloatingPointToSBV(AntlrInput::tokenToUnsigned($m))); }
1502     | badIndexedFunctionName
1503     )
1504     RPAREN_TOK
1505   ;
1506
1507 /**
1508  * Matches an erroneous indexed function name (and args) for better
1509  * error reporting.
1510  */
1511 badIndexedFunctionName
1512 @declarations {
1513   std::string name;
1514 }
1515   : id=(SIMPLE_SYMBOL | QUOTED_SYMBOL | UNTERMINATED_QUOTED_SYMBOL)
1516       { PARSER_STATE->parseError(std::string("Unknown indexed function `") + AntlrInput::tokenText($id) + "'"); }
1517   ;
1518
1519 /**
1520  * Matches a sequence of terms and puts them into the formulas
1521  * vector.
1522  * @param formulas the vector to fill with terms
1523  * @param expr an Expr reference for the elements of the sequence
1524  */
1525 /* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
1526  * time through this rule. */
1527 termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
1528 @declarations {
1529   Expr expr2;
1530 }
1531   : ( term[expr, expr2] { formulas.push_back(expr); } )+
1532   ;
1533
1534 /**
1535  * Matches a string, and strips off the quotes.
1536  */
1537 str[std::string& s, bool fsmtlib]
1538   : STRING_LITERAL_2_0
1539     { s = AntlrInput::tokenText($STRING_LITERAL_2_0);
1540       /* strip off the quotes */
1541       s = s.substr(1, s.size() - 2);
1542       for(size_t i=0; i<s.size(); i++) {
1543         if((unsigned)s[i] > 127 && !isprint(s[i])) {
1544           PARSER_STATE->parseError("Extended/unprintable characters are not part of SMT-LIB, and they must be encoded as escape sequences");
1545         }
1546       }
1547       if(fsmtlib) {
1548         /* handle SMT-LIB standard escapes '\\' and '\"' */
1549         char* p_orig = strdup(s.c_str());
1550         char *p = p_orig, *q = p_orig;
1551         while(*q != '\0') {
1552           if(*q == '\\') {
1553             ++q;
1554             if(*q == '\\' || *q == '"') {
1555               *p++ = *q++;
1556             } else {
1557               assert(*q != '\0');
1558               *p++ = '\\';
1559               *p++ = *q++;
1560             }
1561           } else {
1562             *p++ = *q++;
1563           }
1564         }
1565         *p = '\0';
1566         s = p_orig;
1567         free(p_orig);
1568       }
1569     }
1570   | STRING_LITERAL_2_5
1571     { s = AntlrInput::tokenText($STRING_LITERAL_2_5);
1572       /* strip off the quotes */
1573       s = s.substr(1, s.size() - 2);
1574       for(size_t i=0; i<s.size(); i++) {
1575         if((unsigned)s[i] > 127 && !isprint(s[i])) {
1576           PARSER_STATE->parseError("Extended/unprintable characters are not part of SMT-LIB, and they must be encoded as escape sequences");
1577         }
1578       }
1579       // In the 2.5 version, always handle escapes (regardless of fsmtlib flag).
1580       char* p_orig = strdup(s.c_str());
1581       char *p = p_orig, *q = p_orig;
1582       while(*q != '\0') {
1583         if(*q == '"') {
1584           ++q;
1585           assert(*q == '"');
1586         }
1587         *p++ = *q++;
1588       }
1589       *p = '\0';
1590       s = p_orig;
1591       free(p_orig);
1592     }
1593   ;
1594
1595 /**
1596  * Matches a builtin operator symbol and sets kind to its associated Expr kind.
1597  */
1598 builtinOp[CVC4::Kind& kind]
1599 @init {
1600   Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
1601 }
1602   : NOT_TOK      { $kind = CVC4::kind::NOT;     }
1603   | IMPLIES_TOK  { $kind = CVC4::kind::IMPLIES; }
1604   | AND_TOK      { $kind = CVC4::kind::AND;     }
1605   | OR_TOK       { $kind = CVC4::kind::OR;      }
1606   | XOR_TOK      { $kind = CVC4::kind::XOR;     }
1607   | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
1608   | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
1609   | ITE_TOK      { $kind = CVC4::kind::ITE; }
1610   | GREATER_THAN_TOK
1611                  { $kind = CVC4::kind::GT; }
1612   | GREATER_THAN_EQUAL_TOK
1613                  { $kind = CVC4::kind::GEQ; }
1614   | LESS_THAN_EQUAL_TOK
1615                  { $kind = CVC4::kind::LEQ; }
1616   | LESS_THAN_TOK
1617                  { $kind = CVC4::kind::LT; }
1618   | PLUS_TOK     { $kind = CVC4::kind::PLUS; }
1619   | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
1620   | STAR_TOK     { $kind = CVC4::kind::MULT; }
1621   | DIV_TOK      { $kind = CVC4::kind::DIVISION; }
1622   | INTS_DIV_TOK      { $kind = CVC4::kind::INTS_DIVISION; }
1623   | INTS_MOD_TOK      { $kind = CVC4::kind::INTS_MODULUS; }
1624   | ABS_TOK      { $kind = CVC4::kind::ABS; }
1625   | IS_INT_TOK   { $kind = CVC4::kind::IS_INTEGER; }
1626   | TO_INT_TOK   { $kind = CVC4::kind::TO_INTEGER; }
1627   | TO_REAL_TOK  { $kind = CVC4::kind::TO_REAL; }
1628
1629   | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
1630   | STORE_TOK    { $kind = CVC4::kind::STORE; }
1631
1632   | CONCAT_TOK   { $kind = CVC4::kind::BITVECTOR_CONCAT; }
1633   | BVNOT_TOK   { $kind = CVC4::kind::BITVECTOR_NOT; }
1634   | BVAND_TOK   { $kind = CVC4::kind::BITVECTOR_AND; }
1635   | BVOR_TOK   { $kind = CVC4::kind::BITVECTOR_OR; }
1636   | BVNEG_TOK   { $kind = CVC4::kind::BITVECTOR_NEG; }
1637   | BVADD_TOK   { $kind = CVC4::kind::BITVECTOR_PLUS; }
1638   | BVMUL_TOK   { $kind = CVC4::kind::BITVECTOR_MULT; }
1639   | BVUDIV_TOK   { $kind = CVC4::kind::BITVECTOR_UDIV; }
1640   | BVUREM_TOK   { $kind = CVC4::kind::BITVECTOR_UREM; }
1641   | BVSHL_TOK     { $kind = CVC4::kind::BITVECTOR_SHL; }
1642   | BVLSHR_TOK     { $kind = CVC4::kind::BITVECTOR_LSHR; }
1643   | BVULT_TOK     { $kind = CVC4::kind::BITVECTOR_ULT; }
1644   | BVNAND_TOK     { $kind = CVC4::kind::BITVECTOR_NAND; }
1645   | BVNOR_TOK     { $kind = CVC4::kind::BITVECTOR_NOR; }
1646   | BVXOR_TOK     { $kind = CVC4::kind::BITVECTOR_XOR; }
1647   | BVXNOR_TOK     { $kind = CVC4::kind::BITVECTOR_XNOR; }
1648   | BVCOMP_TOK     { $kind = CVC4::kind::BITVECTOR_COMP; }
1649   | BVSUB_TOK     { $kind = CVC4::kind::BITVECTOR_SUB; }
1650   | BVSDIV_TOK     { $kind = CVC4::kind::BITVECTOR_SDIV; }
1651   | BVSREM_TOK     { $kind = CVC4::kind::BITVECTOR_SREM; }
1652   | BVSMOD_TOK     { $kind = CVC4::kind::BITVECTOR_SMOD; }
1653   | BVASHR_TOK     { $kind = CVC4::kind::BITVECTOR_ASHR; }
1654   | BVULE_TOK     { $kind = CVC4::kind::BITVECTOR_ULE; }
1655   | BVUGT_TOK     { $kind = CVC4::kind::BITVECTOR_UGT; }
1656   | BVUGE_TOK     { $kind = CVC4::kind::BITVECTOR_UGE; }
1657   | BVSLT_TOK     { $kind = CVC4::kind::BITVECTOR_SLT; }
1658   | BVSLE_TOK     { $kind = CVC4::kind::BITVECTOR_SLE; }
1659   | BVSGT_TOK     { $kind = CVC4::kind::BITVECTOR_SGT; }
1660   | BVSGE_TOK     { $kind = CVC4::kind::BITVECTOR_SGE; }
1661
1662   | BV2NAT_TOK     { $kind = CVC4::kind::BITVECTOR_TO_NAT;
1663                      if(PARSER_STATE->strictModeEnabled()) {
1664                        PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode");
1665                      } }
1666   | STRCON_TOK     { $kind = CVC4::kind::STRING_CONCAT; }
1667   | STRLEN_TOK     { $kind = CVC4::kind::STRING_LENGTH; }
1668   | STRSUB_TOK     { $kind = CVC4::kind::STRING_SUBSTR; }
1669   | STRCTN_TOK     { $kind = CVC4::kind::STRING_STRCTN; }
1670   | STRCAT_TOK     { $kind = CVC4::kind::STRING_CHARAT; }
1671   | STRIDOF_TOK    { $kind = CVC4::kind::STRING_STRIDOF; }
1672   | STRREPL_TOK    { $kind = CVC4::kind::STRING_STRREPL; }
1673   | STRPREF_TOK    { $kind = CVC4::kind::STRING_PREFIX; }
1674   | STRSUFF_TOK    { $kind = CVC4::kind::STRING_SUFFIX; }
1675   | STRITOS_TOK    { $kind = CVC4::kind::STRING_ITOS; }
1676   | STRSTOI_TOK    { $kind = CVC4::kind::STRING_STOI; }
1677   | STRU16TOS_TOK    { $kind = CVC4::kind::STRING_U16TOS; }
1678   | STRSTOU16_TOK    { $kind = CVC4::kind::STRING_STOU16; }
1679   | STRU32TOS_TOK    { $kind = CVC4::kind::STRING_U32TOS; }
1680   | STRSTOU32_TOK    { $kind = CVC4::kind::STRING_STOU32; }
1681   | STRINRE_TOK    { $kind = CVC4::kind::STRING_IN_REGEXP; }
1682   | STRTORE_TOK    { $kind = CVC4::kind::STRING_TO_REGEXP; }
1683   | RECON_TOK      { $kind = CVC4::kind::REGEXP_CONCAT; }
1684   | REUNION_TOK    { $kind = CVC4::kind::REGEXP_UNION; }
1685   | REINTER_TOK    { $kind = CVC4::kind::REGEXP_INTER; }
1686   | RESTAR_TOK     { $kind = CVC4::kind::REGEXP_STAR; }
1687   | REPLUS_TOK     { $kind = CVC4::kind::REGEXP_PLUS; }
1688   | REOPT_TOK      { $kind = CVC4::kind::REGEXP_OPT; }
1689   | RERANGE_TOK    { $kind = CVC4::kind::REGEXP_RANGE; }
1690   | RELOOP_TOK    { $kind = CVC4::kind::REGEXP_LOOP; }
1691
1692   | DTSIZE_TOK     { $kind = CVC4::kind::DT_SIZE; }
1693
1694   | FMFCARD_TOK    { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; }
1695
1696   | INST_CLOSURE_TOK  { $kind = CVC4::kind::INST_CLOSURE; }
1697
1698   | FP_TOK        { $kind = CVC4::kind::FLOATINGPOINT_FP; }
1699   | FP_EQ_TOK     { $kind = CVC4::kind::FLOATINGPOINT_EQ; }
1700   | FP_ABS_TOK    { $kind = CVC4::kind::FLOATINGPOINT_ABS; }
1701   | FP_NEG_TOK    { $kind = CVC4::kind::FLOATINGPOINT_NEG; }
1702   | FP_PLUS_TOK   { $kind = CVC4::kind::FLOATINGPOINT_PLUS; }
1703   | FP_SUB_TOK    { $kind = CVC4::kind::FLOATINGPOINT_SUB; }
1704   | FP_MUL_TOK    { $kind = CVC4::kind::FLOATINGPOINT_MULT; }
1705   | FP_DIV_TOK    { $kind = CVC4::kind::FLOATINGPOINT_DIV; }
1706   | FP_FMA_TOK    { $kind = CVC4::kind::FLOATINGPOINT_FMA; }
1707   | FP_SQRT_TOK   { $kind = CVC4::kind::FLOATINGPOINT_SQRT; }
1708   | FP_REM_TOK    { $kind = CVC4::kind::FLOATINGPOINT_REM; }
1709   | FP_RTI_TOK    { $kind = CVC4::kind::FLOATINGPOINT_RTI; }
1710   | FP_MIN_TOK    { $kind = CVC4::kind::FLOATINGPOINT_MIN; }
1711   | FP_MAX_TOK    { $kind = CVC4::kind::FLOATINGPOINT_MAX; }
1712   | FP_LEQ_TOK    { $kind = CVC4::kind::FLOATINGPOINT_LEQ; }
1713   | FP_LT_TOK     { $kind = CVC4::kind::FLOATINGPOINT_LT; }
1714   | FP_GEQ_TOK    { $kind = CVC4::kind::FLOATINGPOINT_GEQ; }
1715   | FP_GT_TOK     { $kind = CVC4::kind::FLOATINGPOINT_GT; }
1716   | FP_ISN_TOK    { $kind = CVC4::kind::FLOATINGPOINT_ISN; }
1717   | FP_ISSN_TOK   { $kind = CVC4::kind::FLOATINGPOINT_ISSN; }
1718   | FP_ISZ_TOK    { $kind = CVC4::kind::FLOATINGPOINT_ISZ; }
1719   | FP_ISINF_TOK  { $kind = CVC4::kind::FLOATINGPOINT_ISINF; }
1720   | FP_ISNAN_TOK  { $kind = CVC4::kind::FLOATINGPOINT_ISNAN; }
1721   | FP_ISNEG_TOK  { $kind = CVC4::kind::FLOATINGPOINT_ISNEG; }
1722   | FP_ISPOS_TOK  { $kind = CVC4::kind::FLOATINGPOINT_ISPOS; }
1723   | FP_TO_REAL_TOK {$kind = CVC4::kind::FLOATINGPOINT_TO_REAL; }
1724   // NOTE: Theory operators go here
1725   ;
1726
1727 quantOp[CVC4::Kind& kind]
1728 @init {
1729   Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
1730 }
1731   : EXISTS_TOK    { $kind = CVC4::kind::EXISTS; }
1732   | FORALL_TOK    { $kind = CVC4::kind::FORALL; }
1733   ;
1734
1735 /**
1736  * Matches a (possibly undeclared) function symbol (returning the string)
1737  * @param check what kind of check to do with the symbol
1738  */
1739 functionName[std::string& name, CVC4::parser::DeclarationCheck check]
1740   : symbol[name,check,SYM_VARIABLE]
1741   ;
1742
1743 /**
1744  * Matches a sequence of sort symbols and fills them into the given
1745  * vector.
1746  */
1747 sortList[std::vector<CVC4::Type>& sorts]
1748 @declarations {
1749   Type t;
1750 }
1751   : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
1752   ;
1753
1754 nonemptySortList[std::vector<CVC4::Type>& sorts]
1755 @declarations {
1756   Type t;
1757 }
1758   : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+
1759   ;
1760
1761 /**
1762  * Matches a sequence of (variable,sort) symbol pairs and fills them
1763  * into the given vector.
1764  */
1765 sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars]
1766 @declarations {
1767   std::string name;
1768   Type t;
1769 }
1770   : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] RPAREN_TOK
1771       { sortedVars.push_back(make_pair(name, t)); }
1772     )*
1773   ;
1774
1775 /**
1776  * Matches the sort symbol, which can be an arbitrary symbol.
1777  * @param check the check to perform on the name
1778  */
1779 sortName[std::string& name, CVC4::parser::DeclarationCheck check]
1780   : symbol[name,check,SYM_SORT]
1781   ;
1782
1783 sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
1784 @declarations {
1785   std::string name;
1786   std::vector<CVC4::Type> args;
1787   std::vector<uint64_t> numerals;
1788 }
1789   : sortName[name,CHECK_NONE]
1790     {
1791       if( check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT) ) {
1792         t = PARSER_STATE->getSort(name);
1793       } else {
1794         t = PARSER_STATE->mkUnresolvedType(name);
1795       }
1796     }
1797   | LPAREN_TOK INDEX_TOK symbol[name,CHECK_NONE,SYM_SORT] nonemptyNumeralList[numerals] RPAREN_TOK
1798     {
1799       if( name == "BitVec" ) {
1800         if( numerals.size() != 1 ) {
1801           PARSER_STATE->parseError("Illegal bitvector type.");
1802         }
1803         if(numerals.front() == 0) {
1804           PARSER_STATE->parseError("Illegal bitvector size: 0");
1805         }
1806         t = EXPR_MANAGER->mkBitVectorType(numerals.front());
1807       } else if ( name == "FloatingPoint" ) {
1808         if( numerals.size() != 2 ) {
1809           PARSER_STATE->parseError("Illegal floating-point type.");
1810         }
1811         if(!validExponentSize(numerals[0])) {
1812           PARSER_STATE->parseError("Illegal floating-point exponent size");
1813         }
1814         if(!validSignificandSize(numerals[1])) {
1815           PARSER_STATE->parseError("Illegal floating-point significand size");
1816         }
1817         t = EXPR_MANAGER->mkFloatingPointType(numerals[0],numerals[1]);
1818       } else {
1819         std::stringstream ss;
1820         ss << "unknown indexed symbol `" << name << "'";
1821         PARSER_STATE->parseError(ss.str());
1822       }
1823     }
1824   | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
1825     {
1826       if(args.empty()) {
1827         PARSER_STATE->parseError("Extra parentheses around sort name not permitted in SMT-LIB");
1828       } else if(name == "Array" &&
1829          PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) ) {
1830         if(args.size() != 2) {
1831           PARSER_STATE->parseError("Illegal array type.");
1832         }
1833         t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
1834       } else if(name == "Set" &&
1835                 PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) ) {
1836         if(args.size() != 1) {
1837           PARSER_STATE->parseError("Illegal set type.");
1838         }
1839         t = EXPR_MANAGER->mkSetType( args[0] );
1840       } else if(check == CHECK_DECLARED ||
1841                 PARSER_STATE->isDeclared(name, SYM_SORT)) {
1842         t = PARSER_STATE->getSort(name, args);
1843       } else {
1844         // make unresolved type
1845         if(args.empty()) {
1846           t = PARSER_STATE->mkUnresolvedType(name);
1847           Debug("parser-param") << "param: make unres type " << name << std::endl;
1848         } else {
1849           t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args);
1850           t = SortConstructorType(t).instantiate( args );
1851           Debug("parser-param") << "param: make unres param type " << name << " " << args.size() << " "
1852                                 << PARSER_STATE->getArity( name ) << std::endl;
1853         }
1854       }
1855     }
1856   ;
1857
1858 /**
1859  * Matches a list of symbols, with check and type arguments as for the
1860  * symbol[] rule below.
1861  */
1862 symbolList[std::vector<std::string>& names,
1863            CVC4::parser::DeclarationCheck check,
1864            CVC4::parser::SymbolType type]
1865 @declarations {
1866   std::string id;
1867 }
1868   : ( symbol[id,check,type] { names.push_back(id); } )*
1869   ;
1870
1871 /**
1872  * Matches an symbol and sets the string reference parameter id.
1873  * @param id string to hold the symbol
1874  * @param check what kinds of check to do on the symbol
1875  * @param type the intended namespace for the symbol
1876  */
1877 symbol[std::string& id,
1878        CVC4::parser::DeclarationCheck check,
1879        CVC4::parser::SymbolType type]
1880   : SIMPLE_SYMBOL
1881     { id = AntlrInput::tokenText($SIMPLE_SYMBOL);
1882       if(!PARSER_STATE->isAbstractValue(id)) {
1883         // if an abstract value, SmtEngine handles declaration
1884         PARSER_STATE->checkDeclaration(id, check, type);
1885       }
1886     }
1887   | 'repeat'
1888     { id = "repeat";
1889       PARSER_STATE->checkDeclaration(id, check, type);
1890     }
1891   | QUOTED_SYMBOL
1892     { id = AntlrInput::tokenText($QUOTED_SYMBOL);
1893       /* strip off the quotes */
1894       id = id.substr(1, id.size() - 2);
1895       if(!PARSER_STATE->isAbstractValue(id)) {
1896         // if an abstract value, SmtEngine handles declaration
1897         PARSER_STATE->checkDeclaration(id, check, type);
1898       }
1899     }
1900   | UNTERMINATED_QUOTED_SYMBOL
1901     ( EOF
1902       { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); }
1903     | '\\'
1904       { PARSER_STATE->unexpectedEOF("backslash not permitted in |quoted| symbol"); }
1905     )
1906   ;
1907
1908 /**
1909  * Matches a nonempty list of numerals.
1910  * @param numerals the (empty) vector to house the numerals.
1911  */
1912 nonemptyNumeralList[std::vector<uint64_t>& numerals]
1913   : ( INTEGER_LITERAL
1914       { numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
1915     )+
1916   ;
1917
1918 /**
1919  * Parses a datatype definition
1920  */
1921 datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4::Type >& params]
1922 @init {
1923   std::string id;
1924 }
1925     /* This really needs to be CHECK_NONE, or mutually-recursive
1926      * datatypes won't work, because this type will already be
1927      * "defined" as an unresolved type; don't worry, we check
1928      * below. */
1929   : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); }
1930    /* ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
1931         t = PARSER_STATE->mkSort(id2);
1932         params.push_back( t );
1933       }
1934       ( symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
1935         t = PARSER_STATE->mkSort(id2);
1936         params.push_back( t ); }
1937       )* ']'
1938     )?*/ //AJR: this isn't necessary if we use z3's style
1939     { datatypes.push_back(Datatype(id,params,isCo));
1940       if(!PARSER_STATE->isUnresolvedType(id)) {
1941         // if not unresolved, must be undeclared
1942         PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
1943       }
1944     }
1945     ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+
1946     { PARSER_STATE->popScope(); }
1947   ;
1948
1949 /**
1950  * Parses a constructor defintion for type
1951  */
1952 constructorDef[CVC4::Datatype& type]
1953 @init {
1954   std::string id;
1955   CVC4::DatatypeConstructor* ctor = NULL;
1956 }
1957   : symbol[id,CHECK_UNDECLARED,SYM_SORT]
1958     { // make the tester
1959       std::string testerId("is-");
1960       testerId.append(id);
1961       PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
1962       ctor = new CVC4::DatatypeConstructor(id, testerId);
1963     }
1964     ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
1965     { // make the constructor
1966       type.addConstructor(*ctor);
1967       Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
1968       delete ctor;
1969     }
1970   ;
1971
1972 selector[CVC4::DatatypeConstructor& ctor]
1973 @init {
1974   std::string id;
1975   Type t, t2;
1976 }
1977   : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t,CHECK_NONE]
1978     { ctor.addArg(id, t);
1979       Debug("parser-idt") << "selector: " << id.c_str()
1980                           << " of type " << t << std::endl;
1981     }
1982   ;
1983
1984 // Base SMT-LIB tokens
1985 ASSERT_TOK : 'assert';
1986 CHECKSAT_TOK : 'check-sat';
1987 DECLARE_FUN_TOK : 'declare-fun';
1988 DECLARE_SORT_TOK : 'declare-sort';
1989 DEFINE_FUN_TOK : 'define-fun';
1990 DEFINE_FUN_REC_TOK : 'define-fun-rec';
1991 DEFINE_SORT_TOK : 'define-sort';
1992 GET_VALUE_TOK : 'get-value';
1993 GET_ASSIGNMENT_TOK : 'get-assignment';
1994 GET_ASSERTIONS_TOK : 'get-assertions';
1995 GET_PROOF_TOK : 'get-proof';
1996 GET_UNSAT_CORE_TOK : 'get-unsat-core';
1997 EXIT_TOK : 'exit';
1998 RESET_TOK : { PARSER_STATE->v2_5() }? 'reset';
1999 RESET_ASSERTIONS_TOK : 'reset-assertions';
2000 ITE_TOK : 'ite';
2001 LET_TOK : 'let';
2002 ATTRIBUTE_TOK : '!';
2003 LPAREN_TOK : '(';
2004 RPAREN_TOK : ')';
2005 INDEX_TOK : '_';
2006 SET_LOGIC_TOK : 'set-logic';
2007 SET_INFO_TOK : 'set-info';
2008 META_INFO_TOK : 'meta-info';
2009 GET_INFO_TOK : 'get-info';
2010 SET_OPTION_TOK : 'set-option';
2011 GET_OPTION_TOK : 'get-option';
2012 PUSH_TOK : 'push';
2013 POP_TOK : 'pop';
2014 AS_TOK : 'as';
2015 CONST_TOK : 'const';
2016
2017 // extended commands
2018 DECLARE_DATATYPES_TOK : 'declare-datatypes';
2019 DECLARE_CODATATYPES_TOK : 'declare-codatatypes';
2020 GET_MODEL_TOK : 'get-model';
2021 ECHO_TOK : 'echo';
2022 REWRITE_RULE_TOK : 'assert-rewrite';
2023 REDUCTION_RULE_TOK : 'assert-reduction';
2024 PROPAGATION_RULE_TOK : 'assert-propagation';
2025 DECLARE_SORTS_TOK : 'declare-sorts';
2026 DECLARE_FUNS_TOK : 'declare-funs';
2027 DECLARE_PREDS_TOK : 'declare-preds';
2028 DEFINE_TOK : 'define';
2029 DECLARE_CONST_TOK : 'declare-const';
2030 DEFINE_CONST_TOK : 'define-const';
2031 SIMPLIFY_TOK : 'simplify';
2032 INCLUDE_TOK : 'include';
2033
2034 // attributes
2035 ATTRIBUTE_PATTERN_TOK : ':pattern';
2036 ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern';
2037 ATTRIBUTE_NAMED_TOK : ':named';
2038 ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level';
2039 ATTRIBUTE_RR_PRIORITY : ':rr-priority';
2040
2041 // operators (NOTE: theory symbols go here)
2042 AMPERSAND_TOK     : '&';
2043 AND_TOK           : 'and';
2044 AT_TOK            : '@';
2045 DISTINCT_TOK      : 'distinct';
2046 DIV_TOK           : '/';
2047 EQUAL_TOK         : '=';
2048 EXISTS_TOK        : 'exists';
2049 FORALL_TOK        : 'forall';
2050 GREATER_THAN_TOK  : '>';
2051 GREATER_THAN_EQUAL_TOK  : '>=';
2052 IMPLIES_TOK       : '=>';
2053 IS_INT_TOK        : 'is_int';
2054 LESS_THAN_TOK     : '<';
2055 LESS_THAN_EQUAL_TOK     : '<=';
2056 MINUS_TOK         : '-';
2057 NOT_TOK           : 'not';
2058 OR_TOK            : 'or';
2059 // PERCENT_TOK       : '%';
2060 PLUS_TOK          : '+';
2061 POUND_TOK         : '#';
2062 SELECT_TOK        : 'select';
2063 STAR_TOK          : '*';
2064 STORE_TOK         : 'store';
2065 // TILDE_TOK         : '~';
2066 TO_INT_TOK        : 'to_int';
2067 TO_REAL_TOK       : 'to_real';
2068 XOR_TOK           : 'xor';
2069
2070 INTS_DIV_TOK : 'div';
2071 INTS_MOD_TOK : 'mod';
2072 ABS_TOK : 'abs';
2073
2074 DIVISIBLE_TOK : 'divisible';
2075
2076 CONCAT_TOK : 'concat';
2077 BVNOT_TOK : 'bvnot';
2078 BVAND_TOK : 'bvand';
2079 BVOR_TOK : 'bvor';
2080 BVNEG_TOK : 'bvneg';
2081 BVADD_TOK : 'bvadd';
2082 BVMUL_TOK : 'bvmul';
2083 BVUDIV_TOK : 'bvudiv';
2084 BVUREM_TOK : 'bvurem';
2085 BVSHL_TOK : 'bvshl';
2086 BVLSHR_TOK : 'bvlshr';
2087 BVULT_TOK : 'bvult';
2088 BVNAND_TOK : 'bvnand';
2089 BVNOR_TOK : 'bvnor';
2090 BVXOR_TOK : 'bvxor';
2091 BVXNOR_TOK : 'bvxnor';
2092 BVCOMP_TOK : 'bvcomp';
2093 BVSUB_TOK : 'bvsub';
2094 BVSDIV_TOK : 'bvsdiv';
2095 BVSREM_TOK : 'bvsrem';
2096 BVSMOD_TOK : 'bvsmod';
2097 BVASHR_TOK : 'bvashr';
2098 BVULE_TOK : 'bvule';
2099 BVUGT_TOK : 'bvugt';
2100 BVUGE_TOK : 'bvuge';
2101 BVSLT_TOK : 'bvslt';
2102 BVSLE_TOK : 'bvsle';
2103 BVSGT_TOK : 'bvsgt';
2104 BVSGE_TOK : 'bvsge';
2105 BV2NAT_TOK : 'bv2nat';
2106 INT2BV_TOK : 'int2bv';
2107
2108 STRCON_TOK : 'str.++';
2109 STRLEN_TOK : 'str.len';
2110 STRSUB_TOK : 'str.substr' ;
2111 STRCTN_TOK : 'str.contains' ;
2112 STRCAT_TOK : 'str.at' ;
2113 STRIDOF_TOK : 'str.indexof' ;
2114 STRREPL_TOK : 'str.replace' ;
2115 STRPREF_TOK : 'str.prefixof' ;
2116 STRSUFF_TOK : 'str.suffixof' ;
2117 STRITOS_TOK : 'int.to.str' ;
2118 STRSTOI_TOK : 'str.to.int' ;
2119 STRU16TOS_TOK : 'u16.to.str' ;
2120 STRSTOU16_TOK : 'str.to.u16' ;
2121 STRU32TOS_TOK : 'u32.to.str' ;
2122 STRSTOU32_TOK : 'str.to.u32' ;
2123 STRINRE_TOK : 'str.in.re';
2124 STRTORE_TOK : 'str.to.re';
2125 RECON_TOK : 're.++';
2126 REUNION_TOK : 're.union';
2127 REINTER_TOK : 're.inter';
2128 RESTAR_TOK : 're.*';
2129 REPLUS_TOK : 're.+';
2130 REOPT_TOK : 're.opt';
2131 RERANGE_TOK : 're.range';
2132 RELOOP_TOK : 're.loop';
2133 RENOSTR_TOK : 're.nostr';
2134 REALLCHAR_TOK : 're.allchar';
2135
2136 DTSIZE_TOK : 'dt.size';
2137
2138 FMFCARD_TOK : 'fmf.card';
2139
2140 INST_CLOSURE_TOK : 'inst-closure';
2141
2142 EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
2143 // Other set theory operators are not
2144 // tokenized and handled directly when
2145 // processing a term
2146
2147 FP_TOK : 'fp';
2148 FP_PINF_TOK : '+oo';
2149 FP_NINF_TOK : '-oo';
2150 FP_PZERO_TOK : '+zero';
2151 FP_NZERO_TOK : '-zero';
2152 FP_NAN_TOK : 'NaN';
2153 FP_EQ_TOK : 'fp.eq';
2154 FP_ABS_TOK : 'fp.abs';
2155 FP_NEG_TOK : 'fp.neg';
2156 FP_PLUS_TOK : 'fp.add';
2157 FP_SUB_TOK : 'fp.sub';
2158 FP_MUL_TOK : 'fp.mul';
2159 FP_DIV_TOK : 'fp.div';
2160 FP_FMA_TOK : 'fp.fma';
2161 FP_SQRT_TOK : 'fp.sqrt';
2162 FP_REM_TOK : 'fp.rem';
2163 FP_RTI_TOK : 'fp.roundToIntegral';
2164 FP_MIN_TOK : 'fp.min';
2165 FP_MAX_TOK : 'fp.max';
2166 FP_LEQ_TOK : 'fp.leq';
2167 FP_LT_TOK : 'fp.lt';
2168 FP_GEQ_TOK : 'fp.geq';
2169 FP_GT_TOK : 'fp.gt';
2170 FP_ISN_TOK : 'fp.isNormal';
2171 FP_ISSN_TOK : 'fp.isSubnormal';
2172 FP_ISZ_TOK : 'fp.isZero';
2173 FP_ISINF_TOK : 'fp.isInfinite';
2174 FP_ISNAN_TOK : 'fp.isNaN';
2175 FP_ISNEG_TOK : 'fp.isNegative';
2176 FP_ISPOS_TOK : 'fp.isPositive';
2177 FP_TO_FP_TOK : 'to_fp';
2178 FP_TO_FPBV_TOK : 'to_fp_bv';
2179 FP_TO_FPFP_TOK : 'to_fp_fp';
2180 FP_TO_FPR_TOK : 'to_fp_real';
2181 FP_TO_FPS_TOK : 'to_fp_signed';
2182 FP_TO_FPU_TOK : 'to_fp_unsigned';
2183 FP_TO_UBV_TOK : 'fp.to_ubv';
2184 FP_TO_SBV_TOK : 'fp.to_sbv';
2185 FP_TO_REAL_TOK : 'fp.to_real';
2186 FP_RNE_TOK : 'RNE';
2187 FP_RNA_TOK : 'RNA';
2188 FP_RTP_TOK : 'RTP';
2189 FP_RTN_TOK : 'RTN';
2190 FP_RTZ_TOK : 'RTZ';
2191 FP_RNE_FULL_TOK : 'roundNearestTiesToEven';
2192 FP_RNA_FULL_TOK : 'roundNearestTiesToAway';
2193 FP_RTP_FULL_TOK : 'roundTowardPositive';
2194 FP_RTN_FULL_TOK : 'roundTowardNegative';
2195 FP_RTZ_FULL_TOK : 'roundTowardZero';
2196
2197 /**
2198  * A sequence of printable ASCII characters (except backslash) that starts
2199  * and ends with | and does not otherwise contain |.
2200  *
2201  * You shouldn't generally use this in parser rules, as the |quoting|
2202  * will be part of the token text.  Use the symbol[] parser rule instead.
2203  */
2204 QUOTED_SYMBOL
2205   : '|' ~('|' | '\\')* '|'
2206   ;
2207 UNTERMINATED_QUOTED_SYMBOL
2208   : '|' ~('|' | '\\')*
2209   ;
2210
2211 /**
2212  * Matches a keyword from the input. A keyword is a simple symbol prefixed
2213  * with a colon.
2214  */
2215 KEYWORD
2216   : ':' (ALPHA | DIGIT | SYMBOL_CHAR)+
2217   ;
2218
2219 /**
2220  * Matches a "simple" symbol: a non-empty sequence of letters, digits and
2221  * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
2222  * digit, and is not the special reserved symbols '!' or '_'.
2223  */
2224 SIMPLE_SYMBOL
2225   : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)+
2226   | ALPHA
2227   | SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
2228   ;
2229
2230 /**
2231  * Matches and skips whitespace in the input.
2232  */
2233 WHITESPACE
2234   : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }
2235   ;
2236
2237 /**
2238  * Matches an integer constant from the input (non-empty sequence of
2239  * digits, with no leading zeroes).
2240  */
2241 INTEGER_LITERAL
2242   : NUMERAL
2243   ;
2244
2245 /**
2246  * Match an integer constant. In non-strict mode, this is any sequence
2247  * of digits. In strict mode, non-zero integers can't have leading
2248  * zeroes.
2249  */
2250 fragment NUMERAL
2251 @init {
2252   char *start = (char*) GETCHARINDEX();
2253 }
2254   : DIGIT+
2255     { Debug("parser-extra") << "NUMERAL: "
2256        << (uintptr_t)start << ".." << GETCHARINDEX()
2257        << " strict? " << (bool)(PARSER_STATE->strictModeEnabled())
2258        << " ^0? " << (bool)(*start == '0')
2259        << " len>1? " << (bool)(start < (char*)(GETCHARINDEX() - 1))
2260        << std::endl; }
2261     { !PARSER_STATE->strictModeEnabled() ||
2262       *start != '0' ||
2263       start == (char*)(GETCHARINDEX() - 1) }?
2264   ;
2265
2266 /**
2267  * Matches a decimal constant from the input.
2268  */
2269 DECIMAL_LITERAL
2270   : NUMERAL '.' DIGIT+
2271   ;
2272
2273 /**
2274  * Matches a hexadecimal constant.
2275  */
2276 HEX_LITERAL
2277   : '#x' HEX_DIGIT+
2278   ;
2279
2280 /**
2281  * Matches a binary constant.
2282  */
2283 BINARY_LITERAL
2284   : '#b' ('0' | '1')+
2285   ;
2286
2287 /**
2288  * Matches a double-quoted string literal from SMT-LIB 2.0.
2289  * Escaping is supported, and * escape character '\' has to be escaped.
2290  *
2291  * You shouldn't generally use this in parser rules, as the quotes
2292  * will be part of the token text.  Use the str[] parser rule instead.
2293  */
2294 STRING_LITERAL_2_0
2295   : { PARSER_STATE->v2_0() }?=>
2296     '"' ('\\' . | ~('\\' | '"'))* '"'
2297   ;
2298
2299 /**
2300  * Matches a double-quoted string literal from SMT-LIB 2.5.
2301  * You escape a double-quote inside the string with "", e.g.,
2302  * "This is a string literal with "" a single, embedded double quote."
2303  *
2304  * You shouldn't generally use this in parser rules, as the quotes
2305  * will be part of the token text.  Use the str[] parser rule instead.
2306  */
2307 STRING_LITERAL_2_5
2308   : { PARSER_STATE->v2_5() }?=>
2309     '"' (~('"') | '""')* '"'
2310   ;
2311
2312 /**
2313  * Matches the comments and ignores them
2314  */
2315 COMMENT
2316   : ';' (~('\n' | '\r'))* { SKIP(); }
2317   ;
2318
2319 /**
2320  * Matches any letter ('a'-'z' and 'A'-'Z').
2321  */
2322 fragment
2323 ALPHA
2324   : 'a'..'z'
2325   | 'A'..'Z'
2326   ;
2327
2328 /**
2329  * Matches the digits (0-9)
2330  */
2331 fragment DIGIT : '0'..'9';
2332
2333 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
2334
2335 /**
2336  * Matches the characters that may appear as a one-character "symbol"
2337  * (which excludes _ and !, which are reserved words in SMT-LIB).
2338  */
2339 fragment SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
2340   : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '.' | '$' | '~'
2341   | '&' | '^' | '<' | '>' | '@'
2342   ;
2343
2344 /**
2345  * Matches the characters that may appear in a "symbol" (i.e., an identifier)
2346  */
2347 fragment SYMBOL_CHAR
2348   : SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE | '_' | '!'
2349   ;