7fb671bb06e7968493c035184e0af544a825abfe
[cvc5.git] / src / parser / smt2 / Smt2.g
1 /* ******************* */
2 /*! \file Smt2.g
3 ** \verbatim
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
13 **
14 ** \brief Parser for SMT-LIB v2 input language.
15 **
16 ** Parser for SMT-LIB v2 input language.
17 **/
18
19 grammar Smt2;
20
21 options {
22 // C output for antlr
23 language = 'C';
24
25 // Skip the default error handling, just break with exceptions
26 // defaultErrorHandler = false;
27
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 !
31 k = 2;
32 }/* options */
33
34 @header {
35 /**
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
41 ** information.
42 **/
43 }/* @header */
44
45 @lexer::includes {
46
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.
51 */
52 #pragma GCC system_header
53
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.
58 */
59 #define ANTLR3_INLINE_INPUT_ASCII
60
61 #include "parser/antlr_tracing.h"
62
63 }/* @lexer::includes */
64
65 @lexer::postinclude {
66 #include <stdint.h>
67
68 #include "parser/smt2/smt2.h"
69 #include "parser/antlr_input.h"
70 #include "parser/antlr_tracing.h"
71
72 using namespace CVC4;
73 using namespace CVC4::parser;
74
75 #undef PARSER_STATE
76 #define PARSER_STATE ((Smt2*)LEXER->super)
77 }/* @lexer::postinclude */
78
79 @parser::includes {
80 #include "expr/command.h"
81 #include "parser/parser.h"
82
83 namespace CVC4 {
84 class Expr;
85
86 namespace parser {
87 namespace smt2 {
88 /**
89 * Just exists to provide the uintptr_t constructor that ANTLR
90 * requires.
91 */
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) {}
97 };/* struct myExpr */
98 }/* CVC4::parser::smt2 namespace */
99 }/* CVC4::parser namespace */
100 }/* CVC4 namespace */
101
102 }/* @parser::includes */
103
104 @parser::postinclude {
105
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"
115 #include <vector>
116
117 using namespace CVC4;
118 using namespace CVC4::parser;
119
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.) */
122 #undef PARSER_STATE
123 #define PARSER_STATE ((Smt2*)PARSER->super)
124 #undef EXPR_MANAGER
125 #define EXPR_MANAGER PARSER_STATE->getExprManager()
126 #undef MK_EXPR
127 #define MK_EXPR EXPR_MANAGER->mkExpr
128 #undef MK_CONST
129 #define MK_CONST EXPR_MANAGER->mkConst
130 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
131
132 }/* parser::postinclude */
133
134 /**
135 * Parses an expression.
136 * @return the parsed expression, or the Null Expr if we've reached the end of the input
137 */
138 parseExpr returns [CVC4::parser::smt2::myExpr expr]
139 : term[expr]
140 | EOF
141 ;
142
143 /**
144 * Parses a command
145 * @return the parsed command, or NULL if we've reached the end of the input
146 */
147 parseCommand returns [CVC4::Command* cmd = NULL]
148 : LPAREN_TOK c = command RPAREN_TOK { $cmd = c; }
149 | EOF { $cmd = 0; }
150 ;
151
152 /**
153 * Parse the internal portion of the command, ignoring the surrounding parentheses.
154 */
155 command returns [CVC4::Command* cmd = NULL]
156 @declarations {
157 std::string name;
158 std::vector<std::string> names;
159 Expr expr;
160 Type t;
161 std::vector<Expr> terms;
162 std::vector<Type> sorts;
163 std::vector<std::pair<std::string, Type> > sortedVarNames;
164 SExpr sexpr;
165 }
166 : /* set the logic */
167 SET_LOGIC_TOK SYMBOL
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.");
172 }
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); }
179 | /* get-info */
180 GET_INFO_TOK KEYWORD
181 { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD)); }
182 | /* set-option */
183 SET_OPTION_TOK KEYWORD symbolicExpr[sexpr]
184 { name = AntlrInput::tokenText($KEYWORD);
185 PARSER_STATE->setOption(name,sexpr);
186 cmd = new SetOptionCommand(name,sexpr); }
187 | /* get-option */
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);
195 if(arity == 0) {
196 Type type = PARSER_STATE->mkSort(name);
197 $cmd = new DeclareTypeCommand(name, 0, type);
198 } else {
199 Type type = PARSER_STATE->mkSortConstructor(name, arity);
200 $cmd = new DeclareTypeCommand(name, arity, type);
201 }
202 }
203 | /* sort definition */
204 DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT]
205 LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
206 {
207 PARSER_STATE->pushScope();
208 for(std::vector<std::string>::const_iterator i = names.begin(),
209 iend = names.end();
210 i != iend;
211 ++i) {
212 sorts.push_back(PARSER_STATE->mkSort(*i));
213 }
214 }
215 sortSymbol[t]
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);
221 }
222 | /* function declaration */
223 DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
224 LPAREN_TOK sortList[sorts] RPAREN_TOK
225 sortSymbol[t]
226 { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
227 if( sorts.size() > 0 ) {
228 t = EXPR_MANAGER->mkFunctionType(sorts, t);
229 }
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
235 sortSymbol[t]
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();
243 i != iend;
244 ++i) {
245 sorts.push_back((*i).second);
246 }
247 t = EXPR_MANAGER->mkFunctionType(sorts, t);
248 }
249 PARSER_STATE->pushScope();
250 for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
251 sortedVarNames.begin(), iend = sortedVarNames.end();
252 i != iend;
253 ++i) {
254 terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
255 }
256 }
257 term[expr]
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
261 // permitted)
262 Expr func = PARSER_STATE->mkFunction(name, t);
263 $cmd = new DefineFunctionCommand(name, func, terms, expr);
264 }
265 | /* value query */
266 ( GET_VALUE_TOK |
267 EVAL_TOK
268 { if(PARSER_STATE->strictModeEnabled()) {
269 PARSER_STATE->parseError("Strict compliance mode doesn't recognize \"eval\". Maybe you want (get-value...)?");
270 }
271 } )
272 LPAREN_TOK termList[terms,expr] RPAREN_TOK
273 { if(terms.size() == 1) {
274 $cmd = new GetValueCommand(terms[0]);
275 } else {
276 CommandSequence* seq = new CommandSequence();
277 for(std::vector<Expr>::const_iterator i = terms.begin(),
278 iend = terms.end();
279 i != iend;
280 ++i) {
281 seq->addCommand(new GetValueCommand(*i));
282 }
283 $cmd = seq;
284 }
285 }
286 | /* get-assignment */
287 GET_ASSIGNMENT_TOK
288 { cmd = new GetAssignmentCommand; }
289 | /* assertion */
290 ASSERT_TOK term[expr]
291 { cmd = new AssertCommand(expr); }
292 | /* checksat */
293 CHECKSAT_TOK
294 { cmd = new CheckSatCommand(MK_CONST(bool(true))); }
295 | /* get-assertions */
296 GET_ASSERTIONS_TOK
297 { cmd = new GetAssertionsCommand; }
298 | /* get-proof */
299 GET_PROOF_TOK
300 { UNSUPPORTED("get-proof command not yet supported"); }
301 | /* get-unsat-core */
302 GET_UNSAT_CORE_TOK
303 { UNSUPPORTED("unsat cores not yet supported"); }
304 | /* push */
305 PUSH_TOK
306 ( k=INTEGER_LITERAL
307 { unsigned n = AntlrInput::tokenToUnsigned(k);
308 if(n == 0) {
309 cmd = new EmptyCommand;
310 } else if(n == 1) {
311 cmd = new PushCommand;
312 } else {
313 CommandSequence* seq = new CommandSequence;
314 do {
315 seq->addCommand(new PushCommand);
316 } while(--n > 0);
317 cmd = seq;
318 }
319 }
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)?");
322 } else {
323 cmd = new PushCommand;
324 }
325 } )
326 | POP_TOK
327 ( k=INTEGER_LITERAL
328 { unsigned n = AntlrInput::tokenToUnsigned(k);
329 if(n == 0) {
330 cmd = new EmptyCommand;
331 } else if(n == 1) {
332 cmd = new PopCommand;
333 } else {
334 CommandSequence* seq = new CommandSequence;
335 do {
336 seq->addCommand(new PopCommand);
337 } while(--n > 0);
338 cmd = seq;
339 }
340 }
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)?");
343 } else {
344 cmd = new PopCommand;
345 }
346 } )
347 | EXIT_TOK
348 { cmd = new QuitCommand; }
349
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.");
354 }
355 }
356 ;
357
358 extendedCommand[CVC4::Command*& cmd]
359 @declarations {
360 std::vector<CVC4::Datatype> dts;
361 Expr e;
362 }
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)); }
370
371
372 | DECLARE_SORTS_TOK
373 | DECLARE_FUNS_TOK
374 | DECLARE_PREDS_TOK
375 | DEFINE_TOK
376 | DEFINE_SORTS_TOK
377 | DECLARE_CONST_TOK
378
379 | SIMPLIFY_TOK term[e]
380 { cmd = new SimplifyCommand(e); }
381 | ECHO_TOK
382 ( STRING_LITERAL
383 { Message() << AntlrInput::tokenText($STRING_LITERAL) << std::endl; }
384 | { Message() << std::endl; } )
385 ;
386
387 symbolicExpr[CVC4::SExpr& sexpr]
388 @declarations {
389 std::vector<SExpr> children;
390 CVC4::Kind k;
391 }
392 : INTEGER_LITERAL
393 { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); }
394 | DECIMAL_LITERAL
395 { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); }
396 | STRING_LITERAL
397 { sexpr = SExpr(AntlrInput::tokenText($STRING_LITERAL)); }
398 | SYMBOL
399 { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); }
400 | builtinOp[k]
401 { std::stringstream ss;
402 ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k);
403 sexpr = SExpr(ss.str());
404 }
405 | KEYWORD
406 { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
407 | LPAREN_TOK
408 (symbolicExpr[sexpr] { children.push_back(sexpr); } )*
409 RPAREN_TOK
410 { sexpr = SExpr(children); }
411 ;
412
413 /**
414 * Matches a term.
415 * @return the expression representing the formula
416 */
417 term[CVC4::Expr& expr]
418 @init {
419 Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
420 Kind kind;
421 Expr op;
422 std::string name;
423 std::vector<Expr> args;
424 SExpr sexpr;
425 }
426 : /* a built-in operator application */
427 LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
428 {
429 if( kind == CVC4::kind::EQUAL &&
430 args.size() > 0 &&
431 args[0].getType() == EXPR_MANAGER->booleanType() ) {
432 /* Use IFF for boolean equalities. */
433 kind = CVC4::kind::IFF;
434 }
435
436 if( !PARSER_STATE->strictModeEnabled() &&
437 (kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
438 args.size() == 1) {
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]);
448 } else {
449 PARSER_STATE->checkOperator(kind, args.size());
450 expr = MK_EXPR(kind, args);
451 }
452 }
453
454 | /* A non-built-in function application */
455 LPAREN_TOK
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;
463 } else {
464 expr = PARSER_STATE->getVariable(name);
465 kind = CVC4::kind::APPLY_UF;
466 }
467 args.push_back(expr);
468 }
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); }
474
475 | /* An indexed function application */
476 LPAREN_TOK indexedFunctionName[op] termList[args,expr] RPAREN_TOK
477 { expr = MK_EXPR(op, args); }
478
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); } )+
484 RPAREN_TOK
485 term[expr]
486 RPAREN_TOK
487 { PARSER_STATE->popScope(); }
488
489 /* a variable */
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));
496 } else {
497 expr = PARSER_STATE->getVariable(name);
498 }
499 }
500
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);
509 // define it
510 Expr func = PARSER_STATE->mkFunction(name, expr.getType());
511 // bind name to expr with define-fun
512 Command* c =
513 new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
514 PARSER_STATE->preemptCommand(c);
515 } else {
516 std::stringstream ss;
517 ss << "Attribute `" << attr << "' not supported";
518 PARSER_STATE->parseError(ss.str());
519 }
520 }
521
522 /* constants */
523 | INTEGER_LITERAL
524 { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
525
526 | DECIMAL_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) ); }
530
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) );
534 } else {
535 PARSER_STATE->parseError("Unexpected symbol `" + AntlrInput::tokenText($bvLit) + "'");
536 }
537 }
538
539 | HEX_LITERAL
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) ); }
543
544 | BINARY_LITERAL
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) ); }
548
549 // NOTE: Theory constants go here
550 ;
551
552 /**
553 * Matches a bit-vector operator (the ones parametrized by numbers)
554 */
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
571 )
572 RPAREN_TOK
573 ;
574
575 /**
576 * Matches an erroneous indexed function name (and args) for better
577 * error reporting.
578 */
579 badIndexedFunctionName
580 @declarations {
581 std::string name;
582 }
583 : symbol[name,CHECK_NONE,SYM_VARIABLE] INTEGER_LITERAL+
584 { PARSER_STATE->parseError(std::string("Unknown indexed function `") + name + "'"); }
585 ;
586
587 /**
588 * Matches a sequence of terms and puts them into the formulas
589 * vector.
590 * @param formulas the vector to fill with terms
591 * @param expr an Expr reference for the elements of the sequence
592 */
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); } )+
597 ;
598
599 /**
600 * Matches a builtin operator symbol and sets kind to its associated Expr kind.
601 */
602 builtinOp[CVC4::Kind& kind]
603 @init {
604 Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
605 }
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; }
614 | GREATER_THAN_TOK
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; }
620 | LESS_THAN_TOK
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; }
626
627 | SELECT_TOK { $kind = CVC4::kind::SELECT; }
628 | STORE_TOK { $kind = CVC4::kind::STORE; }
629
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; }
659
660 // NOTE: Theory operators go here
661 ;
662
663 /**
664 * Matches a (possibly undeclared) function symbol (returning the string)
665 * @param check what kind of check to do with the symbol
666 */
667 functionName[std::string& name, CVC4::parser::DeclarationCheck check]
668 : symbol[name,check,SYM_VARIABLE]
669 ;
670
671 /**
672 * Matches an previously declared function symbol (returning an Expr)
673 */
674 functionSymbol[CVC4::Expr& fun]
675 @declarations {
676 std::string name;
677 }
678 : functionName[name,CHECK_DECLARED]
679 { PARSER_STATE->checkFunctionLike(name);
680 fun = PARSER_STATE->getVariable(name); }
681 ;
682
683 /**
684 * Matches a sequence of sort symbols and fills them into the given
685 * vector.
686 */
687 sortList[std::vector<CVC4::Type>& sorts]
688 @declarations {
689 Type t;
690 }
691 : ( sortSymbol[t] { sorts.push_back(t); } )*
692 ;
693
694 /**
695 * Matches a sequence of (variable,sort) symbol pairs and fills them
696 * into the given vector.
697 */
698 sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars]
699 @declarations {
700 std::string name;
701 Type t;
702 }
703 : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t] RPAREN_TOK
704 { sortedVars.push_back(make_pair(name, t)); }
705 )*
706 ;
707
708 /**
709 * Matches the sort symbol, which can be an arbitrary symbol.
710 * @param check the check to perform on the name
711 */
712 sortName[std::string& name, CVC4::parser::DeclarationCheck check]
713 : symbol[name,check,SYM_SORT]
714 ;
715
716 sortSymbol[CVC4::Type& t]
717 @declarations {
718 std::string name;
719 std::vector<CVC4::Type> args;
720 std::vector<uint64_t> numerals;
721 }
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
725 {
726 if( name == "BitVec" ) {
727 if( numerals.size() != 1 ) {
728 PARSER_STATE->parseError("Illegal bitvector type.");
729 }
730 t = EXPR_MANAGER->mkBitVectorType(numerals.front());
731 } else {
732 Unhandled(name);
733 }
734 }
735 | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
736 {
737 if( name == "Array" ) {
738 if( args.size() != 2 ) {
739 PARSER_STATE->parseError("Illegal array type.");
740 }
741 t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
742 } else {
743 t = PARSER_STATE->getSort(name, args);
744 }
745 }
746 ;
747
748 /**
749 * Matches a list of symbols, with check and type arguments as for the
750 * symbol[] rule below.
751 */
752 symbolList[std::vector<std::string>& names,
753 CVC4::parser::DeclarationCheck check,
754 CVC4::parser::SymbolType type]
755 @declarations {
756 std::string id;
757 }
758 : ( symbol[id,check,type] { names.push_back(id); } )*
759 ;
760
761 /**
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
766 */
767 symbol[std::string& id,
768 CVC4::parser::DeclarationCheck check,
769 CVC4::parser::SymbolType type]
770 : SYMBOL
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); }
776 ;
777
778 /**
779 * Matches a nonempty list of numerals.
780 * @param numerals the (empty) vector to house the numerals.
781 */
782 nonemptyNumeralList[std::vector<uint64_t>& numerals]
783 : ( INTEGER_LITERAL
784 { numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
785 )+
786 ;
787
788 /**
789 * Parses a datatype definition
790 */
791 datatypeDef[std::vector<CVC4::Datatype>& datatypes]
792 @init {
793 std::string id, id2;
794 Type t;
795 std::vector< Type > params;
796 }
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
800 * below. */
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 );
805 }
806 ( symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
807 t = PARSER_STATE->mkSort(id2);
808 params.push_back( t ); }
809 )* ']'
810 )?
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);
815 }
816 }
817 ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+
818 { PARSER_STATE->popScope(); }
819 ;
820
821 /**
822 * Parses a constructor defintion for type
823 */
824 constructorDef[CVC4::Datatype& type]
825 @init {
826 std::string id;
827 CVC4::Datatype::Constructor* ctor = NULL;
828 }
829 : symbol[id,CHECK_UNDECLARED,SYM_SORT]
830 { // make the tester
831 std::string testerId("is_");
832 testerId.append(id);
833 PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
834 ctor = new CVC4::Datatype::Constructor(id, testerId);
835 }
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;
840 delete ctor;
841 }
842 ;
843
844 selector[CVC4::Datatype::Constructor& ctor]
845 @init {
846 std::string id;
847 Type t, t2;
848 }
849 : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t]
850 { ctor.addArg(id, t);
851 Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
852 }
853 ;
854
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';
867 EXIT_TOK : 'exit';
868 ITE_TOK : 'ite';
869 LET_TOK : 'let';
870 ATTRIBUTE_TOK : '!';
871 LPAREN_TOK : '(';
872 RPAREN_TOK : ')';
873 INDEX_TOK : '_';
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';
879 PUSH_TOK : 'push';
880 POP_TOK : 'pop';
881
882 // extended commands
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';
891 EVAL_TOK : 'eval';
892 ECHO_TOK : 'echo';
893
894 // operators (NOTE: theory symbols go here)
895 AMPERSAND_TOK : '&';
896 AND_TOK : 'and';
897 AT_TOK : '@';
898 DISTINCT_TOK : 'distinct';
899 DIV_TOK : '/';
900 EQUAL_TOK : '=';
901 EXISTS_TOK : 'exists';
902 FORALL_TOK : 'forall';
903 GREATER_THAN_TOK : '>';
904 GREATER_THAN_EQUAL_TOK : '>=';
905 IMPLIES_TOK : '=>';
906 LESS_THAN_TOK : '<';
907 LESS_THAN_EQUAL_TOK : '<=';
908 MINUS_TOK : '-';
909 NOT_TOK : 'not';
910 OR_TOK : 'or';
911 // PERCENT_TOK : '%';
912 PLUS_TOK : '+';
913 POUND_TOK : '#';
914 SELECT_TOK : 'select';
915 STAR_TOK : '*';
916 STORE_TOK : 'store';
917 // TILDE_TOK : '~';
918 XOR_TOK : 'xor';
919
920 CONCAT_TOK : 'concat';
921 BVNOT_TOK : 'bvnot';
922 BVAND_TOK : 'bvand';
923 BVOR_TOK : 'bvor';
924 BVNEG_TOK : 'bvneg';
925 BVADD_TOK : 'bvadd';
926 BVMUL_TOK : 'bvmul';
927 BVUDIV_TOK : 'bvudiv';
928 BVUREM_TOK : 'bvurem';
929 BVSHL_TOK : 'bvshl';
930 BVLSHR_TOK : 'bvlshr';
931 BVULT_TOK : 'bvult';
932 BVNAND_TOK : 'bvnand';
933 BVNOR_TOK : 'bvnor';
934 BVXOR_TOK : 'bvxor';
935 BVXNOR_TOK : 'bvxnor';
936 BVCOMP_TOK : 'bvcomp';
937 BVSUB_TOK : 'bvsub';
938 BVSDIV_TOK : 'bvsdiv';
939 BVSREM_TOK : 'bvsrem';
940 BVSMOD_TOK : 'bvsmod';
941 BVASHR_TOK : 'bvashr';
942 BVULE_TOK : 'bvule';
943 BVUGT_TOK : 'bvugt';
944 BVUGE_TOK : 'bvuge';
945 BVSLT_TOK : 'bvslt';
946 BVSLE_TOK : 'bvsle';
947 BVSGT_TOK : 'bvsgt';
948 BVSGE_TOK : 'bvsge';
949
950 /**
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 |.
954 */
955 SYMBOL
956 : SIMPLE_SYMBOL
957 | '|' ~('|')+ '|'
958 ;
959
960 /**
961 * Matches a keyword from the input. A keyword is a simple symbol prefixed
962 * with a colon.
963 */
964 KEYWORD
965 : ':' SIMPLE_SYMBOL
966 ;
967
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 '_'.
971 */
972 fragment SIMPLE_SYMBOL
973 : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)+
974 | ALPHA
975 | SYMBOL_CHAR_NOUNDERSCORE
976 ;
977
978 /**
979 * Matches and skips whitespace in the input.
980 */
981 WHITESPACE
982 : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }
983 ;
984
985 /**
986 * Matches an integer constant from the input (non-empty sequence of
987 * digits, with no leading zeroes).
988 */
989 INTEGER_LITERAL
990 : NUMERAL
991 ;
992
993 /**
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
996 * zeroes.
997 */
998 fragment NUMERAL
999 @init {
1000 char *start = (char*) GETCHARINDEX();
1001 }
1002 : DIGIT+
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))
1008 << std::endl; }
1009 { !PARSER_STATE->strictModeEnabled() ||
1010 *start != '0' ||
1011 start == (char*)(GETCHARINDEX() - 1) }?
1012 ;
1013
1014 /**
1015 * Matches a decimal constant from the input.
1016 */
1017 DECIMAL_LITERAL
1018 : NUMERAL '.' DIGIT+
1019 ;
1020
1021 /**
1022 * Matches a hexadecimal constant.
1023 */
1024 HEX_LITERAL
1025 : '#x' HEX_DIGIT+
1026 ;
1027
1028 /**
1029 * Matches a binary constant.
1030 */
1031 BINARY_LITERAL
1032 : '#b' ('0' | '1')+
1033 ;
1034
1035
1036 /**
1037 * Matches a double quoted string literal. Escaping is supported, and
1038 * escape character '\' has to be escaped.
1039 */
1040 STRING_LITERAL
1041 : '"' (ESCAPE | ~('"'|'\\'))* '"'
1042 ;
1043
1044 /**
1045 * Matches the comments and ignores them
1046 */
1047 COMMENT
1048 : ';' (~('\n' | '\r'))* { SKIP(); }
1049 ;
1050
1051 /**
1052 * Matches any letter ('a'-'z' and 'A'-'Z').
1053 */
1054 fragment
1055 ALPHA
1056 : 'a'..'z'
1057 | 'A'..'Z'
1058 ;
1059
1060 /**
1061 * Matches the digits (0-9)
1062 */
1063 fragment DIGIT : '0'..'9';
1064
1065 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
1066
1067 /**
1068 * Matches the characters that may appear in a "symbol" (i.e., an identifier)
1069 */
1070 fragment SYMBOL_CHAR_NOUNDERSCORE
1071 : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '~'
1072 | '&' | '^' | '<' | '>' | '@'
1073 ;
1074
1075 fragment SYMBOL_CHAR
1076 : SYMBOL_CHAR_NOUNDERSCORE | '_'
1077 ;
1078
1079 /**
1080 * Matches an allowed escaped character.
1081 */
1082 fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');