src/parser/smt2/Smt2.g

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