src/parser/smt1/Smt1.g

   1 /* *******************                                                        */
   2 /*! \file Smt1.g
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Christopher L. Conway, Morgan Deters, Dejan Jovanovic
   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 input language.
  13  **
  14  ** Parser for SMT-LIB input language.
  15  **/
  16
  17 grammar Smt1;
  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 smt1_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 }/* @lexer::includes */
  67
  68 @parser::includes {
  69
  70 // This should come immediately after #include <antlr3.h> in the generated
  71 // files. See the documentation in "parser/antlr_undefines.h" for more details.
  72 #include "parser/antlr_undefines.h"
  73
  74 #include <stdint.h>
  75
  76 #include "base/ptr_closer.h"
  77 #include "smt/command.h"
  78 #include "parser/parser.h"
  79 #include "parser/antlr_tracing.h"
  80
  81 namespace CVC4 {
  82   class Expr;
  83
  84   namespace parser {
  85     namespace smt1 {
  86       /**
  87        * Just exists to provide the uintptr_t constructor that ANTLR
  88        * requires.
  89        */
  90       struct myExpr : public CVC4::Expr {
  91         myExpr() : CVC4::Expr() {}
  92         myExpr(void*) : CVC4::Expr() {}
  93         myExpr(const Expr& e) : CVC4::Expr(e) {}
  94         myExpr(const myExpr& e) : CVC4::Expr(e) {}
  95       };/* struct myExpr */
  96
  97       /**
  98        * Just exists to provide the uintptr_t constructor that ANTLR
  99        * requires.
 100        */
 101       struct myType : public CVC4::Type {
 102         myType() : CVC4::Type() {}
 103         myType(void*) : CVC4::Type() {}
 104         myType(const Type& t) : CVC4::Type(t) {}
 105         myType(const myType& t) : CVC4::Type(t) {}
 106       };/* struct myType */
 107     }/* CVC4::parser::smt1 namespace */
 108   }/* CVC4::parser namespace */
 109 }/* CVC4 namespace */
 110
 111 }/* @parser::includes */
 112
 113 @parser::postinclude {
 114
 115 #include <vector>
 116
 117 #include "base/output.h"
 118 #include "base/ptr_closer.h"
 119 #include "expr/expr.h"
 120 #include "expr/kind.h"
 121 #include "expr/type.h"
 122 #include "parser/antlr_input.h"
 123 #include "parser/parser.h"
 124 #include "parser/smt1/smt1.h"
 125 #include "util/integer.h"
 126 #include "util/rational.h"
 127
 128 using namespace CVC4;
 129 using namespace CVC4::parser;
 130
 131 /* These need to be macros so they can refer to the PARSER macro, which will be defined
 132  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
 133 #undef PARSER_STATE
 134 #define PARSER_STATE ((Smt1*)PARSER->super)
 135 #undef EXPR_MANAGER
 136 #define EXPR_MANAGER PARSER_STATE->getExprManager()
 137 #undef MK_EXPR
 138 #define MK_EXPR EXPR_MANAGER->mkExpr
 139 #undef MK_CONST
 140 #define MK_CONST EXPR_MANAGER->mkConst
 141
 142 }/* @parser::postinclude */
 143
 144
 145 /**
 146  * Parses an expression.
 147  * @return the parsed expression
 148  */
 149 parseExpr returns [CVC4::parser::smt1::myExpr expr]
 150   : annotatedFormula[expr]
 151   | EOF
 152   ;
 153
 154 /**
 155  * Parses a command (the whole benchmark)
 156  * @return the command of the benchmark
 157  */
 158 parseCommand returns [CVC4::Command* cmd_return = NULL]
 159 @declarations {
 160   CVC4::PtrCloser<CVC4::Command> cmd;
 161 }
 162 @after {
 163   cmd_return = cmd.release();
 164 }
 165   : b = benchmark[&cmd]
 166   | LPAREN_TOK c=IDENTIFIER
 167     { std::string s = AntlrInput::tokenText($c);
 168       if(s == "set" || s == "get") {
 169         PARSER_STATE->parseError(std::string("In SMT-LIBv1 mode, expected keyword `benchmark', but it looks like you're writing SMT-LIBv2.  Use --lang smt for SMT-LIBv2."));
 170       } else {
 171         PARSER_STATE->parseError(std::string("expected keyword `benchmark', got `" + s + "'"));
 172       }
 173     }
 174   ;
 175
 176 /**
 177  * Matches the whole SMT-LIB benchmark.
 178  * @return the sequence command containing the whole problem
 179  */
 180 benchmark [CVC4::PtrCloser<CVC4::Command>* cmd]
 181   : LPAREN_TOK BENCHMARK_TOK IDENTIFIER benchAttributes[cmd] RPAREN_TOK
 182   | EOF
 183   ;
 184
 185 /**
 186  * Matches a sequence of benchmark attributes and returns a pointer to a
 187  * command sequence.
 188  * @return the command sequence
 189  */
 190 benchAttributes [CVC4::PtrCloser<CVC4::Command>* cmd]
 191 @init {
 192   CVC4::PtrCloser<CVC4::CommandSequence> cmd_seq(new CommandSequence());
 193   CVC4::PtrCloser<CVC4::Command> attribute;
 194 }
 195 @after {
 196   cmd->reset(cmd_seq.release());
 197 }
 198   : (benchAttribute[&attribute]
 199      { if (attribute) cmd_seq->addCommand(attribute.release()); }
 200     )+
 201   ;
 202
 203 /**
 204  * Matches a benchmark attribute, such as ':logic', ':formula', and returns
 205  * a corresponding command
 206  * @return a command corresponding to the attribute
 207  */
 208 benchAttribute [CVC4::PtrCloser<CVC4::Command>* smt_command]
 209 @declarations {
 210   std::string name;
 211   BenchmarkStatus b_status;
 212   Expr expr;
 213   CVC4::PtrCloser<CVC4::CommandSequence> command_seq;
 214   CVC4::PtrCloser<CVC4::Command> declaration_command;
 215 }
 216   : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE]
 217     { PARSER_STATE->preemptCommand(new SetBenchmarkLogicCommand(name));
 218       PARSER_STATE->setLogic(name);
 219       smt_command->reset(new EmptyCommand());
 220     }
 221   | ASSUMPTION_TOK annotatedFormula[expr]
 222     { smt_command->reset(new AssertCommand(expr)); }
 223   | FORMULA_TOK annotatedFormula[expr]
 224     { smt_command->reset(new CheckSatCommand(expr)); }
 225   | STATUS_TOK status[b_status]
 226     { smt_command->reset(new SetBenchmarkStatusCommand(b_status)); }
 227   | EXTRAFUNS_TOK LPAREN_TOK
 228     { command_seq.reset(new CommandSequence()); }
 229     ( functionDeclaration[&declaration_command]
 230       { command_seq->addCommand(declaration_command.release()); }
 231     )+ RPAREN_TOK
 232       { smt_command->reset(command_seq.release()); }
 233   | EXTRAPREDS_TOK LPAREN_TOK
 234     { command_seq.reset(new CommandSequence()); }
 235     ( predicateDeclaration[&declaration_command]
 236       { command_seq->addCommand(declaration_command.release()); }
 237     )+ RPAREN_TOK
 238       { smt_command->reset(command_seq.release()); }
 239   | EXTRASORTS_TOK LPAREN_TOK
 240       { command_seq.reset(new CommandSequence()); }
 241     ( sortDeclaration[&declaration_command]
 242       { command_seq->addCommand(declaration_command.release()); }
 243     )+ RPAREN_TOK
 244       { smt_command->reset(command_seq.release()); }
 245   | NOTES_TOK STRING_LITERAL
 246     { smt_command->reset(
 247           new CommentCommand(AntlrInput::tokenText($STRING_LITERAL))); }
 248   | annotation[smt_command]
 249   ;
 250
 251 /**
 252  * Matches an annotated formula.
 253  * @return the expression representing the formula
 254  */
 255 annotatedFormula[CVC4::Expr& expr]
 256 @init {
 257   Debug("parser") << "annotated formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
 258   Kind kind;
 259   std::string name;
 260   std::vector<Expr> args; /* = getExprVector(); */
 261   std::vector<Expr> args2;
 262   Expr op; /* Operator expression FIXME: move away kill it */
 263 }
 264   : /* a built-in operator application */
 265     LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr]
 266     { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
 267         /* Unary AND/OR can be replaced with the argument.
 268          * It just so happens expr should already be the only argument. */
 269         assert( expr == args[0] );
 270       } else if( CVC4::kind::isAssociative(kind) &&
 271                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
 272         /* Special treatment for associative operators with lots of children */
 273         expr = EXPR_MANAGER->mkAssociative(kind,args);
 274       } else if(!PARSER_STATE->strictModeEnabled() &&
 275                 kind == CVC4::kind::MINUS && args.size() == 1) {
 276         /* Special fix-up for unary minus improperly used in some benchmarks */
 277         expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
 278       } else {
 279         PARSER_STATE->checkArity(kind, args.size());
 280         expr = MK_EXPR(kind, args);
 281       }
 282     }
 283     termAnnotation[expr]* RPAREN_TOK
 284
 285   | /* A quantifier */
 286     LPAREN_TOK
 287     ( FORALL_TOK { kind = kind::FORALL; } | EXISTS_TOK { kind = kind::EXISTS; } )
 288     { PARSER_STATE->pushScope(); }
 289     ( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK
 290       { args.push_back(PARSER_STATE->mkBoundVar(name, t)); }
 291     )+
 292     annotatedFormula[expr]
 293     { args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) );
 294       args2.push_back(expr);
 295       expr = MK_EXPR(kind, args2);
 296     }
 297     termAnnotation[expr]* RPAREN_TOK
 298     { PARSER_STATE->popScope(); }
 299
 300   | /* A non-built-in function application */
 301
 302     // Semantic predicate not necessary if parenthesized subexpressions
 303     // are disallowed
 304     // { isFunction(LT(2)->getText()) }?
 305     LPAREN_TOK
 306     parameterizedOperator[op]
 307     annotatedFormulas[args,expr]
 308     // TODO: check arity
 309     { expr = MK_EXPR(op,args); }
 310     termAnnotation[expr]* RPAREN_TOK
 311
 312   | /* An ite expression */
 313     LPAREN_TOK ITE_TOK
 314     annotatedFormula[expr]
 315     { args.push_back(expr); }
 316     annotatedFormula[expr]
 317     { args.push_back(expr); }
 318     annotatedFormula[expr]
 319     { args.push_back(expr);
 320       expr = MK_EXPR(CVC4::kind::ITE, args); }
 321     termAnnotation[expr]* RPAREN_TOK
 322
 323   | /* a let/flet binding */
 324     LPAREN_TOK
 325     ( LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED]
 326       | FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] )
 327     annotatedFormula[expr] RPAREN_TOK
 328     { PARSER_STATE->pushScope();
 329       PARSER_STATE->defineVar(name,expr); }
 330     annotatedFormula[expr]
 331     termAnnotation[expr]* RPAREN_TOK
 332     { PARSER_STATE->popScope(); }
 333
 334     /* constants */
 335   | TRUE_TOK          { expr = MK_CONST(bool(true)); }
 336   | FALSE_TOK         { expr = MK_CONST(bool(false)); }
 337   | NUMERAL_TOK
 338     { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); }
 339   | RATIONAL_TOK
 340     { // FIXME: This doesn't work because an SMT rational is not a
 341       // valid GMP rational string
 342       expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); }
 343   | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']'
 344     { expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); }
 345   | n = BITVECTOR1_BV_CONST
 346     { unsigned int bit = AntlrInput::tokenText($n)[3] - '0';
 347       expr = MK_CONST( BitVector(1, bit) );
 348     }
 349     // NOTE: Theory constants go here
 350     /* TODO: quantifiers, arithmetic constants */
 351
 352   | /* a variable */
 353     ( identifier[name,CHECK_DECLARED,SYM_VARIABLE]
 354       | let_identifier[name,CHECK_DECLARED]
 355       | flet_identifier[name,CHECK_DECLARED] )
 356     { expr = PARSER_STATE->getVariable(name); }
 357   ;
 358
 359 /**
 360  * Matches a sequence of annotated formulas and puts them into the
 361  * formulas vector.
 362  * @param formulas the vector to fill with formulas
 363  * @param expr an Expr reference for the elements of the sequence
 364  */
 365 /* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
 366  * time through this rule. */
 367 annotatedFormulas[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
 368   : ( annotatedFormula[expr] { formulas.push_back(expr); } )+
 369   ;
 370
 371 /**
 372 * Matches a builtin operator symbol and sets kind to its associated Expr kind.
 373 */
 374 builtinOp[CVC4::Kind& kind]
 375 @init {
 376   Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
 377 }
 378   : NOT_TOK      { $kind = CVC4::kind::NOT;     }
 379   | IMPLIES_TOK  { $kind = CVC4::kind::IMPLIES; }
 380   | AND_TOK      { $kind = CVC4::kind::AND;     }
 381   | OR_TOK       { $kind = CVC4::kind::OR;      }
 382   | XOR_TOK      { $kind = CVC4::kind::XOR;     }
 383   | IFF_TOK      { $kind = CVC4::kind::EQUAL;   }
 384   | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
 385   | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
 386   // Arithmetic
 387   | GREATER_THAN_TOK
 388                  { $kind = CVC4::kind::GT; }
 389   | GREATER_THAN_TOK EQUAL_TOK
 390                  { $kind = CVC4::kind::GEQ; }
 391   | LESS_THAN_TOK EQUAL_TOK
 392                  { $kind = CVC4::kind::LEQ; }
 393   | LESS_THAN_TOK
 394                  { $kind = CVC4::kind::LT; }
 395   | PLUS_TOK     { $kind = CVC4::kind::PLUS; }
 396   | STAR_TOK     { $kind = CVC4::kind::MULT; }
 397   | TILDE_TOK    { $kind = CVC4::kind::UMINUS; }
 398   | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
 399   | DIV_TOK      { $kind = CVC4::kind::DIVISION; }
 400   // Bit-vectors
 401   | CONCAT_TOK   { $kind = CVC4::kind::BITVECTOR_CONCAT; }
 402   | BVAND_TOK    { $kind = CVC4::kind::BITVECTOR_AND;    }
 403   | BVOR_TOK     { $kind = CVC4::kind::BITVECTOR_OR;     }
 404   | BVXOR_TOK    { $kind = CVC4::kind::BITVECTOR_XOR;    }
 405   | BVNOT_TOK    { $kind = CVC4::kind::BITVECTOR_NOT;    }
 406   | BVNAND_TOK   { $kind = CVC4::kind::BITVECTOR_NAND;   }
 407   | BVNOR_TOK    { $kind = CVC4::kind::BITVECTOR_NOR;    }
 408   | BVXNOR_TOK   { $kind = CVC4::kind::BITVECTOR_XNOR;   }
 409   | BVCOMP_TOK   { $kind = CVC4::kind::BITVECTOR_COMP;   }
 410   | BVMUL_TOK    { $kind = CVC4::kind::BITVECTOR_MULT;   }
 411   | BVADD_TOK    { $kind = CVC4::kind::BITVECTOR_PLUS;   }
 412   | BVSUB_TOK    { $kind = CVC4::kind::BITVECTOR_SUB;    }
 413   | BVNEG_TOK    { $kind = CVC4::kind::BITVECTOR_NEG;    }
 414   | BVUDIV_TOK   { $kind = CVC4::kind::BITVECTOR_UDIV;   }
 415   | BVUREM_TOK   { $kind = CVC4::kind::BITVECTOR_UREM;   }
 416   | BVSDIV_TOK   { $kind = CVC4::kind::BITVECTOR_SDIV;   }
 417   | BVSREM_TOK   { $kind = CVC4::kind::BITVECTOR_SREM;   }
 418   | BVSMOD_TOK   { $kind = CVC4::kind::BITVECTOR_SMOD;   }
 419   | BVSHL_TOK    { $kind = CVC4::kind::BITVECTOR_SHL;    }
 420   | BVLSHR_TOK   { $kind = CVC4::kind::BITVECTOR_LSHR;   }
 421   | BVASHR_TOK   { $kind = CVC4::kind::BITVECTOR_ASHR;   }
 422   | BVULT_TOK    { $kind = CVC4::kind::BITVECTOR_ULT;    }
 423   | BVULE_TOK    { $kind = CVC4::kind::BITVECTOR_ULE;    }
 424   | BVUGT_TOK    { $kind = CVC4::kind::BITVECTOR_UGT;    }
 425   | BVUGE_TOK    { $kind = CVC4::kind::BITVECTOR_UGE;    }
 426   | BVSLT_TOK    { $kind = CVC4::kind::BITVECTOR_SLT;    }
 427   | BVSLE_TOK    { $kind = CVC4::kind::BITVECTOR_SLE;    }
 428   | BVSGT_TOK    { $kind = CVC4::kind::BITVECTOR_SGT;    }
 429   | BVSGE_TOK    { $kind = CVC4::kind::BITVECTOR_SGE;    }
 430   // arrays
 431   | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
 432   | STORE_TOK    { $kind = CVC4::kind::STORE; }
 433   // NOTE: Theory operators go here
 434   ;
 435
 436 /**
 437  * Matches an operator.
 438  */
 439 parameterizedOperator[CVC4::Expr& op]
 440   : functionSymbol[op]
 441   | bitVectorOperator[op]
 442   ;
 443
 444 /**
 445  * Matches a bit-vector operator (the ones parametrized by numbers)
 446  */
 447 bitVectorOperator[CVC4::Expr& op]
 448   : EXTRACT_TOK '[' n1 = NUMERAL_TOK ':' n2 = NUMERAL_TOK ']'
 449     { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), AntlrInput::tokenToUnsigned($n2))); }
 450   | REPEAT_TOK '[' n = NUMERAL_TOK ']'
 451     { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
 452   | ZERO_EXTEND_TOK '[' n = NUMERAL_TOK ']'
 453     { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
 454   | SIGN_EXTEND_TOK '[' n = NUMERAL_TOK ']'
 455     { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); }
 456   | ROTATE_LEFT_TOK '[' n = NUMERAL_TOK ']'
 457     { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
 458   | ROTATE_RIGHT_TOK '[' n = NUMERAL_TOK ']'
 459     { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
 460   ;
 461
 462 /**
 463  * Matches a (possibly undeclared) predicate identifier (returning the string).
 464  * @param check what kind of check to do with the symbol
 465  */
 466 predicateName[std::string& name, CVC4::parser::DeclarationCheck check]
 467   :  functionName[name,check]
 468   ;
 469
 470 /**
 471  * Matches a (possibly undeclared) function identifier (returning the string)
 472  * @param check what kind of check to do with the symbol
 473  */
 474 functionName[std::string& name, CVC4::parser::DeclarationCheck check]
 475   :  identifier[name,check,SYM_VARIABLE]
 476   ;
 477
 478 /**
 479  * Matches an previously declared function symbol (returning an Expr)
 480  */
 481 functionSymbol[CVC4::Expr& fun]
 482 @declarations {
 483         std::string name;
 484 }
 485   : functionName[name,CHECK_DECLARED]
 486     { PARSER_STATE->checkFunctionLike(name);
 487       fun = PARSER_STATE->getVariable(name); }
 488   ;
 489
 490 /**
 491  * Matches an attribute name from the input (:attribute_name).
 492  */
 493 attribute[std::string& s]
 494   : ATTR_IDENTIFIER
 495     { s = AntlrInput::tokenText($ATTR_IDENTIFIER); }
 496   ;
 497
 498 functionDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command]
 499 @declarations {
 500   std::string name;
 501   std::vector<Type> sorts;
 502 }
 503   : LPAREN_TOK functionName[name,CHECK_UNDECLARED]
 504       t = sortSymbol // require at least one sort
 505     { sorts.push_back(t); }
 506       sortList[sorts] RPAREN_TOK
 507     { if( sorts.size() == 1 ) {
 508         assert( t == sorts[0] );
 509       } else {
 510         t = EXPR_MANAGER->mkFunctionType(sorts);
 511       }
 512       Expr func = PARSER_STATE->mkVar(name, t);
 513       smt_command->reset(new DeclareFunctionCommand(name, func, t));
 514     }
 515   ;
 516
 517 /**
 518  * Matches the declaration of a predicate and declares it
 519  */
 520 predicateDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command]
 521 @declarations {
 522   std::string name;
 523   std::vector<Type> p_sorts;
 524 }
 525   : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK
 526     { Type t;
 527       if( p_sorts.empty() ) {
 528         t = EXPR_MANAGER->booleanType();
 529       } else {
 530         t = EXPR_MANAGER->mkPredicateType(p_sorts);
 531       }
 532       Expr func = PARSER_STATE->mkVar(name, t);
 533       smt_command->reset(new DeclareFunctionCommand(name, func, t));
 534     }
 535   ;
 536
 537 sortDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command]
 538 @declarations {
 539   std::string name;
 540 }
 541   : sortName[name,CHECK_UNDECLARED]
 542     { Debug("parser") << "sort decl: '" << name << "'" << std::endl;
 543       Type type = PARSER_STATE->mkSort(name);
 544       smt_command->reset(new DeclareTypeCommand(name, 0, type));
 545     }
 546   ;
 547
 548 /**
 549  * Matches a sequence of sort symbols and fills them into the given vector.
 550  */
 551 sortList[std::vector<CVC4::Type>& sorts]
 552   : ( t = sortSymbol { sorts.push_back(t); })*
 553   ;
 554
 555 /**
 556  * Matches the sort symbol, which can be an arbitrary identifier.
 557  * @param check the check to perform on the name
 558  */
 559 sortName[std::string& name, CVC4::parser::DeclarationCheck check]
 560   : identifier[name,check,SYM_SORT]
 561   ;
 562
 563 sortSymbol returns [CVC4::parser::smt1::myType t]
 564 @declarations {
 565   std::string name;
 566 }
 567   : sortName[name,CHECK_NONE]
 568         { $t = PARSER_STATE->getSort(name); }
 569   | BITVECTOR_TOK '[' NUMERAL_TOK ']' {
 570         $t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK));
 571     }
 572   /* attaching 'Array' to '[' allows us to parse regular 'Array' correctly in
 573    * e.g. QF_AX, and also 'Array[m:n]' in e.g. QF_AUFBV */
 574   | 'Array[' n1=NUMERAL_TOK ':' n2=NUMERAL_TOK ']' {
 575         $t = EXPR_MANAGER->mkArrayType(EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n1)),
 576                                        EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n2)));
 577     }
 578   ;
 579
 580 /**
 581  * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'.
 582  */
 583 status[ CVC4::BenchmarkStatus& status ]
 584   : SAT_TOK       { $status = SMT_SATISFIABLE;    }
 585   | UNSAT_TOK     { $status = SMT_UNSATISFIABLE;  }
 586   | UNKNOWN_TOK   { $status = SMT_UNKNOWN;        }
 587   ;
 588
 589 /**
 590  * Matches an annotation, which is an attribute name, with an optional user
 591  * value.
 592  */
 593 annotation[CVC4::PtrCloser<CVC4::Command>* smt_command]
 594 @init {
 595   std::string key, value;
 596   std::vector<Expr> pats;
 597   Expr pat;
 598 }
 599   : PATTERN_ANNOTATION_BEGIN
 600     { PARSER_STATE->warning(":pat not supported here; ignored"); }
 601     annotatedFormulas[pats,pat] '}'
 602   | attribute[key]
 603     ( userValue[value]
 604       { smt_command->reset(
 605             new SetInfoCommand(key.c_str() + 1, SExpr(value))); }
 606     | { smt_command->reset(
 607             new EmptyCommand(std::string("annotation: ") + key)); }
 608     )
 609   ;
 610
 611 /**
 612  * Matches an annotation, which is an attribute name, with an optional user
 613  * value.
 614  */
 615 termAnnotation[CVC4::Expr& expr]
 616 @init {
 617   std::string key, value;
 618   std::vector<Expr> pats;
 619   Expr pat;
 620 }
 621   : PATTERN_ANNOTATION_BEGIN annotatedFormulas[pats,pat] '}'
 622     { if(expr.getKind() == kind::FORALL || expr.getKind() == kind::EXISTS) {
 623         pat = MK_EXPR(kind::INST_PATTERN, pats);
 624         if(expr.getNumChildren() == 3) {
 625           // we have other user patterns attached to the quantifier
 626           // already; add this one to the existing list
 627           pats = expr[2].getChildren();
 628           pats.push_back(pat);
 629           expr = MK_EXPR(expr.getKind(), expr[0], expr[1], MK_EXPR(kind::INST_PATTERN_LIST, pats));
 630         } else {
 631           // this is the only user pattern for the quantifier
 632           expr = MK_EXPR(expr.getKind(), expr[0], expr[1], MK_EXPR(kind::INST_PATTERN_LIST, pat));
 633         }
 634       } else {
 635         PARSER_STATE->warning(":pat only supported on quantifiers");
 636       }
 637     }
 638   | ':pat'
 639     { PARSER_STATE->warning("expected an instantiation pattern after :pat"); }
 640   | attribute[key] userValue[value]?
 641     { PARSER_STATE->attributeNotSupported(key); }
 642   ;
 643
 644 /**
 645  * Matches an identifier and sets the string reference parameter id.
 646  * @param id string to hold the identifier
 647  * @param check what kinds of check to do on the symbol
 648  * @param type the intended namespace for the identifier
 649  */
 650 identifier[std::string& id,
 651                    CVC4::parser::DeclarationCheck check,
 652            CVC4::parser::SymbolType type]
 653   : IDENTIFIER
 654     { id = AntlrInput::tokenText($IDENTIFIER);
 655       Debug("parser") << "identifier: " << id
 656                       << " check? " << check
 657                       << " type? " << type << std::endl;
 658       PARSER_STATE->checkDeclaration(id, check, type); }
 659   ;
 660
 661 /**
 662  * Matches a let-bound identifier and sets the string reference parameter id.
 663  * @param id string to hold the identifier
 664  * @param check what kinds of check to do on the symbol
 665  */
 666 let_identifier[std::string& id,
 667                    CVC4::parser::DeclarationCheck check]
 668   : LET_IDENTIFIER
 669     { id = AntlrInput::tokenText($LET_IDENTIFIER);
 670       Debug("parser") << "let_identifier: " << id
 671                       << " check? " << check << std::endl;
 672       PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); }
 673   ;
 674
 675 /**
 676  * Matches an flet-bound identifier and sets the string reference parameter id.
 677  * @param id string to hold the identifier
 678  * @param check what kinds of check to do on the symbol
 679  */
 680 flet_identifier[std::string& id,
 681                     CVC4::parser::DeclarationCheck check]
 682   : FLET_IDENTIFIER
 683     { id = AntlrInput::tokenText($FLET_IDENTIFIER);
 684       Debug("parser") << "flet_identifier: " << id
 685                       << " check? " << check << std::endl;
 686       PARSER_STATE->checkDeclaration(id, check); }
 687   ;
 688
 689 // Base SMT-LIB tokens
 690 ASSUMPTION_TOK  : ':assumption';
 691 BENCHMARK_TOK   : 'benchmark';
 692 EXTRAFUNS_TOK   : ':extrafuns';
 693 EXTRAPREDS_TOK  : ':extrapreds';
 694 EXTRASORTS_TOK  : ':extrasorts';
 695 FALSE_TOK       : 'false';
 696 FLET_TOK        : 'flet';
 697 FORMULA_TOK     : ':formula';
 698 ITE_TOK         : 'ite' | 'if_then_else';
 699 LET_TOK         : 'let';
 700 LOGIC_TOK       : ':logic';
 701 LPAREN_TOK      : '(';
 702 NOTES_TOK       : ':notes';
 703 RPAREN_TOK      : ')';
 704 SAT_TOK         : 'sat';
 705 STATUS_TOK      : ':status';
 706 THEORY_TOK      : 'theory';
 707 TRUE_TOK        : 'true';
 708 UNKNOWN_TOK     : 'unknown';
 709 UNSAT_TOK       : 'unsat';
 710
 711 // operators (NOTE: theory symbols go here)
 712 AMPERSAND_TOK     : '&';
 713 AND_TOK           : 'and';
 714 AT_TOK            : '@';
 715 DISTINCT_TOK      : 'distinct';
 716 DIV_TOK           : '/';
 717 EQUAL_TOK         : '=';
 718 EXISTS_TOK        : 'exists';
 719 FORALL_TOK        : 'forall';
 720 GREATER_THAN_TOK  : '>';
 721 IFF_TOK           : 'iff';
 722 IMPLIES_TOK       : 'implies';
 723 LESS_THAN_TOK     : '<';
 724 MINUS_TOK         : '-';
 725 NOT_TOK           : 'not';
 726 OR_TOK            : 'or';
 727 PERCENT_TOK       : '%';
 728 PIPE_TOK          : '|';
 729 PLUS_TOK          : '+';
 730 POUND_TOK         : '#';
 731 SELECT_TOK        : 'select';
 732 STAR_TOK          : '*';
 733 STORE_TOK         : 'store';
 734 TILDE_TOK         : '~';
 735 XOR_TOK           : 'xor';
 736
 737 // Bitvector tokens
 738 BITVECTOR_TOK     : 'BitVec';
 739 CONCAT_TOK        : 'concat';
 740 EXTRACT_TOK       : 'extract';
 741 BVAND_TOK         : 'bvand';
 742 BVOR_TOK          : 'bvor';
 743 BVXOR_TOK         : 'bvxor';
 744 BVNOT_TOK         : 'bvnot';
 745 BVNAND_TOK        : 'bvnand';
 746 BVNOR_TOK         : 'bvnor';
 747 BVXNOR_TOK        : 'bvxnor';
 748 BVCOMP_TOK        : 'bvcomp';
 749 BVMUL_TOK         : 'bvmul';
 750 BVADD_TOK         : 'bvadd';
 751 BVSUB_TOK         : 'bvsub';
 752 BVNEG_TOK         : 'bvneg';
 753 BVUDIV_TOK        : 'bvudiv';
 754 BVUREM_TOK        : 'bvurem';
 755 BVSDIV_TOK        : 'bvsdiv';
 756 BVSREM_TOK        : 'bvsrem';
 757 BVSMOD_TOK        : 'bvsmod';
 758 BVSHL_TOK         : 'bvshl';
 759 BVLSHR_TOK        : 'bvlshr';
 760 BVASHR_TOK        : 'bvashr';
 761 BVULT_TOK         : 'bvult';
 762 BVULE_TOK         : 'bvule';
 763 BVUGT_TOK         : 'bvugt';
 764 BVUGE_TOK         : 'bvuge';
 765 BVSLT_TOK         : 'bvslt';
 766 BVSLE_TOK         : 'bvsle';
 767 BVSGT_TOK         : 'bvsgt';
 768 BVSGE_TOK         : 'bvsge';
 769 REPEAT_TOK        : 'repeat';
 770 ZERO_EXTEND_TOK   : 'zero_extend';
 771 SIGN_EXTEND_TOK   : 'sign_extend';
 772 ROTATE_LEFT_TOK   : 'rotate_left';
 773 ROTATE_RIGHT_TOK  : 'rotate_right';
 774
 775 /**
 776  * Matches a bit-vector constant of the form bv123
 777  */
 778 BITVECTOR_BV_CONST
 779   : 'bv' DIGIT+
 780   ;
 781
 782 /**
 783  * Matches a bit-vector constant of the form bit(0|1)
 784  */
 785 BITVECTOR1_BV_CONST
 786   : 'bit0' | 'bit1'
 787   ;
 788
 789
 790 /**
 791  * Matches an identifier from the input. An identifier is a sequence of letters,
 792  * digits and "_", "'", "." symbols, starting with a letter.
 793  */
 794 IDENTIFIER
 795   :  ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
 796   ;
 797
 798 /**
 799  * Matches an identifier starting with a colon.
 800  */
 801 ATTR_IDENTIFIER
 802   :  ':' IDENTIFIER
 803   ;
 804
 805 /**
 806  * Matches an identifier starting with a question mark.
 807  */
 808 LET_IDENTIFIER
 809   : '?' IDENTIFIER
 810   ;
 811
 812 /**
 813  * Matches an identifier starting with a dollar sign.
 814  */
 815 FLET_IDENTIFIER
 816   : '$' IDENTIFIER
 817   ;
 818
 819 /**
 820  * Matches the value of user-defined annotations or attributes. The
 821  * only constraint imposed on a user-defined value is that it start
 822  * with an open brace and end with closed brace.
 823  */
 824 userValue[std::string& s]
 825   : USER_VALUE
 826     { s = AntlrInput::tokenText($USER_VALUE);
 827       assert(*s.begin() == '{');
 828       assert(*s.rbegin() == '}');
 829       // trim whitespace
 830       s.erase(s.begin(), s.begin() + 1);
 831       s.erase(s.begin(), std::find_if(s.begin(), s.end(), std::not1(std::ptr_fun<int, int>(std::isspace))));
 832       s.erase(s.end() - 1);
 833       s.erase(std::find_if(s.rbegin(), s.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), s.end());
 834     }
 835   ;
 836
 837 PATTERN_ANNOTATION_BEGIN
 838   : ':pat' (' ' | '\t' | '\f' | '\r' | '\n')* '{'
 839   ;
 840
 841 USER_VALUE
 842   : '{' ('\\{' | '\\}' | ~('{' | '}'))* '}'
 843   ;
 844
 845 /**
 846  * Matches and skips whitespace in the input.
 847  */
 848 WHITESPACE
 849   : (' ' | '\t' | '\f' | '\r' | '\n')+
 850     { SKIP(); }
 851   ;
 852
 853 /**
 854  * Matches a numeral from the input (non-empty sequence of digits).
 855  */
 856 NUMERAL_TOK
 857   : DIGIT+
 858   ;
 859
 860 RATIONAL_TOK
 861   : DIGIT+ '.' DIGIT+
 862   ;
 863
 864 /**
 865  * Matches a double quoted string literal. Escaping is supported, and escape
 866  * character '\' has to be escaped.
 867  */
 868 STRING_LITERAL
 869   :  '"' (ESCAPE | ~('"'|'\\'))* '"'
 870   ;
 871
 872 /**
 873  * Matches the comments and ignores them
 874  */
 875 COMMENT
 876   : ';' (~('\n' | '\r'))*
 877     { SKIP(); }
 878   ;
 879
 880
 881 /**
 882  * Matches any letter ('a'-'z' and 'A'-'Z').
 883  */
 884 fragment
 885 ALPHA
 886   :  'a'..'z'
 887   |  'A'..'Z'
 888   ;
 889
 890 /**
 891  * Matches the digits (0-9)
 892  */
 893 fragment DIGIT :   '0'..'9';
 894 // fragment NON_ZERO_DIGIT : '1'..'9';
 895 // fragment NUMERAL_SEQ : '0' | NON_ZERO_DIGIT DIGIT*;
 896
 897 /**
 898  * Matches an allowed escaped character.
 899  */
 900 fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');
 901