src/parser/smt/Smt.g

   1 /* *******************                                                        */
   2 /*! \file Smt.g
   3  ** \verbatim
   4  ** Original author: cconway
   5  ** Major contributors: dejan
   6  ** Minor contributors (to current version): mdeters, taking
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Parser for SMT-LIB input language.
  15  **
  16  ** Parser for SMT-LIB input language.
  17  **/
  18
  19 grammar Smt;
  20
  21 options {
  22   language = 'C';                  // C output for antlr
  23 //  defaultErrorHandler = false;      // Skip the default error handling, just break with exceptions
  24   k = 2;
  25 }
  26
  27 @header {
  28 /**
  29  ** This file is part of the CVC4 prototype.
  30  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  31  ** Courant Institute of Mathematical Sciences
  32  ** New York University
  33  ** See the file COPYING in the top-level source directory for licensing
  34  ** information.
  35  **/
  36 }
  37
  38 @lexer::includes {
  39 /** This suppresses warnings about the redefinition of token symbols between
  40   * different parsers. The redefinitions should be harmless as long as no
  41   * client: (a) #include's the lexer headers for two grammars AND (b) uses the
  42   * token symbol definitions.
  43   */
  44 #pragma GCC system_header
  45
  46 /* This improves performance by ~10 percent on big inputs.
  47  * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
  48  * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
  49  * Otherwise, we have to let the lexer detect the encoding at runtime.
  50  */
  51 #define ANTLR3_INLINE_INPUT_ASCII
  52 }
  53
  54 @parser::includes {
  55 #include "expr/command.h"
  56 #include "parser/parser.h"
  57
  58 namespace CVC4 {
  59   class Expr;
  60 }
  61 }
  62
  63 @parser::postinclude {
  64 #include "expr/expr.h"
  65 #include "expr/kind.h"
  66 #include "expr/type.h"
  67 #include "parser/antlr_input.h"
  68 #include "parser/parser.h"
  69 #include "parser/smt/smt.h"
  70 #include "util/integer.h"
  71 #include "util/output.h"
  72 #include "util/rational.h"
  73 #include <vector>
  74
  75 using namespace CVC4;
  76 using namespace CVC4::parser;
  77
  78 /* These need to be macros so they can refer to the PARSER macro, which will be defined
  79  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
  80 #undef PARSER_STATE
  81 #define PARSER_STATE ((Smt*)PARSER->super)
  82 #undef EXPR_MANAGER
  83 #define EXPR_MANAGER PARSER_STATE->getExprManager()
  84 #undef MK_EXPR
  85 #define MK_EXPR EXPR_MANAGER->mkExpr
  86 #undef MK_CONST
  87 #define MK_CONST EXPR_MANAGER->mkConst
  88
  89 }
  90
  91
  92 /**
  93  * Parses an expression.
  94  * @return the parsed expression
  95  */
  96 parseExpr returns [CVC4::Expr expr]
  97   : annotatedFormula[expr]
  98   | EOF
  99   ;
 100
 101 /**
 102  * Parses a command (the whole benchmark)
 103  * @return the command of the benchmark
 104  */
 105 parseCommand returns [CVC4::Command* cmd]
 106   : b = benchmark { $cmd = b; }
 107   ;
 108
 109 /**
 110  * Matches the whole SMT-LIB benchmark.
 111  * @return the sequence command containing the whole problem
 112  */
 113 benchmark returns [CVC4::Command* cmd]
 114   : LPAREN_TOK BENCHMARK_TOK IDENTIFIER c = benchAttributes RPAREN_TOK
 115         { $cmd = c; }
 116   | EOF { $cmd = 0; }
 117   ;
 118
 119 /**
 120  * Matches a sequence of benchmark attributes and returns a pointer to a
 121  * command sequence.
 122  * @return the command sequence
 123  */
 124 benchAttributes returns [CVC4::CommandSequence* cmd_seq]
 125 @init {
 126   cmd_seq = new CommandSequence();
 127 }
 128   : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+
 129   ;
 130
 131 /**
 132  * Matches a benchmark attribute, sucha as ':logic', ':formula', and returns
 133  * a corresponding command
 134  * @return a command corresponding to the attribute
 135  */
 136 benchAttribute returns [CVC4::Command* smt_command]
 137 @declarations {
 138   std::string name;
 139   BenchmarkStatus b_status;
 140   Expr expr;
 141 }
 142   : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE]
 143     { PARSER_STATE->setLogic(name);
 144       smt_command = new SetBenchmarkLogicCommand(name);   }
 145   | ASSUMPTION_TOK annotatedFormula[expr]
 146     { smt_command = new AssertCommand(expr);   }
 147   | FORMULA_TOK annotatedFormula[expr]
 148     { smt_command = new CheckSatCommand(expr); }
 149   | STATUS_TOK status[b_status]
 150     { smt_command = new SetBenchmarkStatusCommand(b_status); }
 151   | EXTRAFUNS_TOK LPAREN_TOK (functionDeclaration)+ RPAREN_TOK
 152   | EXTRAPREDS_TOK LPAREN_TOK (predicateDeclaration)+ RPAREN_TOK
 153   | EXTRASORTS_TOK LPAREN_TOK sortDeclaration+ RPAREN_TOK
 154   | NOTES_TOK STRING_LITERAL
 155   | annotation
 156   ;
 157
 158 /**
 159  * Matches an annotated formula.
 160  * @return the expression representing the formula
 161  */
 162 annotatedFormula[CVC4::Expr& expr]
 163 @init {
 164   Debug("parser") << "annotated formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
 165   Kind kind;
 166   std::string name;
 167   std::vector<Expr> args; /* = getExprVector(); */
 168   Expr op; /* Operator expression FIXME: move away kill it */
 169 }
 170   : /* a built-in operator application */
 171     LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK
 172     { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
 173         /* Unary AND/OR can be replaced with the argument.
 174                It just so happens expr should already by the only argument. */
 175         Assert( expr == args[0] );
 176       } else if( CVC4::kind::isAssociative(kind) &&
 177                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
 178         /* Special treatment for associative operators with lots of children */
 179         expr = EXPR_MANAGER->mkAssociative(kind,args);
 180       } else {
 181         PARSER_STATE->checkArity(kind, args.size());
 182         expr = MK_EXPR(kind, args);
 183       }
 184     }
 185
 186   | /* A non-built-in function application */
 187
 188     // Semantic predicate not necessary if parenthesized subexpressions
 189     // are disallowed
 190     // { isFunction(LT(2)->getText()) }?
 191     LPAREN_TOK
 192     parameterizedOperator[op]
 193     annotatedFormulas[args,expr] RPAREN_TOK
 194     // TODO: check arity
 195     { expr = MK_EXPR(op,args); }
 196
 197   | /* An ite expression */
 198     LPAREN_TOK ITE_TOK
 199     annotatedFormula[expr]
 200     { args.push_back(expr); }
 201     annotatedFormula[expr]
 202     { args.push_back(expr); }
 203     annotatedFormula[expr]
 204     { args.push_back(expr); }
 205     RPAREN_TOK
 206     { expr = MK_EXPR(CVC4::kind::ITE, args); }
 207
 208   | /* a let/flet binding */
 209     LPAREN_TOK
 210     (LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED]
 211       | FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] )
 212     annotatedFormula[expr] RPAREN_TOK
 213     { PARSER_STATE->pushScope();
 214       PARSER_STATE->defineVar(name,expr); }
 215     annotatedFormula[expr]
 216     RPAREN_TOK
 217     { PARSER_STATE->popScope(); }
 218
 219   | /* a variable */
 220     ( identifier[name,CHECK_DECLARED,SYM_VARIABLE]
 221       | let_identifier[name,CHECK_DECLARED]
 222       | flet_identifier[name,CHECK_DECLARED] )
 223     { expr = PARSER_STATE->getVariable(name); }
 224
 225     /* constants */
 226   | TRUE_TOK          { expr = MK_CONST(true); }
 227   | FALSE_TOK         { expr = MK_CONST(false); }
 228   | NUMERAL_TOK
 229     { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); }
 230   | RATIONAL_TOK
 231     { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
 232       expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); }
 233     // NOTE: Theory constants go here
 234     /* TODO: quantifiers, arithmetic constants */
 235   ;
 236
 237 /**
 238  * Matches a sequence of annotated formulas and puts them into the formulas
 239  * vector.
 240  * @param formulas the vector to fill with formulas
 241  * @param expr an Expr reference for the elements of the sequence
 242  */
 243 /* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
 244  * time through this rule. */
 245 annotatedFormulas[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
 246   : ( annotatedFormula[expr] { formulas.push_back(expr); } )+
 247   ;
 248
 249 /**
 250 * Matches a builtin operator symbol and sets kind to its associated Expr kind.
 251 */
 252 builtinOp[CVC4::Kind& kind]
 253 @init {
 254   Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
 255 }
 256   : NOT_TOK      { $kind = CVC4::kind::NOT;     }
 257   | IMPLIES_TOK  { $kind = CVC4::kind::IMPLIES; }
 258   | AND_TOK      { $kind = CVC4::kind::AND;     }
 259   | OR_TOK       { $kind = CVC4::kind::OR;      }
 260   | XOR_TOK      { $kind = CVC4::kind::XOR;     }
 261   | IFF_TOK      { $kind = CVC4::kind::IFF;     }
 262   | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
 263   | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
 264     // Arithmetic
 265   | GREATER_THAN_TOK
 266                  { $kind = CVC4::kind::GT; }
 267   | GREATER_THAN_TOK EQUAL_TOK
 268                  { $kind = CVC4::kind::GEQ; }
 269   | LESS_THAN_TOK EQUAL_TOK
 270                  { $kind = CVC4::kind::LEQ; }
 271   | LESS_THAN_TOK
 272                  { $kind = CVC4::kind::LT; }
 273   | PLUS_TOK     { $kind = CVC4::kind::PLUS; }
 274   | STAR_TOK     { $kind = CVC4::kind::MULT; }
 275   | TILDE_TOK    { $kind = CVC4::kind::UMINUS; }
 276   | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
 277   | DIV_TOK      { $kind = CVC4::kind::DIVISION; }
 278   // Bit-vectors
 279   | CONCAT_TOK   { $kind = CVC4::kind::BITVECTOR_CONCAT; }
 280   | BVAND_TOK    { $kind = CVC4::kind::BITVECTOR_AND;    }
 281   | BVOR_TOK     { $kind = CVC4::kind::BITVECTOR_OR;     }
 282   | BVXOR_TOK    { $kind = CVC4::kind::BITVECTOR_XOR;    }
 283   | BVNOT_TOK    { $kind = CVC4::kind::BITVECTOR_NOT;    }
 284   | BVNAND_TOK   { $kind = CVC4::kind::BITVECTOR_NAND;   }
 285   | BVNOR_TOK    { $kind = CVC4::kind::BITVECTOR_NOR;    }
 286   | BVXNOR_TOK   { $kind = CVC4::kind::BITVECTOR_XNOR;   }
 287   | BVCOMP_TOK   { $kind = CVC4::kind::BITVECTOR_COMP;   }
 288   | BVMUL_TOK    { $kind = CVC4::kind::BITVECTOR_MULT;   }
 289   | BVADD_TOK    { $kind = CVC4::kind::BITVECTOR_PLUS;   }
 290   | BVSUB_TOK    { $kind = CVC4::kind::BITVECTOR_SUB;    }
 291   | BVNEG_TOK    { $kind = CVC4::kind::BITVECTOR_NEG;    }
 292   | BVUDIV_TOK   { $kind = CVC4::kind::BITVECTOR_UDIV;   }
 293   | BVUREM_TOK   { $kind = CVC4::kind::BITVECTOR_UREM;   }
 294   | BVSDIV_TOK   { $kind = CVC4::kind::BITVECTOR_SDIV;   }
 295   | BVSREM_TOK   { $kind = CVC4::kind::BITVECTOR_SREM;   }
 296   | BVSMOD_TOK   { $kind = CVC4::kind::BITVECTOR_SMOD;   }
 297   | BVSHL_TOK    { $kind = CVC4::kind::BITVECTOR_SHL;    }
 298   | BVLSHR_TOK   { $kind = CVC4::kind::BITVECTOR_LSHR;   }
 299   | BVASHR_TOK   { $kind = CVC4::kind::BITVECTOR_ASHR;   }
 300   | BVULT_TOK    { $kind = CVC4::kind::BITVECTOR_ULT;    }
 301   | BVULE_TOK    { $kind = CVC4::kind::BITVECTOR_ULE;    }
 302   | BVUGT_TOK    { $kind = CVC4::kind::BITVECTOR_UGT;    }
 303   | BVUGE_TOK    { $kind = CVC4::kind::BITVECTOR_UGE;    }
 304   | BVSLT_TOK    { $kind = CVC4::kind::BITVECTOR_SLT;    }
 305   | BVSLE_TOK    { $kind = CVC4::kind::BITVECTOR_SLE;    }
 306   | BVSGT_TOK    { $kind = CVC4::kind::BITVECTOR_SGT;    }
 307   | BVSGE_TOK    { $kind = CVC4::kind::BITVECTOR_SGE;    }
 308     // NOTE: Theory operators go here
 309   | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
 310   | STORE_TOK    { $kind = CVC4::kind::STORE; }
 311   ;
 312
 313 /**
 314  * Matches an operator.
 315  */
 316 parameterizedOperator[CVC4::Expr& op]
 317   : functionSymbol[op]
 318   | bitVectorOperator[op]
 319   ;
 320
 321 /**
 322  * Matches a bit-vector operator (the ones parametrized by numbers)
 323  */
 324 bitVectorOperator[CVC4::Expr& op]
 325   : EXTRACT_TOK '[' n1 = NUMERAL_TOK ':' n2 = NUMERAL_TOK ']'
 326     { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), AntlrInput::tokenToUnsigned($n2))); }
 327   | REPEAT_TOK '[' n = NUMERAL_TOK ']'
 328     { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
 329   | ZERO_EXTEND_TOK '[' n = NUMERAL_TOK ']'
 330     { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
 331   | SIGN_EXTEND_TOK '[' n = NUMERAL_TOK ']'
 332     { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); }
 333   | ROTATE_LEFT_TOK '[' n = NUMERAL_TOK ']'
 334     { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
 335   | ROTATE_RIGHT_TOK '[' n = NUMERAL_TOK ']'
 336     { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
 337   ;
 338
 339 /**
 340  * Matches a (possibly undeclared) predicate identifier (returning the string).
 341  * @param check what kind of check to do with the symbol
 342  */
 343 predicateName[std::string& name, CVC4::parser::DeclarationCheck check]
 344   :  functionName[name,check]
 345   ;
 346
 347 /**
 348  * Matches a (possibly undeclared) function identifier (returning the string)
 349  * @param check what kind of check to do with the symbol
 350  */
 351 functionName[std::string& name, CVC4::parser::DeclarationCheck check]
 352   :  identifier[name,check,SYM_VARIABLE]
 353   ;
 354
 355 /**
 356  * Matches an previously declared function symbol (returning an Expr)
 357  */
 358 functionSymbol[CVC4::Expr& fun]
 359 @declarations {
 360         std::string name;
 361 }
 362   : functionName[name,CHECK_DECLARED]
 363     { PARSER_STATE->checkFunction(name);
 364       fun = PARSER_STATE->getVariable(name); }
 365   ;
 366
 367 /**
 368  * Matches an attribute name from the input (:attribute_name).
 369  */
 370 attribute
 371   :  ATTR_IDENTIFIER
 372   ;
 373
 374 functionDeclaration
 375 @declarations {
 376   std::string name;
 377   std::vector<Type> sorts;
 378 }
 379   : LPAREN_TOK functionName[name,CHECK_UNDECLARED]
 380       t = sortSymbol // require at least one sort
 381     { sorts.push_back(t); }
 382       sortList[sorts] RPAREN_TOK
 383     { if( sorts.size() == 1 ) {
 384         Assert( t == sorts[0] );
 385       } else {
 386         t = EXPR_MANAGER->mkFunctionType(sorts);
 387       }
 388       PARSER_STATE->mkVar(name, t); }
 389   ;
 390
 391 /**
 392  * Matches the declaration of a predicate and declares it
 393  */
 394 predicateDeclaration
 395 @declarations {
 396   std::string name;
 397   std::vector<Type> p_sorts;
 398 }
 399   : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK
 400     { Type t;
 401       if( p_sorts.empty() ) {
 402         t = EXPR_MANAGER->booleanType();
 403       } else {
 404         t = EXPR_MANAGER->mkPredicateType(p_sorts);
 405       }
 406       PARSER_STATE->mkVar(name, t); }
 407   ;
 408
 409 sortDeclaration
 410 @declarations {
 411   std::string name;
 412 }
 413   : sortName[name,CHECK_UNDECLARED]
 414     { Debug("parser") << "sort decl: '" << name << "'" << std::endl;
 415       PARSER_STATE->mkSort(name); }
 416   ;
 417
 418 /**
 419  * Matches a sequence of sort symbols and fills them into the given vector.
 420  */
 421 sortList[std::vector<CVC4::Type>& sorts]
 422   : ( t = sortSymbol { sorts.push_back(t); })*
 423   ;
 424
 425 /**
 426  * Matches the sort symbol, which can be an arbitrary identifier.
 427  * @param check the check to perform on the name
 428  */
 429 sortName[std::string& name, CVC4::parser::DeclarationCheck check]
 430   : identifier[name,check,SYM_SORT]
 431   ;
 432
 433 sortSymbol returns [CVC4::Type t]
 434 @declarations {
 435   std::string name;
 436 }
 437   : sortName[name,CHECK_NONE]
 438         { $t = PARSER_STATE->getSort(name); }
 439   | BITVECTOR_TOK '[' NUMERAL_TOK ']' {
 440         $t = EXPR_MANAGER->bitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK));
 441   }
 442   ;
 443
 444 /**
 445  * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'.
 446  */
 447 status[ CVC4::BenchmarkStatus& status ]
 448   : SAT_TOK       { $status = SMT_SATISFIABLE;    }
 449   | UNSAT_TOK     { $status = SMT_UNSATISFIABLE;  }
 450   | UNKNOWN_TOK   { $status = SMT_UNKNOWN;        }
 451   ;
 452
 453 /**
 454  * Matches an annotation, which is an attribute name, with an optional user
 455  */
 456 annotation
 457   : attribute (USER_VALUE)?
 458   ;
 459
 460 /**
 461  * Matches an identifier and sets the string reference parameter id.
 462  * @param id string to hold the identifier
 463  * @param check what kinds of check to do on the symbol
 464  * @param type the intended namespace for the identifier
 465  */
 466 identifier[std::string& id,
 467                    CVC4::parser::DeclarationCheck check,
 468            CVC4::parser::SymbolType type]
 469   : IDENTIFIER
 470     { id = AntlrInput::tokenText($IDENTIFIER);
 471       Debug("parser") << "identifier: " << id
 472                       << " check? " << toString(check)
 473                       << " type? " << toString(type) << std::endl;
 474       PARSER_STATE->checkDeclaration(id, check, type); }
 475   ;
 476
 477 /**
 478  * Matches a let-bound identifier and sets the string reference parameter id.
 479  * @param id string to hold the identifier
 480  * @param check what kinds of check to do on the symbol
 481  */
 482 let_identifier[std::string& id,
 483                    CVC4::parser::DeclarationCheck check]
 484   : LET_IDENTIFIER
 485     { id = AntlrInput::tokenText($LET_IDENTIFIER);
 486       Debug("parser") << "let_identifier: " << id
 487                       << " check? " << toString(check) << std::endl;
 488       PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); }
 489   ;
 490
 491 /**
 492  * Matches an flet-bound identifier and sets the string reference parameter id.
 493  * @param id string to hold the identifier
 494  * @param check what kinds of check to do on the symbol
 495  */
 496 flet_identifier[std::string& id,
 497                     CVC4::parser::DeclarationCheck check]
 498   : FLET_IDENTIFIER
 499     { id = AntlrInput::tokenText($FLET_IDENTIFIER);
 500       Debug("parser") << "flet_identifier: " << id
 501                       << " check? " << toString(check) << std::endl;
 502       PARSER_STATE->checkDeclaration(id, check); }
 503   ;
 504
 505 // Base SMT-LIB tokens
 506 ASSUMPTION_TOK  : ':assumption';
 507 BENCHMARK_TOK   : 'benchmark';
 508 EXTRAFUNS_TOK   : ':extrafuns';
 509 EXTRAPREDS_TOK  : ':extrapreds';
 510 EXTRASORTS_TOK  : ':extrasorts';
 511 FALSE_TOK       : 'false';
 512 FLET_TOK        : 'flet';
 513 FORMULA_TOK     : ':formula';
 514 ITE_TOK         : 'ite' | 'if_then_else';
 515 LET_TOK         : 'let';
 516 LOGIC_TOK       : ':logic';
 517 LPAREN_TOK      : '(';
 518 NOTES_TOK       : ':notes';
 519 RPAREN_TOK      : ')';
 520 SAT_TOK         : 'sat';
 521 STATUS_TOK      : ':status';
 522 THEORY_TOK      : 'theory';
 523 TRUE_TOK        : 'true';
 524 UNKNOWN_TOK     : 'unknown';
 525 UNSAT_TOK       : 'unsat';
 526
 527 // operators (NOTE: theory symbols go here)
 528 AMPERSAND_TOK     : '&';
 529 AND_TOK           : 'and';
 530 AT_TOK            : '@';
 531 DISTINCT_TOK      : 'distinct';
 532 DIV_TOK           : '/';
 533 EQUAL_TOK         : '=';
 534 EXISTS_TOK        : 'exists';
 535 FORALL_TOK        : 'forall';
 536 GREATER_THAN_TOK  : '>';
 537 IFF_TOK           : 'iff';
 538 IMPLIES_TOK       : 'implies';
 539 LESS_THAN_TOK     : '<';
 540 MINUS_TOK         : '-';
 541 NOT_TOK           : 'not';
 542 OR_TOK            : 'or';
 543 PERCENT_TOK       : '%';
 544 PIPE_TOK          : '|';
 545 PLUS_TOK          : '+';
 546 POUND_TOK         : '#';
 547 SELECT_TOK        : 'select';
 548 STAR_TOK          : '*';
 549 STORE_TOK         : 'store';
 550 TILDE_TOK         : '~';
 551 XOR_TOK           : 'xor';
 552
 553 // Bitvector tokens
 554 BITVECTOR_TOK     : 'BitVec';
 555 CONCAT_TOK        : 'concat';
 556 EXTRACT_TOK       : 'extract';
 557 BVAND_TOK         : 'bvand';
 558 BVOR_TOK          : 'bvor';
 559 BVXOR_TOK         : 'bvxor';
 560 BVNOT_TOK         : 'bvnot';
 561 BVNAND_TOK        : 'bvnand';
 562 BVNOR_TOK         : 'bvnor';
 563 BVXNOR_TOK        : 'bvxnor';
 564 BVCOMP_TOK        : 'bvcomp';
 565 BVMUL_TOK         : 'bvmul';
 566 BVADD_TOK         : 'bvadd';
 567 BVSUB_TOK         : 'bvsub';
 568 BVNEG_TOK         : 'bvneg';
 569 BVUDIV_TOK        : 'bvudiv';
 570 BVUREM_TOK        : 'bvurem';
 571 BVSDIV_TOK        : 'bvsdiv';
 572 BVSREM_TOK        : 'bvsrem';
 573 BVSMOD_TOK        : 'bvsmod';
 574 BVSHL_TOK         : 'bvshl';
 575 BVLSHR_TOK        : 'bvlshr';
 576 BVASHR_TOK        : 'bvashr';
 577 BVULT_TOK         : 'bvult';
 578 BVULE_TOK         : 'bvule';
 579 BVUGT_TOK         : 'bvugt';
 580 BVUGE_TOK         : 'bvuge';
 581 BVSLT_TOK         : 'bvslt';
 582 BVSLE_TOK         : 'bvsle';
 583 BVSGT_TOK         : 'bvsgt';
 584 BVSGE_TOK         : 'bvsge';
 585 REPEAT_TOK        : 'repeat';
 586 ZERO_EXTEND_TOK   : 'zero_extend';
 587 SIGN_EXTEND_TOK   : 'sign_extend';
 588 ROTATE_LEFT_TOK   : 'rotate_left';
 589 ROTATE_RIGHT_TOK  : 'rotate_right';
 590
 591 /**
 592  * Matches an identifier from the input. An identifier is a sequence of letters,
 593  * digits and "_", "'", "." symbols, starting with a letter.
 594  */
 595 IDENTIFIER
 596   :  ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
 597   ;
 598
 599 /**
 600  * Matches an identifier starting with a colon.
 601  */
 602 ATTR_IDENTIFIER
 603   :  ':' IDENTIFIER
 604   ;
 605
 606 /**
 607  * Matches an identifier starting with a question mark.
 608  */
 609 LET_IDENTIFIER
 610   : '?' IDENTIFIER
 611   ;
 612
 613 /**
 614  * Matches an identifier starting with a dollar sign.
 615  */
 616 FLET_IDENTIFIER
 617   : '$' IDENTIFIER
 618   ;
 619
 620 /**
 621  * Matches the value of user-defined annotations or attributes. The only constraint imposed on a user-defined value is that it start with
 622  * an open brace and end with closed brace.
 623  */
 624 USER_VALUE
 625   :   '{'
 626       ( ~('{' | '}') )*
 627     '}'
 628   ;
 629
 630
 631 /**
 632  * Matches and skips whitespace in the input.
 633  */
 634 WHITESPACE
 635   :  (' ' | '\t' | '\f' | '\r' | '\n')+             { $channel = HIDDEN;; }
 636   ;
 637
 638 /**
 639  * Matches a numeral from the input (non-empty sequence of digits).
 640  */
 641 NUMERAL_TOK
 642   : DIGIT+
 643   ;
 644
 645 RATIONAL_TOK
 646   : DIGIT+ '.' DIGIT+
 647   ;
 648
 649 /**
 650  * Matches a double quoted string literal. Escaping is supported, and escape
 651  * character '\' has to be escaped.
 652  */
 653 STRING_LITERAL
 654   :  '"' (ESCAPE | ~('"'|'\\'))* '"'
 655   ;
 656
 657 /**
 658  * Matches the comments and ignores them
 659  */
 660 COMMENT
 661   : ';' (~('\n' | '\r'))*                    { $channel = HIDDEN;; }
 662   ;
 663
 664
 665 /**
 666  * Matches any letter ('a'-'z' and 'A'-'Z').
 667  */
 668 fragment
 669 ALPHA
 670   :  'a'..'z'
 671   |  'A'..'Z'
 672   ;
 673
 674 /**
 675  * Matches the digits (0-9)
 676  */
 677 fragment DIGIT :   '0'..'9';
 678 // fragment NON_ZERO_DIGIT : '1'..'9';
 679 // fragment NUMERAL_SEQ : '0' | NON_ZERO_DIGIT DIGIT*;
 680
 681 /**
 682  * Matches an allowed escaped character.
 683  */
 684 fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');
 685