1 /* ******************* */
4 ** Original author: cconway
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): taking
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 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
14 ** \brief Parser for SMT-LIB v2 input language.
16 ** Parser for SMT-LIB v2 input language.
25 // Skip the default error handling, just break with exceptions
26 // defaultErrorHandler = false;
28 // Only lookahead of <= k requested (disable for LL* parsing)
29 // Note that CVC4's BoundedTokenBuffer requires a fixed k !
30 // If you change this k, change it also in smt2_input.cpp !
36 ** This file is part of the CVC4 prototype.
37 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
38 ** Courant Institute of Mathematical Sciences
39 ** New York University
40 ** See the file COPYING in the top-level source directory for licensing
47 /** This suppresses warnings about the redefinition of token symbols between
48 * different parsers. The redefinitions should be harmless as long as no
49 * client: (a) #include's the lexer headers for two grammars AND (b) uses the
50 * token symbol definitions.
52 #pragma GCC system_header
54 /* This improves performance by ~10 percent on big inputs.
55 * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
56 * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
57 * Otherwise, we have to let the lexer detect the encoding at runtime.
59 #define ANTLR3_INLINE_INPUT_ASCII
61 #include "parser/antlr_tracing.h"
63 }/* @lexer::includes */
68 #include "parser/smt2/smt2.h"
69 #include "parser/antlr_input.h"
70 #include "parser/antlr_tracing.h"
73 using namespace CVC4::parser;
76 #define PARSER_STATE ((Smt2*)LEXER->super)
77 }/* @lexer::postinclude */
80 #include "expr/command.h"
81 #include "parser/parser.h"
89 * Just exists to provide the uintptr_t constructor that ANTLR
92 struct myExpr : public CVC4::Expr {
93 myExpr() : CVC4::Expr() {}
94 myExpr(void*) : CVC4::Expr() {}
95 myExpr(const Expr& e) : CVC4::Expr(e) {}
96 myExpr(const myExpr& e) : CVC4::Expr(e) {}
98 }/* CVC4::parser::smt2 namespace */
99 }/* CVC4::parser namespace */
100 }/* CVC4 namespace */
102 }/* @parser::includes */
104 @parser::postinclude {
106 #include "expr/expr.h"
107 #include "expr/kind.h"
108 #include "expr/type.h"
109 #include "parser/antlr_input.h"
110 #include "parser/parser.h"
111 #include "parser/smt2/smt2.h"
112 #include "util/integer.h"
113 #include "util/output.h"
114 #include "util/rational.h"
117 using namespace CVC4;
118 using namespace CVC4::parser;
120 /* These need to be macros so they can refer to the PARSER macro, which will be defined
121 * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
123 #define PARSER_STATE ((Smt2*)PARSER->super)
125 #define EXPR_MANAGER PARSER_STATE->getExprManager()
127 #define MK_EXPR EXPR_MANAGER->mkExpr
129 #define MK_CONST EXPR_MANAGER->mkConst
130 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
132 }/* parser::postinclude */
135 * Parses an expression.
136 * @return the parsed expression, or the Null Expr if we've reached the end of the input
138 parseExpr returns [CVC4::parser::smt2::myExpr expr]
145 * @return the parsed command, or NULL if we've reached the end of the input
147 parseCommand returns [CVC4::Command* cmd = NULL]
148 : LPAREN_TOK c = command RPAREN_TOK { $cmd = c; }
153 * Parse the internal portion of the command, ignoring the surrounding parentheses.
155 command returns [CVC4::Command* cmd = NULL]
158 std::vector<std::string> names;
161 std::vector<Expr> terms;
162 std::vector<Type> sorts;
163 std::vector<std::pair<std::string, Type> > sortedVarNames;
166 : /* set the logic */
168 { name = AntlrInput::tokenText($SYMBOL);
169 Debug("parser") << "set logic: '" << name << "'" << std::endl;
170 if( PARSER_STATE->strictModeEnabled() && PARSER_STATE->logicIsSet() ) {
171 PARSER_STATE->parseError("Only one set-logic is allowed.");
173 PARSER_STATE->setLogic(name);
174 $cmd = new SetBenchmarkLogicCommand(name); }
175 | SET_INFO_TOK KEYWORD symbolicExpr[sexpr]
176 { name = AntlrInput::tokenText($KEYWORD);
177 PARSER_STATE->setInfo(name,sexpr);
178 cmd = new SetInfoCommand(name,sexpr); }
181 { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD)); }
183 SET_OPTION_TOK KEYWORD symbolicExpr[sexpr]
184 { name = AntlrInput::tokenText($KEYWORD);
185 PARSER_STATE->setOption(name,sexpr);
186 cmd = new SetOptionCommand(name,sexpr); }
188 GET_OPTION_TOK KEYWORD
189 { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD)); }
190 | /* sort declaration */
191 DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL
192 { Debug("parser") << "declare sort: '" << name
193 << "' arity=" << n << std::endl;
194 unsigned arity = AntlrInput::tokenToUnsigned(n);
196 Type type = PARSER_STATE->mkSort(name);
197 $cmd = new DeclareTypeCommand(name, 0, type);
199 Type type = PARSER_STATE->mkSortConstructor(name, arity);
200 $cmd = new DeclareTypeCommand(name, arity, type);
203 | /* sort definition */
204 DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT]
205 LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
207 PARSER_STATE->pushScope();
208 for(std::vector<std::string>::const_iterator i = names.begin(),
212 sorts.push_back(PARSER_STATE->mkSort(*i));
216 { PARSER_STATE->popScope();
217 // Do NOT call mkSort, since that creates a new sort!
218 // This name is not its own distinct sort, it's an alias.
219 PARSER_STATE->defineParameterizedType(name, sorts, t);
220 $cmd = new DefineTypeCommand(name, sorts, t);
222 | /* function declaration */
223 DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
224 LPAREN_TOK sortList[sorts] RPAREN_TOK
226 { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
227 if( sorts.size() > 0 ) {
228 t = EXPR_MANAGER->mkFunctionType(sorts, t);
230 PARSER_STATE->mkVar(name, t);
231 $cmd = new DeclareFunctionCommand(name, t); }
232 | /* function definition */
233 DEFINE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
234 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
236 { /* add variables to parser state before parsing term */
237 Debug("parser") << "define fun: '" << name << "'" << std::endl;
238 if( sortedVarNames.size() > 0 ) {
239 std::vector<CVC4::Type> sorts;
240 sorts.reserve(sortedVarNames.size());
241 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
242 sortedVarNames.begin(), iend = sortedVarNames.end();
245 sorts.push_back((*i).second);
247 t = EXPR_MANAGER->mkFunctionType(sorts, t);
249 PARSER_STATE->pushScope();
250 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
251 sortedVarNames.begin(), iend = sortedVarNames.end();
254 terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
258 { PARSER_STATE->popScope();
259 // declare the name down here (while parsing term, signature
260 // must not be extended with the name itself; no recursion
262 Expr func = PARSER_STATE->mkFunction(name, t);
263 $cmd = new DefineFunctionCommand(name, func, terms, expr);
268 { if(PARSER_STATE->strictModeEnabled()) {
269 PARSER_STATE->parseError("Strict compliance mode doesn't recognize \"eval\". Maybe you want (get-value...)?");
272 LPAREN_TOK termList[terms,expr] RPAREN_TOK
273 { if(terms.size() == 1) {
274 $cmd = new GetValueCommand(terms[0]);
276 CommandSequence* seq = new CommandSequence();
277 for(std::vector<Expr>::const_iterator i = terms.begin(),
281 seq->addCommand(new GetValueCommand(*i));
286 | /* get-assignment */
288 { cmd = new GetAssignmentCommand; }
290 ASSERT_TOK term[expr]
291 { cmd = new AssertCommand(expr); }
294 { cmd = new CheckSatCommand(MK_CONST(bool(true))); }
295 | /* get-assertions */
297 { cmd = new GetAssertionsCommand; }
300 { UNSUPPORTED("get-proof command not yet supported"); }
301 | /* get-unsat-core */
303 { UNSUPPORTED("unsat cores not yet supported"); }
307 { unsigned n = AntlrInput::tokenToUnsigned(k);
309 cmd = new EmptyCommand;
311 cmd = new PushCommand;
313 CommandSequence* seq = new CommandSequence;
315 seq->addCommand(new PushCommand);
320 | { if(PARSER_STATE->strictModeEnabled()) {
321 PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to PUSH. Maybe you want (push 1)?");
323 cmd = new PushCommand;
328 { unsigned n = AntlrInput::tokenToUnsigned(k);
330 cmd = new EmptyCommand;
332 cmd = new PopCommand;
334 CommandSequence* seq = new CommandSequence;
336 seq->addCommand(new PopCommand);
341 | { if(PARSER_STATE->strictModeEnabled()) {
342 PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to POP. Maybe you want (pop 1)?");
344 cmd = new PopCommand;
348 { cmd = new QuitCommand; }
350 /* CVC4-extended SMT-LIBv2 commands */
351 | extendedCommand[cmd]
352 { if(PARSER_STATE->strictModeEnabled()) {
353 PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode.");
358 extendedCommand[CVC4::Command*& cmd]
360 std::vector<CVC4::Datatype> dts;
363 /* Z3's extended SMT-LIBv2 set of commands syntax */
364 : DECLARE_DATATYPES_TOK
365 { /* open a scope to keep the UnresolvedTypes contained */
366 PARSER_STATE->pushScope(); }
367 LPAREN_TOK ( LPAREN_TOK datatypeDef[dts] RPAREN_TOK )+ RPAREN_TOK
368 { PARSER_STATE->popScope();
369 cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
379 | SIMPLIFY_TOK term[e]
380 { cmd = new SimplifyCommand(e); }
383 { Message() << AntlrInput::tokenText($STRING_LITERAL) << std::endl; }
384 | { Message() << std::endl; } )
387 symbolicExpr[CVC4::SExpr& sexpr]
389 std::vector<SExpr> children;
393 { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); }
395 { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); }
397 { sexpr = SExpr(AntlrInput::tokenText($STRING_LITERAL)); }
399 { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); }
401 { std::stringstream ss;
402 ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k);
403 sexpr = SExpr(ss.str());
406 { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
408 (symbolicExpr[sexpr] { children.push_back(sexpr); } )*
410 { sexpr = SExpr(children); }
415 * @return the expression representing the formula
417 term[CVC4::Expr& expr]
419 Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
423 std::vector<Expr> args;
426 : /* a built-in operator application */
427 LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
429 if( kind == CVC4::kind::EQUAL &&
431 args[0].getType() == EXPR_MANAGER->booleanType() ) {
432 /* Use IFF for boolean equalities. */
433 kind = CVC4::kind::IFF;
436 if( !PARSER_STATE->strictModeEnabled() &&
437 (kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
439 /* Unary AND/OR can be replaced with the argument.
440 It just so happens expr should already by the only argument. */
441 Assert( expr == args[0] );
442 } else if( CVC4::kind::isAssociative(kind) &&
443 args.size() > EXPR_MANAGER->maxArity(kind) ) {
444 /* Special treatment for associative operators with lots of children */
445 expr = EXPR_MANAGER->mkAssociative(kind,args);
446 } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) {
447 expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
449 PARSER_STATE->checkOperator(kind, args.size());
450 expr = MK_EXPR(kind, args);
454 | /* A non-built-in function application */
456 functionName[name,CHECK_DECLARED]
457 { PARSER_STATE->checkFunctionLike(name);
458 const bool isDefinedFunction =
459 PARSER_STATE->isDefinedFunction(name);
460 if(isDefinedFunction) {
461 expr = PARSER_STATE->getFunction(name);
462 kind = CVC4::kind::APPLY;
464 expr = PARSER_STATE->getVariable(name);
465 kind = CVC4::kind::APPLY_UF;
467 args.push_back(expr);
469 termList[args,expr] RPAREN_TOK
470 { Debug("parser") << "args has size " << args.size() << std::endl << "expr is " << expr << std::endl;
471 for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
472 Debug("parser") << "++ " << *i << std::endl;
473 expr = MK_EXPR(kind, args); }
475 | /* An indexed function application */
476 LPAREN_TOK indexedFunctionName[op] termList[args,expr] RPAREN_TOK
477 { expr = MK_EXPR(op, args); }
479 | /* a let binding */
480 LPAREN_TOK LET_TOK LPAREN_TOK
481 { PARSER_STATE->pushScope(); }
482 ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[expr] RPAREN_TOK
483 { PARSER_STATE->defineVar(name,expr); } )+
487 { PARSER_STATE->popScope(); }
490 | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
491 { const bool isDefinedFunction =
492 PARSER_STATE->isDefinedFunction(name);
493 if(isDefinedFunction) {
494 expr = MK_EXPR(CVC4::kind::APPLY,
495 PARSER_STATE->getFunction(name));
497 expr = PARSER_STATE->getVariable(name);
501 /* attributed expressions */
502 | LPAREN_TOK ATTRIBUTE_TOK term[expr] KEYWORD symbolicExpr[sexpr] RPAREN_TOK
503 { std::string attr = AntlrInput::tokenText($KEYWORD);
504 if(attr == ":named") {
505 name = sexpr.getValue();
506 // FIXME ensure expr is a closed subterm
507 // check that sexpr is a fresh function symbol
508 PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
510 Expr func = PARSER_STATE->mkFunction(name, expr.getType());
511 // bind name to expr with define-fun
513 new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
514 PARSER_STATE->preemptCommand(c);
516 std::stringstream ss;
517 ss << "Attribute `" << attr << "' not supported";
518 PARSER_STATE->parseError(ss.str());
524 { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
527 { // FIXME: This doesn't work because an SMT rational is not a
528 // valid GMP rational string
529 expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
531 | LPAREN_TOK INDEX_TOK bvLit=SYMBOL size=INTEGER_LITERAL RPAREN_TOK
532 { if(AntlrInput::tokenText($bvLit).find("bv") == 0) {
533 expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) );
535 PARSER_STATE->parseError("Unexpected symbol `" + AntlrInput::tokenText($bvLit) + "'");
540 { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
541 std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
542 expr = MK_CONST( BitVector(hexString, 16) ); }
545 { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
546 std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
547 expr = MK_CONST( BitVector(binString, 2) ); }
549 // NOTE: Theory constants go here
553 * Matches a bit-vector operator (the ones parametrized by numbers)
555 indexedFunctionName[CVC4::Expr& op]
556 : LPAREN_TOK INDEX_TOK
557 ( 'extract' n1=INTEGER_LITERAL n2=INTEGER_LITERAL
558 { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1),
559 AntlrInput::tokenToUnsigned($n2))); }
560 | 'repeat' n=INTEGER_LITERAL
561 { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
562 | 'zero_extend' n=INTEGER_LITERAL
563 { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
564 | 'sign_extend' n=INTEGER_LITERAL
565 { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); }
566 | 'rotate_left' n=INTEGER_LITERAL
567 { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
568 | 'rotate_right' n=INTEGER_LITERAL
569 { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
570 | badIndexedFunctionName
576 * Matches an erroneous indexed function name (and args) for better
579 badIndexedFunctionName
583 : symbol[name,CHECK_NONE,SYM_VARIABLE] INTEGER_LITERAL+
584 { PARSER_STATE->parseError(std::string("Unknown indexed function `") + name + "'"); }
588 * Matches a sequence of terms and puts them into the formulas
590 * @param formulas the vector to fill with terms
591 * @param expr an Expr reference for the elements of the sequence
593 /* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
594 * time through this rule. */
595 termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
596 : ( term[expr] { formulas.push_back(expr); } )+
600 * Matches a builtin operator symbol and sets kind to its associated Expr kind.
602 builtinOp[CVC4::Kind& kind]
604 Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
606 : NOT_TOK { $kind = CVC4::kind::NOT; }
607 | IMPLIES_TOK { $kind = CVC4::kind::IMPLIES; }
608 | AND_TOK { $kind = CVC4::kind::AND; }
609 | OR_TOK { $kind = CVC4::kind::OR; }
610 | XOR_TOK { $kind = CVC4::kind::XOR; }
611 | EQUAL_TOK { $kind = CVC4::kind::EQUAL; }
612 | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
613 | ITE_TOK { $kind = CVC4::kind::ITE; }
615 { $kind = CVC4::kind::GT; }
616 | GREATER_THAN_EQUAL_TOK
617 { $kind = CVC4::kind::GEQ; }
618 | LESS_THAN_EQUAL_TOK
619 { $kind = CVC4::kind::LEQ; }
621 { $kind = CVC4::kind::LT; }
622 | PLUS_TOK { $kind = CVC4::kind::PLUS; }
623 | MINUS_TOK { $kind = CVC4::kind::MINUS; }
624 | STAR_TOK { $kind = CVC4::kind::MULT; }
625 | DIV_TOK { $kind = CVC4::kind::DIVISION; }
627 | SELECT_TOK { $kind = CVC4::kind::SELECT; }
628 | STORE_TOK { $kind = CVC4::kind::STORE; }
630 | CONCAT_TOK { $kind = CVC4::kind::BITVECTOR_CONCAT; }
631 | BVNOT_TOK { $kind = CVC4::kind::BITVECTOR_NOT; }
632 | BVAND_TOK { $kind = CVC4::kind::BITVECTOR_AND; }
633 | BVOR_TOK { $kind = CVC4::kind::BITVECTOR_OR; }
634 | BVNEG_TOK { $kind = CVC4::kind::BITVECTOR_NEG; }
635 | BVADD_TOK { $kind = CVC4::kind::BITVECTOR_PLUS; }
636 | BVMUL_TOK { $kind = CVC4::kind::BITVECTOR_MULT; }
637 | BVUDIV_TOK { $kind = CVC4::kind::BITVECTOR_UDIV; }
638 | BVUREM_TOK { $kind = CVC4::kind::BITVECTOR_UREM; }
639 | BVSHL_TOK { $kind = CVC4::kind::BITVECTOR_SHL; }
640 | BVLSHR_TOK { $kind = CVC4::kind::BITVECTOR_LSHR; }
641 | BVULT_TOK { $kind = CVC4::kind::BITVECTOR_ULT; }
642 | BVNAND_TOK { $kind = CVC4::kind::BITVECTOR_NAND; }
643 | BVNOR_TOK { $kind = CVC4::kind::BITVECTOR_NOR; }
644 | BVXOR_TOK { $kind = CVC4::kind::BITVECTOR_XOR; }
645 | BVXNOR_TOK { $kind = CVC4::kind::BITVECTOR_XNOR; }
646 | BVCOMP_TOK { $kind = CVC4::kind::BITVECTOR_COMP; }
647 | BVSUB_TOK { $kind = CVC4::kind::BITVECTOR_SUB; }
648 | BVSDIV_TOK { $kind = CVC4::kind::BITVECTOR_SDIV; }
649 | BVSREM_TOK { $kind = CVC4::kind::BITVECTOR_SREM; }
650 | BVSMOD_TOK { $kind = CVC4::kind::BITVECTOR_SMOD; }
651 | BVASHR_TOK { $kind = CVC4::kind::BITVECTOR_ASHR; }
652 | BVULE_TOK { $kind = CVC4::kind::BITVECTOR_ULE; }
653 | BVUGT_TOK { $kind = CVC4::kind::BITVECTOR_UGT; }
654 | BVUGE_TOK { $kind = CVC4::kind::BITVECTOR_UGE; }
655 | BVSLT_TOK { $kind = CVC4::kind::BITVECTOR_SLT; }
656 | BVSLE_TOK { $kind = CVC4::kind::BITVECTOR_SLE; }
657 | BVSGT_TOK { $kind = CVC4::kind::BITVECTOR_SGT; }
658 | BVSGE_TOK { $kind = CVC4::kind::BITVECTOR_SGE; }
660 // NOTE: Theory operators go here
664 * Matches a (possibly undeclared) function symbol (returning the string)
665 * @param check what kind of check to do with the symbol
667 functionName[std::string& name, CVC4::parser::DeclarationCheck check]
668 : symbol[name,check,SYM_VARIABLE]
672 * Matches an previously declared function symbol (returning an Expr)
674 functionSymbol[CVC4::Expr& fun]
678 : functionName[name,CHECK_DECLARED]
679 { PARSER_STATE->checkFunctionLike(name);
680 fun = PARSER_STATE->getVariable(name); }
684 * Matches a sequence of sort symbols and fills them into the given
687 sortList[std::vector<CVC4::Type>& sorts]
691 : ( sortSymbol[t] { sorts.push_back(t); } )*
695 * Matches a sequence of (variable,sort) symbol pairs and fills them
696 * into the given vector.
698 sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars]
703 : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t] RPAREN_TOK
704 { sortedVars.push_back(make_pair(name, t)); }
709 * Matches the sort symbol, which can be an arbitrary symbol.
710 * @param check the check to perform on the name
712 sortName[std::string& name, CVC4::parser::DeclarationCheck check]
713 : symbol[name,check,SYM_SORT]
716 sortSymbol[CVC4::Type& t]
719 std::vector<CVC4::Type> args;
720 std::vector<uint64_t> numerals;
722 : sortName[name,CHECK_NONE]
723 { t = PARSER_STATE->getSort(name); }
724 | LPAREN_TOK INDEX_TOK symbol[name,CHECK_NONE,SYM_SORT] nonemptyNumeralList[numerals] RPAREN_TOK
726 if( name == "BitVec" ) {
727 if( numerals.size() != 1 ) {
728 PARSER_STATE->parseError("Illegal bitvector type.");
730 t = EXPR_MANAGER->mkBitVectorType(numerals.front());
735 | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
737 if( name == "Array" ) {
738 if( args.size() != 2 ) {
739 PARSER_STATE->parseError("Illegal array type.");
741 t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
743 t = PARSER_STATE->getSort(name, args);
749 * Matches a list of symbols, with check and type arguments as for the
750 * symbol[] rule below.
752 symbolList[std::vector<std::string>& names,
753 CVC4::parser::DeclarationCheck check,
754 CVC4::parser::SymbolType type]
758 : ( symbol[id,check,type] { names.push_back(id); } )*
762 * Matches an symbol and sets the string reference parameter id.
763 * @param id string to hold the symbol
764 * @param check what kinds of check to do on the symbol
765 * @param type the intended namespace for the symbol
767 symbol[std::string& id,
768 CVC4::parser::DeclarationCheck check,
769 CVC4::parser::SymbolType type]
771 { id = AntlrInput::tokenText($SYMBOL);
772 Debug("parser") << "symbol: " << id
773 << " check? " << check
774 << " type? " << type << std::endl;
775 PARSER_STATE->checkDeclaration(id, check, type); }
779 * Matches a nonempty list of numerals.
780 * @param numerals the (empty) vector to house the numerals.
782 nonemptyNumeralList[std::vector<uint64_t>& numerals]
784 { numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
789 * Parses a datatype definition
791 datatypeDef[std::vector<CVC4::Datatype>& datatypes]
795 std::vector< Type > params;
797 /* This really needs to be CHECK_NONE, or mutually-recursive
798 * datatypes won't work, because this type will already be
799 * "defined" as an unresolved type; don't worry, we check
801 : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
802 ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
803 t = PARSER_STATE->mkSort(id2);
804 params.push_back( t );
806 ( symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
807 t = PARSER_STATE->mkSort(id2);
808 params.push_back( t ); }
811 { datatypes.push_back(Datatype(id,params));
812 if(!PARSER_STATE->isUnresolvedType(id)) {
813 // if not unresolved, must be undeclared
814 PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
817 ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+
818 { PARSER_STATE->popScope(); }
822 * Parses a constructor defintion for type
824 constructorDef[CVC4::Datatype& type]
827 CVC4::Datatype::Constructor* ctor = NULL;
829 : symbol[id,CHECK_UNDECLARED,SYM_SORT]
831 std::string testerId("is_");
833 PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
834 ctor = new CVC4::Datatype::Constructor(id, testerId);
836 ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
837 { // make the constructor
838 type.addConstructor(*ctor);
839 Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
844 selector[CVC4::Datatype::Constructor& ctor]
849 : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t]
850 { ctor.addArg(id, t);
851 Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
855 // Base SMT-LIB tokens
856 ASSERT_TOK : 'assert';
857 CHECKSAT_TOK : 'check-sat';
858 DECLARE_FUN_TOK : 'declare-fun';
859 DECLARE_SORT_TOK : 'declare-sort';
860 DEFINE_FUN_TOK : 'define-fun';
861 DEFINE_SORT_TOK : 'define-sort';
862 GET_VALUE_TOK : 'get-value';
863 GET_ASSIGNMENT_TOK : 'get-assignment';
864 GET_ASSERTIONS_TOK : 'get-assertions';
865 GET_PROOF_TOK : 'get-proof';
866 GET_UNSAT_CORE_TOK : 'get-unsat-core';
874 SET_LOGIC_TOK : 'set-logic';
875 SET_INFO_TOK : 'set-info';
876 GET_INFO_TOK : 'get-info';
877 SET_OPTION_TOK : 'set-option';
878 GET_OPTION_TOK : 'get-option';
883 DECLARE_DATATYPES_TOK : 'declare-datatypes';
884 DECLARE_SORTS_TOK : 'declare-sorts';
885 DECLARE_FUNS_TOK : 'declare-funs';
886 DECLARE_PREDS_TOK : 'declare-preds';
887 DEFINE_TOK : 'define';
888 DEFINE_SORTS_TOK : 'define-sorts';
889 DECLARE_CONST_TOK : 'declare-const';
890 SIMPLIFY_TOK : 'simplify';
894 // operators (NOTE: theory symbols go here)
898 DISTINCT_TOK : 'distinct';
901 EXISTS_TOK : 'exists';
902 FORALL_TOK : 'forall';
903 GREATER_THAN_TOK : '>';
904 GREATER_THAN_EQUAL_TOK : '>=';
907 LESS_THAN_EQUAL_TOK : '<=';
911 // PERCENT_TOK : '%';
914 SELECT_TOK : 'select';
920 CONCAT_TOK : 'concat';
927 BVUDIV_TOK : 'bvudiv';
928 BVUREM_TOK : 'bvurem';
930 BVLSHR_TOK : 'bvlshr';
932 BVNAND_TOK : 'bvnand';
935 BVXNOR_TOK : 'bvxnor';
936 BVCOMP_TOK : 'bvcomp';
938 BVSDIV_TOK : 'bvsdiv';
939 BVSREM_TOK : 'bvsrem';
940 BVSMOD_TOK : 'bvsmod';
941 BVASHR_TOK : 'bvashr';
951 * Matches a symbol from the input. A symbol is a "simple" symbol or a
952 * sequence of printable ASCII characters that starts and ends with | and
953 * does not otherwise contain |.
961 * Matches a keyword from the input. A keyword is a simple symbol prefixed
968 /** Matches a "simple" symbol: a non-empty sequence of letters, digits and
969 * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
970 * digit, and is not the special reserved symbol '_'.
972 fragment SIMPLE_SYMBOL
973 : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)+
975 | SYMBOL_CHAR_NOUNDERSCORE
979 * Matches and skips whitespace in the input.
982 : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }
986 * Matches an integer constant from the input (non-empty sequence of
987 * digits, with no leading zeroes).
994 * Match an integer constant. In non-strict mode, this is any sequence
995 * of digits. In strict mode, non-zero integers can't have leading
1000 char *start = (char*) GETCHARINDEX();
1003 { Debug("parser-extra") << "NUMERAL: "
1004 << (uintptr_t)start << ".." << GETCHARINDEX()
1005 << " strict? " << (bool)(PARSER_STATE->strictModeEnabled())
1006 << " ^0? " << (bool)(*start == '0')
1007 << " len>1? " << (bool)(start < (char*)(GETCHARINDEX() - 1))
1009 { !PARSER_STATE->strictModeEnabled() ||
1011 start == (char*)(GETCHARINDEX() - 1) }?
1015 * Matches a decimal constant from the input.
1018 : NUMERAL '.' DIGIT+
1022 * Matches a hexadecimal constant.
1029 * Matches a binary constant.
1037 * Matches a double quoted string literal. Escaping is supported, and
1038 * escape character '\' has to be escaped.
1041 : '"' (ESCAPE | ~('"'|'\\'))* '"'
1045 * Matches the comments and ignores them
1048 : ';' (~('\n' | '\r'))* { SKIP(); }
1052 * Matches any letter ('a'-'z' and 'A'-'Z').
1061 * Matches the digits (0-9)
1063 fragment DIGIT : '0'..'9';
1065 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
1068 * Matches the characters that may appear in a "symbol" (i.e., an identifier)
1070 fragment SYMBOL_CHAR_NOUNDERSCORE
1071 : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '~'
1072 | '&' | '^' | '<' | '>' | '@'
1075 fragment SYMBOL_CHAR
1076 : SYMBOL_CHAR_NOUNDERSCORE | '_'
1080 * Matches an allowed escaped character.
1082 fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');