src/parser/smt2/Smt2.g

   1 /* *******************                                                        */
   2 /*! \file Smt2.g
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Andrew Reynolds, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing 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 the CVC4 project.
  35  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
  36  ** in the top-level source directory) and their institutional affiliations.
  37  ** All rights reserved.  See the file COPYING in the top-level source
  38  ** directory for licensing information.
  39  **/
  40 }/* @header */
  41
  42 @lexer::includes {
  43
  44 /** This suppresses warnings about the redefinition of token symbols between
  45   * different parsers. The redefinitions should be harmless as long as no
  46   * client: (a) #include's the lexer headers for two grammars AND (b) uses the
  47   * token symbol definitions.
  48   */
  49 #pragma GCC system_header
  50
  51 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
  52 /* This improves performance by ~10 percent on big inputs.
  53  * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
  54  * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
  55  * Otherwise, we have to let the lexer detect the encoding at runtime.
  56  */
  57 #  define ANTLR3_INLINE_INPUT_ASCII
  58 #  define ANTLR3_INLINE_INPUT_8BIT
  59 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
  60
  61 #include "parser/antlr_tracing.h"
  62
  63 }/* @lexer::includes */
  64
  65 @lexer::postinclude {
  66 #include <stdint.h>
  67
  68 #include "parser/smt2/smt2.h"
  69 #include "parser/antlr_input.h"
  70
  71 using namespace CVC4;
  72 using namespace CVC4::parser;
  73
  74 #undef PARSER_STATE
  75 #define PARSER_STATE ((Smt2*)LEXER->super)
  76 }/* @lexer::postinclude */
  77
  78 @parser::includes {
  79
  80 #include <memory>
  81
  82 #include "parser/parser.h"
  83 #include "parser/antlr_tracing.h"
  84 #include "smt/command.h"
  85
  86 namespace CVC4 {
  87   class Expr;
  88
  89   namespace parser {
  90     namespace smt2 {
  91       /**
  92        * Just exists to provide the uintptr_t constructor that ANTLR
  93        * requires.
  94        */
  95       struct myExpr : public CVC4::Expr {
  96         myExpr() : CVC4::Expr() {}
  97         myExpr(void*) : CVC4::Expr() {}
  98         myExpr(const Expr& e) : CVC4::Expr(e) {}
  99         myExpr(const myExpr& e) : CVC4::Expr(e) {}
 100       };/* struct myExpr */
 101     }/* CVC4::parser::smt2 namespace */
 102   }/* CVC4::parser namespace */
 103
 104   namespace api {
 105     class Term;
 106   }
 107 }/* CVC4 namespace */
 108
 109 }/* @parser::includes */
 110
 111 @parser::postinclude {
 112
 113 #include <set>
 114 #include <sstream>
 115 #include <string>
 116 #include <unordered_set>
 117 #include <vector>
 118
 119 #include "api/cvc4cpp.h"
 120 #include "base/output.h"
 121 #include "expr/expr.h"
 122 #include "expr/kind.h"
 123 #include "expr/type.h"
 124 #include "options/set_language.h"
 125 #include "parser/antlr_input.h"
 126 #include "parser/parser.h"
 127 #include "parser/smt2/smt2.h"
 128 #include "util/floatingpoint.h"
 129 #include "util/hash.h"
 130 #include "util/integer.h"
 131 #include "util/rational.h"
 132 // \todo Review the need for this header
 133 #include "math.h"
 134
 135 using namespace CVC4;
 136 using namespace CVC4::parser;
 137
 138 /* These need to be macros so they can refer to the PARSER macro, which
 139  * will be defined by ANTLR *after* this section. (If they were functions,
 140  * PARSER would be undefined.) */
 141 #undef PARSER_STATE
 142 #define PARSER_STATE ((Smt2*)PARSER->super)
 143 #undef EXPR_MANAGER
 144 #define EXPR_MANAGER PARSER_STATE->getExprManager()
 145 #undef MK_EXPR
 146 #define MK_EXPR EXPR_MANAGER->mkExpr
 147 #undef MK_CONST
 148 #define MK_CONST EXPR_MANAGER->mkConst
 149 #undef SOLVER
 150 #define SOLVER PARSER_STATE->getSolver()
 151 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
 152
 153 static bool isClosed(const Expr& e, std::set<Expr>& free, std::unordered_set<Expr, ExprHashFunction>& closedCache) {
 154   if(closedCache.find(e) != closedCache.end()) {
 155     return true;
 156   }
 157
 158   if(e.getKind() == kind::FORALL || e.getKind() == kind::EXISTS || e.getKind() == kind::LAMBDA) {
 159     isClosed(e[1], free, closedCache);
 160     for(Expr::const_iterator i = e[0].begin(); i != e[0].end(); ++i) {
 161       free.erase(*i);
 162     }
 163   } else if(e.getKind() == kind::BOUND_VARIABLE) {
 164     free.insert(e);
 165     return false;
 166   } else {
 167     if(e.hasOperator()) {
 168       isClosed(e.getOperator(), free, closedCache);
 169     }
 170     for(Expr::const_iterator i = e.begin(); i != e.end(); ++i) {
 171       isClosed(*i, free, closedCache);
 172     }
 173   }
 174
 175   if(free.empty()) {
 176     closedCache.insert(e);
 177     return true;
 178   } else {
 179     return false;
 180   }
 181 }
 182
 183 static inline bool isClosed(const Expr& e, std::set<Expr>& free) {
 184   std::unordered_set<Expr, ExprHashFunction> cache;
 185   return isClosed(e, free, cache);
 186 }
 187
 188 }/* parser::postinclude */
 189
 190 /**
 191  * Parses an expression.
 192  * @return the parsed expression, or the Null Expr if we've reached the
 193  * end of the input
 194  */
 195 parseExpr returns [CVC4::parser::smt2::myExpr expr]
 196 @declarations {
 197   Expr expr2;
 198 }
 199   : term[expr, expr2]
 200   | EOF
 201   ;
 202
 203 /**
 204  * Parses a command
 205  * @return the parsed command, or NULL if we've reached the end of the input
 206  */
 207 parseCommand returns [CVC4::Command* cmd_return = NULL]
 208 @declarations {
 209   std::unique_ptr<CVC4::Command> cmd;
 210   std::string name;
 211 }
 212 @after {
 213   cmd_return = cmd.release();
 214 }
 215   : LPAREN_TOK command[&cmd] RPAREN_TOK
 216
 217     /* This extended command has to be in the outermost production so that
 218      * the RPAREN_TOK is properly eaten and we are in a good state to read
 219      * the included file's tokens. */
 220   | LPAREN_TOK INCLUDE_TOK str[name,true] RPAREN_TOK
 221     { if(!PARSER_STATE->canIncludeFile()) {
 222         PARSER_STATE->parseError("include-file feature was disabled for this "
 223                                  "run.");
 224       }
 225       if(PARSER_STATE->strictModeEnabled()) {
 226         PARSER_STATE->parseError("Extended commands are not permitted while "
 227                                  "operating in strict compliance mode.");
 228       }
 229       PARSER_STATE->includeFile(name);
 230       // The command of the included file will be produced at the next
 231       // parseCommand() call
 232       cmd.reset(new EmptyCommand("include::" + name));
 233     }
 234
 235   | EOF
 236   ;
 237
 238 /**
 239  * Parses a SyGuS command.
 240  * @return the parsed SyGuS command, or NULL if we've reached the end of the
 241  * input
 242  */
 243 parseSygus returns [CVC4::Command* cmd_return = NULL]
 244 @declarations {
 245   std::unique_ptr<CVC4::Command> cmd;
 246   std::string name;
 247 }
 248 @after {
 249   cmd_return = cmd.release();
 250 }
 251   : LPAREN_TOK sygusCommand[&cmd] RPAREN_TOK
 252   | EOF
 253   ;
 254
 255 /**
 256  * Parse the internal portion of the command, ignoring the surrounding
 257  * parentheses.
 258  */
 259 command [std::unique_ptr<CVC4::Command>* cmd]
 260 @declarations {
 261   std::string name;
 262   std::vector<std::string> names;
 263   Expr expr, expr2;
 264   Type t;
 265   std::vector<Expr> terms;
 266   std::vector<Type> sorts;
 267   std::vector<std::pair<std::string, Type> > sortedVarNames;
 268   std::vector<Expr> flattenVars;
 269 }
 270   : /* set the logic */
 271     SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
 272     { Debug("parser") << "set logic: '" << name << "'" << std::endl;
 273       if( PARSER_STATE->logicIsSet() ) {
 274         PARSER_STATE->parseError("Only one set-logic is allowed.");
 275       }
 276       PARSER_STATE->setLogic(name);
 277       if( PARSER_STATE->sygus() ){
 278         cmd->reset(new SetBenchmarkLogicCommand(PARSER_STATE->getLogic().getLogicString()));
 279       }else{
 280         cmd->reset(new SetBenchmarkLogicCommand(name));
 281       }
 282     }
 283   | /* set-info */
 284     SET_INFO_TOK metaInfoInternal[cmd]
 285   | /* get-info */
 286     GET_INFO_TOK KEYWORD
 287     { cmd->reset(new GetInfoCommand(
 288           AntlrInput::tokenText($KEYWORD).c_str() + 1));
 289     }
 290   | /* set-option */
 291     SET_OPTION_TOK setOptionInternal[cmd]
 292   | /* get-option */
 293     GET_OPTION_TOK KEYWORD
 294     { cmd->reset(new GetOptionCommand(
 295           AntlrInput::tokenText($KEYWORD).c_str() + 1));
 296     }
 297   | /* sort declaration */
 298     DECLARE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 299     { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) &&
 300          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) &&
 301          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) &&
 302          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) {
 303           PARSER_STATE->parseErrorLogic("Free sort symbols not allowed in ");
 304       }
 305     }
 306     symbol[name,CHECK_UNDECLARED,SYM_SORT]
 307     { PARSER_STATE->checkUserSymbol(name); }
 308     n=INTEGER_LITERAL
 309     { Debug("parser") << "declare sort: '" << name
 310                       << "' arity=" << n << std::endl;
 311       unsigned arity = AntlrInput::tokenToUnsigned(n);
 312       if(arity == 0) {
 313         Type type = PARSER_STATE->mkSort(name);
 314         cmd->reset(new DeclareTypeCommand(name, 0, type));
 315       } else {
 316         Type type = PARSER_STATE->mkSortConstructor(name, arity);
 317         cmd->reset(new DeclareTypeCommand(name, arity, type));
 318       }
 319     }
 320   | /* sort definition */
 321     DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 322     symbol[name,CHECK_UNDECLARED,SYM_SORT]
 323     { PARSER_STATE->checkUserSymbol(name); }
 324     LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
 325     { PARSER_STATE->pushScope(true);
 326       for(std::vector<std::string>::const_iterator i = names.begin(),
 327             iend = names.end();
 328           i != iend;
 329           ++i) {
 330         sorts.push_back(PARSER_STATE->mkSort(*i));
 331       }
 332     }
 333     sortSymbol[t,CHECK_DECLARED]
 334     { PARSER_STATE->popScope();
 335       // Do NOT call mkSort, since that creates a new sort!
 336       // This name is not its own distinct sort, it's an alias.
 337       PARSER_STATE->defineParameterizedType(name, sorts, t);
 338       cmd->reset(new DefineTypeCommand(name, sorts, t));
 339     }
 340   | /* function declaration */
 341     DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 342     symbol[name,CHECK_NONE,SYM_VARIABLE]
 343     { PARSER_STATE->checkUserSymbol(name); }
 344     LPAREN_TOK sortList[sorts] RPAREN_TOK
 345     sortSymbol[t,CHECK_DECLARED]
 346     { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
 347       if( !sorts.empty() ) {
 348         t = PARSER_STATE->mkFlatFunctionType(sorts, t);
 349       }
 350       if(t.isFunction() && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
 351         PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) cannot "
 352                                       "be declared in logic ");
 353       }
 354       // we allow overloading for function declarations
 355       if (PARSER_STATE->sygus())
 356       {
 357         // it is a higher-order universal variable
 358         Expr func = PARSER_STATE->mkBoundVar(name, t);
 359         cmd->reset(new DeclareSygusFunctionCommand(name, func, t));
 360       }
 361       else
 362       {
 363         Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
 364         cmd->reset(new DeclareFunctionCommand(name, func, t));
 365       }
 366     }
 367   | /* function definition */
 368     DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 369     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 370     { PARSER_STATE->checkUserSymbol(name); }
 371     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
 372     sortSymbol[t,CHECK_DECLARED]
 373     { /* add variables to parser state before parsing term */
 374       Debug("parser") << "define fun: '" << name << "'" << std::endl;
 375       if( sortedVarNames.size() > 0 ) {
 376         sorts.reserve(sortedVarNames.size());
 377         for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 378               sortedVarNames.begin(), iend = sortedVarNames.end();
 379             i != iend;
 380             ++i) {
 381           sorts.push_back((*i).second);
 382         }
 383         t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
 384       }
 385       PARSER_STATE->pushScope(true);
 386       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
 387             sortedVarNames.begin(), iend = sortedVarNames.end();
 388           i != iend;
 389           ++i) {
 390         terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
 391       }
 392     }
 393     term[expr, expr2]
 394     {
 395       if( !flattenVars.empty() ){
 396         // if this function has any implicit variables flattenVars,
 397         // we apply the body of the definition to the flatten vars
 398         expr = PARSER_STATE->mkHoApply(expr, flattenVars);
 399         terms.insert(terms.end(), flattenVars.begin(), flattenVars.end());
 400       }
 401       PARSER_STATE->popScope();
 402       // declare the name down here (while parsing term, signature
 403       // must not be extended with the name itself; no recursion
 404       // permitted)
 405       // we allow overloading for function definitions
 406       Expr func = PARSER_STATE->mkFunction(name, t,
 407                                            ExprManager::VAR_FLAG_DEFINED, true);
 408       cmd->reset(new DefineFunctionCommand(name, func, terms, expr));
 409     }
 410   | /* value query */
 411     GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 412     ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
 413       { cmd->reset(new GetValueCommand(terms)); }
 414     | ~LPAREN_TOK
 415       { PARSER_STATE->parseError("The get-value command expects a list of "
 416                                  "terms.  Perhaps you forgot a pair of "
 417                                  "parentheses?");
 418       }
 419     )
 420   | /* get-assignment */
 421     GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 422     { cmd->reset(new GetAssignmentCommand()); }
 423   | /* assertion */
 424     ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 425     /* { if( PARSER_STATE->sygus() ){
 426      *     PARSER_STATE->parseError("Sygus does not support assert command.");
 427      *   }
 428      * } */
 429     { PARSER_STATE->clearLastNamedTerm(); }
 430     term[expr, expr2]
 431     { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr;
 432       cmd->reset(new AssertCommand(expr, inUnsatCore));
 433       if(inUnsatCore) {
 434         // set the expression name, if there was a named term
 435         std::pair<Expr, std::string> namedTerm = PARSER_STATE->lastNamedTerm();
 436         Command* csen = new SetExpressionNameCommand(namedTerm.first, namedTerm.second);
 437         csen->setMuted(true);
 438         PARSER_STATE->preemptCommand(csen);
 439       }
 440       // if sygus, check whether it has a free variable
 441       // this is because, due to the sygus format, one can write assertions
 442       // that have free function variables in them
 443       if (PARSER_STATE->sygus())
 444       {
 445         if (expr.hasFreeVariable())
 446         {
 447           PARSER_STATE->parseError("Assertion has free variable. Perhaps you "
 448                                    "meant constraint instead of assert?");
 449         }
 450       }
 451     }
 452   | /* check-sat */
 453     CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 454     { if( PARSER_STATE->sygus() ){
 455         PARSER_STATE->parseError("Sygus does not support check-sat command.");
 456       }
 457     }
 458     ( term[expr, expr2]
 459       { if(PARSER_STATE->strictModeEnabled()) {
 460           PARSER_STATE->parseError(
 461               "Extended commands (such as check-sat with an argument) are not "
 462               "permitted while operating in strict compliance mode.");
 463         }
 464       }
 465     | { expr = Expr(); }
 466     )
 467     { cmd->reset(new CheckSatCommand(expr)); }
 468   | /* check-sat-assuming */
 469     CHECK_SAT_ASSUMING_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 470     ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
 471       { cmd->reset(new CheckSatAssumingCommand(terms)); }
 472     | ~LPAREN_TOK
 473       { PARSER_STATE->parseError("The check-sat-assuming command expects a "
 474                                  "list of terms.  Perhaps you forgot a pair of "
 475                                  "parentheses?");
 476       }
 477     )
 478   | /* get-assertions */
 479     GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 480     { cmd->reset(new GetAssertionsCommand()); }
 481   | /* get-proof */
 482     GET_PROOF_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 483     { cmd->reset(new GetProofCommand()); }
 484   | /* get-unsat-assumptions */
 485     GET_UNSAT_ASSUMPTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 486     { cmd->reset(new GetUnsatAssumptionsCommand); }
 487   | /* get-unsat-core */
 488     GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 489     { cmd->reset(new GetUnsatCoreCommand); }
 490   | /* push */
 491     PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 492     { if( PARSER_STATE->sygus() ){
 493         PARSER_STATE->parseError("Sygus does not support push command.");
 494       }
 495     }
 496     ( k=INTEGER_LITERAL
 497       { unsigned n = AntlrInput::tokenToUnsigned(k);
 498         if(n == 0) {
 499           cmd->reset(new EmptyCommand());
 500         } else if(n == 1) {
 501           PARSER_STATE->pushScope();
 502           cmd->reset(new PushCommand());
 503         } else {
 504           std::unique_ptr<CommandSequence> seq(new CommandSequence());
 505           do {
 506             PARSER_STATE->pushScope();
 507             Command* push_cmd = new PushCommand();
 508             push_cmd->setMuted(n > 1);
 509             seq->addCommand(push_cmd);
 510             --n;
 511             } while(n > 0);
 512           cmd->reset(seq.release());
 513         }
 514       }
 515     | { if(PARSER_STATE->strictModeEnabled()) {
 516           PARSER_STATE->parseError(
 517               "Strict compliance mode demands an integer to be provided to "
 518               "PUSH.  Maybe you want (push 1)?");
 519         } else {
 520           PARSER_STATE->pushScope();
 521           cmd->reset(new PushCommand());
 522         }
 523       } )
 524   | POP_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 525     { if( PARSER_STATE->sygus() ){
 526         PARSER_STATE->parseError("Sygus does not support pop command.");
 527       }
 528     }
 529     ( k=INTEGER_LITERAL
 530       { unsigned n = AntlrInput::tokenToUnsigned(k);
 531         if(n > PARSER_STATE->scopeLevel()) {
 532           PARSER_STATE->parseError("Attempted to pop above the top stack "
 533                                    "frame.");
 534         }
 535         if(n == 0) {
 536           cmd->reset(new EmptyCommand());
 537         } else if(n == 1) {
 538           PARSER_STATE->popScope();
 539           cmd->reset(new PopCommand());
 540         } else {
 541           std::unique_ptr<CommandSequence> seq(new CommandSequence());
 542           do {
 543             PARSER_STATE->popScope();
 544             Command* pop_command = new PopCommand();
 545             pop_command->setMuted(n > 1);
 546             seq->addCommand(pop_command);
 547             --n;
 548           } while(n > 0);
 549           cmd->reset(seq.release());
 550         }
 551       }
 552     | { if(PARSER_STATE->strictModeEnabled()) {
 553           PARSER_STATE->parseError(
 554               "Strict compliance mode demands an integer to be provided to POP."
 555               "Maybe you want (pop 1)?");
 556         } else {
 557           PARSER_STATE->popScope();
 558           cmd->reset(new PopCommand());
 559         }
 560       }
 561     )
 562     /* exit */
 563   | EXIT_TOK
 564     { cmd->reset(new QuitCommand()); }
 565
 566     /* New SMT-LIB 2.5 command set */
 567   | smt25Command[cmd]
 568     { if(PARSER_STATE->v2_0() && PARSER_STATE->strictModeEnabled()) {
 569         PARSER_STATE->parseError(
 570             "SMT-LIB 2.5 commands are not permitted while operating in strict "
 571             "compliance mode and in SMT-LIB 2.0 mode.");
 572       }
 573     }
 574
 575     /* CVC4-extended SMT-LIB commands */
 576   | extendedCommand[cmd]
 577     { if(PARSER_STATE->strictModeEnabled()) {
 578         PARSER_STATE->parseError(
 579             "Extended commands are not permitted while operating in strict "
 580             "compliance mode.");
 581       }
 582     }
 583
 584     /* error handling */
 585   | SIMPLE_SYMBOL
 586     { std::string id = AntlrInput::tokenText($SIMPLE_SYMBOL);
 587       if(id == "benchmark") {
 588         PARSER_STATE->parseError(
 589             "In SMT-LIBv2 mode, but got something that looks like SMT-LIBv1. "
 590             "Use --lang smt1 for SMT-LIBv1.");
 591       } else {
 592         PARSER_STATE->parseError("expected SMT-LIBv2 command, got `" + id +
 593                                  "'.");
 594       }
 595     }
 596   ;
 597
 598 sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
 599 @declarations {
 600   std::string name, fun;
 601   std::vector<std::string> names;
 602   Expr expr, expr2;
 603   Type t, range;
 604   std::vector<Expr> terms;
 605   std::vector<Expr> sygus_vars;
 606   std::vector<std::pair<std::string, Type> > sortedVarNames;
 607   Type sygus_ret;
 608   Expr synth_fun;
 609   Type sygus_type;
 610   bool isInv;
 611 }
 612   : /* declare-var */
 613     DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 614     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 615     { PARSER_STATE->checkUserSymbol(name); }
 616     sortSymbol[t,CHECK_DECLARED]
 617     {
 618       Expr var = PARSER_STATE->mkBoundVar(name, t);
 619       cmd->reset(new DeclareSygusVarCommand(name, var, t));
 620     }
 621   | /* declare-primed-var */
 622     DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
 623     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
 624     { PARSER_STATE->checkUserSymbol(name); }
 625     sortSymbol[t,CHECK_DECLARED]
 626     {
 627       // spurious command, we do not need to create a variable. We only keep
 628       // track of the command for sanity checking / dumping
 629       cmd->reset(new DeclareSygusPrimedVarCommand(name, t));
 630     }
 631
 632   | /* synth-fun */
 633     ( SYNTH_FUN_TOK { isInv = false; }
 634       | SYNTH_INV_TOK { isInv = true; range = EXPR_MANAGER->booleanType(); }
 635     )
 636     { PARSER_STATE->checkThatLogicIsSet(); }
 637     symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
 638     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
 639     ( sortSymbol[range,CHECK_DECLARED] )?
 640     {
 641       if (range.isNull())
 642       {
 643         PARSER_STATE->parseError("Must supply return type for synth-fun.");
 644       }
 645       if (range.isFunction())
 646       {
 647         PARSER_STATE->parseError(
 648             "Cannot use synth-fun with function return type.");
 649       }
 650       std::vector<Type> var_sorts;
 651       for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames)
 652       {
 653         var_sorts.push_back(p.second);
 654       }
 655       Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
 656       Type synth_fun_type = var_sorts.size() > 0
 657                                 ? EXPR_MANAGER->mkFunctionType(var_sorts, range)
 658                                 : range;
 659       // we do not allow overloading for synth fun
 660       synth_fun = PARSER_STATE->mkBoundVar(fun, synth_fun_type);
 661       // set the sygus type to be range by default, which is overwritten below
 662       // if a grammar is provided
 663       sygus_type = range;
 664       // create new scope for parsing the grammar, if any
 665       PARSER_STATE->pushScope(true);
 666       for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames)
 667       {
 668         sygus_vars.push_back(PARSER_STATE->mkBoundVar(p.first, p.second));
 669       }
 670     }
 671     (
 672       // optionally, read the sygus grammar
 673       //
 674       // the sygus type specifies the required grammar for synth_fun, expressed
 675       // as a type
 676       sygusGrammar[sygus_type, sygus_vars, fun]
 677     )?
 678     {
 679       PARSER_STATE->popScope();
 680       Debug("parser-sygus") << "...read synth fun " << fun << std::endl;
 681       cmd->reset(
 682           new SynthFunCommand(fun, synth_fun, sygus_type, isInv, sygus_vars));
 683     }
 684   | /* constraint */
 685     CONSTRAINT_TOK {
 686       PARSER_STATE->checkThatLogicIsSet();
 687       Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
 688       Debug("parser-sygus") << "Sygus : read constraint..." << std::endl;
 689     }
 690     term[expr, expr2]
 691     { Debug("parser-sygus") << "...read constraint " << expr << std::endl;
 692       cmd->reset(new SygusConstraintCommand(expr));
 693     }
 694   | INV_CONSTRAINT_TOK {
 695       PARSER_STATE->checkThatLogicIsSet();
 696       Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
 697       Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl;
 698     }
 699     ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
 700         if( !terms.empty() ){
 701           if( !PARSER_STATE->isDefinedFunction(name) ){
 702             std::stringstream ss;
 703             ss << "Function " << name << " in inv-constraint is not defined.";
 704             PARSER_STATE->parseError(ss.str());
 705           }
 706         }
 707         terms.push_back( PARSER_STATE->getVariable(name) );
 708       }
 709     )+ {
 710       if( terms.size()!=4 ){
 711         PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 "
 712                                  "arguments.");
 713       }
 714
 715       cmd->reset(new SygusInvConstraintCommand(terms));
 716     }
 717   | /* check-synth */
 718     CHECK_SYNTH_TOK
 719     { PARSER_STATE->checkThatLogicIsSet(); }
 720     {
 721       cmd->reset(new CheckSynthCommand());
 722     }
 723   | command[cmd]
 724   ;
 725
 726 /** Reads a sygus grammar
 727  *
 728  * The resulting sygus datatype encoding the grammar is stored in ret.
 729  * The argument sygus_vars indicates the sygus bound variable list, which is
 730  * the argument list of the function-to-synthesize (or null if the grammar
 731  * has bound variables).
 732  * The argument fun is a unique identifier to avoid naming clashes for the
 733  * datatypes constructed by this call.
 734  */
 735 sygusGrammar[CVC4::Type & ret,
 736              std::vector<CVC4::Expr>& sygus_vars,
 737              std::string& fun]
 738 @declarations
 739 {
 740   Type t;
 741   std::string name;
 742   unsigned startIndex = 0;
 743   std::vector<std::vector<CVC4::SygusGTerm>> sgts;
 744   std::vector<CVC4::Datatype> datatypes;
 745   std::vector<Type> sorts;
 746   std::vector<std::vector<Expr>> ops;
 747   std::vector<std::vector<std::string>> cnames;
 748   std::vector<std::vector<std::vector<CVC4::Type>>> cargs;
 749   std::vector<bool> allow_const;
 750   std::vector<std::vector<std::string>> unresolved_gterm_sym;
 751   std::map<CVC4::Type, CVC4::Type> sygus_to_builtin;
 752   std::map<CVC4::Type, CVC4::Expr> sygus_to_builtin_expr;
 753 }
 754   : LPAREN_TOK { PARSER_STATE->pushScope(); }
 755   (LPAREN_TOK
 756        symbol[name, CHECK_NONE, SYM_VARIABLE] sortSymbol[t, CHECK_DECLARED] {
 757          std::stringstream ss;
 758          ss << fun << "_" << name;
 759          if (name == "Start")
 760          {
 761            startIndex = datatypes.size();
 762          }
 763          std::string dname = ss.str();
 764          sgts.push_back(std::vector<CVC4::SygusGTerm>());
 765          sgts.back().push_back(CVC4::SygusGTerm());
 766          PARSER_STATE->pushSygusDatatypeDef(t,
 767                                             dname,
 768                                             datatypes,
 769                                             sorts,
 770                                             ops,
 771                                             cnames,
 772                                             cargs,
 773                                             allow_const,
 774                                             unresolved_gterm_sym);
 775          Type unres_t;
 776          if (!PARSER_STATE->isUnresolvedType(dname))
 777          {
 778            // if not unresolved, must be undeclared
 779            Debug("parser-sygus") << "Make unresolved type : " << dname
 780                                  << std::endl;
 781            PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
 782            unres_t = PARSER_STATE->mkUnresolvedType(dname);
 783          }
 784          else
 785          {
 786            Debug("parser-sygus") << "Get sort : " << dname << std::endl;
 787            unres_t = PARSER_STATE->getSort(dname);
 788          }
 789          sygus_to_builtin[unres_t] = t;
 790          Debug("parser-sygus") << "--- Read sygus grammar " << name
 791                                << " under function " << fun << "..."
 792                                << std::endl
 793                                << "    type to resolve " << unres_t << std::endl
 794                                << "    builtin type " << t << std::endl;
 795        }
 796    // Note the official spec for NTDef is missing the ( parens )
 797    // but they are necessary to parse SyGuS examples
 798    LPAREN_TOK(sygusGTerm[sgts.back().back(), fun] {
 799      sgts.back().push_back(CVC4::SygusGTerm());
 800    })
 801    + RPAREN_TOK { sgts.back().pop_back(); } RPAREN_TOK)
 802       + RPAREN_TOK
 803   {
 804     unsigned numSTerms = sgts.size();
 805     Debug("parser-sygus") << "--- Process " << numSTerms << " sygus gterms..."
 806                           << std::endl;
 807     for (unsigned i = 0; i < numSTerms; i++)
 808     {
 809       for (unsigned j = 0, size = sgts[i].size(); j < size; j++)
 810       {
 811         Type sub_ret;
 812         PARSER_STATE->processSygusGTerm(sgts[i][j],
 813                                         i,
 814                                         datatypes,
 815                                         sorts,
 816                                         ops,
 817                                         cnames,
 818                                         cargs,
 819                                         allow_const,
 820                                         unresolved_gterm_sym,
 821                                         sygus_vars,
 822                                         sygus_to_builtin,
 823                                         sygus_to_builtin_expr,
 824                                         sub_ret);
 825       }
 826     }
 827     // swap index if necessary
 828     Debug("parser-sygus") << "--- Making sygus datatypes..." << std::endl;
 829     unsigned ndatatypes = datatypes.size();
 830     for (unsigned i = 0; i < ndatatypes; i++)
 831     {
 832       Debug("parser-sygus") << "..." << datatypes[i].getName()
 833                             << " has builtin sort " << sorts[i] << std::endl;
 834     }
 835     Expr bvl;
 836     if (!sygus_vars.empty())
 837     {
 838       bvl = MK_EXPR(kind::BOUND_VAR_LIST, sygus_vars);
 839     }
 840     for (unsigned i = 0; i < ndatatypes; i++)
 841     {
 842       Debug("parser-sygus") << "...make " << datatypes[i].getName()
 843                             << " with builtin sort " << sorts[i] << std::endl;
 844       if (sorts[i].isNull())
 845       {
 846         PARSER_STATE->parseError(
 847             "Internal error : could not infer "
 848             "builtin sort for nested gterm.");
 849       }
 850       datatypes[i].setSygus(sorts[i], bvl, allow_const[i], false);
 851       PARSER_STATE->mkSygusDatatype(datatypes[i],
 852                                     ops[i],
 853                                     cnames[i],
 854                                     cargs[i],
 855                                     unresolved_gterm_sym[i],
 856                                     sygus_to_builtin);
 857     }
 858     PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts, ops);
 859     PARSER_STATE->popScope();
 860     Debug("parser-sygus") << "--- Make " << ndatatypes
 861                           << " mutual datatypes..." << std::endl;
 862     for (unsigned i = 0; i < ndatatypes; i++)
 863     {
 864       Debug("parser-sygus") << "  " << i << " : " << datatypes[i].getName()
 865                             << std::endl;
 866     }
 867     std::vector<DatatypeType> datatypeTypes =
 868         PARSER_STATE->mkMutualDatatypeTypes(datatypes);
 869     ret = datatypeTypes[0];
 870   };
 871
 872 // SyGuS grammar term.
 873 //
 874 // fun is the name of the synth-fun this grammar term is for.
 875 // This method adds N operators to ops[index], N names to cnames[index] and N
 876 // type argument vectors to cargs[index] (where typically N=1)
 877 // This method may also add new elements pairwise into
 878 // datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
 879 sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
 880 @declarations {
 881   std::string name, name2;
 882   Kind k;
 883   Type t;
 884   std::string sname;
 885   std::vector< Expr > let_vars;
 886   bool readingLet = false;
 887   std::string s;
 888   CVC4::api::Term atomTerm;
 889 }
 890   : LPAREN_TOK
 891     //read operator
 892     ( builtinOp[k]{
 893         Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : "
 894                               << name << std::endl;
 895         sgt.d_name = kind::kindToString(k);
 896         sgt.d_gterm_type = SygusGTerm::gterm_op;
 897         sgt.d_expr = EXPR_MANAGER->operatorOf(k);
 898       }
 899      | SYGUS_LET_TOK LPAREN_TOK {
 900          sgt.d_name = std::string("let");
 901          sgt.d_gterm_type = SygusGTerm::gterm_let;
 902          PARSER_STATE->pushScope(true);
 903          readingLet = true;
 904        }
 905        ( LPAREN_TOK
 906         symbol[sname,CHECK_NONE,SYM_VARIABLE]
 907         sortSymbol[t,CHECK_DECLARED] {
 908           Expr v = PARSER_STATE->mkBoundVar(sname,t);
 909           sgt.d_let_vars.push_back( v );
 910           sgt.addChild();
 911         }
 912         sygusGTerm[sgt.d_children.back(), fun]
 913         RPAREN_TOK )+ RPAREN_TOK
 914     | SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED]
 915       { sgt.d_gterm_type = SygusGTerm::gterm_constant;
 916         sgt.d_type = t;
 917         Debug("parser-sygus") << "Sygus grammar constant." << std::endl;
 918       }
 919     | SYGUS_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
 920       { sgt.d_gterm_type = SygusGTerm::gterm_variable;
 921         sgt.d_type = t;
 922         Debug("parser-sygus") << "Sygus grammar variable." << std::endl;
 923       }
 924     | SYGUS_LOCAL_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
 925       { sgt.d_gterm_type = SygusGTerm::gterm_local_variable;
 926         sgt.d_type = t;
 927         Debug("parser-sygus") << "Sygus grammar local variable...ignore."
 928                               << std::endl;
 929       }
 930     | SYGUS_INPUT_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
 931       { sgt.d_gterm_type = SygusGTerm::gterm_input_variable;
 932         sgt.d_type = t;
 933         Debug("parser-sygus") << "Sygus grammar (input) variable."
 934                               << std::endl;
 935       }
 936     | symbol[name,CHECK_NONE,SYM_VARIABLE] {
 937         bool isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
 938         if(isBuiltinOperator) {
 939           Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : "
 940                                 << name << std::endl;
 941           k = PARSER_STATE->getOperatorKind(name);
 942           sgt.d_name = kind::kindToString(k);
 943           sgt.d_gterm_type = SygusGTerm::gterm_op;
 944           sgt.d_expr = EXPR_MANAGER->operatorOf(k);
 945         }else{
 946           // what is this sygus term trying to accomplish here, if the
 947           // symbol isn't yet declared?!  probably the following line will
 948           // fail, but we need an operator to continue here..
 949           Debug("parser-sygus")
 950               << "Sygus grammar " << fun << " : op (declare="
 951               << PARSER_STATE->isDeclared(name) << ", define="
 952               << PARSER_STATE->isDefinedFunction(name) << ") : " << name
 953               << std::endl;
 954           if(!PARSER_STATE->isDeclared(name) &&
 955              !PARSER_STATE->isDefinedFunction(name) ){
 956             PARSER_STATE->parseError("Functions in sygus grammars must be "
 957                                      "defined.");
 958           }
 959           sgt.d_name = name;
 960           sgt.d_gterm_type = SygusGTerm::gterm_op;
 961           sgt.d_expr = PARSER_STATE->getVariable(name) ;
 962         }
 963       }
 964     )
 965     //read arguments
 966     { Debug("parser-sygus") << "Read arguments under " << sgt.d_name
 967                             << std::endl;
 968       sgt.addChild();
 969     }
 970     ( sygusGTerm[sgt.d_children.back(), fun]
 971       { Debug("parser-sygus") << "Finished read argument #"
 972                               << sgt.d_children.size() << "..." << std::endl;
 973         sgt.addChild();
 974       }
 975     )*
 976     RPAREN_TOK {
 977       //pop last child index
 978       sgt.d_children.pop_back();
 979       if( readingLet ){
 980         PARSER_STATE->popScope();
 981       }
 982     }
 983     | termAtomic[atomTerm]
 984       {
 985         Debug("parser-sygus") << "Sygus grammar " << fun << " : atomic "
 986                               << "expression " << atomTerm << std::endl;
 987         std::stringstream ss;
 988         ss << atomTerm;
 989         sgt.d_expr = atomTerm.getExpr();
 990         sgt.d_name = ss.str();
 991         sgt.d_gterm_type = SygusGTerm::gterm_op;
 992       }
 993   | symbol[name,CHECK_NONE,SYM_VARIABLE]
 994     {
 995       if( name[0] == '-' ){  //hack for unary minus
 996         Debug("parser-sygus") << "Sygus grammar " << fun
 997                               << " : unary minus integer literal " << name
 998                               << std::endl;
 999         sgt.d_expr = MK_CONST(Rational(name));
1000         sgt.d_name = name;
1001         sgt.d_gterm_type = SygusGTerm::gterm_op;
1002       }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){
1003         Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol "
1004                               << name << std::endl;
1005         sgt.d_expr = PARSER_STATE->getVariable(name);
1006         sgt.d_name = name;
1007         sgt.d_gterm_type = SygusGTerm::gterm_op;
1008       }else{
1009         //prepend function name to base sorts when reading an operator
1010         std::stringstream ss;
1011         ss << fun << "_" << name;
1012         name = ss.str();
1013         if( PARSER_STATE->isDeclared(name, SYM_SORT) ){
1014           Debug("parser-sygus") << "Sygus grammar " << fun
1015                                 << " : nested sort " << name << std::endl;
1016           sgt.d_type = PARSER_STATE->getSort(name);
1017           sgt.d_gterm_type = SygusGTerm::gterm_nested_sort;
1018         }else{
1019           Debug("parser-sygus") << "Sygus grammar " << fun
1020                                 << " : unresolved symbol " << name
1021                                 << std::endl;
1022           sgt.d_gterm_type = SygusGTerm::gterm_unresolved;
1023           sgt.d_name = name;
1024         }
1025       }
1026     }
1027   ;
1028
1029 // Separate this into its own rule (can be invoked by set-info or meta-info)
1030 metaInfoInternal[std::unique_ptr<CVC4::Command>* cmd]
1031 @declarations {
1032   std::string name;
1033   SExpr sexpr;
1034 }
1035   : KEYWORD symbolicExpr[sexpr]
1036     { name = AntlrInput::tokenText($KEYWORD);
1037       if(name == ":cvc4-logic" || name == ":cvc4_logic") {
1038         PARSER_STATE->setLogic(sexpr.getValue());
1039       }
1040       PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
1041       cmd->reset(new SetInfoCommand(name.c_str() + 1, sexpr));
1042     }
1043   ;
1044
1045 setOptionInternal[std::unique_ptr<CVC4::Command>* cmd]
1046 @init {
1047   std::string name;
1048   SExpr sexpr;
1049 }
1050   : keyword[name] symbolicExpr[sexpr]
1051     { PARSER_STATE->setOption(name.c_str() + 1, sexpr);
1052       cmd->reset(new SetOptionCommand(name.c_str() + 1, sexpr));
1053       // Ugly that this changes the state of the parser; but
1054       // global-declarations affects parsing, so we can't hold off
1055       // on this until some SmtEngine eventually (if ever) executes it.
1056       if(name == ":global-declarations") {
1057         PARSER_STATE->setGlobalDeclarations(sexpr.getValue() == "true");
1058       }
1059     }
1060   ;
1061
1062 smt25Command[std::unique_ptr<CVC4::Command>* cmd]
1063 @declarations {
1064   std::string name;
1065   std::string fname;
1066   Expr expr, expr2;
1067   std::vector<std::pair<std::string, Type> > sortedVarNames;
1068   SExpr sexpr;
1069   Type t;
1070   Expr func;
1071   std::vector<Expr> bvs;
1072   std::vector< std::vector<std::pair<std::string, Type> > > sortedVarNamesList;
1073   std::vector<std::vector<Expr>> flattenVarsList;
1074   std::vector<std::vector<Expr>> formals;
1075   std::vector<Expr> funcs;
1076   std::vector<Expr> func_defs;
1077   Expr aexpr;
1078   std::unique_ptr<CVC4::CommandSequence> seq;
1079   std::vector<Type> sorts;
1080   std::vector<Expr> flattenVars;
1081 }
1082     /* meta-info */
1083   : META_INFO_TOK metaInfoInternal[cmd]
1084
1085     /* declare-const */
1086   | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1087     symbol[name,CHECK_NONE,SYM_VARIABLE]
1088     { PARSER_STATE->checkUserSymbol(name); }
1089     sortSymbol[t,CHECK_DECLARED]
1090     { // allow overloading here
1091       Expr c = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
1092       cmd->reset(new DeclareFunctionCommand(name, c, t)); }
1093
1094     /* get model */
1095   | GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1096     { cmd->reset(new GetModelCommand()); }
1097
1098     /* echo */
1099   | ECHO_TOK
1100     ( simpleSymbolicExpr[sexpr]
1101       { cmd->reset(new EchoCommand(sexpr.toString())); }
1102     | { cmd->reset(new EchoCommand()); }
1103     )
1104
1105     /* reset: reset everything, returning solver to initial state.
1106      * Logic and options must be set again. */
1107   | RESET_TOK
1108     { cmd->reset(new ResetCommand());
1109       PARSER_STATE->reset();
1110     }
1111     /* reset-assertions: reset assertions, assertion stack, declarations,
1112      * etc., but the logic and options remain as they were. */
1113   | RESET_ASSERTIONS_TOK
1114     { cmd->reset(new ResetAssertionsCommand());
1115       PARSER_STATE->resetAssertions();
1116     }
1117   | DEFINE_FUN_REC_TOK
1118     { PARSER_STATE->checkThatLogicIsSet(); }
1119     symbol[fname,CHECK_NONE,SYM_VARIABLE]
1120     { PARSER_STATE->checkUserSymbol(fname); }
1121     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1122     sortSymbol[t,CHECK_DECLARED]
1123     {
1124       func = PARSER_STATE->mkDefineFunRec(fname, sortedVarNames, t, flattenVars);
1125       PARSER_STATE->pushDefineFunRecScope(sortedVarNames, func, flattenVars, bvs, true );
1126     }
1127     term[expr, expr2]
1128     { PARSER_STATE->popScope();
1129       if( !flattenVars.empty() ){
1130         expr = PARSER_STATE->mkHoApply( expr, flattenVars );
1131       }
1132       cmd->reset(new DefineFunctionRecCommand(func,bvs,expr));
1133     }
1134   | DEFINE_FUNS_REC_TOK
1135     { PARSER_STATE->checkThatLogicIsSet();}
1136     LPAREN_TOK
1137     ( LPAREN_TOK
1138       symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE]
1139       { PARSER_STATE->checkUserSymbol(fname); }
1140       LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1141       sortSymbol[t,CHECK_DECLARED]
1142       {
1143         flattenVars.clear();
1144         func = PARSER_STATE->mkDefineFunRec( fname, sortedVarNames, t, flattenVars );
1145         funcs.push_back( func );
1146
1147         // add to lists (need to remember for when parsing the bodies)
1148         sortedVarNamesList.push_back( sortedVarNames );
1149         flattenVarsList.push_back( flattenVars );
1150
1151         // set up parsing the next variable list block
1152         sortedVarNames.clear();
1153         flattenVars.clear();
1154       }
1155       RPAREN_TOK
1156     )+
1157     RPAREN_TOK
1158     LPAREN_TOK
1159     {
1160       //set up the first scope
1161       if( sortedVarNamesList.empty() ){
1162         PARSER_STATE->parseError("Must define at least one function in "
1163                                  "define-funs-rec");
1164       }
1165       bvs.clear();
1166       PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[0], funcs[0],
1167                                            flattenVarsList[0], bvs, true);
1168     }
1169     (
1170     term[expr,expr2]
1171     {
1172       unsigned j = func_defs.size();
1173       if( !flattenVarsList[j].empty() ){
1174         expr = PARSER_STATE->mkHoApply( expr, flattenVarsList[j] );
1175       }
1176       func_defs.push_back( expr );
1177       formals.push_back(bvs);
1178       j++;
1179       //set up the next scope
1180       PARSER_STATE->popScope();
1181       if( func_defs.size()<funcs.size() ){
1182         bvs.clear();
1183         PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[j], funcs[j],
1184                                              flattenVarsList[j], bvs, true);
1185       }
1186     }
1187     )+
1188     RPAREN_TOK
1189     { if( funcs.size()!=func_defs.size() ){
1190         PARSER_STATE->parseError(std::string(
1191             "Number of functions defined does not match number listed in "
1192             "define-funs-rec"));
1193       }
1194       cmd->reset( new DefineFunctionRecCommand(funcs,formals,func_defs));
1195     }
1196   ;
1197
1198 extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
1199 @declarations {
1200   std::vector<CVC4::Datatype> dts;
1201   Expr e, e2;
1202   Type t;
1203   std::string name;
1204   std::vector<std::string> names;
1205   std::vector<Expr> terms;
1206   std::vector<Type> sorts;
1207   std::vector<std::pair<std::string, Type> > sortedVarNames;
1208   std::unique_ptr<CVC4::CommandSequence> seq;
1209 }
1210     /* Extended SMT-LIB set of commands syntax, not permitted in
1211      * --smtlib2 compliance mode. */
1212   : DECLARE_DATATYPES_2_5_TOK datatypes_2_5_DefCommand[false, cmd]
1213   | DECLARE_CODATATYPES_2_5_TOK datatypes_2_5_DefCommand[true, cmd]
1214   | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
1215   | DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd]
1216   | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
1217   | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
1218   | rewriterulesCommand[cmd]
1219
1220     /* Support some of Z3's extended SMT-LIB commands */
1221
1222   | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1223     { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) &&
1224          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) &&
1225          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) &&
1226          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) {
1227         PARSER_STATE->parseErrorLogic("Free sort symbols not allowed in ");
1228       }
1229     }
1230     { seq.reset(new CVC4::CommandSequence()); }
1231     LPAREN_TOK
1232     ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
1233       { PARSER_STATE->checkUserSymbol(name);
1234         Type type = PARSER_STATE->mkSort(name);
1235         seq->addCommand(new DeclareTypeCommand(name, 0, type));
1236       }
1237     )+
1238     RPAREN_TOK
1239     { cmd->reset(seq.release()); }
1240
1241   | DECLARE_FUNS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1242     { seq.reset(new CVC4::CommandSequence()); }
1243     LPAREN_TOK
1244     ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1245       { PARSER_STATE->checkUserSymbol(name); }
1246       nonemptySortList[sorts] RPAREN_TOK
1247       { Type t;
1248         if(sorts.size() > 1) {
1249           if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
1250             PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) "
1251                                           "cannot be declared in logic ");
1252           }
1253           // must flatten
1254           Type range = sorts.back();
1255           sorts.pop_back();
1256           t = PARSER_STATE->mkFlatFunctionType(sorts, range);
1257         } else {
1258           t = sorts[0];
1259         }
1260         // allow overloading
1261         Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
1262         seq->addCommand(new DeclareFunctionCommand(name, func, t));
1263         sorts.clear();
1264       }
1265     )+
1266     RPAREN_TOK
1267     { cmd->reset(seq.release()); }
1268   | DECLARE_PREDS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1269     { seq.reset(new CVC4::CommandSequence()); }
1270     LPAREN_TOK
1271     ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1272       { PARSER_STATE->checkUserSymbol(name); }
1273       sortList[sorts] RPAREN_TOK
1274       { Type t = EXPR_MANAGER->booleanType();
1275         if(sorts.size() > 0) {
1276           if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
1277             PARSER_STATE->parseErrorLogic("Predicates (of non-zero arity) "
1278                                           "cannot be declared in logic ");
1279           }
1280           t = EXPR_MANAGER->mkFunctionType(sorts, t);
1281         }
1282         // allow overloading
1283         Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
1284         seq->addCommand(new DeclareFunctionCommand(name, func, t));
1285         sorts.clear();
1286       }
1287     )+
1288     RPAREN_TOK
1289     { cmd->reset(seq.release()); }
1290
1291   | DEFINE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1292     ( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1293       { PARSER_STATE->checkUserSymbol(name); }
1294       term[e,e2]
1295       { Expr func = PARSER_STATE->mkFunction(name, e.getType(),
1296                                              ExprManager::VAR_FLAG_DEFINED);
1297         cmd->reset(new DefineFunctionCommand(name, func, e));
1298       }
1299     | LPAREN_TOK
1300       symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1301       { PARSER_STATE->checkUserSymbol(name); }
1302       sortedVarList[sortedVarNames] RPAREN_TOK
1303       { /* add variables to parser state before parsing term */
1304         Debug("parser") << "define fun: '" << name << "'" << std::endl;
1305         PARSER_STATE->pushScope(true);
1306         for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
1307               sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
1308             ++i) {
1309           terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
1310         }
1311       }
1312       term[e,e2]
1313       { PARSER_STATE->popScope();
1314         // declare the name down here (while parsing term, signature
1315         // must not be extended with the name itself; no recursion
1316         // permitted)
1317         Type t = e.getType();
1318         if( sortedVarNames.size() > 0 ) {
1319           std::vector<CVC4::Type> sorts;
1320           sorts.reserve(sortedVarNames.size());
1321           for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator
1322                 i = sortedVarNames.begin(), iend = sortedVarNames.end();
1323               i != iend; ++i) {
1324             sorts.push_back((*i).second);
1325           }
1326           t = EXPR_MANAGER->mkFunctionType(sorts, t);
1327         }
1328         Expr func = PARSER_STATE->mkFunction(name, t,
1329                                              ExprManager::VAR_FLAG_DEFINED);
1330         cmd->reset(new DefineFunctionCommand(name, func, terms, e));
1331       }
1332     )
1333   | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1334     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
1335     { PARSER_STATE->checkUserSymbol(name); }
1336     sortSymbol[t,CHECK_DECLARED]
1337     { /* add variables to parser state before parsing term */
1338       Debug("parser") << "define const: '" << name << "'" << std::endl;
1339       PARSER_STATE->pushScope(true);
1340       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
1341             sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
1342           ++i) {
1343         terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
1344       }
1345     }
1346     term[e, e2]
1347     { PARSER_STATE->popScope();
1348       // declare the name down here (while parsing term, signature
1349       // must not be extended with the name itself; no recursion
1350       // permitted)
1351       Expr func = PARSER_STATE->mkFunction(name, t,
1352                                            ExprManager::VAR_FLAG_DEFINED);
1353       cmd->reset(new DefineFunctionCommand(name, func, terms, e));
1354     }
1355
1356   | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1357     term[e,e2]
1358     { cmd->reset(new SimplifyCommand(e)); }
1359   | GET_QE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1360     term[e,e2]
1361     { cmd->reset(new GetQuantifierEliminationCommand(e, true)); }
1362   | GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
1363     term[e,e2]
1364     { cmd->reset(new GetQuantifierEliminationCommand(e, false)); }
1365   | DECLARE_HEAP LPAREN_TOK
1366     sortSymbol[t,CHECK_DECLARED]
1367     sortSymbol[t, CHECK_DECLARED]
1368     // We currently do nothing with the type information declared for the heap.
1369     { cmd->reset(new EmptyCommand()); }
1370     RPAREN_TOK
1371   ;
1372
1373
1374 datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
1375 @declarations {
1376   std::vector<CVC4::Datatype> dts;
1377   std::string name;
1378   std::vector<Type> sorts;
1379   std::vector<std::string> dnames;
1380   std::vector<unsigned> arities;
1381 }
1382   : { PARSER_STATE->checkThatLogicIsSet();
1383     /* open a scope to keep the UnresolvedTypes contained */
1384     PARSER_STATE->pushScope(true); }
1385   LPAREN_TOK /* parametric sorts */
1386   ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
1387     { sorts.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER) ); }
1388   )*
1389   RPAREN_TOK
1390   LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
1391   { PARSER_STATE->popScope();
1392     cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts, true)));
1393   }
1394   ;
1395
1396 datatypeDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
1397 @declarations {
1398   std::vector<CVC4::Datatype> dts;
1399   std::string name;
1400   std::vector<std::string> dnames;
1401   std::vector<int> arities;
1402 }
1403  : { PARSER_STATE->checkThatLogicIsSet(); }
1404  symbol[name,CHECK_UNDECLARED,SYM_SORT]
1405  {
1406    dnames.push_back(name);
1407    arities.push_back(-1);
1408  }
1409  datatypesDef[isCo, dnames, arities, cmd]
1410  ;
1411
1412 datatypesDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
1413 @declarations {
1414   std::vector<CVC4::Datatype> dts;
1415   std::string name;
1416   std::vector<std::string> dnames;
1417   std::vector<int> arities;
1418 }
1419   : { PARSER_STATE->checkThatLogicIsSet(); }
1420   LPAREN_TOK /* datatype definition prelude */
1421   ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL RPAREN_TOK
1422     { unsigned arity = AntlrInput::tokenToUnsigned(n);
1423       Debug("parser-dt") << "Datatype : " << name << ", arity = " << arity << std::endl;
1424       dnames.push_back(name);
1425       arities.push_back( static_cast<int>(arity) );
1426     }
1427   )*
1428   RPAREN_TOK
1429   LPAREN_TOK
1430   datatypesDef[isCo, dnames, arities, cmd]
1431   RPAREN_TOK
1432   ;
1433
1434 /**
1435  * Read a list of datatype definitions for datatypes with names dnames and
1436  * parametric arities arities. A negative value in arities indicates that the
1437  * arity for the corresponding datatype has not been fixed.
1438  */
1439 datatypesDef[bool isCo,
1440              const std::vector<std::string>& dnames,
1441              const std::vector<int>& arities,
1442              std::unique_ptr<CVC4::Command>* cmd]
1443 @declarations {
1444   std::vector<CVC4::Datatype> dts;
1445   std::string name;
1446   std::vector<Type> params;
1447 }
1448   : { PARSER_STATE->pushScope(true); }
1449     ( LPAREN_TOK {
1450       params.clear();
1451       Debug("parser-dt") << "Processing datatype #" << dts.size() << std::endl;
1452       if( dts.size()>=dnames.size() ){
1453         PARSER_STATE->parseError("Too many datatypes defined in this block.");
1454       }
1455     }
1456     ( PAR_TOK { PARSER_STATE->pushScope(true); } LPAREN_TOK
1457       ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
1458         { params.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER) ); }
1459       )*
1460       RPAREN_TOK {
1461         // if the arity was fixed by prelude and is not equal to the number of parameters
1462         if( arities[dts.size()]>=0 && static_cast<int>(params.size())!=arities[dts.size()] ){
1463           PARSER_STATE->parseError("Wrong number of parameters for datatype.");
1464         }
1465         Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
1466         dts.push_back(Datatype(dnames[dts.size()],params,isCo));
1467       }
1468       LPAREN_TOK
1469       ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
1470       RPAREN_TOK { PARSER_STATE->popScope(); }
1471     | { // if the arity was fixed by prelude and is not equal to 0
1472         if( arities[dts.size()]>0 ){
1473           PARSER_STATE->parseError("No parameters given for datatype.");
1474         }
1475         Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
1476         dts.push_back(Datatype(dnames[dts.size()],params,isCo));
1477       }
1478       ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
1479     )
1480     RPAREN_TOK
1481     )+
1482   {
1483     PARSER_STATE->popScope();
1484     cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts, true)));
1485   }
1486   ;
1487
1488 rewriterulesCommand[std::unique_ptr<CVC4::Command>* cmd]
1489 @declarations {
1490   std::vector<std::pair<std::string, Type> > sortedVarNames;
1491   std::vector<Expr> args, guards, heads, triggers;
1492   Expr head, body, expr, expr2, bvl;
1493   Kind kind;
1494 }
1495   : /* rewrite rules */
1496     REWRITE_RULE_TOK
1497     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1498     {
1499       kind = CVC4::kind::RR_REWRITE;
1500       PARSER_STATE->pushScope(true);
1501       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
1502             sortedVarNames.begin(), iend = sortedVarNames.end();
1503           i != iend;
1504           ++i) {
1505         args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
1506       }
1507       bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
1508     }
1509     LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK
1510     LPAREN_TOK (termList[guards,expr])? RPAREN_TOK
1511     term[head, expr2] term[body, expr2]
1512     {
1513       args.clear();
1514       args.push_back(head);
1515       args.push_back(body);
1516       /* triggers */
1517       if( !triggers.empty() ){
1518         expr2 = MK_EXPR(kind::INST_PATTERN_LIST, triggers);
1519         args.push_back(expr2);
1520       };
1521       expr = MK_EXPR(kind, args);
1522       args.clear();
1523       args.push_back(bvl);
1524       /* guards */
1525       switch( guards.size() ){
1526       case 0:
1527         args.push_back(MK_CONST(bool(true))); break;
1528       case 1:
1529         args.push_back(guards[0]); break;
1530       default:
1531         expr2 = MK_EXPR(kind::AND, guards);
1532         args.push_back(expr2); break;
1533       };
1534       args.push_back(expr);
1535       expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
1536       cmd->reset(new AssertCommand(expr, false)); }
1537     /* propagation rule */
1538   | rewritePropaKind[kind]
1539     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1540     {
1541       PARSER_STATE->pushScope(true);
1542       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
1543             sortedVarNames.begin(), iend = sortedVarNames.end();
1544           i != iend;
1545           ++i) {
1546         args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
1547       }
1548       bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
1549     }
1550     LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK
1551     LPAREN_TOK (termList[guards,expr])? RPAREN_TOK
1552     LPAREN_TOK (termList[heads,expr])? RPAREN_TOK
1553     term[body, expr2]
1554     {
1555       args.clear();
1556       /* heads */
1557       switch( heads.size() ){
1558       case 0:
1559         args.push_back(MK_CONST(bool(true))); break;
1560       case 1:
1561         args.push_back(heads[0]); break;
1562       default:
1563         expr2 = MK_EXPR(kind::AND, heads);
1564         args.push_back(expr2); break;
1565       };
1566       args.push_back(body);
1567       /* triggers */
1568       if( !triggers.empty() ){
1569         expr2 = MK_EXPR(kind::INST_PATTERN_LIST, triggers);
1570         args.push_back(expr2);
1571       };
1572       expr = MK_EXPR(kind, args);
1573       args.clear();
1574       args.push_back(bvl);
1575       /* guards */
1576       switch( guards.size() ){
1577       case 0:
1578         args.push_back(MK_CONST(bool(true))); break;
1579       case 1:
1580         args.push_back(guards[0]); break;
1581       default:
1582         expr2 = MK_EXPR(kind::AND, guards);
1583         args.push_back(expr2); break;
1584       };
1585       args.push_back(expr);
1586       expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
1587       cmd->reset(new AssertCommand(expr, false));
1588     }
1589   ;
1590
1591 rewritePropaKind[CVC4::Kind& kind]
1592   : REDUCTION_RULE_TOK    { $kind = CVC4::kind::RR_REDUCTION; }
1593   | PROPAGATION_RULE_TOK  { $kind = CVC4::kind::RR_DEDUCTION; }
1594   ;
1595
1596 pattern[CVC4::Expr& expr]
1597 @declarations {
1598   std::vector<Expr> patexpr;
1599 }
1600   : LPAREN_TOK termList[patexpr,expr] RPAREN_TOK
1601     {
1602       expr = MK_EXPR(kind::INST_PATTERN, patexpr);
1603     }
1604   ;
1605
1606 simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
1607 @declarations {
1608   CVC4::Kind k;
1609   std::string s;
1610   std::vector<unsigned int> s_vec;
1611 }
1612   : INTEGER_LITERAL
1613     { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
1614   | DECIMAL_LITERAL
1615     { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
1616   | HEX_LITERAL
1617     { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
1618       std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
1619       sexpr = SExpr(Integer(hexString, 16));
1620     }
1621   | BINARY_LITERAL
1622     { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
1623       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
1624       sexpr = SExpr(Integer(binString, 2));
1625     }
1626   | str[s,false]
1627     { sexpr = SExpr(s); }
1628 //  | LPAREN_TOK STRCST_TOK
1629 //      ( INTEGER_LITERAL {
1630 //      s_vec.push_back( atoi( AntlrInput::tokenText($INTEGER_LITERAL) ) + 65 );
1631 //    } )* RPAREN_TOK
1632 //   {
1633 //  sexpr = SExpr( MK_CONST( ::CVC4::String(s_vec) ) );
1634 //  }
1635   | symbol[s,CHECK_NONE,SYM_SORT]
1636     { sexpr = SExpr(SExpr::Keyword(s)); }
1637   | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK
1638         | DECLARE_SORT_TOK
1639         | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK
1640         | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK
1641         | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_ASSUMPTIONS_TOK
1642         | GET_UNSAT_CORE_TOK | EXIT_TOK
1643         | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK
1644         | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK
1645         | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK
1646         | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK)
1647     { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); }
1648   | builtinOp[k]
1649     { std::stringstream ss;
1650       ss << language::SetLanguage(CVC4::language::output::LANG_SMTLIB_V2_5)
1651          << EXPR_MANAGER->mkConst(k);
1652       sexpr = SExpr(ss.str());
1653     }
1654   ;
1655
1656 keyword[std::string& s]
1657   : KEYWORD
1658     { s = AntlrInput::tokenText($KEYWORD); }
1659   ;
1660
1661 simpleSymbolicExpr[CVC4::SExpr& sexpr]
1662   : simpleSymbolicExprNoKeyword[sexpr]
1663   | KEYWORD
1664     { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
1665   ;
1666
1667 symbolicExpr[CVC4::SExpr& sexpr]
1668 @declarations {
1669   std::vector<SExpr> children;
1670 }
1671   : simpleSymbolicExpr[sexpr]
1672   | LPAREN_TOK
1673     ( symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK
1674     { sexpr = SExpr(children); }
1675   ;
1676
1677 /**
1678  * Matches a term.
1679  * @return the expression representing the formula
1680  */
1681 term[CVC4::Expr& expr, CVC4::Expr& expr2]
1682 @init {
1683   std::string name;
1684 }
1685 : termNonVariable[expr, expr2]
1686     /* a variable */
1687   | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
1688     { expr = PARSER_STATE->getExpressionForName(name);
1689       assert( !expr.isNull() );
1690     }
1691   ;
1692
1693 /**
1694  * Matches a non-variable term.
1695  * @return the expression expr representing the term or formula, and expr2, an
1696  * optional annotation for expr (for instance, for attributed expressions).
1697  */
1698 termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
1699 @init {
1700   Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
1701   Kind kind = kind::NULL_EXPR;
1702   Expr op;
1703   std::string name, name2;
1704   std::vector<Expr> args;
1705   std::vector< std::pair<std::string, Type> > sortedVarNames;
1706   Expr f, f2, f3, f4;
1707   std::string attr;
1708   Expr attexpr;
1709   std::vector<Expr> patexprs;
1710   std::vector<Expr> patconds;
1711   std::unordered_set<std::string> names;
1712   std::vector< std::pair<std::string, Expr> > binders;
1713   bool isBuiltinOperator = false;
1714   bool isOverloadedFunction = false;
1715   bool readVariable = false;
1716   int match_vindex = -1;
1717   std::vector<Type> match_ptypes;
1718   Type type;
1719   Type type2;
1720   api::Term atomTerm;
1721 }
1722   : /* a built-in operator application */
1723     LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
1724     {
1725       if( !PARSER_STATE->strictModeEnabled() &&
1726           (kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
1727           args.size() == 1) {
1728         /* Unary AND/OR can be replaced with the argument.
1729          * It just so happens expr should already be the only argument. */
1730         assert( expr == args[0] );
1731       } else if( CVC4::kind::isAssociative(kind) &&
1732                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
1733         /* Special treatment for associative operators with lots of children */
1734         expr = EXPR_MANAGER->mkAssociative(kind, args);
1735       } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) {
1736         expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
1737       }
1738       else if ((kind == CVC4::kind::XOR || kind == CVC4::kind::MINUS
1739                 || kind == CVC4::kind::DIVISION)
1740                && args.size() > 2)
1741       {
1742         /* left-associative, but CVC4 internally only supports 2 args */
1743         expr = EXPR_MANAGER->mkLeftAssociative(kind,args);
1744       } else if( kind == CVC4::kind::IMPLIES && args.size() > 2 ) {
1745         /* right-associative, but CVC4 internally only supports 2 args */
1746         expr = EXPR_MANAGER->mkRightAssociative(kind,args);
1747       } else if( ( kind == CVC4::kind::EQUAL ||
1748                    kind == CVC4::kind::LT || kind == CVC4::kind::GT ||
1749                    kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) &&
1750                  args.size() > 2 ) {
1751         /* "chainable", but CVC4 internally only supports 2 args */
1752         expr = MK_EXPR(MK_CONST(Chain(kind)), args);
1753       } else if( PARSER_STATE->strictModeEnabled() && kind == CVC4::kind::ABS &&
1754                  args.size() == 1 && !args[0].getType().isInteger() ) {
1755         /* first, check that ABS is even defined in this logic */
1756         PARSER_STATE->checkOperator(kind, args.size());
1757         PARSER_STATE->parseError("abs can only be applied to Int, not Real, "
1758                                  "while in strict SMT-LIB compliance mode");
1759       } else {
1760         PARSER_STATE->checkOperator(kind, args.size());
1761         expr = MK_EXPR(kind, args);
1762       }
1763     }
1764   | LPAREN_TOK AS_TOK ( termNonVariable[f, f2] | symbol[name,CHECK_DECLARED,SYM_VARIABLE] { readVariable = true; } )
1765     sortSymbol[type, CHECK_DECLARED] RPAREN_TOK
1766     {
1767       if(readVariable) {
1768         Trace("parser-overloading") << "Getting variable expression of type " << name << " with type " << type << std::endl;
1769         // get the variable expression for the type
1770         f = PARSER_STATE->getExpressionForNameAndType(name, type);
1771         assert( !f.isNull() );
1772       }
1773       if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) {
1774         // could be a parametric type constructor or just an overloaded constructor
1775         if(((DatatypeType)type).isParametric()) {
1776           std::vector<CVC4::Expr> v;
1777           Expr e = f.getOperator();
1778           const DatatypeConstructor& dtc =
1779               Datatype::datatypeOf(e)[Datatype::indexOf(e)];
1780           v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
1781                                MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() ));
1782           v.insert(v.end(), f.begin(), f.end());
1783           expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
1784         }else{
1785           expr = f;
1786         }
1787       } else if(f.getKind() == CVC4::kind::EMPTYSET) {
1788         Debug("parser") << "Empty set encountered: " << f << " "
1789                           << f2 << " " << type <<  std::endl;
1790         expr = MK_CONST( ::CVC4::EmptySet(type) );
1791       } else if(f.getKind() == CVC4::kind::UNIVERSE_SET) {
1792         expr = EXPR_MANAGER->mkNullaryOperator(type, kind::UNIVERSE_SET);
1793       } else if(f.getKind() == CVC4::kind::SEP_NIL) {
1794         //We don't want the nil reference to be a constant: for instance, it
1795         //could be of type Int but is not a const rational. However, the
1796         //expression has 0 children. So we convert to a SEP_NIL variable.
1797         expr = EXPR_MANAGER->mkNullaryOperator(type, kind::SEP_NIL);
1798       } else {
1799         if(f.getType() != type) {
1800           PARSER_STATE->parseError("Type ascription not satisfied.");
1801         }else{
1802           expr = f;
1803         }
1804       }
1805     }
1806   | LPAREN_TOK quantOp[kind]
1807     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
1808     {
1809       PARSER_STATE->pushScope(true);
1810       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
1811             sortedVarNames.begin(), iend = sortedVarNames.end();
1812           i != iend;
1813           ++i) {
1814         args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
1815       }
1816       Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
1817       args.clear();
1818       args.push_back(bvl);
1819     }
1820     term[f, f2] RPAREN_TOK
1821     {
1822       PARSER_STATE->popScope();
1823       switch(f.getKind()) {
1824       case CVC4::kind::RR_REWRITE:
1825       case CVC4::kind::RR_REDUCTION:
1826       case CVC4::kind::RR_DEDUCTION:
1827         if(kind == CVC4::kind::EXISTS) {
1828           PARSER_STATE->parseError("Use Exists instead of Forall for a rewrite "
1829                                    "rule.");
1830         }
1831         args.push_back(f2); // guards
1832         args.push_back(f); // rule
1833         expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
1834         break;
1835       default:
1836         args.push_back(f);
1837         if(! f2.isNull()){
1838           args.push_back(f2);
1839         }
1840         expr = MK_EXPR(kind, args);
1841       }
1842     }
1843   | LPAREN_TOK functionName[name, CHECK_NONE]
1844     { isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
1845       if(isBuiltinOperator) {
1846         /* A built-in operator not already handled by the lexer */
1847         kind = PARSER_STATE->getOperatorKind(name);
1848       } else {
1849         /* A non-built-in function application */
1850         PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE);
1851         expr = PARSER_STATE->getVariable(name);
1852         if(!expr.isNull()) {
1853           //hack to allow constants with parentheses (disabled for now)
1854           //if( PARSER_STATE->sygus() && !PARSER_STATE->isFunctionLike(expr) ){
1855           //  op = PARSER_STATE->getVariable(name);
1856           //}else{
1857           PARSER_STATE->checkFunctionLike(expr);
1858           kind = PARSER_STATE->getKindForFunction(expr);
1859           args.push_back(expr);
1860         }else{
1861           isOverloadedFunction = true;
1862         }
1863       }
1864     }
1865     //(termList[args,expr])? RPAREN_TOK
1866     termList[args,expr] RPAREN_TOK
1867     { Debug("parser") << "args has size " << args.size() << std::endl
1868                       << "expr is " << expr << std::endl;
1869       for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) {
1870         Debug("parser") << "++ " << *i << std::endl;
1871       }
1872       if(isOverloadedFunction) {
1873         std::vector< Type > argTypes;
1874         for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) {
1875           argTypes.push_back( (*i).getType() );
1876         }
1877         expr = PARSER_STATE->getOverloadedFunctionForTypes(name, argTypes);
1878         if(!expr.isNull()) {
1879           PARSER_STATE->checkFunctionLike(expr);
1880           kind = PARSER_STATE->getKindForFunction(expr);
1881           args.insert(args.begin(),expr);
1882         }else{
1883           PARSER_STATE->parseError("Cannot find unambiguous overloaded function for argument types.");
1884         }
1885       }
1886       Kind lassocKind = CVC4::kind::UNDEFINED_KIND;
1887       if (args.size() >= 2)
1888       {
1889         if (kind == CVC4::kind::INTS_DIVISION)
1890         {
1891           // Builtin operators that are not tokenized, are left associative,
1892           // but not internally variadic must set this.
1893           lassocKind = kind;
1894         }
1895         else
1896         {
1897           // may be partially applied function, in this case we use HO_APPLY
1898           Type argt = args[0].getType();
1899           if (argt.isFunction())
1900           {
1901             unsigned arity = static_cast<FunctionType>(argt).getArity();
1902             if (args.size() - 1 < arity)
1903             {
1904               Debug("parser") << "Partial application of " << args[0];
1905               Debug("parser") << " : #argTypes = " << arity;
1906               Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
1907               // must curry the partial application
1908               lassocKind = CVC4::kind::HO_APPLY;
1909             }
1910           }
1911         }
1912       }
1913       if (lassocKind != CVC4::kind::UNDEFINED_KIND)
1914       {
1915         expr = EXPR_MANAGER->mkLeftAssociative(lassocKind, args);
1916       }
1917       else
1918       {
1919         if (isBuiltinOperator)
1920         {
1921           PARSER_STATE->checkOperator(kind, args.size());
1922         }
1923         expr = MK_EXPR(kind, args);
1924       }
1925     }
1926   | LPAREN_TOK
1927     ( /* An indexed function application */
1928       indexedFunctionName[op, kind] termList[args,expr] RPAREN_TOK {
1929         if(kind==CVC4::kind::APPLY_SELECTOR) {
1930           //tuple selector case
1931           Integer x = op.getConst<CVC4::Rational>().getNumerator();
1932           if (!x.fitsUnsignedInt()) {
1933             PARSER_STATE->parseError("index of tupSel is larger than size of unsigned int");
1934           }
1935           unsigned int n = x.toUnsignedInt();
1936           if (args.size()>1) {
1937             PARSER_STATE->parseError("tupSel applied to more than one tuple argument");
1938           }
1939           Type t = args[0].getType();
1940           if (!t.isTuple()) {
1941             PARSER_STATE->parseError("tupSel applied to non-tuple");
1942           }
1943           size_t length = ((DatatypeType)t).getTupleLength();
1944           if (n >= length) {
1945             std::stringstream ss;
1946             ss << "tuple is of length " << length << "; cannot access index " << n;
1947             PARSER_STATE->parseError(ss.str());
1948           }
1949           const Datatype & dt = ((DatatypeType)t).getDatatype();
1950           op = dt[0][n].getSelector();
1951         }
1952         if (kind!=kind::NULL_EXPR) {
1953           expr = MK_EXPR( kind, op, args );
1954         } else {
1955           expr = MK_EXPR(op, args);
1956         }
1957         PARSER_STATE->checkOperator(expr.getKind(), args.size());
1958       }
1959     | /* Array constant (in Z3 syntax) */
1960       LPAREN_TOK AS_TOK CONST_TOK sortSymbol[type, CHECK_DECLARED]
1961       RPAREN_TOK term[f, f2] RPAREN_TOK
1962       {
1963         if(!type.isArray()) {
1964           std::stringstream ss;
1965           ss << "expected array constant term, but cast is not of array type"
1966              << std::endl
1967              << "cast type: " << type;
1968           PARSER_STATE->parseError(ss.str());
1969         }
1970         if(!f.isConst()) {
1971           std::stringstream ss;
1972           ss << "expected constant term inside array constant, but found "
1973              << "nonconstant term:" << std::endl
1974              << "the term: " << f;
1975           PARSER_STATE->parseError(ss.str());
1976         }
1977         if(!ArrayType(type).getConstituentType().isComparableTo(f.getType())) {
1978           std::stringstream ss;
1979           ss << "type mismatch inside array constant term:" << std::endl
1980              << "array type:          " << type << std::endl
1981              << "expected const type: " << ArrayType(type).getConstituentType()
1982              << std::endl
1983              << "computed const type: " << f.getType();
1984           PARSER_STATE->parseError(ss.str());
1985         }
1986         expr = MK_CONST( ::CVC4::ArrayStoreAll(type, f) );
1987       }
1988     )
1989   | /* a let or sygus let binding */
1990     LPAREN_TOK (
1991       LET_TOK LPAREN_TOK
1992       { PARSER_STATE->pushScope(true); }
1993       ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
1994         term[expr, f2]
1995         RPAREN_TOK
1996         // this is a parallel let, so we have to save up all the contributions
1997         // of the let and define them only later on
1998         { if(names.count(name) == 1) {
1999             std::stringstream ss;
2000             ss << "warning: symbol `" << name << "' bound multiple times by let;"
2001                << " the last binding will be used, shadowing earlier ones";
2002             PARSER_STATE->warning(ss.str());
2003           } else {
2004             names.insert(name);
2005           }
2006           binders.push_back(std::make_pair(name, expr)); } )+ |
2007       SYGUS_LET_TOK LPAREN_TOK
2008       { PARSER_STATE->pushScope(true); }
2009       ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
2010         sortSymbol[type,CHECK_DECLARED]
2011         term[expr, f2]
2012         RPAREN_TOK
2013         // this is a parallel let, so we have to save up all the contributions
2014         // of the let and define them only later on
2015         { if(names.count(name) == 1) {
2016             std::stringstream ss;
2017             ss << "warning: symbol `" << name << "' bound multiple times by let;"
2018                << " the last binding will be used, shadowing earlier ones";
2019             PARSER_STATE->warning(ss.str());
2020           } else {
2021             names.insert(name);
2022           }
2023           binders.push_back(std::make_pair(name, expr)); } )+ )
2024     { // now implement these bindings
2025       for(std::vector< std::pair<std::string, Expr> >::iterator
2026             i = binders.begin(); i != binders.end(); ++i) {
2027         PARSER_STATE->defineVar((*i).first, (*i).second);
2028       }
2029     }
2030     RPAREN_TOK
2031     term[expr, f2]
2032     RPAREN_TOK
2033     { PARSER_STATE->popScope(); }
2034   | /* match expression */
2035     LPAREN_TOK MATCH_TOK term[expr, f2] {
2036       if( !expr.getType().isDatatype() ){
2037         PARSER_STATE->parseError("Cannot match on non-datatype term.");
2038       }
2039     }
2040     LPAREN_TOK
2041     (
2042       /* match cases */
2043        LPAREN_TOK INDEX_TOK term[f, f2] {
2044           if( match_vindex==-1 ){
2045             match_vindex = (int)patexprs.size();
2046           }
2047           patexprs.push_back( f );
2048           patconds.push_back(MK_CONST(bool(true)));
2049         }
2050         RPAREN_TOK
2051       | LPAREN_TOK LPAREN_TOK term[f, f2] {
2052            args.clear();
2053            PARSER_STATE->pushScope(true);
2054            //f should be a constructor
2055            type = f.getType();
2056            Debug("parser-dt") << "Pattern head : " << f << " " << f.getType() << std::endl;
2057            if( !type.isConstructor() ){
2058              PARSER_STATE->parseError("Pattern must be application of a constructor or a variable.");
2059            }
2060            if( Datatype::datatypeOf(f).isParametric() ){
2061              type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType());
2062            }
2063            match_ptypes = ((ConstructorType)type).getArgTypes();
2064          }
2065          //arguments
2066          ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
2067              if( args.size()>=match_ptypes.size() ){
2068                PARSER_STATE->parseError("Too many arguments for pattern.");
2069              }
2070              //make of proper type
2071              Expr arg = PARSER_STATE->mkBoundVar(name, match_ptypes[args.size()]);
2072              args.push_back( arg );
2073            }
2074          )*
2075          RPAREN_TOK
2076          term[f3, f2] {
2077            const DatatypeConstructor& dtc = Datatype::datatypeOf(f)[Datatype::indexOf(f)];
2078            if( args.size()!=dtc.getNumArgs() ){
2079              PARSER_STATE->parseError("Bad number of arguments for application of constructor in pattern.");
2080            }
2081            //FIXME: make MATCH a kind and make this a rewrite
2082            // build a lambda
2083            std::vector<Expr> largs;
2084            largs.push_back( MK_EXPR( CVC4::kind::BOUND_VAR_LIST, args ) );
2085            largs.push_back( f3 );
2086            std::vector< Expr > aargs;
2087            aargs.push_back( MK_EXPR( CVC4::kind::LAMBDA, largs ) );
2088            for( unsigned i=0; i<dtc.getNumArgs(); i++ ){
2089              //can apply total version since we will be guarded by ITE condition
2090              // however, we need to apply partial version since we don't have the internal selector available
2091              aargs.push_back( MK_EXPR( CVC4::kind::APPLY_SELECTOR, dtc[i].getSelector(), expr ) );
2092            }
2093            patexprs.push_back( MK_EXPR( CVC4::kind::APPLY, aargs ) );
2094            patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) );
2095          }
2096          RPAREN_TOK
2097          { PARSER_STATE->popScope(); }
2098        | LPAREN_TOK symbol[name,CHECK_DECLARED,SYM_VARIABLE] {
2099            f = PARSER_STATE->getVariable(name);
2100            type = f.getType();
2101            if( !type.isConstructor() || !((ConstructorType)type).getArgTypes().empty() ){
2102              PARSER_STATE->parseError("Must apply constructors of arity greater than 0 to arguments in pattern.");
2103            }
2104          }
2105          term[f3, f2] {
2106            const DatatypeConstructor& dtc = Datatype::datatypeOf(f)[Datatype::indexOf(f)];
2107            patexprs.push_back( f3 );
2108            patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) );
2109          }
2110          RPAREN_TOK
2111     )+
2112     RPAREN_TOK RPAREN_TOK  {
2113       if( match_vindex==-1 ){
2114         const Datatype& dt = ((DatatypeType)expr.getType()).getDatatype();
2115         std::map< unsigned, bool > processed;
2116         unsigned count = 0;
2117         //ensure that all datatype constructors are matched (to ensure exhaustiveness)
2118         for( unsigned i=0; i<patconds.size(); i++ ){
2119           unsigned curr_index = Datatype::indexOf(patconds[i].getOperator());
2120           if( curr_index<0 && curr_index>=dt.getNumConstructors() ){
2121             PARSER_STATE->parseError("Pattern is not legal for the head of a match.");
2122           }
2123           if( processed.find( curr_index )==processed.end() ){
2124             processed[curr_index] = true;
2125             count++;
2126           }
2127         }
2128         if( count!=dt.getNumConstructors() ){
2129           PARSER_STATE->parseError("Patterns are not exhaustive in a match construct.");
2130         }
2131       }
2132       //now, make the ITE
2133       int end_index = match_vindex==-1 ? patexprs.size()-1 : match_vindex;
2134       bool first_time = true;
2135       for( int index = end_index; index>=0; index-- ){
2136         if( first_time ){
2137           expr = patexprs[index];
2138           first_time = false;
2139         }else{
2140           expr = MK_EXPR( CVC4::kind::ITE, patconds[index], patexprs[index], expr );
2141         }
2142       }
2143     }
2144
2145     /* attributed expressions */
2146   | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
2147     ( attribute[expr, attexpr, attr]
2148       { if( ! attexpr.isNull()) {
2149           patexprs.push_back( attexpr );
2150         }
2151       }
2152     )+ RPAREN_TOK
2153     {
2154       if(attr == ":rewrite-rule") {
2155         Expr guard;
2156         Expr body;
2157         if(expr[1].getKind() == kind::IMPLIES ||
2158            expr[1].getKind() == kind::EQUAL) {
2159           guard = expr[0];
2160           body = expr[1];
2161         } else {
2162           guard = MK_CONST(bool(true));
2163           body = expr;
2164         }
2165         expr2 = guard;
2166         args.push_back(body[0]);
2167         args.push_back(body[1]);
2168         if(!f2.isNull()) {
2169           args.push_back(f2);
2170         }
2171
2172         if( body.getKind()==kind::IMPLIES ){
2173           kind = kind::RR_DEDUCTION;
2174         }else if( body.getKind()==kind::EQUAL ){
2175           kind = body[0].getType().isBoolean() ? kind::RR_REDUCTION : kind::RR_REWRITE;
2176         }else{
2177           PARSER_STATE->parseError("Error parsing rewrite rule.");
2178         }
2179         expr = MK_EXPR( kind, args );
2180       } else if(! patexprs.empty()) {
2181         if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){
2182           for( size_t i=0; i<f2.getNumChildren(); i++ ){
2183             if( f2[i].getKind()==kind::INST_PATTERN ){
2184               patexprs.push_back( f2[i] );
2185             }else{
2186               std::stringstream ss;
2187               ss << "warning: rewrite rules do not support " << f2[i]
2188                  << " within instantiation pattern list";
2189               PARSER_STATE->warning(ss.str());
2190             }
2191           }
2192         }
2193         expr2 = MK_EXPR(kind::INST_PATTERN_LIST, patexprs);
2194       } else {
2195         expr2 = f2;
2196       }
2197     }
2198   | /* lambda */
2199     LPAREN_TOK HO_LAMBDA_TOK
2200     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
2201     {
2202       PARSER_STATE->pushScope(true);
2203       for(const std::pair<std::string, CVC4::Type>& svn : sortedVarNames){
2204         args.push_back(PARSER_STATE->mkBoundVar(svn.first, svn.second));
2205       }
2206       Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
2207       args.clear();
2208       args.push_back(bvl);
2209     }
2210     term[f, f2] RPAREN_TOK
2211     {
2212       args.push_back( f );
2213       PARSER_STATE->popScope();
2214       expr = MK_EXPR( CVC4::kind::LAMBDA, args );
2215     }
2216
2217   | LPAREN_TOK TUPLE_CONST_TOK termList[args,expr] RPAREN_TOK
2218   {
2219     std::vector<api::Sort> sorts;
2220     std::vector<api::Term> terms;
2221     for (const Expr& arg : args)
2222     {
2223       sorts.emplace_back(arg.getType());
2224       terms.emplace_back(arg);
2225     }
2226     expr = SOLVER->mkTuple(sorts, terms).getExpr();
2227   }
2228   | /* an atomic term (a term with no subterms) */
2229     termAtomic[atomTerm] { expr = atomTerm.getExpr(); }
2230   ;
2231
2232
2233 /**
2234  * Matches an atomic term (a term with no subterms).
2235  * @return the expression expr representing the term or formula.
2236  */
2237 termAtomic[CVC4::api::Term& atomTerm]
2238 @init {
2239   Type type;
2240   Type type2;
2241   std::string s;
2242 }
2243     /* constants */
2244   : INTEGER_LITERAL
2245     {
2246       std::string intStr = AntlrInput::tokenText($INTEGER_LITERAL);
2247       atomTerm = SOLVER->mkReal(intStr);
2248     }
2249   | DECIMAL_LITERAL
2250     {
2251       std::string realStr = AntlrInput::tokenText($DECIMAL_LITERAL);
2252       atomTerm = SOLVER->ensureTermSort(SOLVER->mkReal(realStr),
2253                                         SOLVER->getRealSort());
2254     }
2255
2256   // Pi constant
2257   | REAL_PI_TOK { atomTerm = SOLVER->mkPi(); }
2258
2259   // Constants using indexed identifiers, e.g. (_ +oo 8 24) (positive infinity
2260   // as a 32-bit floating-point constant)
2261   | LPAREN_TOK INDEX_TOK
2262     ( bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL
2263       {
2264         if(AntlrInput::tokenText($bvLit).find("bv") == 0)
2265         {
2266           std::string bvStr = AntlrInput::tokenTextSubstr($bvLit, 2);
2267           uint32_t bvSize = AntlrInput::tokenToUnsigned($size);
2268           atomTerm = SOLVER->mkBitVector(bvSize, bvStr, 10);
2269         }
2270         else
2271         {
2272            PARSER_STATE->parseError("Unexpected symbol `" +
2273                                     AntlrInput::tokenText($bvLit) + "'");
2274         }
2275       }
2276
2277     // Floating-point constants
2278     | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2279       {
2280         atomTerm = SOLVER->mkPosInf(AntlrInput::tokenToUnsigned($eb),
2281                                 AntlrInput::tokenToUnsigned($sb));
2282       }
2283     | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2284       {
2285         atomTerm = SOLVER->mkNegInf(AntlrInput::tokenToUnsigned($eb),
2286                                 AntlrInput::tokenToUnsigned($sb));
2287       }
2288     | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2289       {
2290         atomTerm = SOLVER->mkNaN(AntlrInput::tokenToUnsigned($eb),
2291                              AntlrInput::tokenToUnsigned($sb));
2292       }
2293     | FP_PZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2294       {
2295         atomTerm = SOLVER->mkPosZero(AntlrInput::tokenToUnsigned($eb),
2296                                  AntlrInput::tokenToUnsigned($sb));
2297       }
2298     | FP_NZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2299       {
2300         atomTerm = SOLVER->mkNegZero(AntlrInput::tokenToUnsigned($eb),
2301                                  AntlrInput::tokenToUnsigned($sb));
2302       }
2303
2304     // Empty heap constant in seperation logic
2305     | EMP_TOK
2306       sortSymbol[type,CHECK_DECLARED]
2307       sortSymbol[type2,CHECK_DECLARED]
2308       {
2309         api::Term v1 = SOLVER->mkVar("_emp1", api::Sort(type));
2310         api::Term v2 = SOLVER->mkVar("_emp2", api::Sort(type2));
2311         atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2);
2312       }
2313
2314     // NOTE: Theory parametric constants go here
2315     )
2316     RPAREN_TOK
2317
2318   // Bit-vector constants
2319   | HEX_LITERAL
2320   {
2321     assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0);
2322     std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
2323     atomTerm = SOLVER->mkBitVector(hexStr, 16);
2324     }
2325   | BINARY_LITERAL
2326     {
2327       assert(AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0);
2328       std::string binStr = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
2329       atomTerm = SOLVER->mkBitVector(binStr, 2);
2330     }
2331
2332   // Floating-point rounding mode constants
2333   | FP_RNE_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN); }
2334   | FP_RNA_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY); }
2335   | FP_RTP_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_POSITIVE); }
2336   | FP_RTN_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE); }
2337   | FP_RTZ_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_ZERO); }
2338   | FP_RNE_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN); }
2339   | FP_RNA_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY); }
2340   | FP_RTP_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_POSITIVE); }
2341   | FP_RTN_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE); }
2342   | FP_RTZ_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_ZERO); }
2343
2344   // String constant
2345   | str[s,false] { atomTerm = SOLVER->mkString(s, true); }
2346
2347   // Regular expression constants
2348   | RENOSTR_TOK { atomTerm = SOLVER->mkRegexpEmpty(); }
2349   | REALLCHAR_TOK { atomTerm = SOLVER->mkRegexpSigma(); }
2350
2351   // Set constants
2352   | EMPTYSET_TOK { atomTerm = SOLVER->mkEmptySet(SOLVER->getNullSort()); }
2353   | UNIVSET_TOK
2354     {
2355       // the Boolean sort is a placeholder here since we don't have type info
2356       // without type annotation
2357       atomTerm = SOLVER->mkUniverseSet(SOLVER->getBooleanSort());
2358     }
2359
2360   // Separation logic constants
2361   | NILREF_TOK
2362     {
2363       // the Boolean sort is a placeholder here since we don't have type info
2364       // without type annotation
2365       atomTerm = SOLVER->mkSepNil(SOLVER->getBooleanSort());
2366     }
2367
2368   // NOTE: Theory constants go here
2369
2370   // Empty tuple constant
2371   | TUPLE_CONST_TOK
2372     {
2373       atomTerm = SOLVER->mkTuple(std::vector<api::Sort>(),
2374                                  std::vector<api::Term>());
2375     }
2376   ;
2377
2378 /**
2379  * Read attribute
2380  */
2381 attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr]
2382 @init {
2383   SExpr sexpr;
2384   Expr patexpr;
2385   std::vector<Expr> patexprs;
2386   Expr e2;
2387   bool hasValue = false;
2388 }
2389   : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )?
2390   {
2391     attr = AntlrInput::tokenText($KEYWORD);
2392     // EXPR_MANAGER->setNamedAttribute( expr, attr );
2393     if(attr == ":rewrite-rule") {
2394       if(hasValue) {
2395         std::stringstream ss;
2396         ss << "warning: Attribute " << attr
2397            << " does not take a value (ignoring)";
2398         PARSER_STATE->warning(ss.str());
2399       }
2400       // do nothing
2401     }
2402     else if (attr==":axiom" || attr==":conjecture" || attr==":fun-def")
2403     {
2404       if(hasValue) {
2405         std::stringstream ss;
2406         ss << "warning: Attribute " << attr
2407            << " does not take a value (ignoring)";
2408         PARSER_STATE->warning(ss.str());
2409       }
2410       Expr avar;
2411       bool success = true;
2412       std::string attr_name = attr;
2413       attr_name.erase( attr_name.begin() );
2414       if( attr==":fun-def" ){
2415         if( expr.getKind()!=kind::EQUAL || expr[0].getKind()!=kind::APPLY_UF ){
2416           success = false;
2417         }else{
2418           FunctionType t = (FunctionType)expr[0].getOperator().getType();
2419           for( unsigned i=0; i<expr[0].getNumChildren(); i++ ){
2420             if( expr[0][i].getKind() != kind::BOUND_VARIABLE ||
2421                 expr[0][i].getType() != t.getArgTypes()[i] ){
2422               success = false;
2423               break;
2424             }else{
2425               for( unsigned j=0; j<i; j++ ){
2426                 if( expr[0][j]==expr[0][i] ){
2427                   success = false;
2428                   break;
2429                 }
2430               }
2431             }
2432           }
2433         }
2434         if( !success ){
2435           std::stringstream ss;
2436           ss << "warning: Function definition should be an equality whose LHS "
2437              << "is an uninterpreted function applied to unique variables.";
2438           PARSER_STATE->warning(ss.str());
2439         }else{
2440           avar = expr[0];
2441         }
2442       }else{
2443         Type t = EXPR_MANAGER->booleanType();
2444         avar = PARSER_STATE->mkVar(attr_name, t);
2445       }
2446       if( success ){
2447         //Will set the attribute on auxiliary var (preserves attribute on
2448         //formula through rewriting).
2449         retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
2450         Command* c = new SetUserAttributeCommand( attr_name, avar );
2451         c->setMuted(true);
2452         PARSER_STATE->preemptCommand(c);
2453       }
2454     } else {
2455       PARSER_STATE->attributeNotSupported(attr);
2456     }
2457   }
2458   | ATTRIBUTE_PATTERN_TOK LPAREN_TOK
2459     ( term[patexpr, e2]
2460       { patexprs.push_back( patexpr ); }
2461     )+ RPAREN_TOK
2462     {
2463       attr = std::string(":pattern");
2464       retExpr = MK_EXPR(kind::INST_PATTERN, patexprs);
2465     }
2466   | ATTRIBUTE_NO_PATTERN_TOK term[patexpr, e2]
2467     {
2468       attr = std::string(":no-pattern");
2469       retExpr = MK_EXPR(kind::INST_NO_PATTERN, patexpr);
2470     }
2471   | tok=( ATTRIBUTE_INST_LEVEL | ATTRIBUTE_RR_PRIORITY ) INTEGER_LITERAL
2472     {
2473       Expr n = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) );
2474       std::vector<Expr> values;
2475       values.push_back( n );
2476       std::string attr_name(AntlrInput::tokenText($tok));
2477       attr_name.erase( attr_name.begin() );
2478       Type t = EXPR_MANAGER->booleanType();
2479       Expr avar = PARSER_STATE->mkVar(attr_name, t);
2480       retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
2481       Command* c = new SetUserAttributeCommand( attr_name, avar, values );
2482       c->setMuted(true);
2483       PARSER_STATE->preemptCommand(c);
2484     }
2485   | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
2486     {
2487       attr = std::string(":named");
2488       if(!sexpr.isKeyword()) {
2489         PARSER_STATE->parseError("improperly formed :named annotation");
2490       }
2491       std::string name = sexpr.getValue();
2492       PARSER_STATE->checkUserSymbol(name);
2493       // ensure expr is a closed subterm
2494       std::set<Expr> freeVars;
2495       if(!isClosed(expr, freeVars)) {
2496         assert(!freeVars.empty());
2497         std::stringstream ss;
2498         ss << ":named annotations can only name terms that are closed; this "
2499            << "one contains free variables:";
2500         for(std::set<Expr>::const_iterator i = freeVars.begin();
2501             i != freeVars.end(); ++i) {
2502           ss << " " << *i;
2503         }
2504         PARSER_STATE->parseError(ss.str());
2505       }
2506       // check that sexpr is a fresh function symbol, and reserve it
2507       PARSER_STATE->reserveSymbolAtAssertionLevel(name);
2508       // define it
2509       Expr func = PARSER_STATE->mkFunction(name, expr.getType());
2510       // remember the last term to have been given a :named attribute
2511       PARSER_STATE->setLastNamedTerm(expr, name);
2512       // bind name to expr with define-fun
2513       Command* c =
2514         new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
2515       c->setMuted(true);
2516       PARSER_STATE->preemptCommand(c);
2517     }
2518   ;
2519
2520 /**
2521  * Matches a bit-vector operator (the ones parametrized by numbers)
2522  */
2523 indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind]
2524 @init {
2525   Expr expr;
2526   Expr expr2;
2527 }
2528   : LPAREN_TOK INDEX_TOK
2529     ( 'extract' n1=INTEGER_LITERAL n2=INTEGER_LITERAL
2530       { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1),
2531                                        AntlrInput::tokenToUnsigned($n2))); }
2532     | 'repeat' n=INTEGER_LITERAL
2533       { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
2534     | 'zero_extend' n=INTEGER_LITERAL
2535       { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
2536     | 'sign_extend' n=INTEGER_LITERAL
2537       { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); }
2538     | 'rotate_left' n=INTEGER_LITERAL
2539       { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
2540     | 'rotate_right' n=INTEGER_LITERAL
2541       { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
2542     | DIVISIBLE_TOK n=INTEGER_LITERAL
2543       { op = MK_CONST(Divisible(AntlrInput::tokenToUnsigned($n))); }
2544     | INT2BV_TOK n=INTEGER_LITERAL
2545       { op = MK_CONST(IntToBitVector(AntlrInput::tokenToUnsigned($n)));
2546         if(PARSER_STATE->strictModeEnabled()) {
2547           PARSER_STATE->parseError(
2548               "bv2nat and int2bv are not part of SMT-LIB, and aren't available "
2549               "in SMT-LIB strict compliance mode");
2550         } }
2551     | FP_TO_FP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2552       { op = MK_CONST(FloatingPointToFPGeneric(
2553                 AntlrInput::tokenToUnsigned($eb),
2554                 AntlrInput::tokenToUnsigned($sb)));
2555       }
2556     | FP_TO_FPBV_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2557       { op = MK_CONST(FloatingPointToFPIEEEBitVector(
2558                 AntlrInput::tokenToUnsigned($eb),
2559                 AntlrInput::tokenToUnsigned($sb)));
2560       }
2561     | FP_TO_FPFP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2562       { op = MK_CONST(FloatingPointToFPFloatingPoint(
2563                 AntlrInput::tokenToUnsigned($eb),
2564                 AntlrInput::tokenToUnsigned($sb)));
2565       }
2566     | FP_TO_FPR_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2567       { op = MK_CONST(FloatingPointToFPReal(AntlrInput::tokenToUnsigned($eb),
2568                                             AntlrInput::tokenToUnsigned($sb)));
2569       }
2570     | FP_TO_FPS_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2571       { op = MK_CONST(FloatingPointToFPSignedBitVector(
2572                 AntlrInput::tokenToUnsigned($eb),
2573                 AntlrInput::tokenToUnsigned($sb)));
2574       }
2575     | FP_TO_FPU_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
2576       { op = MK_CONST(FloatingPointToFPUnsignedBitVector(
2577                 AntlrInput::tokenToUnsigned($eb),
2578                 AntlrInput::tokenToUnsigned($sb)));
2579       }
2580     | FP_TO_UBV_TOK m=INTEGER_LITERAL
2581       { op = MK_CONST(FloatingPointToUBV(AntlrInput::tokenToUnsigned($m))); }
2582     | FP_TO_SBV_TOK m=INTEGER_LITERAL
2583       { op = MK_CONST(FloatingPointToSBV(AntlrInput::tokenToUnsigned($m))); }
2584     | TESTER_TOK term[expr, expr2] {
2585         if( expr.getKind()==kind::APPLY_CONSTRUCTOR && expr.getNumChildren()==0 ){
2586           //for nullary constructors, must get the operator
2587           expr = expr.getOperator();
2588         }
2589         if( !expr.getType().isConstructor() ){
2590           PARSER_STATE->parseError("Bad syntax for test (_ is X), X must be a constructor.");
2591         }
2592         op = Datatype::datatypeOf(expr)[Datatype::indexOf(expr)].getTester();
2593         kind = CVC4::kind::APPLY_TESTER;
2594       }
2595     | TUPLE_SEL_TOK m=INTEGER_LITERAL {
2596         kind = CVC4::kind::APPLY_SELECTOR;
2597         //put m in op so that the caller (termNonVariable) can deal with this case
2598         op = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m)));
2599       }
2600     | badIndexedFunctionName
2601     )
2602     RPAREN_TOK
2603   ;
2604
2605 /**
2606  * Matches an erroneous indexed function name (and args) for better
2607  * error reporting.
2608  */
2609 badIndexedFunctionName
2610 @declarations {
2611   std::string name;
2612 }
2613   : id=(SIMPLE_SYMBOL | QUOTED_SYMBOL | UNTERMINATED_QUOTED_SYMBOL)
2614     { PARSER_STATE->parseError(std::string("Unknown indexed function `") +
2615           AntlrInput::tokenText($id) + "'");
2616     }
2617   ;
2618
2619 /**
2620  * Matches a sequence of terms and puts them into the formulas
2621  * vector.
2622  * @param formulas the vector to fill with terms
2623  * @param expr an Expr reference for the elements of the sequence
2624  */
2625 /* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
2626  * time through this rule. */
2627 termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
2628 @declarations {
2629   Expr expr2;
2630 }
2631   : ( term[expr, expr2] { formulas.push_back(expr); } )+
2632   ;
2633
2634 /**
2635  * Matches a string, and strips off the quotes.
2636  */
2637 str[std::string& s, bool fsmtlib]
2638   : STRING_LITERAL
2639     {
2640       s = AntlrInput::tokenText($STRING_LITERAL);
2641       /* strip off the quotes */
2642       s = s.substr(1, s.size() - 2);
2643       for (size_t i = 0; i < s.size(); i++)
2644       {
2645         if ((unsigned)s[i] > 127 && !isprint(s[i]))
2646         {
2647           PARSER_STATE->parseError(
2648               "Extended/unprintable characters are not "
2649               "part of SMT-LIB, and they must be encoded "
2650               "as escape sequences");
2651         }
2652       }
2653       if (fsmtlib || PARSER_STATE->escapeDupDblQuote())
2654       {
2655         char* p_orig = strdup(s.c_str());
2656         char *p = p_orig, *q = p_orig;
2657         while (*q != '\0')
2658         {
2659           if (PARSER_STATE->escapeDupDblQuote() && *q == '"')
2660           {
2661             // Handle SMT-LIB >=2.5 standard escape '""'.
2662             ++q;
2663             assert(*q == '"');
2664           }
2665           else if (!PARSER_STATE->escapeDupDblQuote() && *q == '\\')
2666           {
2667             ++q;
2668             // Handle SMT-LIB 2.0 standard escapes '\\' and '\"'.
2669             if (*q != '\\' && *q != '"')
2670             {
2671               assert(*q != '\0');
2672               *p++ = '\\';
2673             }
2674           }
2675           *p++ = *q++;
2676         }
2677         *p = '\0';
2678         s = p_orig;
2679         free(p_orig);
2680       }
2681     }
2682   ;
2683
2684 /**
2685  * Matches a builtin operator symbol and sets kind to its associated Expr kind.
2686  */
2687 builtinOp[CVC4::Kind& kind]
2688 @init {
2689   Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
2690 }
2691   : NOT_TOK      { $kind = CVC4::kind::NOT;     }
2692   | IMPLIES_TOK  { $kind = CVC4::kind::IMPLIES; }
2693   | AND_TOK      { $kind = CVC4::kind::AND;     }
2694   | OR_TOK       { $kind = CVC4::kind::OR;      }
2695   | XOR_TOK      { $kind = CVC4::kind::XOR;     }
2696   | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
2697   | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
2698   | ITE_TOK      { $kind = CVC4::kind::ITE; }
2699   | GREATER_THAN_TOK
2700                  { $kind = CVC4::kind::GT; }
2701   | GREATER_THAN_EQUAL_TOK
2702                  { $kind = CVC4::kind::GEQ; }
2703   | LESS_THAN_EQUAL_TOK
2704                  { $kind = CVC4::kind::LEQ; }
2705   | LESS_THAN_TOK
2706                  { $kind = CVC4::kind::LT; }
2707   | PLUS_TOK     { $kind = CVC4::kind::PLUS; }
2708   | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
2709   | STAR_TOK     { $kind = CVC4::kind::MULT; }
2710   | DIV_TOK      { $kind = CVC4::kind::DIVISION; }
2711
2712   | BV2NAT_TOK
2713     { $kind = CVC4::kind::BITVECTOR_TO_NAT;
2714       if(PARSER_STATE->strictModeEnabled()) {
2715         PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, "
2716                                  "and aren't available in SMT-LIB strict "
2717                                  "compliance mode");
2718       }
2719     }
2720
2721   | DTSIZE_TOK       { $kind = CVC4::kind::DT_SIZE; }
2722   | FMFCARD_TOK      { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; }
2723   | FMFCARDVAL_TOK   { $kind = CVC4::kind::CARDINALITY_VALUE; }
2724   | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; }
2725
2726   // NOTE: Theory operators no longer go here, add to smt2.cpp. Only
2727   // special cases may go here. When this comment was written (2015
2728   // Apr), the special cases were: core theory operators, arith
2729   // operators which start with symbols like * / + >= etc, quantifier
2730   // theory operators, and operators which depended on parser's state
2731   // to accept or reject.
2732   ;
2733
2734 quantOp[CVC4::Kind& kind]
2735 @init {
2736   Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
2737 }
2738   : EXISTS_TOK    { $kind = CVC4::kind::EXISTS; }
2739   | FORALL_TOK    { $kind = CVC4::kind::FORALL; }
2740   ;
2741
2742 /**
2743  * Matches a (possibly undeclared) function symbol (returning the string)
2744  * @param check what kind of check to do with the symbol
2745  */
2746 functionName[std::string& name, CVC4::parser::DeclarationCheck check]
2747   : symbol[name,check,SYM_VARIABLE]
2748   ;
2749
2750 /**
2751  * Matches a sequence of sort symbols and fills them into the given
2752  * vector.
2753  */
2754 sortList[std::vector<CVC4::Type>& sorts]
2755 @declarations {
2756   Type t;
2757 }
2758   : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
2759   ;
2760
2761 nonemptySortList[std::vector<CVC4::Type>& sorts]
2762 @declarations {
2763   Type t;
2764 }
2765   : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+
2766   ;
2767
2768 /**
2769  * Matches a sequence of (variable,sort) symbol pairs and fills them
2770  * into the given vector.
2771  */
2772 sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars]
2773 @declarations {
2774   std::string name;
2775   Type t;
2776 }
2777   : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
2778       sortSymbol[t,CHECK_DECLARED] RPAREN_TOK
2779       { sortedVars.push_back(make_pair(name, t)); }
2780     )*
2781   ;
2782
2783 /**
2784  * Matches the sort symbol, which can be an arbitrary symbol.
2785  * @param check the check to perform on the name
2786  */
2787 sortName[std::string& name, CVC4::parser::DeclarationCheck check]
2788   : symbol[name,check,SYM_SORT]
2789   ;
2790
2791 sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
2792 @declarations {
2793   std::string name;
2794   std::vector<CVC4::Type> args;
2795   std::vector<uint64_t> numerals;
2796   bool indexed = false;
2797 }
2798   : sortName[name,CHECK_NONE]
2799     {
2800       if(check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT)) {
2801         t = PARSER_STATE->getSort(name);
2802       } else {
2803         t = PARSER_STATE->mkUnresolvedType(name);
2804       }
2805     }
2806   | LPAREN_TOK (INDEX_TOK {indexed = true;} | {indexed = false;})
2807     symbol[name,CHECK_NONE,SYM_SORT]
2808     ( nonemptyNumeralList[numerals]
2809       { // allow sygus inputs to elide the `_'
2810         if( !indexed && !PARSER_STATE->sygus() ) {
2811           std::stringstream ss;
2812           ss << "SMT-LIB requires use of an indexed sort here, e.g. (_ " << name
2813              << " ...)";
2814           PARSER_STATE->parseError(ss.str());
2815         }
2816         if( name == "BitVec" ) {
2817           if( numerals.size() != 1 ) {
2818             PARSER_STATE->parseError("Illegal bitvector type.");
2819           }
2820           if(numerals.front() == 0) {
2821             PARSER_STATE->parseError("Illegal bitvector size: 0");
2822           }
2823           t = EXPR_MANAGER->mkBitVectorType(numerals.front());
2824         } else if ( name == "FloatingPoint" ) {
2825           if( numerals.size() != 2 ) {
2826             PARSER_STATE->parseError("Illegal floating-point type.");
2827           }
2828           if(!validExponentSize(numerals[0])) {
2829             PARSER_STATE->parseError("Illegal floating-point exponent size");
2830           }
2831           if(!validSignificandSize(numerals[1])) {
2832             PARSER_STATE->parseError("Illegal floating-point significand size");
2833           }
2834           t = EXPR_MANAGER->mkFloatingPointType(numerals[0],numerals[1]);
2835         } else {
2836           std::stringstream ss;
2837           ss << "unknown indexed sort symbol `" << name << "'";
2838           PARSER_STATE->parseError(ss.str());
2839         }
2840       }
2841     | sortList[args]
2842       { if( indexed ) {
2843           std::stringstream ss;
2844           ss << "Unexpected use of indexing operator `_' before `" << name
2845              << "', try leaving it out";
2846           PARSER_STATE->parseError(ss.str());
2847         }
2848         if(args.empty()) {
2849           PARSER_STATE->parseError("Extra parentheses around sort name not "
2850                                    "permitted in SMT-LIB");
2851         } else if(name == "Array" &&
2852            PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) ) {
2853           if(args.size() != 2) {
2854             PARSER_STATE->parseError("Illegal array type.");
2855           }
2856           t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
2857         } else if(name == "Set" &&
2858                   PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) ) {
2859           if(args.size() != 1) {
2860             PARSER_STATE->parseError("Illegal set type.");
2861           }
2862           t = EXPR_MANAGER->mkSetType( args[0] );
2863         } else if(name == "Tuple") {
2864           t = EXPR_MANAGER->mkTupleType(args);
2865         } else if(check == CHECK_DECLARED ||
2866                   PARSER_STATE->isDeclared(name, SYM_SORT)) {
2867           t = PARSER_STATE->getSort(name, args);
2868         } else {
2869           // make unresolved type
2870           if(args.empty()) {
2871             t = PARSER_STATE->mkUnresolvedType(name);
2872             Debug("parser-param") << "param: make unres type " << name
2873                                   << std::endl;
2874           } else {
2875             t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args);
2876             t = SortConstructorType(t).instantiate( args );
2877             Debug("parser-param")
2878                 << "param: make unres param type " << name << " " << args.size()
2879                 << " " << PARSER_STATE->getArity( name ) << std::endl;
2880           }
2881         }
2882       }
2883     ) RPAREN_TOK
2884   | LPAREN_TOK HO_ARROW_TOK sortList[args] RPAREN_TOK
2885     {
2886       if(args.size()<2) {
2887         PARSER_STATE->parseError("Arrow types must have at least 2 arguments");
2888       }
2889       //flatten the type
2890       Type rangeType = args.back();
2891       args.pop_back();
2892       t = PARSER_STATE->mkFlatFunctionType( args, rangeType );
2893     }
2894   ;
2895
2896 /**
2897  * Matches a list of symbols, with check and type arguments as for the
2898  * symbol[] rule below.
2899  */
2900 symbolList[std::vector<std::string>& names,
2901            CVC4::parser::DeclarationCheck check,
2902            CVC4::parser::SymbolType type]
2903 @declarations {
2904   std::string id;
2905 }
2906   : ( symbol[id,check,type] { names.push_back(id); } )*
2907   ;
2908
2909 /**
2910  * Matches an symbol and sets the string reference parameter id.
2911  * @param id string to hold the symbol
2912  * @param check what kinds of check to do on the symbol
2913  * @param type the intended namespace for the symbol
2914  */
2915 symbol[std::string& id,
2916        CVC4::parser::DeclarationCheck check,
2917        CVC4::parser::SymbolType type]
2918   : SIMPLE_SYMBOL
2919     { id = AntlrInput::tokenText($SIMPLE_SYMBOL);
2920       if(!PARSER_STATE->isAbstractValue(id)) {
2921         // if an abstract value, SmtEngine handles declaration
2922         PARSER_STATE->checkDeclaration(id, check, type);
2923       }
2924     }
2925   | ( 'repeat' { id = "repeat"; }
2926     /* these are keywords in SyGuS but we don't want to inhibit their
2927      * use as symbols in SMT-LIB */
2928     | SET_OPTIONS_TOK { id = "set-options"; }
2929     | DECLARE_VAR_TOK { id = "declare-var"; }
2930     | DECLARE_PRIMED_VAR_TOK { id = "declare-primed-var"; }
2931     | SYNTH_FUN_TOK { id = "synth-fun"; }
2932     | SYNTH_INV_TOK { id = "synth-inv"; }
2933     | CONSTRAINT_TOK { id = "constraint"; }
2934     | INV_CONSTRAINT_TOK { id = "inv-constraint"; }
2935     | CHECK_SYNTH_TOK { id = "check-synth"; }
2936     )
2937     { PARSER_STATE->checkDeclaration(id, check, type); }
2938   | QUOTED_SYMBOL
2939     { id = AntlrInput::tokenText($QUOTED_SYMBOL);
2940       /* strip off the quotes */
2941       id = id.substr(1, id.size() - 2);
2942       if(!PARSER_STATE->isAbstractValue(id)) {
2943         // if an abstract value, SmtEngine handles declaration
2944         PARSER_STATE->checkDeclaration(id, check, type);
2945       }
2946     }
2947   | UNTERMINATED_QUOTED_SYMBOL
2948     ( EOF
2949       { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); }
2950     | '\\'
2951       { PARSER_STATE->unexpectedEOF("backslash not permitted in |quoted| "
2952                                     "symbol"); }
2953     )
2954   ;
2955
2956 /**
2957  * Matches a nonempty list of numerals.
2958  * @param numerals the (empty) vector to house the numerals.
2959  */
2960 nonemptyNumeralList[std::vector<uint64_t>& numerals]
2961   : ( INTEGER_LITERAL
2962       { numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
2963     )+
2964   ;
2965
2966 /**
2967  * Parses a datatype definition
2968  */
2969 datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes,
2970             std::vector< CVC4::Type >& params]
2971 @init {
2972   std::string id;
2973 }
2974     /* This really needs to be CHECK_NONE, or mutually-recursive
2975      * datatypes won't work, because this type will already be
2976      * "defined" as an unresolved type; don't worry, we check
2977      * below. */
2978   : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); }
2979    /* ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
2980         t = PARSER_STATE->mkSort(id2);
2981         params.push_back( t );
2982       }
2983       ( symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
2984         t = PARSER_STATE->mkSort(id2);
2985         params.push_back( t ); }
2986       )* ']'
2987     )?*/ //AJR: this isn't necessary if we use z3's style
2988     { datatypes.push_back(Datatype(id,params,isCo));
2989       if(!PARSER_STATE->isUnresolvedType(id)) {
2990         // if not unresolved, must be undeclared
2991         PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
2992       }
2993     }
2994     ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+
2995     { PARSER_STATE->popScope(); }
2996   ;
2997
2998 /**
2999  * Parses a constructor defintion for type
3000  */
3001 constructorDef[CVC4::Datatype& type]
3002 @init {
3003   std::string id;
3004   CVC4::DatatypeConstructor* ctor = NULL;
3005 }
3006   : symbol[id,CHECK_NONE,SYM_VARIABLE]
3007     { // make the tester
3008       std::string testerId("is-");
3009       testerId.append(id);
3010       ctor = new CVC4::DatatypeConstructor(id, testerId);
3011     }
3012     ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
3013     { // make the constructor
3014       type.addConstructor(*ctor);
3015       Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
3016       delete ctor;
3017     }
3018   ;
3019
3020 selector[CVC4::DatatypeConstructor& ctor]
3021 @init {
3022   std::string id;
3023   Type t, t2;
3024 }
3025   : symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t,CHECK_NONE]
3026     { ctor.addArg(id, t);
3027       Debug("parser-idt") << "selector: " << id.c_str()
3028                           << " of type " << t << std::endl;
3029     }
3030   ;
3031
3032 // Base SMT-LIB tokens
3033 ASSERT_TOK : 'assert';
3034 CHECK_SAT_TOK : 'check-sat';
3035 CHECK_SAT_ASSUMING_TOK : 'check-sat-assuming';
3036 DECLARE_FUN_TOK : 'declare-fun';
3037 DECLARE_SORT_TOK : 'declare-sort';
3038 DEFINE_FUN_TOK : 'define-fun';
3039 DEFINE_FUN_REC_TOK : 'define-fun-rec';
3040 DEFINE_FUNS_REC_TOK : 'define-funs-rec';
3041 DEFINE_SORT_TOK : 'define-sort';
3042 GET_VALUE_TOK : 'get-value';
3043 GET_ASSIGNMENT_TOK : 'get-assignment';
3044 GET_ASSERTIONS_TOK : 'get-assertions';
3045 GET_PROOF_TOK : 'get-proof';
3046 GET_UNSAT_ASSUMPTIONS_TOK : 'get-unsat-assumptions';
3047 GET_UNSAT_CORE_TOK : 'get-unsat-core';
3048 EXIT_TOK : 'exit';
3049 RESET_TOK : { PARSER_STATE->v2_5() }? 'reset';
3050 RESET_ASSERTIONS_TOK : 'reset-assertions';
3051 ITE_TOK : 'ite';
3052 LET_TOK : { !PARSER_STATE->sygus() }? 'let';
3053 SYGUS_LET_TOK : { PARSER_STATE->sygus() }? 'let';
3054 ATTRIBUTE_TOK : '!';
3055 LPAREN_TOK : '(';
3056 RPAREN_TOK : ')';
3057 INDEX_TOK : '_';
3058 SET_LOGIC_TOK : 'set-logic';
3059 SET_INFO_TOK : 'set-info';
3060 META_INFO_TOK : 'meta-info';
3061 GET_INFO_TOK : 'get-info';
3062 SET_OPTION_TOK : 'set-option';
3063 GET_OPTION_TOK : 'get-option';
3064 PUSH_TOK : 'push';
3065 POP_TOK : 'pop';
3066 AS_TOK : 'as';
3067 CONST_TOK : 'const';
3068
3069 // extended commands
3070 DECLARE_CODATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-codatatype';
3071 DECLARE_DATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-datatype';
3072 DECLARE_DATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-datatypes';
3073 DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-datatypes';
3074 DECLARE_CODATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-codatatypes';
3075 DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-codatatypes';
3076 PAR_TOK : { PARSER_STATE->v2_6() }?'par';
3077 TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'is';
3078 MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'match';
3079 GET_MODEL_TOK : 'get-model';
3080 ECHO_TOK : 'echo';
3081 REWRITE_RULE_TOK : 'assert-rewrite';
3082 REDUCTION_RULE_TOK : 'assert-reduction';
3083 PROPAGATION_RULE_TOK : 'assert-propagation';
3084 DECLARE_SORTS_TOK : 'declare-sorts';
3085 DECLARE_FUNS_TOK : 'declare-funs';
3086 DECLARE_PREDS_TOK : 'declare-preds';
3087 DEFINE_TOK : 'define';
3088 DECLARE_CONST_TOK : 'declare-const';
3089 DEFINE_CONST_TOK : 'define-const';
3090 SIMPLIFY_TOK : 'simplify';
3091 INCLUDE_TOK : 'include';
3092 GET_QE_TOK : 'get-qe';
3093 GET_QE_DISJUNCT_TOK : 'get-qe-disjunct';
3094 DECLARE_HEAP : 'declare-heap';
3095 EMP_TOK : 'emp';
3096
3097 // SyGuS commands
3098 SYNTH_FUN_TOK : 'synth-fun';
3099 SYNTH_INV_TOK : 'synth-inv';
3100 CHECK_SYNTH_TOK : 'check-synth';
3101 DECLARE_VAR_TOK : 'declare-var';
3102 DECLARE_PRIMED_VAR_TOK : 'declare-primed-var';
3103 CONSTRAINT_TOK : 'constraint';
3104 INV_CONSTRAINT_TOK : 'inv-constraint';
3105 SET_OPTIONS_TOK : 'set-options';
3106 SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant';
3107 SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable';
3108 SYGUS_INPUT_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'InputVariable';
3109 SYGUS_LOCAL_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'LocalVariable';
3110
3111 // attributes
3112 ATTRIBUTE_PATTERN_TOK : ':pattern';
3113 ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern';
3114 ATTRIBUTE_NAMED_TOK : ':named';
3115 ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level';
3116 ATTRIBUTE_RR_PRIORITY : ':rr-priority';
3117
3118 // operators (NOTE: theory symbols go here)
3119 AMPERSAND_TOK     : '&';
3120 AND_TOK           : 'and';
3121 AT_TOK            : '@';
3122 DISTINCT_TOK      : 'distinct';
3123 DIV_TOK           : '/';
3124 EQUAL_TOK         : '=';
3125 EXISTS_TOK        : 'exists';
3126 FORALL_TOK        : 'forall';
3127 GREATER_THAN_TOK  : '>';
3128 GREATER_THAN_EQUAL_TOK  : '>=';
3129 IMPLIES_TOK       : '=>';
3130 LESS_THAN_TOK     : '<';
3131 LESS_THAN_EQUAL_TOK     : '<=';
3132 MINUS_TOK         : '-';
3133 NOT_TOK           : 'not';
3134 OR_TOK            : 'or';
3135 // PERCENT_TOK       : '%';
3136 PLUS_TOK          : '+';
3137 //POUND_TOK         : '#';
3138 STAR_TOK          : '*';
3139 // TILDE_TOK         : '~';
3140 XOR_TOK           : 'xor';
3141
3142
3143 DIVISIBLE_TOK : 'divisible';
3144
3145 BV2NAT_TOK : 'bv2nat';
3146 INT2BV_TOK : 'int2bv';
3147
3148 RENOSTR_TOK : 're.nostr';
3149 REALLCHAR_TOK : 're.allchar';
3150
3151 DTSIZE_TOK : 'dt.size';
3152
3153 FMFCARD_TOK : 'fmf.card';
3154 FMFCARDVAL_TOK : 'fmf.card.val';
3155
3156 INST_CLOSURE_TOK : 'inst-closure';
3157
3158 EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
3159 UNIVSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'univset';
3160 NILREF_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'sep.nil';
3161 TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }? 'mkTuple';
3162 TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }? 'tupSel';
3163 // Other set theory operators are not
3164 // tokenized and handled directly when
3165 // processing a term
3166
3167 REAL_PI_TOK : 'real.pi';
3168
3169 FP_PINF_TOK : '+oo';
3170 FP_NINF_TOK : '-oo';
3171 FP_PZERO_TOK : '+zero';
3172 FP_NZERO_TOK : '-zero';
3173 FP_NAN_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'NaN';
3174
3175 FP_TO_FP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp';
3176 FP_TO_FPBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_bv';
3177 FP_TO_FPFP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_fp';
3178 FP_TO_FPR_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_real';
3179 FP_TO_FPS_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_signed';
3180 FP_TO_FPU_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_unsigned';
3181 FP_TO_UBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'fp.to_ubv';
3182 FP_TO_SBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'fp.to_sbv';
3183 FP_RNE_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RNE';
3184 FP_RNA_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RNA';
3185 FP_RTP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTP';
3186 FP_RTN_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTN';
3187 FP_RTZ_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTZ';
3188 FP_RNE_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundNearestTiesToEven';
3189 FP_RNA_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundNearestTiesToAway';
3190 FP_RTP_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardPositive';
3191 FP_RTN_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardNegative';
3192 FP_RTZ_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardZero';
3193
3194 HO_ARROW_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? '->';
3195 HO_LAMBDA_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? 'lambda';
3196
3197 /**
3198  * A sequence of printable ASCII characters (except backslash) that starts
3199  * and ends with | and does not otherwise contain |.
3200  *
3201  * You shouldn't generally use this in parser rules, as the |quoting|
3202  * will be part of the token text.  Use the symbol[] parser rule instead.
3203  */
3204 QUOTED_SYMBOL
3205   : '|' ~('|' | '\\')* '|'
3206   ;
3207 UNTERMINATED_QUOTED_SYMBOL
3208   : '|' ~('|' | '\\')*
3209   ;
3210
3211 /**
3212  * Matches a keyword from the input. A keyword is a simple symbol prefixed
3213  * with a colon.
3214  */
3215 KEYWORD
3216   : ':' (ALPHA | DIGIT | SYMBOL_CHAR)+
3217   ;
3218
3219 /**
3220  * Matches a "simple" symbol: a non-empty sequence of letters, digits and
3221  * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
3222  * digit, and is not the special reserved symbols '!' or '_'.
3223  */
3224 SIMPLE_SYMBOL
3225   : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)+
3226   | ALPHA
3227   | SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
3228   ;
3229
3230 /**
3231  * Matches and skips whitespace in the input.
3232  */
3233 WHITESPACE
3234   : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }
3235   ;
3236
3237 /**
3238  * Matches an integer constant from the input (non-empty sequence of
3239  * digits, with no leading zeroes).
3240  */
3241 INTEGER_LITERAL
3242   : NUMERAL
3243   ;
3244
3245 /**
3246  * Match an integer constant. In non-strict mode, this is any sequence
3247  * of digits. In strict mode, non-zero integers can't have leading
3248  * zeroes.
3249  */
3250 fragment NUMERAL
3251 @init {
3252   char *start = (char*) GETCHARINDEX();
3253 }
3254   : DIGIT+
3255     { Debug("parser-extra") << "NUMERAL: "
3256        << (uintptr_t)start << ".." << GETCHARINDEX()
3257        << " strict? " << (bool)(PARSER_STATE->strictModeEnabled())
3258        << " ^0? " << (bool)(*start == '0')
3259        << " len>1? " << (bool)(start < (char*)(GETCHARINDEX() - 1))
3260        << std::endl; }
3261     { !PARSER_STATE->strictModeEnabled() ||
3262       *start != '0' ||
3263       start == (char*)(GETCHARINDEX() - 1) }?
3264   ;
3265
3266 /**
3267  * Matches a decimal constant from the input.
3268  */
3269 DECIMAL_LITERAL
3270   : NUMERAL '.' DIGIT+
3271   ;
3272
3273 /**
3274  * Matches a hexadecimal constant.
3275  */
3276 HEX_LITERAL
3277   : '#x' HEX_DIGIT+
3278   ;
3279
3280 /**
3281  * Matches a binary constant.
3282  */
3283 BINARY_LITERAL
3284   : '#b' ('0' | '1')+
3285   ;
3286
3287 /**
3288  * Matches a double-quoted string literal. Depending on the language that is
3289  * being parsed, different escape sequences are supported:
3290  *
3291  * For SMT-LIB 2.0 the sequence \" is interpreted as a double quote (") and the
3292  * sequence \\ is interpreted as a backslash (\).
3293  *
3294  * For SMT-LIB >=2.5 and SyGuS a double-quote inside a string is escaped with
3295  * "", e.g., "This is a string literal with "" a single, embedded double
3296  * quote."
3297  *
3298  * You shouldn't generally use this in parser rules, as the quotes
3299  * will be part of the token text.  Use the str[] parser rule instead.
3300  */
3301 STRING_LITERAL
3302   : { !PARSER_STATE->escapeDupDblQuote() }?=>
3303     '"' ('\\' . | ~('\\' | '"'))* '"'
3304   | { PARSER_STATE->escapeDupDblQuote() }?=>
3305     '"' (~('"') | '""')* '"'
3306   ;
3307
3308 /**
3309  * Matches the comments and ignores them
3310  */
3311 COMMENT
3312   : ';' (~('\n' | '\r'))* { SKIP(); }
3313   ;
3314
3315 /**
3316  * Matches any letter ('a'-'z' and 'A'-'Z').
3317  */
3318 fragment
3319 ALPHA
3320   : 'a'..'z'
3321   | 'A'..'Z'
3322   ;
3323
3324 /**
3325  * Matches the digits (0-9)
3326  */
3327 fragment DIGIT : '0'..'9';
3328
3329 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
3330
3331 /**
3332  * Matches the characters that may appear as a one-character "symbol"
3333  * (which excludes _ and !, which are reserved words in SMT-LIB).
3334  */
3335 fragment SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
3336   : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '.' | '$' | '~'
3337   | '&' | '^' | '<' | '>' | '@'
3338   ;
3339
3340 /**
3341  * Matches the characters that may appear in a "symbol" (i.e., an identifier)
3342  */
3343 fragment SYMBOL_CHAR
3344   : SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE | '_' | '!'
3345   ;