1 /* ******************* */
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
12 ** \brief Parser for SMT-LIB input language.
14 ** Parser for SMT-LIB input language.
23 // Skip the default error handling, just break with exceptions
24 // defaultErrorHandler = false;
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 !
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.
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"
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.
53 #pragma GCC system_header
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.
61 # define ANTLR3_INLINE_INPUT_ASCII
62 # define ANTLR3_INLINE_INPUT_8BIT
63 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
65 #include "parser/antlr_tracing.h"
66 }/* @lexer::includes */
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"
76 #include "base/ptr_closer.h"
77 #include "smt/command.h"
78 #include "parser/parser.h"
79 #include "parser/antlr_tracing.h"
87 * Just exists to provide the uintptr_t constructor that ANTLR
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) {}
98 * Just exists to provide the uintptr_t constructor that ANTLR
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 */
111 }/* @parser::includes */
113 @parser::postinclude {
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"
128 using namespace CVC4;
129 using namespace CVC4::parser;
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.) */
134 #define PARSER_STATE ((Smt1*)PARSER->super)
136 #define EXPR_MANAGER PARSER_STATE->getExprManager()
138 #define MK_EXPR EXPR_MANAGER->mkExpr
140 #define MK_CONST EXPR_MANAGER->mkConst
142 }/* @parser::postinclude */
146 * Parses an expression.
147 * @return the parsed expression
149 parseExpr returns [CVC4::parser::smt1::myExpr expr]
150 : annotatedFormula[expr]
155 * Parses a command (the whole benchmark)
156 * @return the command of the benchmark
158 parseCommand returns [CVC4::Command* cmd_return = NULL]
160 CVC4::PtrCloser<CVC4::Command> cmd;
163 cmd_return = cmd.release();
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."));
171 PARSER_STATE->parseError(std::string("expected keyword `benchmark', got `" + s + "'"));
177 * Matches the whole SMT-LIB benchmark.
178 * @return the sequence command containing the whole problem
180 benchmark [CVC4::PtrCloser<CVC4::Command>* cmd]
181 : LPAREN_TOK BENCHMARK_TOK IDENTIFIER benchAttributes[cmd] RPAREN_TOK
186 * Matches a sequence of benchmark attributes and returns a pointer to a
188 * @return the command sequence
190 benchAttributes [CVC4::PtrCloser<CVC4::Command>* cmd]
192 CVC4::PtrCloser<CVC4::CommandSequence> cmd_seq(new CommandSequence());
193 CVC4::PtrCloser<CVC4::Command> attribute;
196 cmd->reset(cmd_seq.release());
198 : (benchAttribute[&attribute]
199 { if (attribute) cmd_seq->addCommand(attribute.release()); }
204 * Matches a benchmark attribute, such as ':logic', ':formula', and returns
205 * a corresponding command
206 * @return a command corresponding to the attribute
208 benchAttribute [CVC4::PtrCloser<CVC4::Command>* smt_command]
211 BenchmarkStatus b_status;
213 CVC4::PtrCloser<CVC4::CommandSequence> command_seq;
214 CVC4::PtrCloser<CVC4::Command> declaration_command;
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());
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()); }
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()); }
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()); }
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]
252 * Matches an annotated formula.
253 * @return the expression representing the formula
255 annotatedFormula[CVC4::Expr& expr]
257 Debug("parser") << "annotated formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
260 std::vector<Expr> args; /* = getExprVector(); */
261 std::vector<Expr> args2;
262 Expr op; /* Operator expression FIXME: move away kill it */
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]);
279 PARSER_STATE->checkArity(kind, args.size());
280 expr = MK_EXPR(kind, args);
283 termAnnotation[expr]* RPAREN_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)); }
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);
297 termAnnotation[expr]* RPAREN_TOK
298 { PARSER_STATE->popScope(); }
300 | /* A non-built-in function application */
302 // Semantic predicate not necessary if parenthesized subexpressions
304 // { isFunction(LT(2)->getText()) }?
306 parameterizedOperator[op]
307 annotatedFormulas[args,expr]
309 { expr = MK_EXPR(op,args); }
310 termAnnotation[expr]* RPAREN_TOK
312 | /* An ite expression */
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
323 | /* a let/flet binding */
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(); }
335 | TRUE_TOK { expr = MK_CONST(bool(true)); }
336 | FALSE_TOK { expr = MK_CONST(bool(false)); }
338 { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_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) );
349 // NOTE: Theory constants go here
350 /* TODO: quantifiers, arithmetic constants */
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); }
360 * Matches a sequence of annotated formulas and puts them into the
362 * @param formulas the vector to fill with formulas
363 * @param expr an Expr reference for the elements of the sequence
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); } )+
372 * Matches a builtin operator symbol and sets kind to its associated Expr kind.
374 builtinOp[CVC4::Kind& kind]
376 Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
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; }
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; }
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; }
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; }
431 | SELECT_TOK { $kind = CVC4::kind::SELECT; }
432 | STORE_TOK { $kind = CVC4::kind::STORE; }
433 // NOTE: Theory operators go here
437 * Matches an operator.
439 parameterizedOperator[CVC4::Expr& op]
441 | bitVectorOperator[op]
445 * Matches a bit-vector operator (the ones parametrized by numbers)
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))); }
463 * Matches a (possibly undeclared) predicate identifier (returning the string).
464 * @param check what kind of check to do with the symbol
466 predicateName[std::string& name, CVC4::parser::DeclarationCheck check]
467 : functionName[name,check]
471 * Matches a (possibly undeclared) function identifier (returning the string)
472 * @param check what kind of check to do with the symbol
474 functionName[std::string& name, CVC4::parser::DeclarationCheck check]
475 : identifier[name,check,SYM_VARIABLE]
479 * Matches an previously declared function symbol (returning an Expr)
481 functionSymbol[CVC4::Expr& fun]
485 : functionName[name,CHECK_DECLARED]
486 { PARSER_STATE->checkFunctionLike(name);
487 fun = PARSER_STATE->getVariable(name); }
491 * Matches an attribute name from the input (:attribute_name).
493 attribute[std::string& s]
495 { s = AntlrInput::tokenText($ATTR_IDENTIFIER); }
498 functionDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command]
501 std::vector<Type> sorts;
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] );
510 t = EXPR_MANAGER->mkFunctionType(sorts);
512 Expr func = PARSER_STATE->mkVar(name, t);
513 smt_command->reset(new DeclareFunctionCommand(name, func, t));
518 * Matches the declaration of a predicate and declares it
520 predicateDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command]
523 std::vector<Type> p_sorts;
525 : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK
527 if( p_sorts.empty() ) {
528 t = EXPR_MANAGER->booleanType();
530 t = EXPR_MANAGER->mkPredicateType(p_sorts);
532 Expr func = PARSER_STATE->mkVar(name, t);
533 smt_command->reset(new DeclareFunctionCommand(name, func, t));
537 sortDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command]
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));
549 * Matches a sequence of sort symbols and fills them into the given vector.
551 sortList[std::vector<CVC4::Type>& sorts]
552 : ( t = sortSymbol { sorts.push_back(t); })*
556 * Matches the sort symbol, which can be an arbitrary identifier.
557 * @param check the check to perform on the name
559 sortName[std::string& name, CVC4::parser::DeclarationCheck check]
560 : identifier[name,check,SYM_SORT]
563 sortSymbol returns [CVC4::parser::smt1::myType t]
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));
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)));
581 * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'.
583 status[ CVC4::BenchmarkStatus& status ]
584 : SAT_TOK { $status = SMT_SATISFIABLE; }
585 | UNSAT_TOK { $status = SMT_UNSATISFIABLE; }
586 | UNKNOWN_TOK { $status = SMT_UNKNOWN; }
590 * Matches an annotation, which is an attribute name, with an optional user
593 annotation[CVC4::PtrCloser<CVC4::Command>* smt_command]
595 std::string key, value;
596 std::vector<Expr> pats;
599 : PATTERN_ANNOTATION_BEGIN
600 { PARSER_STATE->warning(":pat not supported here; ignored"); }
601 annotatedFormulas[pats,pat] '}'
604 { smt_command->reset(
605 new SetInfoCommand(key.c_str() + 1, SExpr(value))); }
606 | { smt_command->reset(
607 new EmptyCommand(std::string("annotation: ") + key)); }
612 * Matches an annotation, which is an attribute name, with an optional user
615 termAnnotation[CVC4::Expr& expr]
617 std::string key, value;
618 std::vector<Expr> pats;
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();
629 expr = MK_EXPR(expr.getKind(), expr[0], expr[1], MK_EXPR(kind::INST_PATTERN_LIST, pats));
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));
635 PARSER_STATE->warning(":pat only supported on quantifiers");
639 { PARSER_STATE->warning("expected an instantiation pattern after :pat"); }
640 | attribute[key] userValue[value]?
641 { PARSER_STATE->attributeNotSupported(key); }
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
650 identifier[std::string& id,
651 CVC4::parser::DeclarationCheck check,
652 CVC4::parser::SymbolType type]
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); }
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
666 let_identifier[std::string& id,
667 CVC4::parser::DeclarationCheck check]
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); }
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
680 flet_identifier[std::string& id,
681 CVC4::parser::DeclarationCheck check]
683 { id = AntlrInput::tokenText($FLET_IDENTIFIER);
684 Debug("parser") << "flet_identifier: " << id
685 << " check? " << check << std::endl;
686 PARSER_STATE->checkDeclaration(id, check); }
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';
697 FORMULA_TOK : ':formula';
698 ITE_TOK : 'ite' | 'if_then_else';
700 LOGIC_TOK : ':logic';
702 NOTES_TOK : ':notes';
705 STATUS_TOK : ':status';
706 THEORY_TOK : 'theory';
708 UNKNOWN_TOK : 'unknown';
711 // operators (NOTE: theory symbols go here)
715 DISTINCT_TOK : 'distinct';
718 EXISTS_TOK : 'exists';
719 FORALL_TOK : 'forall';
720 GREATER_THAN_TOK : '>';
722 IMPLIES_TOK : 'implies';
731 SELECT_TOK : 'select';
738 BITVECTOR_TOK : 'BitVec';
739 CONCAT_TOK : 'concat';
740 EXTRACT_TOK : 'extract';
745 BVNAND_TOK : 'bvnand';
747 BVXNOR_TOK : 'bvxnor';
748 BVCOMP_TOK : 'bvcomp';
753 BVUDIV_TOK : 'bvudiv';
754 BVUREM_TOK : 'bvurem';
755 BVSDIV_TOK : 'bvsdiv';
756 BVSREM_TOK : 'bvsrem';
757 BVSMOD_TOK : 'bvsmod';
759 BVLSHR_TOK : 'bvlshr';
760 BVASHR_TOK : 'bvashr';
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';
776 * Matches a bit-vector constant of the form bv123
783 * Matches a bit-vector constant of the form bit(0|1)
791 * Matches an identifier from the input. An identifier is a sequence of letters,
792 * digits and "_", "'", "." symbols, starting with a letter.
795 : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
799 * Matches an identifier starting with a colon.
806 * Matches an identifier starting with a question mark.
813 * Matches an identifier starting with a dollar sign.
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.
824 userValue[std::string& s]
826 { s = AntlrInput::tokenText($USER_VALUE);
827 assert(*s.begin() == '{');
828 assert(*s.rbegin() == '}');
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());
837 PATTERN_ANNOTATION_BEGIN
838 : ':pat' (' ' | '\t' | '\f' | '\r' | '\n')* '{'
842 : '{' ('\\{' | '\\}' | ~('{' | '}'))* '}'
846 * Matches and skips whitespace in the input.
849 : (' ' | '\t' | '\f' | '\r' | '\n')+
854 * Matches a numeral from the input (non-empty sequence of digits).
865 * Matches a double quoted string literal. Escaping is supported, and escape
866 * character '\' has to be escaped.
869 : '"' (ESCAPE | ~('"'|'\\'))* '"'
873 * Matches the comments and ignores them
876 : ';' (~('\n' | '\r'))*
882 * Matches any letter ('a'-'z' and 'A'-'Z').
891 * Matches the digits (0-9)
893 fragment DIGIT : '0'..'9';
894 // fragment NON_ZERO_DIGIT : '1'..'9';
895 // fragment NUMERAL_SEQ : '0' | NON_ZERO_DIGIT DIGIT*;
898 * Matches an allowed escaped character.
900 fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');