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"
72 using namespace CVC4::parser;
75 #define PARSER_STATE ((Smt2*)LEXER->super)
76 }/* @lexer::postinclude */
79 #include "expr/command.h"
80 #include "parser/parser.h"
81 #include "parser/antlr_tracing.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 PARSER_STATE->checkThatLogicIsSet();
195 unsigned arity = AntlrInput::tokenToUnsigned(n);
197 Type type = PARSER_STATE->mkSort(name);
198 $cmd = new DeclareTypeCommand(name, 0, type);
200 Type type = PARSER_STATE->mkSortConstructor(name, arity);
201 $cmd = new DeclareTypeCommand(name, arity, type);
204 | /* sort definition */
205 DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT]
206 LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
208 PARSER_STATE->checkThatLogicIsSet();
209 PARSER_STATE->pushScope();
210 for(std::vector<std::string>::const_iterator i = names.begin(),
214 sorts.push_back(PARSER_STATE->mkSort(*i));
217 sortSymbol[t,CHECK_DECLARED]
218 { PARSER_STATE->popScope();
219 // Do NOT call mkSort, since that creates a new sort!
220 // This name is not its own distinct sort, it's an alias.
221 PARSER_STATE->defineParameterizedType(name, sorts, t);
222 $cmd = new DefineTypeCommand(name, sorts, t);
224 | /* function declaration */
225 DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
226 LPAREN_TOK sortList[sorts] RPAREN_TOK
227 sortSymbol[t,CHECK_DECLARED]
228 { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
229 PARSER_STATE->checkThatLogicIsSet();
230 if( sorts.size() > 0 ) {
231 t = EXPR_MANAGER->mkFunctionType(sorts, t);
233 PARSER_STATE->mkVar(name, t);
234 $cmd = new DeclareFunctionCommand(name, t); }
235 | /* function definition */
236 DEFINE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
237 LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
238 sortSymbol[t,CHECK_DECLARED]
239 { /* add variables to parser state before parsing term */
240 Debug("parser") << "define fun: '" << name << "'" << std::endl;
241 PARSER_STATE->checkThatLogicIsSet();
242 if( sortedVarNames.size() > 0 ) {
243 std::vector<CVC4::Type> sorts;
244 sorts.reserve(sortedVarNames.size());
245 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
246 sortedVarNames.begin(), iend = sortedVarNames.end();
249 sorts.push_back((*i).second);
251 t = EXPR_MANAGER->mkFunctionType(sorts, t);
253 PARSER_STATE->pushScope();
254 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
255 sortedVarNames.begin(), iend = sortedVarNames.end();
258 terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
262 { PARSER_STATE->popScope();
263 // declare the name down here (while parsing term, signature
264 // must not be extended with the name itself; no recursion
266 Expr func = PARSER_STATE->mkFunction(name, t);
267 $cmd = new DefineFunctionCommand(name, func, terms, expr);
270 GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK
271 { PARSER_STATE->checkThatLogicIsSet();
272 if(terms.size() == 1) {
273 $cmd = new GetValueCommand(terms[0]);
275 CommandSequence* seq = new CommandSequence();
276 for(std::vector<Expr>::const_iterator i = terms.begin(),
280 seq->addCommand(new GetValueCommand(*i));
285 | /* get-assignment */
287 { PARSER_STATE->checkThatLogicIsSet();
288 cmd = new GetAssignmentCommand; }
290 ASSERT_TOK term[expr]
291 { PARSER_STATE->checkThatLogicIsSet();
292 cmd = new AssertCommand(expr); }
295 { PARSER_STATE->checkThatLogicIsSet();
296 cmd = new CheckSatCommand(MK_CONST(bool(true))); }
297 | /* get-assertions */
299 { PARSER_STATE->checkThatLogicIsSet();
300 cmd = new GetAssertionsCommand; }
303 { PARSER_STATE->checkThatLogicIsSet();
304 cmd = new GetProofCommand; }
305 | /* get-unsat-core */
307 { PARSER_STATE->checkThatLogicIsSet();
308 UNSUPPORTED("unsat cores not yet supported"); }
311 { PARSER_STATE->checkThatLogicIsSet(); }
313 { unsigned n = AntlrInput::tokenToUnsigned(k);
315 cmd = new EmptyCommand;
317 cmd = new PushCommand;
319 CommandSequence* seq = new CommandSequence;
321 seq->addCommand(new PushCommand);
326 | { if(PARSER_STATE->strictModeEnabled()) {
327 PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to PUSH. Maybe you want (push 1)?");
329 cmd = new PushCommand;
333 { PARSER_STATE->checkThatLogicIsSet(); }
335 { unsigned n = AntlrInput::tokenToUnsigned(k);
337 cmd = new EmptyCommand;
339 cmd = new PopCommand;
341 CommandSequence* seq = new CommandSequence;
343 seq->addCommand(new PopCommand);
348 | { if(PARSER_STATE->strictModeEnabled()) {
349 PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to POP. Maybe you want (pop 1)?");
351 cmd = new PopCommand;
355 { cmd = new QuitCommand; }
357 /* CVC4-extended SMT-LIBv2 commands */
358 | extendedCommand[cmd]
359 { PARSER_STATE->checkThatLogicIsSet();
360 if(PARSER_STATE->strictModeEnabled()) {
361 PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode.");
366 extendedCommand[CVC4::Command*& cmd]
368 std::vector<CVC4::Datatype> dts;
373 std::vector<std::string> names;
374 std::vector<Type> sorts;
376 /* Extended SMT-LIBv2 set of commands syntax, not permitted in
377 * --smtlib2 compliance mode. */
378 : DECLARE_DATATYPES_TOK
379 { /* open a scope to keep the UnresolvedTypes contained */
380 PARSER_STATE->pushScope(); }
381 LPAREN_TOK ( LPAREN_TOK datatypeDef[dts] RPAREN_TOK )+ RPAREN_TOK
382 { PARSER_STATE->popScope();
383 cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
385 ( simpleSymbolicExpr[sexpr]
386 { std::stringstream ss;
388 cmd = new EchoCommand(ss.str());
390 | { cmd = new EchoCommand(); }
394 simpleSymbolicExpr[CVC4::SExpr& sexpr]
400 { sexpr = SExpr(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
402 { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
404 { sexpr = SExpr(s); }
406 { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); }
408 { std::stringstream ss;
409 ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k);
410 sexpr = SExpr(ss.str());
413 { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
416 symbolicExpr[CVC4::SExpr& sexpr]
418 std::vector<SExpr> children;
420 : simpleSymbolicExpr[sexpr]
422 (symbolicExpr[sexpr] { children.push_back(sexpr); } )*
424 { sexpr = SExpr(children); }
429 * @return the expression representing the formula
431 term[CVC4::Expr& expr]
433 Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
437 std::vector<Expr> args;
440 : /* a built-in operator application */
441 LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
443 if( kind == CVC4::kind::EQUAL &&
445 args[0].getType() == EXPR_MANAGER->booleanType() ) {
446 /* Use IFF for boolean equalities. */
447 kind = CVC4::kind::IFF;
450 if( !PARSER_STATE->strictModeEnabled() &&
451 (kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
453 /* Unary AND/OR can be replaced with the argument.
454 It just so happens expr should already by the only argument. */
455 Assert( expr == args[0] );
456 } else if( CVC4::kind::isAssociative(kind) &&
457 args.size() > EXPR_MANAGER->maxArity(kind) ) {
458 /* Special treatment for associative operators with lots of children */
459 expr = EXPR_MANAGER->mkAssociative(kind,args);
460 } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) {
461 expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
463 PARSER_STATE->checkOperator(kind, args.size());
464 expr = MK_EXPR(kind, args);
468 | /* A non-built-in function application */
470 functionName[name,CHECK_DECLARED]
471 { PARSER_STATE->checkFunctionLike(name);
472 const bool isDefinedFunction =
473 PARSER_STATE->isDefinedFunction(name);
474 if(isDefinedFunction) {
475 expr = PARSER_STATE->getFunction(name);
476 kind = CVC4::kind::APPLY;
478 expr = PARSER_STATE->getVariable(name);
479 Type t = expr.getType();
480 if( t.isConstructor() ){
481 kind = CVC4::kind::APPLY_CONSTRUCTOR;
482 }else if( t.isSelector() ){
483 kind = CVC4::kind::APPLY_SELECTOR;
484 }else if( t.isTester() ){
485 kind = CVC4::kind::APPLY_TESTER;
487 kind = CVC4::kind::APPLY_UF;
490 args.push_back(expr);
492 termList[args,expr] RPAREN_TOK
493 { Debug("parser") << "args has size " << args.size() << std::endl << "expr is " << expr << std::endl;
494 for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
495 Debug("parser") << "++ " << *i << std::endl;
496 expr = MK_EXPR(kind, args); }
498 | /* An indexed function application */
499 LPAREN_TOK indexedFunctionName[op] termList[args,expr] RPAREN_TOK
500 { expr = MK_EXPR(op, args); }
502 | /* a let binding */
503 LPAREN_TOK LET_TOK LPAREN_TOK
504 { PARSER_STATE->pushScope(); }
505 ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[expr] RPAREN_TOK
506 { PARSER_STATE->defineVar(name,expr); } )+
510 { PARSER_STATE->popScope(); }
513 | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
514 { const bool isDefinedFunction =
515 PARSER_STATE->isDefinedFunction(name);
516 if(isDefinedFunction) {
517 expr = MK_EXPR(CVC4::kind::APPLY,
518 PARSER_STATE->getFunction(name));
520 expr = PARSER_STATE->getVariable(name);
521 Type t = PARSER_STATE->getType(name);
522 if(t.isConstructor() && ConstructorType(t).getArity() == 0) {
523 // don't require parentheses, immediately turn it into an apply
524 expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
529 /* attributed expressions */
530 | LPAREN_TOK ATTRIBUTE_TOK term[expr] KEYWORD symbolicExpr[sexpr] RPAREN_TOK
531 { std::string attr = AntlrInput::tokenText($KEYWORD);
532 if(attr == ":named") {
533 name = sexpr.getValue();
534 // FIXME ensure expr is a closed subterm
535 // check that sexpr is a fresh function symbol
536 PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
538 Expr func = PARSER_STATE->mkFunction(name, expr.getType());
539 // bind name to expr with define-fun
541 new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
542 PARSER_STATE->preemptCommand(c);
544 std::stringstream ss;
545 ss << "Attribute `" << attr << "' not supported";
546 PARSER_STATE->parseError(ss.str());
552 { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
555 { // FIXME: This doesn't work because an SMT rational is not a
556 // valid GMP rational string
557 expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
559 | LPAREN_TOK INDEX_TOK bvLit=SYMBOL size=INTEGER_LITERAL RPAREN_TOK
560 { if(AntlrInput::tokenText($bvLit).find("bv") == 0) {
561 expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) );
563 PARSER_STATE->parseError("Unexpected symbol `" + AntlrInput::tokenText($bvLit) + "'");
568 { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
569 std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
570 expr = MK_CONST( BitVector(hexString, 16) ); }
573 { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
574 std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
575 expr = MK_CONST( BitVector(binString, 2) ); }
577 // NOTE: Theory constants go here
581 * Matches a bit-vector operator (the ones parametrized by numbers)
583 indexedFunctionName[CVC4::Expr& op]
584 : LPAREN_TOK INDEX_TOK
585 ( 'extract' n1=INTEGER_LITERAL n2=INTEGER_LITERAL
586 { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1),
587 AntlrInput::tokenToUnsigned($n2))); }
588 | 'repeat' n=INTEGER_LITERAL
589 { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
590 | 'zero_extend' n=INTEGER_LITERAL
591 { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
592 | 'sign_extend' n=INTEGER_LITERAL
593 { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); }
594 | 'rotate_left' n=INTEGER_LITERAL
595 { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
596 | 'rotate_right' n=INTEGER_LITERAL
597 { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
598 | badIndexedFunctionName
604 * Matches an erroneous indexed function name (and args) for better
607 badIndexedFunctionName
611 : symbol[name,CHECK_NONE,SYM_VARIABLE] INTEGER_LITERAL+
612 { PARSER_STATE->parseError(std::string("Unknown indexed function `") + name + "'"); }
616 * Matches a sequence of terms and puts them into the formulas
618 * @param formulas the vector to fill with terms
619 * @param expr an Expr reference for the elements of the sequence
621 /* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
622 * time through this rule. */
623 termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
624 : ( term[expr] { formulas.push_back(expr); } )+
628 * Matches a string, and strips off the quotes.
632 { s = AntlrInput::tokenText($STRING_LITERAL);
633 /* strip off the quotes */
634 s = s.substr(1, s.size() - 2);
639 * Matches a builtin operator symbol and sets kind to its associated Expr kind.
641 builtinOp[CVC4::Kind& kind]
643 Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
645 : NOT_TOK { $kind = CVC4::kind::NOT; }
646 | IMPLIES_TOK { $kind = CVC4::kind::IMPLIES; }
647 | AND_TOK { $kind = CVC4::kind::AND; }
648 | OR_TOK { $kind = CVC4::kind::OR; }
649 | XOR_TOK { $kind = CVC4::kind::XOR; }
650 | EQUAL_TOK { $kind = CVC4::kind::EQUAL; }
651 | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
652 | ITE_TOK { $kind = CVC4::kind::ITE; }
654 { $kind = CVC4::kind::GT; }
655 | GREATER_THAN_EQUAL_TOK
656 { $kind = CVC4::kind::GEQ; }
657 | LESS_THAN_EQUAL_TOK
658 { $kind = CVC4::kind::LEQ; }
660 { $kind = CVC4::kind::LT; }
661 | PLUS_TOK { $kind = CVC4::kind::PLUS; }
662 | MINUS_TOK { $kind = CVC4::kind::MINUS; }
663 | STAR_TOK { $kind = CVC4::kind::MULT; }
664 | DIV_TOK { $kind = CVC4::kind::DIVISION; }
665 | INTS_DIV_TOK { $kind = CVC4::kind::INTS_DIVISION; }
666 | INTS_MOD_TOK { $kind = CVC4::kind::INTS_MODULUS; }
668 | SELECT_TOK { $kind = CVC4::kind::SELECT; }
669 | STORE_TOK { $kind = CVC4::kind::STORE; }
671 | CONCAT_TOK { $kind = CVC4::kind::BITVECTOR_CONCAT; }
672 | BVNOT_TOK { $kind = CVC4::kind::BITVECTOR_NOT; }
673 | BVAND_TOK { $kind = CVC4::kind::BITVECTOR_AND; }
674 | BVOR_TOK { $kind = CVC4::kind::BITVECTOR_OR; }
675 | BVNEG_TOK { $kind = CVC4::kind::BITVECTOR_NEG; }
676 | BVADD_TOK { $kind = CVC4::kind::BITVECTOR_PLUS; }
677 | BVMUL_TOK { $kind = CVC4::kind::BITVECTOR_MULT; }
678 | BVUDIV_TOK { $kind = CVC4::kind::BITVECTOR_UDIV; }
679 | BVUREM_TOK { $kind = CVC4::kind::BITVECTOR_UREM; }
680 | BVSHL_TOK { $kind = CVC4::kind::BITVECTOR_SHL; }
681 | BVLSHR_TOK { $kind = CVC4::kind::BITVECTOR_LSHR; }
682 | BVULT_TOK { $kind = CVC4::kind::BITVECTOR_ULT; }
683 | BVNAND_TOK { $kind = CVC4::kind::BITVECTOR_NAND; }
684 | BVNOR_TOK { $kind = CVC4::kind::BITVECTOR_NOR; }
685 | BVXOR_TOK { $kind = CVC4::kind::BITVECTOR_XOR; }
686 | BVXNOR_TOK { $kind = CVC4::kind::BITVECTOR_XNOR; }
687 | BVCOMP_TOK { $kind = CVC4::kind::BITVECTOR_COMP; }
688 | BVSUB_TOK { $kind = CVC4::kind::BITVECTOR_SUB; }
689 | BVSDIV_TOK { $kind = CVC4::kind::BITVECTOR_SDIV; }
690 | BVSREM_TOK { $kind = CVC4::kind::BITVECTOR_SREM; }
691 | BVSMOD_TOK { $kind = CVC4::kind::BITVECTOR_SMOD; }
692 | BVASHR_TOK { $kind = CVC4::kind::BITVECTOR_ASHR; }
693 | BVULE_TOK { $kind = CVC4::kind::BITVECTOR_ULE; }
694 | BVUGT_TOK { $kind = CVC4::kind::BITVECTOR_UGT; }
695 | BVUGE_TOK { $kind = CVC4::kind::BITVECTOR_UGE; }
696 | BVSLT_TOK { $kind = CVC4::kind::BITVECTOR_SLT; }
697 | BVSLE_TOK { $kind = CVC4::kind::BITVECTOR_SLE; }
698 | BVSGT_TOK { $kind = CVC4::kind::BITVECTOR_SGT; }
699 | BVSGE_TOK { $kind = CVC4::kind::BITVECTOR_SGE; }
701 // NOTE: Theory operators go here
705 * Matches a (possibly undeclared) function symbol (returning the string)
706 * @param check what kind of check to do with the symbol
708 functionName[std::string& name, CVC4::parser::DeclarationCheck check]
709 : symbol[name,check,SYM_VARIABLE]
713 * Matches an previously declared function symbol (returning an Expr)
715 functionSymbol[CVC4::Expr& fun]
719 : functionName[name,CHECK_DECLARED]
720 { PARSER_STATE->checkFunctionLike(name);
721 fun = PARSER_STATE->getVariable(name); }
725 * Matches a sequence of sort symbols and fills them into the given
728 sortList[std::vector<CVC4::Type>& sorts]
732 : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
735 nonemptySortList[std::vector<CVC4::Type>& sorts]
739 : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+
743 * Matches a sequence of (variable,sort) symbol pairs and fills them
744 * into the given vector.
746 sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars]
751 : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] RPAREN_TOK
752 { sortedVars.push_back(make_pair(name, t)); }
757 * Matches the sort symbol, which can be an arbitrary symbol.
758 * @param check the check to perform on the name
760 sortName[std::string& name, CVC4::parser::DeclarationCheck check]
761 : symbol[name,check,SYM_SORT]
764 sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
767 std::vector<CVC4::Type> args;
768 std::vector<uint64_t> numerals;
770 : sortName[name,CHECK_NONE]
772 if( check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT) ){
773 t = PARSER_STATE->getSort(name);
775 t = PARSER_STATE->mkUnresolvedType(name);
778 | LPAREN_TOK INDEX_TOK symbol[name,CHECK_NONE,SYM_SORT] nonemptyNumeralList[numerals] RPAREN_TOK
780 if( name == "BitVec" ) {
781 if( numerals.size() != 1 ) {
782 PARSER_STATE->parseError("Illegal bitvector type.");
784 t = EXPR_MANAGER->mkBitVectorType(numerals.front());
789 | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
791 if( name == "Array" ) {
792 if( args.size() != 2 ) {
793 PARSER_STATE->parseError("Illegal array type.");
795 t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
797 t = PARSER_STATE->getSort(name, args);
803 * Matches a list of symbols, with check and type arguments as for the
804 * symbol[] rule below.
806 symbolList[std::vector<std::string>& names,
807 CVC4::parser::DeclarationCheck check,
808 CVC4::parser::SymbolType type]
812 : ( symbol[id,check,type] { names.push_back(id); } )*
816 * Matches an symbol and sets the string reference parameter id.
817 * @param id string to hold the symbol
818 * @param check what kinds of check to do on the symbol
819 * @param type the intended namespace for the symbol
821 symbol[std::string& id,
822 CVC4::parser::DeclarationCheck check,
823 CVC4::parser::SymbolType type]
825 { id = AntlrInput::tokenText($SYMBOL);
826 Debug("parser") << "symbol: " << id
827 << " check? " << check
828 << " type? " << type << std::endl;
829 PARSER_STATE->checkDeclaration(id, check, type); }
833 * Matches a nonempty list of numerals.
834 * @param numerals the (empty) vector to house the numerals.
836 nonemptyNumeralList[std::vector<uint64_t>& numerals]
838 { numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
843 * Parses a datatype definition
845 datatypeDef[std::vector<CVC4::Datatype>& datatypes]
849 std::vector< Type > params;
851 /* This really needs to be CHECK_NONE, or mutually-recursive
852 * datatypes won't work, because this type will already be
853 * "defined" as an unresolved type; don't worry, we check
855 : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
856 ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
857 t = PARSER_STATE->mkSort(id2);
858 params.push_back( t );
860 ( symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
861 t = PARSER_STATE->mkSort(id2);
862 params.push_back( t ); }
865 { datatypes.push_back(Datatype(id,params));
866 if(!PARSER_STATE->isUnresolvedType(id)) {
867 // if not unresolved, must be undeclared
868 PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
871 ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+
872 { PARSER_STATE->popScope(); }
876 * Parses a constructor defintion for type
878 constructorDef[CVC4::Datatype& type]
881 CVC4::DatatypeConstructor* ctor = NULL;
883 : symbol[id,CHECK_UNDECLARED,SYM_SORT]
885 std::string testerId("is_");
887 PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
888 ctor = new CVC4::DatatypeConstructor(id, testerId);
890 ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
891 { // make the constructor
892 type.addConstructor(*ctor);
893 Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
898 selector[CVC4::DatatypeConstructor& ctor]
903 : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t,CHECK_NONE]
904 { ctor.addArg(id, t);
905 Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
909 // Base SMT-LIB tokens
910 ASSERT_TOK : 'assert';
911 CHECKSAT_TOK : 'check-sat';
912 DECLARE_FUN_TOK : 'declare-fun';
913 DECLARE_SORT_TOK : 'declare-sort';
914 DEFINE_FUN_TOK : 'define-fun';
915 DEFINE_SORT_TOK : 'define-sort';
916 GET_VALUE_TOK : 'get-value';
917 GET_ASSIGNMENT_TOK : 'get-assignment';
918 GET_ASSERTIONS_TOK : 'get-assertions';
919 GET_PROOF_TOK : 'get-proof';
920 GET_UNSAT_CORE_TOK : 'get-unsat-core';
928 SET_LOGIC_TOK : 'set-logic';
929 SET_INFO_TOK : 'set-info';
930 GET_INFO_TOK : 'get-info';
931 SET_OPTION_TOK : 'set-option';
932 GET_OPTION_TOK : 'get-option';
937 DECLARE_DATATYPES_TOK : 'declare-datatypes';
940 // operators (NOTE: theory symbols go here)
944 DISTINCT_TOK : 'distinct';
947 EXISTS_TOK : 'exists';
948 FORALL_TOK : 'forall';
949 GREATER_THAN_TOK : '>';
950 GREATER_THAN_EQUAL_TOK : '>=';
953 LESS_THAN_EQUAL_TOK : '<=';
957 // PERCENT_TOK : '%';
960 SELECT_TOK : 'select';
966 INTS_DIV_TOK : 'div';
967 INTS_MOD_TOK : 'mod';
969 CONCAT_TOK : 'concat';
976 BVUDIV_TOK : 'bvudiv';
977 BVUREM_TOK : 'bvurem';
979 BVLSHR_TOK : 'bvlshr';
981 BVNAND_TOK : 'bvnand';
984 BVXNOR_TOK : 'bvxnor';
985 BVCOMP_TOK : 'bvcomp';
987 BVSDIV_TOK : 'bvsdiv';
988 BVSREM_TOK : 'bvsrem';
989 BVSMOD_TOK : 'bvsmod';
990 BVASHR_TOK : 'bvashr';
1000 * Matches a symbol from the input. A symbol is a "simple" symbol or a
1001 * sequence of printable ASCII characters that starts and ends with | and
1002 * does not otherwise contain |.
1010 * Matches a keyword from the input. A keyword is a simple symbol prefixed
1017 /** Matches a "simple" symbol: a non-empty sequence of letters, digits and
1018 * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
1019 * digit, and is not the special reserved symbol '_'.
1021 fragment SIMPLE_SYMBOL
1022 : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)+
1024 | SYMBOL_CHAR_NOUNDERSCORE
1028 * Matches and skips whitespace in the input.
1031 : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }
1035 * Matches an integer constant from the input (non-empty sequence of
1036 * digits, with no leading zeroes).
1043 * Match an integer constant. In non-strict mode, this is any sequence
1044 * of digits. In strict mode, non-zero integers can't have leading
1049 char *start = (char*) GETCHARINDEX();
1052 { Debug("parser-extra") << "NUMERAL: "
1053 << (uintptr_t)start << ".." << GETCHARINDEX()
1054 << " strict? " << (bool)(PARSER_STATE->strictModeEnabled())
1055 << " ^0? " << (bool)(*start == '0')
1056 << " len>1? " << (bool)(start < (char*)(GETCHARINDEX() - 1))
1058 { !PARSER_STATE->strictModeEnabled() ||
1060 start == (char*)(GETCHARINDEX() - 1) }?
1064 * Matches a decimal constant from the input.
1067 : NUMERAL '.' DIGIT+
1071 * Matches a hexadecimal constant.
1078 * Matches a binary constant.
1086 * Matches a double quoted string literal. Escaping is supported, and
1087 * escape character '\' has to be escaped.
1090 : '"' (ESCAPE | ~('"'|'\\'))* '"'
1094 * Matches the comments and ignores them
1097 : ';' (~('\n' | '\r'))* { SKIP(); }
1101 * Matches any letter ('a'-'z' and 'A'-'Z').
1110 * Matches the digits (0-9)
1112 fragment DIGIT : '0'..'9';
1114 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
1117 * Matches the characters that may appear in a "symbol" (i.e., an identifier)
1119 fragment SYMBOL_CHAR_NOUNDERSCORE
1120 : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '~'
1121 | '&' | '^' | '<' | '>' | '@'
1124 fragment SYMBOL_CHAR
1125 : SYMBOL_CHAR_NOUNDERSCORE | '_'
1129 * Matches an allowed escaped character.
1131 fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');