1 /* ******************* */
4 ** Original author: cconway
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): dejan, ajreynol
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 CVC presentation input language
16 ** Parser for CVC 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 cvc_input.cpp !
37 ASSERT_TOK = 'ASSERT';
39 CHECKSAT_TOK = 'CHECKSAT';
40 OPTION_TOK = 'OPTION';
44 PUSH_SCOPE_TOK = 'PUSH_SCOPE';
45 POP_SCOPE_TOK = 'POP_SCOPE';
46 POPTO_SCOPE_TOK = 'POPTO_SCOPE';
48 DATATYPE_TOK = 'DATATYPE';
50 CONTEXT_TOK = 'CONTEXT';
51 FORGET_TOK = 'FORGET';
52 GET_TYPE_TOK = 'GET_TYPE';
53 CHECK_TYPE_TOK = 'CHECK_TYPE';
54 GET_CHILD_TOK = 'GET_CHILD';
55 GET_OP_TOK = 'GET_OP';
56 GET_VALUE_TOK = 'GET_VALUE';
57 SUBSTITUTE_TOK = 'SUBSTITUTE';
60 UNTRACE_TOK = 'UNTRACE';
62 TRANSFORM_TOK = 'TRANSFORM';
64 PRINT_TYPE_TOK = 'PRINT_TYPE';
68 INCLUDE_TOK = 'INCLUDE';
69 DUMP_PROOF_TOK = 'DUMP_PROOF';
70 DUMP_ASSUMPTIONS_TOK = 'DUMP_ASSUMPTIONS';
71 DUMP_SIG_TOK = 'DUMP_SIG';
72 DUMP_TCC_TOK = 'DUMP_TCC';
73 DUMP_TCC_ASSUMPTIONS_TOK = 'DUMP_TCC_ASSUMPTIONS';
74 DUMP_TCC_PROOF_TOK = 'DUMP_TCC_PROOF';
75 DUMP_CLOSURE_TOK = 'DUMP_CLOSURE';
76 DUMP_CLOSURE_PROOF_TOK = 'DUMP_CLOSURE_PROOF';
78 ASSERTIONS_TOK = 'ASSERTIONS';
79 ASSUMPTIONS_TOK = 'ASSUMPTIONS';
80 COUNTEREXAMPLE_TOK = 'COUNTEREXAMPLE';
81 COUNTERMODEL_TOK = 'COUNTERMODEL';
82 ARITH_VAR_ORDER_TOK = 'ARITH_VAR_ORDER';
87 BOOLEAN_TOK = 'BOOLEAN';
108 SUBTYPE_TOK = 'SUBTYPE';
110 FORALL_TOK = 'FORALL';
111 EXISTS_TOK = 'EXISTS';
112 PATTERN_TOK = 'PATTERN';
161 BITVECTOR_TOK = 'BITVECTOR';
162 LEFTSHIFT_TOK = '<<';
163 RIGHTSHIFT_TOK = '>>';
164 BVPLUS_TOK = 'BVPLUS';
166 BVUDIV_TOK = 'BVUDIV';
167 BVSDIV_TOK = 'BVSDIV';
168 BVUREM_TOK = 'BVUREM';
169 BVSREM_TOK = 'BVSREM';
170 BVSMOD_TOK = 'BVSMOD';
172 BVASHR_TOK = 'BVASHR';
173 BVLSHR_TOK = 'BVLSHR';
174 BVUMINUS_TOK = 'BVUMINUS';
175 BVMULT_TOK = 'BVMULT';
179 BVNAND_TOK = 'BVNAND';
181 BVCOMP_TOK = 'BVCOMP';
182 BVXNOR_TOK = 'BVXNOR';
184 //BVTOINT_TOK = 'BVTOINT';
185 //INTTOBV_TOK = 'INTTOBV';
186 //BOOLEXTRACT_TOK = 'BOOLEXTRACT';
187 //IS_INTEGER_TOK = 'IS_INTEGER';
193 BVZEROEXTEND_TOK = 'BVZEROEXTEND';
194 BVREPEAT_TOK = 'BVREPEAT';
195 BVROTL_TOK = 'BVROTL';
196 BVROTR_TOK = 'BVROTR';
205 // Idea and code guidance from Sam Harwell,
206 // http://www.antlr.org/wiki/display/ANTLR3/Operator+precedence+parser
208 bool isRightToLeft(int type) {
209 // return true here for any operators that are right-to-left associative
211 case IMPLIES_TOK: return true;
212 default: return false;
214 }/* isRightToLeft() */
216 int getOperatorPrecedence(int type) {
218 case BITVECTOR_TOK: return 1;
221 case LBRACE: return 2;
222 case LBRACKET: return 3;
223 case ARROW_TOK: return 4;
224 //case IS_INTEGER_TOK: return 5;
228 case BVSGE_TOK: return 6;
232 case BVGE_TOK: return 7;
234 case RIGHTSHIFT_TOK: return 8;
236 case BVZEROEXTEND_TOK:
239 case BVROTR_TOK: return 9;
247 case BVLSHR_TOK: return 10;
250 case BVSUB_TOK: return 11;
251 case BVNEG_TOK: return 12;
252 case BVXNOR_TOK: return 13;
254 case BVCOMP_TOK: return 14;
255 case BVNAND_TOK: return 15;
256 case BVXOR_TOK: return 16;
257 case BVAND_TOK: return 17;
259 case CONCAT_TOK: return 19;
260 //case UMINUS_TOK: return 20;
261 case WITH_TOK: return 21;
262 case EXP_TOK: return 22;
266 case MOD_TOK: return 23;
268 case MINUS_TOK: return 24;
273 case FLOOR_TOK: return 25;
275 case DISEQUAL_TOK: return 26;
276 case NOT_TOK: return 27;
277 case AND_TOK: return 28;
279 case XOR_TOK: return 29;
280 case IMPLIES_TOK: return 30;// right-to-left
281 case IFF_TOK: return 31;
283 case EXISTS_TOK: return 32;
285 case IN_TOK: return 33;
288 Unhandled(CvcParserTokenNames[type]);
290 }/* getOperatorPrecedence() */
292 Kind getOperatorKind(int type, bool& negate) {
297 case IFF_TOK: return kind::IFF;
298 case IMPLIES_TOK: return kind::IMPLIES;
299 case OR_TOK: return kind::OR;
300 case XOR_TOK: return kind::XOR;
301 case AND_TOK: return kind::AND;
304 case EQUAL_TOK: return kind::EQUAL;
305 case DISEQUAL_TOK: negate = true; return kind::EQUAL;
306 case GT_TOK: return kind::GT;
307 case GEQ_TOK: return kind::GEQ;
308 case LT_TOK: return kind::LT;
309 case LEQ_TOK: return kind::LEQ;
312 case PLUS_TOK: return kind::PLUS;
313 case MINUS_TOK: return kind::MINUS;
314 case STAR_TOK: return kind::MULT;
315 case INTDIV_TOK: Unhandled(CvcParserTokenNames[type]);
316 case DIV_TOK: return kind::DIVISION;
317 case EXP_TOK: Unhandled(CvcParserTokenNames[type]);
320 case CONCAT_TOK: return kind::BITVECTOR_CONCAT;
321 case BAR: return kind::BITVECTOR_OR;
322 case BVAND_TOK: return kind::BITVECTOR_AND;
325 Unhandled(CvcParserTokenNames[type]);
327 }/* getOperatorKind() */
329 unsigned findPivot(const std::vector<unsigned>& operators,
330 unsigned startIndex, unsigned stopIndex) {
331 unsigned pivot = startIndex;
332 unsigned pivotRank = getOperatorPrecedence(operators[pivot]);
333 /*Debug("prec") << "initial pivot at " << pivot
334 << "(" << CvcParserTokenNames[operators[pivot]] << ") "
335 << "level " << pivotRank << std::endl;*/
336 for(unsigned i = startIndex + 1; i <= stopIndex; ++i) {
337 unsigned current = getOperatorPrecedence(operators[i]);
338 bool rtl = isRightToLeft(operators[i]);
339 if(current > pivotRank || (current == pivotRank && !rtl)) {
340 /*Debug("prec") << "new pivot at " << i
341 << "(" << CvcParserTokenNames[operators[i]] << ") "
342 << "level " << current << " rtl == " << rtl << std::endl;*/
350 Expr createPrecedenceTree(ExprManager* em,
351 const std::vector<CVC4::Expr>& expressions,
352 const std::vector<unsigned>& operators,
353 unsigned startIndex, unsigned stopIndex) {
354 Assert(expressions.size() == operators.size() + 1);
355 Assert(startIndex < expressions.size());
356 Assert(stopIndex < expressions.size());
357 Assert(startIndex <= stopIndex);
359 if(stopIndex == startIndex) {
360 return expressions[startIndex];
363 unsigned pivot = findPivot(operators, startIndex, stopIndex - 1);
364 //Debug("prec") << "pivot[" << startIndex << "," << stopIndex - 1 << "] at " << pivot << std::endl;
366 Expr e = em->mkExpr(getOperatorKind(operators[pivot], negate),
367 createPrecedenceTree(em, expressions, operators, startIndex, pivot),
368 createPrecedenceTree(em, expressions, operators, pivot + 1, stopIndex));
369 return negate ? em->mkExpr(kind::NOT, e) : e;
370 }/* createPrecedenceTree() recursive variant */
372 Expr createPrecedenceTree(ExprManager* em,
373 const std::vector<CVC4::Expr>& expressions,
374 const std::vector<unsigned>& operators) {
375 if(Debug.isOn("prec") && operators.size() > 1) {
376 for(unsigned i = 0; i < expressions.size(); ++i) {
377 Debug("prec") << expressions[i];
378 if(operators.size() > i) {
379 Debug("prec") << ' ' << CvcParserTokenNames[operators[i]] << ' ';
382 Debug("prec") << std::endl;
385 Expr e = createPrecedenceTree(em, expressions, operators, 0, expressions.size() - 1);
386 if(Debug.isOn("prec") && operators.size() > 1) {
387 Expr::setlanguage::Scope ls(Debug("prec"), language::output::LANG_AST);
388 Debug("prec") << "=> " << e << std::endl;
391 }/* createPrecedenceTree() base variant */
393 /** Add n NOTs to the front of e and return the result. */
394 Expr addNots(ExprManager* em, size_t n, Expr e) {
396 e = em->mkExpr(kind::NOT, e);
401 }/* @parser::members */
405 ** This file is part of the CVC4 prototype.
406 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
407 ** Courant Institute of Mathematical Sciences
408 ** New York University
409 ** See the file COPYING in the top-level source directory for licensing
416 /** This suppresses warnings about the redefinition of token symbols between different
417 * parsers. The redefinitions should be harmless as long as no client: (a) #include's
418 * the lexer headers for two grammars AND (b) uses the token symbol definitions. */
419 #pragma GCC system_header
421 /* This improves performance by ~10 percent on big inputs.
422 * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
423 * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
424 * Otherwise, we have to let the lexer detect the encoding at runtime.
426 #define ANTLR3_INLINE_INPUT_ASCII
428 #include "parser/antlr_tracing.h"
429 #include "util/integer.h"
430 #include "parser/antlr_input.h"
431 #include "parser/parser.h"
433 }/* @lexer::includes */
438 #include "expr/command.h"
439 #include "parser/parser.h"
440 #include "util/subrange_bound.h"
441 #include "parser/antlr_tracing.h"
449 * This class is just here to get around an unfortunate bit of Antlr.
450 * We use strings below as return values from rules, which require
451 * them to be constructible by a void*. So we derive the string
452 * class to provide just such a conversion.
454 class myString : public std::string {
456 myString(const std::string& s) : std::string(s) {}
457 myString(void*) : std::string() {}
458 myString() : std::string() {}
459 };/* class myString */
462 * Just exists to give us the void* construction that
465 class mySubrangeBound : public CVC4::SubrangeBound {
467 mySubrangeBound() : CVC4::SubrangeBound() {}
468 mySubrangeBound(void*) : CVC4::SubrangeBound() {}
469 mySubrangeBound(const Integer& i) : CVC4::SubrangeBound(i) {}
470 mySubrangeBound(const SubrangeBound& b) : CVC4::SubrangeBound(b) {}
471 };/* class mySubrangeBound */
474 * Just exists to give us the void* construction that
477 struct myExpr : public CVC4::Expr {
478 myExpr() : CVC4::Expr() {}
479 myExpr(void*) : CVC4::Expr() {}
480 myExpr(const Expr& e) : CVC4::Expr(e) {}
481 myExpr(const myExpr& e) : CVC4::Expr(e) {}
482 };/* struct myExpr */
484 }/* CVC4::parser::cvc namespace */
485 }/* CVC4::parser namespace */
486 }/* CVC4 namespace */
488 }/* @parser::includes */
490 @parser::postinclude {
492 #include "expr/expr.h"
493 #include "expr/kind.h"
494 #include "expr/type.h"
495 #include "parser/antlr_input.h"
496 #include "parser/parser.h"
497 #include "util/output.h"
501 #define REPEAT_COMMAND(k, CommandCtor) \
503 unsigned __k = (k); \
505 ? (Command*) new CommandCtor \
507 CommandSequence* __seq = new CommandSequence(); \
509 __seq->addCommand(new CommandCtor); \
515 using namespace CVC4;
516 using namespace CVC4::parser;
518 /* These need to be macros so they can refer to the PARSER macro, which will be defined
519 * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
521 #define PARSER_STATE ((Parser*)PARSER->super)
523 #define EXPR_MANAGER PARSER_STATE->getExprManager()
525 #define MK_EXPR EXPR_MANAGER->mkExpr
527 #define MK_CONST EXPR_MANAGER->mkConst
528 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
530 }/* @parser::postinclude */
533 * Parses an expression.
534 * @return the parsed expression
536 parseExpr returns [CVC4::Expr expr = CVC4::Expr()]
542 * Parses a command (the whole benchmark)
543 * @return the command of the benchmark
545 parseCommand returns [CVC4::Command* cmd = NULL]
546 : c=command { $cmd = c; }
547 | EOF { $cmd = NULL; }
551 * Matches a command of the input. If a declaration, it will return an empty
554 command returns [CVC4::Command* cmd = NULL]
555 : ( mainCommand[cmd] SEMICOLON
557 | LET_TOK { PARSER_STATE->pushScope(); }
558 typeOrVarLetDecl[CHECK_DECLARED] ( COMMA typeOrVarLetDecl[CHECK_DECLARED] )*
561 PARSER_STATE->popScope();
565 cmd = new EmptyCommand();
570 typeOrVarLetDecl[CVC4::parser::DeclarationCheck check]
571 options { backtrack = true; }
572 : letDecl | typeLetDecl[check]
575 mainCommand[CVC4::Command*& cmd]
581 std::vector<CVC4::Datatype> dts;
582 Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl;
585 /* our bread & butter */
586 : ASSERT_TOK formula[f] { cmd = new AssertCommand(f); }
588 | QUERY_TOK formula[f] { cmd = new QueryCommand(f); }
589 | CHECKSAT_TOK formula[f] { cmd = new CheckSatCommand(f); }
590 | CHECKSAT_TOK { cmd = new CheckSatCommand(MK_CONST(bool(true))); }
594 ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
596 { cmd = new SetOptionCommand(s, sexpr); }
599 | PUSH_TOK ( k=numeral { cmd = REPEAT_COMMAND(k, PushCommand()); }
600 | { cmd = new PushCommand(); } )
601 | POP_TOK ( k=numeral { cmd = REPEAT_COMMAND(k, PopCommand()); }
602 | { cmd = new PopCommand(); } )
603 | POPTO_TOK k=numeral?
604 { UNSUPPORTED("POPTO command"); }
606 /* push / pop scopes */
607 | PUSH_SCOPE_TOK k=numeral?
608 { UNSUPPORTED("PUSH_SCOPE command"); }
609 | POP_SCOPE_TOK k=numeral?
610 { UNSUPPORTED("POP_SCOPE command"); }
611 | POPTO_SCOPE_TOK k=numeral?
612 { UNSUPPORTED("POPTO_SCOPE command"); }
615 { UNSUPPORTED("RESET command"); }
617 // Datatypes can be mututally-recursive if they're in the same
618 // definition block, separated by a comma. So we parse everything
619 // and then ask the ExprManager to resolve everything in one go.
621 { /* open a scope to keep the UnresolvedTypes contained */
622 PARSER_STATE->pushScope(); }
624 ( COMMA datatypeDef[dts] )*
626 { PARSER_STATE->popScope();
627 cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
630 ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
631 { UNSUPPORTED("CONTEXT command"); }
632 | { UNSUPPORTED("CONTEXT command"); }
635 | FORGET_TOK identifier[id,CHECK_NONE,SYM_VARIABLE]
636 { UNSUPPORTED("FORGET command"); }
638 | GET_TYPE_TOK formula[f]
639 { UNSUPPORTED("GET_TYPE command"); }
641 | CHECK_TYPE_TOK formula[f] COLON type[t,CHECK_DECLARED]
642 { UNSUPPORTED("CHECK_TYPE command"); }
644 | GET_CHILD_TOK formula[f] k=numeral
645 { UNSUPPORTED("GET_CHILD command"); }
647 | GET_OP_TOK formula[f]
648 { UNSUPPORTED("GET_OP command"); }
650 | GET_VALUE_TOK formula[f]
651 { cmd = new GetValueCommand(f); }
653 | SUBSTITUTE_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED] EQUAL_TOK
654 formula[f] LBRACKET identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[f] RBRACKET
655 { UNSUPPORTED("SUBSTITUTE command"); }
657 /* Like the --debug command line option, DBG turns on both tracing
660 ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
661 { Debug.on(s); Trace.on(s); }
662 | { Message() << "Please specify what to debug." << std::endl; }
666 ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
668 | { Message() << "Please specify something to trace." << std::endl; }
671 ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
673 | { Message() << "Please specify something to untrace." << std::endl; }
677 ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
678 { Message() << "No help available for `" << s << "'." << std::endl; }
679 | { Message() << "Please use --help at the command line for help." << std::endl; }
682 | TRANSFORM_TOK formula[f]
683 { cmd = new SimplifyCommand(f); }
685 | PRINT_TOK formula[f]
686 { UNSUPPORTED("PRINT command"); }
687 | PRINT_TYPE_TOK type[t,CHECK_DECLARED]
688 { UNSUPPORTED("PRINT_TYPE command"); }
690 | CALL_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] formula[f]
691 { UNSUPPORTED("CALL command"); }
694 ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
695 { Message() << s << std::endl; }
696 | { Message() << std::endl; }
700 { cmd = new QuitCommand(); }
703 ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
704 { UNSUPPORTED("INCLUDE command"); }
705 | { PARSER_STATE->parseError("No filename given to INCLUDE command"); }
709 | DUMP_ASSUMPTIONS_TOK
712 | DUMP_TCC_ASSUMPTIONS_TOK
715 | DUMP_CLOSURE_PROOF_TOK
716 ) { UNSUPPORTED("DUMP* command"); }
718 /* these are all synonyms */
719 | ( WHERE_TOK | ASSERTIONS_TOK | ASSUMPTIONS_TOK )
720 { cmd = new GetAssertionsCommand(); }
723 { UNSUPPORTED("COUNTEREXAMPLE command"); }
725 { UNSUPPORTED("COUNTERMODEL command"); }
727 | ARITH_VAR_ORDER_TOK LPAREN formula[f] ( COMMA formula[f] )* RPAREN
728 { UNSUPPORTED("ARITH_VAR_ORDER command"); }
730 | toplevelDeclaration[cmd]
733 symbolicExpr[CVC4::SExpr& sexpr]
735 std::vector<SExpr> children;
738 : INTEGER_LITERAL ('.' DIGIT+)?
739 { sexpr = SExpr((const char*)$symbolicExpr.text->chars); }
741 { sexpr = SExpr(s); }
743 { sexpr = SExpr(AntlrInput::tokenText($IDENTIFIER)); }
744 | LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN
745 { sexpr = SExpr(children); }
749 * Match a top-level declaration.
751 toplevelDeclaration[CVC4::Command*& cmd]
753 std::vector<std::string> ids;
755 Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl;
757 : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON
758 ( declareVariables[cmd,t,ids,true]
759 | declareTypes[cmd,ids] )
763 * A bound variable declaration.
765 boundVarDecl[std::vector<std::string>& ids, CVC4::Type& t]
766 : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[*(Command**)NULL,t,ids,false]
770 * A series of bound variable declarations.
774 std::vector<std::string> ids;
777 : boundVarDecl[ids,t] ( COMMA boundVarDecl[ids,t] )*
780 boundVarDeclsReturn[std::vector<CVC4::Expr>& terms,
781 std::vector<CVC4::Type>& types]
783 std::vector<std::string> ids;
788 : boundVarDeclReturn[terms,types] ( COMMA boundVarDeclReturn[terms,types] )*
791 boundVarDeclReturn[std::vector<CVC4::Expr>& terms,
792 std::vector<CVC4::Type>& types]
794 std::vector<std::string> ids;
796 // NOTE: do not clear the vectors here!
798 : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED]
799 { const std::vector<Expr>& vars = PARSER_STATE->mkVars(ids, t);
800 terms.insert(terms.end(), vars.begin(), vars.end());
801 for(unsigned i = 0; i < vars.size(); ++i) {
808 * Match the right-hand-side of a type declaration. Unlike
809 * declareVariables[] below, don't need to return the Type, since it's
810 * always the KindType (the type of types). Also don't need toplevel
811 * because type declarations are always top-level, except for
812 * type-lets, which don't use this rule.
814 declareTypes[CVC4::Command*& cmd, const std::vector<std::string>& idList]
818 /* A sort declaration (e.g., "T : TYPE") */
820 { DeclarationSequence* seq = new DeclarationSequence();
821 for(std::vector<std::string>::const_iterator i = idList.begin();
824 // Don't allow a type variable to clash with a previously
825 // declared type variable, however a type variable and a
826 // non-type variable can clash unambiguously. Break from CVC3
828 PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT);
829 Type sort = PARSER_STATE->mkSort(*i);
830 Command* decl = new DeclareTypeCommand(*i, 0, sort);
831 seq->addCommand(decl);
836 /* A type alias "T : TYPE = foo..." */
837 | TYPE_TOK EQUAL_TOK type[t,CHECK_DECLARED]
838 { for(std::vector<std::string>::const_iterator i = idList.begin();
841 PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT);
842 PARSER_STATE->defineType(*i, t);
848 * Match the right-hand side of a variable declaration. Returns the
849 * type. Some IDs might have been declared previously, and are not
850 * re-declared if topLevel is true (CVC allows re-declaration if the
851 * types are compatible---if they aren't compatible, an error is
852 * thrown). Also if topLevel is true, variable definitions are
853 * permitted and "cmd" is output.
855 declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::string>& idList, bool topLevel]
858 Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
860 /* A variable declaration (or definition) */
861 : type[t,CHECK_DECLARED] ( EQUAL_TOK formula[f] )?
862 { DeclarationSequence* seq = NULL;
864 cmd = seq = new DeclarationSequence();
867 Debug("parser") << "working on " << idList.front() << " : " << t << std::endl;
868 // CVC language allows redeclaration of variables if types are the same
869 for(std::vector<std::string>::const_iterator i = idList.begin(),
870 i_end = idList.end();
873 if(PARSER_STATE->isDeclared(*i, SYM_VARIABLE)) {
874 Type oldType = PARSER_STATE->getType(*i);
875 Debug("parser") << " " << *i << " was declared previously "
876 << "with type " << oldType << std::endl;
878 std::stringstream ss;
879 ss << Expr::setlanguage(language::output::LANG_CVC4)
880 << "incompatible type for `" << *i << "':" << std::endl
881 << " old type: " << oldType << std::endl
882 << " new type: " << t << std::endl;
883 PARSER_STATE->parseError(ss.str());
885 Debug("parser") << " types " << t << " and " << oldType
886 << " are compatible" << std::endl;
889 Debug("parser") << " " << *i << " not declared" << std::endl;
890 PARSER_STATE->mkVar(*i, t);
892 Command* decl = new DeclareFunctionCommand(*i, t);
893 seq->addCommand(decl);
899 // must be top-level; doesn't make sense to write something
900 // like e.g. FORALL(x:INT = 4): [...]
901 PARSER_STATE->parseError("cannot construct a definition here; maybe you want a LET");
903 Debug("parser") << "made " << idList.front() << " = " << f << std::endl;
904 for(std::vector<std::string>::const_iterator i = idList.begin(),
905 i_end = idList.end();
908 PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
909 PARSER_STATE->defineFunction(*i, f);
910 Command* decl = new DefineFunctionCommand(*i, Expr(), f);
911 seq->addCommand(decl);
918 * Matches a list of identifiers separated by a comma and puts them in the
920 * @param idList the list to fill with identifiers.
921 * @param check what kinds of check to perform on the symbols
923 identifierList[std::vector<std::string>& idList,
924 CVC4::parser::DeclarationCheck check,
925 CVC4::parser::SymbolType type]
930 : identifier[id,check,type] { idList.push_back(id); }
931 ( COMMA identifier[id,check,type] { idList.push_back(id); } )*
935 * Matches an identifier and returns a string.
937 identifier[std::string& id,
938 CVC4::parser::DeclarationCheck check,
939 CVC4::parser::SymbolType type]
941 { id = AntlrInput::tokenText($IDENTIFIER);
942 PARSER_STATE->checkDeclaration(id, check, type); }
946 * Match the type in a declaration and do the declaration binding. If
947 * "check" is CHECK_NONE, then identifiers occurring in the type need
948 * not exist! They are created as "unresolved" types and linked up in
949 * a type-substitution pass. Right now, only datatype definitions are
950 * supported in this way (since type names can occur without any
951 * forward-declaration in CVC language datatype definitions, we have
952 * to create types for them on-the-fly). Before passing CHECK_NONE
953 * you really should have a clear idea of WHY you need to parse that
954 * way; then you should trace through Parser::mkMutualDatatypeType()
955 * to figure out just what you're in for.
958 CVC4::parser::DeclarationCheck check]
962 std::vector<Type> args;
964 /* a type, possibly a function */
965 : restrictedTypePossiblyFunctionLHS[t,check,lhs]
968 args = TupleType(t).getTypes();
973 ( ARROW_TOK type[t2,check] { args.push_back(t2); } )?
976 PARSER_STATE->parseError("improperly-placed type list; expected `->' after to define a function; or else maybe these parentheses were meant to be square brackets, to define a tuple type?");
979 t = EXPR_MANAGER->mkFunctionType(args);
983 /* type-lets: typeLetDecl defines the types, we just manage the
984 * scopes here. NOTE that LET in the CVC language is always
986 | LET_TOK { PARSER_STATE->pushScope(); }
987 typeLetDecl[check] ( COMMA typeLetDecl[check] )* IN_TOK type[t,check]
988 { PARSER_STATE->popScope(); }
991 // A restrictedType is one that is not a "bare" function type (it can
992 // be enclosed in parentheses) and is not a type list. To support the
995 // f : (nat, nat) -> nat;
997 // we have to permit restrictedTypes to be type lists (as on the LHS
998 // there). The "type" rule above uses restictedTypePossiblyFunctionLHS
999 // directly in order to implement that; this rule allows a type list to
1000 // parse but then issues an error.
1001 restrictedType[CVC4::Type& t,
1002 CVC4::parser::DeclarationCheck check]
1006 : restrictedTypePossiblyFunctionLHS[t,check,lhs]
1007 { if(lhs) { PARSER_STATE->parseError("improperly-placed type list; maybe these parentheses were meant to be square brackets, to define a tuple type?"); } }
1011 * lhs is set to "true" on output if we have a list of types, so an
1012 * ARROW must follow. An ARROW can always follow; lhs means it MUST.
1014 restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
1015 CVC4::parser::DeclarationCheck check,
1021 std::vector<Type> types;
1025 : identifier[id,check,SYM_SORT]
1026 parameterization[check,types]?
1028 if(check == CHECK_DECLARED ||
1029 PARSER_STATE->isDeclared(id, SYM_SORT)) {
1030 Debug("parser-param") << "param: getSort " << id << " " << types.size() << " " << PARSER_STATE->getArity( id )
1031 << " " << PARSER_STATE->isDeclared(id, SYM_SORT) << std::endl;
1032 if( types.size()>0 ){
1033 t = PARSER_STATE->getSort(id, types);
1035 t = PARSER_STATE->getSort(id);
1038 if( types.empty() ){
1039 t = PARSER_STATE->mkUnresolvedType(id);
1040 Debug("parser-param") << "param: make unres type " << id << std::endl;
1042 t = PARSER_STATE->mkUnresolvedTypeConstructor(id,types);
1043 t = SortConstructorType(t).instantiate( types );
1044 Debug("parser-param") << "param: make unres param type " << id << " " << types.size() << " "
1045 << PARSER_STATE->getArity( id ) << std::endl;
1051 | ARRAY_TOK restrictedType[t,check] OF_TOK restrictedType[t2,check]
1052 { t = EXPR_MANAGER->mkArrayType(t, t2); }
1055 | SUBTYPE_TOK LPAREN formula[f] ( COMMA formula[f] )? RPAREN
1056 { UNSUPPORTED("subtypes not supported yet");
1059 /* subrange types */
1060 | LBRACKET k1=bound DOTDOT k2=bound RBRACKET
1061 { std::stringstream ss;
1062 ss << "subranges not supported yet: [" << k1 << ":" << k2 << ']';
1063 UNSUPPORTED(ss.str());
1064 if(k1.hasBound() && k2.hasBound() &&
1065 k1.getBound() > k2.getBound()) {
1067 ss << "Subrange [" << k1.getBound() << ".." << k2.getBound()
1068 << "] inappropriate: range must be nonempty!";
1069 PARSER_STATE->parseError(ss.str());
1071 Debug("subranges") << ss.str() << std::endl;
1074 /* tuple types / old-style function types */
1075 | LBRACKET type[t,check] { types.push_back(t); }
1076 ( COMMA type[t,check] { types.push_back(t); } )* RBRACKET
1077 { if(types.size() == 1) {
1078 if(types.front().isFunction()) {
1079 // old style function syntax [ T -> U ]
1080 PARSER_STATE->parseError("old-style function type syntax not supported anymore; please use the new syntax");
1082 PARSER_STATE->parseError("I'm not sure what you're trying to do here; tuples must have > 1 type");
1085 // tuple type [ T, U, V... ]
1086 t = EXPR_MANAGER->mkTupleType(types);
1091 | SQHASH identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check]
1092 ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] )* HASHSQ
1093 { UNSUPPORTED("records not supported yet");
1096 /* bitvector types */
1097 | BITVECTOR_TOK LPAREN k=numeral RPAREN
1098 { t = EXPR_MANAGER->mkBitVectorType(k); }
1101 | BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); }
1102 | REAL_TOK { t = EXPR_MANAGER->realType(); }
1103 | INT_TOK { t = EXPR_MANAGER->integerType(); }
1105 /* Parenthesized general type, or the lhs of an ARROW (a list of
1106 * types). These two things are combined to avoid conflicts in
1108 | LPAREN type[t,check] { types.push_back(t); }
1109 ( COMMA type[t,check] { lhs = true; types.push_back(t); } )* RPAREN
1110 { if(lhs) { t = EXPR_MANAGER->mkTupleType(types); }
1111 // if !lhs, t is already set up correctly, nothing to do..
1115 parameterization[CVC4::parser::DeclarationCheck check,
1116 std::vector<CVC4::Type>& params]
1120 : LBRACKET restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); }
1121 ( COMMA restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); } )* RBRACKET
1124 bound returns [CVC4::parser::cvc::mySubrangeBound bound]
1125 : UNDERSCORE { $bound = SubrangeBound(); }
1126 | k=integer { $bound = SubrangeBound(k); }
1129 typeLetDecl[CVC4::parser::DeclarationCheck check]
1134 : identifier[id,CHECK_NONE,SYM_SORT] (COLON TYPE_TOK)? EQUAL_TOK restrictedType[t,check]
1135 { PARSER_STATE->defineType(id, t); }
1139 * Matches a CVC4 expression. Formulas and terms are not really
1140 * distinguished during parsing; please ignore the naming of the
1143 * @return the expression representing the formula/term
1145 formula[CVC4::Expr& f]
1147 Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
1149 std::vector<CVC4::Expr> expressions;
1150 std::vector<unsigned> operators;
1155 { f = addNots(EXPR_MANAGER, n, f); }
1157 { f = addNots(EXPR_MANAGER, n, f);
1158 expressions.push_back(f);
1160 i=morecomparisons[expressions,operators]?
1161 { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
1165 morecomparisons[std::vector<CVC4::Expr>& expressions,
1166 std::vector<unsigned>& operators] returns [size_t i = 0]
1170 $i = expressions.size();
1172 : booleanBinop[op] { operators.push_back(op); }
1175 { expressions.push_back(addNots(EXPR_MANAGER, n, f)); }
1177 { f = addNots(EXPR_MANAGER, n, f);
1178 expressions.push_back(f);
1180 inner=morecomparisons[expressions,operators]?
1184 /** Matches 0 or more NOTs. */
1185 nots returns [size_t n = 0]
1186 : ( NOT_TOK { ++$n; } )*
1189 prefixFormula[CVC4::Expr& f]
1191 std::vector<std::string> ids;
1192 std::vector<Expr> terms;
1193 std::vector<Type> types;
1197 : FORALL_TOK { PARSER_STATE->pushScope(); } LPAREN
1198 boundVarDecl[ids,t] (COMMA boundVarDecl[ids,t])* RPAREN
1199 COLON instantiationPatterns? formula[f]
1200 { PARSER_STATE->popScope();
1201 UNSUPPORTED("quantifiers not supported yet");
1202 f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType());
1204 | EXISTS_TOK { PARSER_STATE->pushScope(); } LPAREN
1205 boundVarDecl[ids,t] (COMMA boundVarDecl[ids,t])* RPAREN
1206 COLON instantiationPatterns? formula[f]
1207 { PARSER_STATE->popScope();
1208 UNSUPPORTED("quantifiers not supported yet");
1209 f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType());
1212 /* lets: letDecl defines the variables and functionss, we just
1213 * manage the scopes here. NOTE that LET in the CVC language is
1214 * always sequential! */
1215 | LET_TOK { PARSER_STATE->pushScope(); }
1216 letDecl ( COMMA letDecl )*
1217 IN_TOK formula[f] { PARSER_STATE->popScope(); }
1220 | LAMBDA { PARSER_STATE->pushScope(); } LPAREN
1221 boundVarDeclsReturn[terms,types]
1222 RPAREN COLON formula[f]
1223 { PARSER_STATE->popScope();
1224 Type t = EXPR_MANAGER->mkFunctionType(types, f.getType());
1225 std::string name = "lambda";
1226 Expr func = PARSER_STATE->mkAnonymousFunction(name, t);
1227 Command* cmd = new DefineFunctionCommand(name, func, terms, f);
1228 PARSER_STATE->preemptCommand(cmd);
1232 /* array literals */
1233 | ARRAY_TOK { PARSER_STATE->pushScope(); } LPAREN
1234 boundVarDecl[ids,t] RPAREN COLON formula[f]
1235 { PARSER_STATE->popScope();
1236 UNSUPPORTED("array literals not supported yet");
1237 f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType()));
1241 instantiationPatterns
1245 : ( PATTERN_TOK LPAREN formula[f] (COMMA formula[f])* RPAREN COLON )+
1249 * Matches (and defines) a single LET declaration.
1256 : identifier[name,CHECK_NONE,SYM_VARIABLE] EQUAL_TOK formula[e]
1257 { Debug("parser") << Expr::setlanguage(language::output::LANG_CVC4) << e.getType() << std::endl;
1258 PARSER_STATE->defineVar(name, e);
1259 Debug("parser") << "LET[" << PARSER_STATE->getDeclarationLevel() << "]: "
1260 << name << std::endl
1261 << " ==>" << " " << e << std::endl;
1265 booleanBinop[unsigned& op]
1267 op = LT(1)->getType(LT(1));
1276 comparison[CVC4::Expr& f]
1278 std::vector<CVC4::Expr> expressions;
1279 std::vector<unsigned> operators;
1282 : term[f] { expressions.push_back(f); }
1283 ( comparisonBinop[op] term[f]
1284 { operators.push_back(op); expressions.push_back(f); } )*
1285 { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
1288 comparisonBinop[unsigned& op]
1290 op = LT(1)->getType(LT(1));
1302 std::vector<CVC4::Expr> expressions;
1303 std::vector<unsigned> operators;
1307 : storeTerm[f] { expressions.push_back(f); }
1308 ( arithmeticBinop[op] storeTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
1309 { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
1312 arithmeticBinop[unsigned& op]
1314 op = LT(1)->getType(LT(1));
1324 /** Parses an array assignment term. */
1325 storeTerm[CVC4::Expr& f]
1327 ( WITH_TOK arrayStore[f] ( COMMA arrayStore[f] )* )*
1331 * Parses just part of the array assignment (and constructs
1334 arrayStore[CVC4::Expr& f]
1337 std::vector<Expr> dims;
1339 : ( LBRACKET formula[f2] { dims.push_back(f2); } RBRACKET )+
1340 ASSIGN_TOK uminusTerm[f3]
1341 { Assert(dims.size() >= 1);
1342 // these loops are a bit complicated; they're only used for the
1343 // multidimensional ...WITH [a][b] :=... syntax
1344 for(unsigned i = 0; i < dims.size() - 1; ++i) {
1345 f = MK_EXPR(CVC4::kind::SELECT, f, dims[i]);
1347 // a[i][j][k] := v turns into
1348 // store(a, i, store(a[i], j, store(a[i][j], k, v)))
1349 for(unsigned i = dims.size() - 1; i > 0; --i) {
1350 f3 = MK_EXPR(CVC4::kind::STORE, f, dims[i], f3);
1351 // strip off one layer of the select
1355 // outermost wrapping
1356 f = MK_EXPR(CVC4::kind::STORE, f, dims[0], f3);
1360 /** Parses a unary minus term. */
1361 uminusTerm[CVC4::Expr& f]
1363 unsigned minusCount = 0;
1366 : (MINUS_TOK { ++minusCount; })+ bvBinaryOpTerm[f]
1367 { while(minusCount > 0) { --minusCount; f = MK_EXPR(CVC4::kind::UMINUS, f); } }
1371 /** Parses bitvectors. Starts with binary operators @, &, and |. */
1372 bvBinaryOpTerm[CVC4::Expr& f]
1374 std::vector<CVC4::Expr> expressions;
1375 std::vector<unsigned> operators;
1378 : bvNegTerm[f] { expressions.push_back(f); }
1379 ( bvBinop[op] bvNegTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
1380 { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
1382 bvBinop[unsigned& op]
1384 op = LT(1)->getType(LT(1));
1391 bvNegTerm[CVC4::Expr& f]
1393 : BVNEG_TOK bvNegTerm[f]
1394 { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
1399 * Parses an array select / bitvector extract / bitvector shift /
1400 * function or constructor application. These are all parsed the same
1401 * way because they are all effectively post-fix operators and can
1402 * continue piling onto an expression. Array selects and bitvector
1403 * extracts even share similar syntax with their use of [ square
1404 * brackets ], so we left-factor as much out as possible to make ANTLR
1407 postfixTerm[CVC4::Expr& f]
1410 bool extract = false, left = false;
1411 std::vector<Expr> args;
1416 ( /* array select / bitvector extract */
1418 ( formula[f2] { extract = false; }
1419 | k1=numeral COLON k2=numeral { extract = true; } )
1422 /* bitvector extract */
1423 f = MK_EXPR(MK_CONST(BitVectorExtract(k1, k2)), f);
1426 f = MK_EXPR(CVC4::kind::SELECT, f, f2);
1430 /* left- or right-shift */
1431 | ( LEFTSHIFT_TOK { left = true; }
1432 | RIGHTSHIFT_TOK { left = false; } ) k=numeral
1434 // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit
1436 f = MK_EXPR(kind::BITVECTOR_CONCAT, f, MK_CONST(BitVector(k)));
1438 unsigned n = BitVectorType(f.getType()).getSize();
1439 f = MK_EXPR(kind::BITVECTOR_CONCAT, MK_CONST(BitVector(k)),
1440 MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f));
1444 /* function/constructor application */
1445 | LPAREN { args.push_back(f); }
1446 formula[f] { args.push_back(f); }
1447 ( COMMA formula[f] { args.push_back(f); } )* RPAREN
1448 // TODO: check arity
1449 { Type t = args.front().getType();
1450 Debug("parser") << "type is " << t << std::endl;
1451 Debug("parser") << "expr is " << args.front() << std::endl;
1452 if(PARSER_STATE->isDefinedFunction(args.front())) {
1453 f = MK_EXPR(CVC4::kind::APPLY, args);
1454 } else if(t.isFunction()) {
1455 f = MK_EXPR(CVC4::kind::APPLY_UF, args);
1456 } else if(t.isConstructor()) {
1457 f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
1458 } else if(t.isSelector()) {
1459 f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args);
1460 } else if(t.isTester()) {
1461 f = MK_EXPR(CVC4::kind::APPLY_TESTER, args);
1467 /* record / tuple select */
1468 // FIXME - clash in lexer between tuple-select and real; can
1469 // resolve with syntactic predicate in ANTLR 3.3, but broken in
1472 ( identifier[id,CHECK_NONE,SYM_VARIABLE]
1473 { UNSUPPORTED("record select not implemented yet");
1476 { UNSUPPORTED("tuple select not implemented yet");
1477 // This will assert-fail if k too big or f not a tuple
1478 // that's ok for now, once a TUPLE_SELECT operator exists,
1479 // that will do any necessary type checking
1480 f = EXPR_MANAGER->mkVar(TupleType(f.getType()).getTypes()[k]); }
1483 ( typeAscription[f, t]
1484 { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) {
1485 std::vector<CVC4::Expr> v;
1486 Expr e = f.getOperator();
1487 const Datatype::Constructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)];
1488 v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
1489 MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator() ));
1490 v.insert(v.end(), f.begin(), f.end());
1491 f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
1493 if(f.getType() != t) {
1494 PARSER_STATE->parseError("Type ascription not satisfied.");
1501 bvTerm[CVC4::Expr& f]
1506 : BVXOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1507 { f = MK_EXPR(CVC4::kind::BITVECTOR_XOR, f, f2); }
1508 | BVNAND_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1509 { f = MK_EXPR(CVC4::kind::BITVECTOR_NAND, f, f2); }
1510 | BVNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1511 { f = MK_EXPR(CVC4::kind::BITVECTOR_NOR, f, f2); }
1512 | BVCOMP_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1513 { f = MK_EXPR(CVC4::kind::BITVECTOR_COMP, f, f2); }
1514 | BVXNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1515 { f = MK_EXPR(CVC4::kind::BITVECTOR_XNOR, f, f2); }
1517 /* BV unary minus */
1518 | BVUMINUS_TOK LPAREN formula[f] RPAREN
1519 { f = MK_EXPR(CVC4::kind::BITVECTOR_NEG, f); }
1521 | BVPLUS_TOK LPAREN k=numeral COMMA formula[f]
1522 ( COMMA formula[f2] { f = MK_EXPR(CVC4::kind::BITVECTOR_PLUS, f, f2); } )+ RPAREN
1523 { unsigned size = BitVectorType(f.getType()).getSize();
1525 PARSER_STATE->parseError("BVPLUS(k,_,_,...) must have k > 0");
1528 f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f);
1529 } else if(k < size) {
1530 f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f);
1533 /* BV subtraction */
1534 | BVSUB_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN
1535 { f = MK_EXPR(CVC4::kind::BITVECTOR_SUB, f, f2);
1537 PARSER_STATE->parseError("BVSUB(k,_,_) must have k > 0");
1539 unsigned size = BitVectorType(f.getType()).getSize();
1541 f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f);
1542 } else if(k < size) {
1543 f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f);
1546 /* BV multiplication */
1547 | BVMULT_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN
1548 { f = MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2);
1550 PARSER_STATE->parseError("BVMULT(k,_,_) must have k > 0");
1552 unsigned size = BitVectorType(f.getType()).getSize();
1554 f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f);
1555 } else if(k < size) {
1556 f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f);
1559 /* BV unsigned division */
1560 | BVUDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1561 { f = MK_EXPR(CVC4::kind::BITVECTOR_UDIV, f, f2); }
1562 /* BV signed division */
1563 | BVSDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1564 { f = MK_EXPR(CVC4::kind::BITVECTOR_SDIV, f, f2); }
1565 /* BV unsigned remainder */
1566 | BVUREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1567 { f = MK_EXPR(CVC4::kind::BITVECTOR_UREM, f, f2); }
1568 /* BV signed remainder */
1569 | BVSREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1570 { f = MK_EXPR(CVC4::kind::BITVECTOR_SREM, f, f2); }
1571 /* BV signed modulo */
1572 | BVSMOD_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1573 { f = MK_EXPR(CVC4::kind::BITVECTOR_SMOD, f, f2); }
1575 | BVSHL_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1576 { f = MK_EXPR(CVC4::kind::BITVECTOR_SHL, f, f2); }
1577 /* BV arithmetic right shift */
1578 | BVASHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1579 { f = MK_EXPR(CVC4::kind::BITVECTOR_ASHR, f, f2); }
1580 /* BV logical left shift */
1581 | BVLSHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1582 { f = MK_EXPR(CVC4::kind::BITVECTOR_LSHR, f, f2); }
1583 /* BV sign extension */
1584 | SX_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1585 { unsigned n = BitVectorType(f.getType()).getSize();
1586 // Sign extension in TheoryBitVector is defined as in SMT-LIBv2
1587 // which is different than in the CVC language
1588 // SX(BITVECTOR(k), n) in CVC language extends to n bits
1589 // In SMT-LIBv2, such a thing expands to k + n bits
1590 f = MK_EXPR(MK_CONST(BitVectorSignExtend(k - n)), f); }
1591 /* BV zero extension */
1592 | BVZEROEXTEND_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1593 { unsigned n = BitVectorType(f.getType()).getSize();
1594 // Zero extension in TheoryBitVector is defined as in SMT-LIBv2
1595 // which is the same as in CVC3, but different than SX!
1596 // SX(BITVECTOR(k), n) in CVC language extends to n bits
1597 // BVZEROEXTEND(BITVECTOR(k), n) in CVC language extends to k + n bits
1598 f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f); }
1599 /* BV repeat operation */
1600 | BVREPEAT_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1601 { f = MK_EXPR(MK_CONST(BitVectorRepeat(k)), f); }
1602 /* BV rotate right */
1603 | BVROTR_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1604 { f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); }
1605 /* BV rotate left */
1606 | BVROTL_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1607 { f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); }
1609 /* BV comparisons */
1610 | BVLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1611 { f = MK_EXPR(CVC4::kind::BITVECTOR_ULT, f, f2); }
1612 | BVLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1613 { f = MK_EXPR(CVC4::kind::BITVECTOR_ULE, f, f2); }
1614 | BVGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1615 { f = MK_EXPR(CVC4::kind::BITVECTOR_UGT, f, f2); }
1616 | BVGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1617 { f = MK_EXPR(CVC4::kind::BITVECTOR_UGE, f, f2); }
1618 | BVSLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1619 { f = MK_EXPR(CVC4::kind::BITVECTOR_SLT, f, f2); }
1620 | BVSLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1621 { f = MK_EXPR(CVC4::kind::BITVECTOR_SLE, f, f2); }
1622 | BVSGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1623 { f = MK_EXPR(CVC4::kind::BITVECTOR_SGT, f, f2); }
1624 | BVSGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1625 { f = MK_EXPR(CVC4::kind::BITVECTOR_SGE, f, f2); }
1628 | IS_INTEGER_TOK LPAREN formula[f] RPAREN
1629 { f = MK_EXPR(CVC4::kind::BITVECTOR_IS_INTEGER, f); }
1635 /** Parses a simple term. */
1636 simpleTerm[CVC4::Expr& f]
1639 std::vector<Expr> args;
1640 Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
1646 /* parenthesized sub-formula / tuple literals */
1647 | LPAREN formula[f] { args.push_back(f); }
1648 ( COMMA formula[f] { args.push_back(f); } )* RPAREN
1649 { if(args.size() > 1) {
1650 /* If args has elements, we must be a tuple literal.
1651 * Otherwise, f is already the sub-formula, and
1652 * there's nothing to do */
1653 f = EXPR_MANAGER->mkExpr(kind::TUPLE, args);
1657 /* boolean literals */
1658 | TRUE_TOK { f = MK_CONST(bool(true)); }
1659 | FALSE_TOK { f = MK_CONST(bool(false)); }
1660 /* arithmetic literals */
1661 /* syntactic predicate: never match INTEGER.DIGIT as an integer and a dot!
1662 * This is a rational constant! Otherwise the parser interprets it as a tuple
1664 | DECIMAL_LITERAL { f = MK_CONST(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
1665 | INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
1666 /* bitvector literals */
1668 { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 );
1669 std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4);
1670 f = MK_CONST( BitVector(hexString, 16) ); }
1672 { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 );
1673 std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4);
1674 f = MK_CONST( BitVector(binString, 2) ); }
1675 /* record literals */
1676 | PARENHASH recordEntry (COMMA recordEntry)+ HASHPAREN
1677 { UNSUPPORTED("records not implemented yet");
1680 /* variable / zero-ary constructor application */
1681 | identifier[name,CHECK_DECLARED,SYM_VARIABLE]
1682 /* ascriptions will be required for parameterized zero-ary constructors */
1683 { f = PARSER_STATE->getVariable(name); }
1684 { // datatypes: zero-ary constructors
1685 Type t2 = PARSER_STATE->getType(name);
1686 if(t2.isConstructor() && ConstructorType(t2).getArity() == 0) {
1687 // don't require parentheses, immediately turn it into an apply
1688 f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, f);
1694 * Matches (and performs) a type ascription.
1695 * The f arg is the term to check (it is an input-only argument).
1697 typeAscription[const CVC4::Expr& f, CVC4::Type& t]
1700 : COLON COLON type[t,CHECK_DECLARED]
1704 * Matches an entry in a record literal.
1711 : identifier[id,CHECK_DECLARED,SYM_VARIABLE] ASSIGN_TOK formula[f]
1715 * Parses an ITE term.
1717 iteTerm[CVC4::Expr& f]
1719 std::vector<Expr> args;
1720 Debug("parser-extra") << "ite: " << AntlrInput::tokenText(LT(1)) << std::endl;
1722 : IF_TOK formula[f] { args.push_back(f); }
1723 THEN_TOK formula[f] { args.push_back(f); }
1724 iteElseTerm[f] { args.push_back(f); }
1726 { f = MK_EXPR(CVC4::kind::ITE, args); }
1730 * Parses the else part of the ITE, i.e. ELSE f, or ELSIF b THEN f1 ...
1732 iteElseTerm[CVC4::Expr& f]
1734 std::vector<Expr> args;
1735 Debug("parser-extra") << "else: " << AntlrInput::tokenText(LT(1)) << std::endl;
1737 : ELSE_TOK formula[f]
1738 | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); }
1739 THEN_TOK iteThen = formula[f] { args.push_back(f); }
1740 iteElse = iteElseTerm[f] { args.push_back(f); }
1741 { f = MK_EXPR(CVC4::kind::ITE, args); }
1745 * Parses a datatype definition
1747 datatypeDef[std::vector<CVC4::Datatype>& datatypes]
1749 std::string id, id2;
1751 std::vector< Type > params;
1753 /* This really needs to be CHECK_NONE, or mutually-recursive
1754 * datatypes won't work, because this type will already be
1755 * "defined" as an unresolved type; don't worry, we check
1757 : identifier[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
1758 ( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] {
1759 t = PARSER_STATE->mkSort(id2);
1760 params.push_back( t );
1762 ( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] {
1763 t = PARSER_STATE->mkSort(id2);
1764 params.push_back( t ); }
1767 { datatypes.push_back(Datatype(id,params));
1768 if(!PARSER_STATE->isUnresolvedType(id)) {
1769 // if not unresolved, must be undeclared
1770 PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
1773 EQUAL_TOK constructorDef[datatypes.back()]
1774 ( BAR constructorDef[datatypes.back()] )*
1775 { PARSER_STATE->popScope(); }
1779 * Parses a constructor defintion for type
1781 constructorDef[CVC4::Datatype& type]
1784 CVC4::Datatype::Constructor* ctor = NULL;
1786 : identifier[id,CHECK_UNDECLARED,SYM_SORT]
1787 { // make the tester
1788 std::string testerId("is_");
1789 testerId.append(id);
1790 PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
1791 ctor = new CVC4::Datatype::Constructor(id, testerId);
1795 ( COMMA selector[*ctor] )*
1798 { // make the constructor
1799 type.addConstructor(*ctor);
1800 Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
1805 selector[CVC4::Datatype::Constructor& ctor]
1810 : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON type[t,CHECK_NONE]
1811 { ctor.addArg(id, t);
1812 Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
1817 * Matches an identifier from the input. An identifier is a sequence of letters,
1818 * digits and "_", "'", "." symbols, starting with a letter.
1820 IDENTIFIER : (ALPHA | '_') (ALPHA | DIGIT | '_' | '\'' | '\\' | '?' | '$' | '~')*;
1823 * Matches an integer literal.
1832 * Matches a decimal literal.
1835 : INTEGER_LITERAL '.' DIGIT+
1839 * Same as an integer literal converted to an unsigned int, but
1840 * slightly more convenient AND works around a strange ANTLR bug (?)
1841 * in the BVPLUS/BVMINUS/BVMULT rules where $INTEGER_LITERAL was
1842 * returning a reference to the wrong token?!
1844 numeral returns [unsigned k = 0]
1846 { $k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); }
1850 * Similar to numeral but for arbitrary-precision, signed integer.
1852 integer returns [CVC4::Integer k = 0]
1854 { $k = AntlrInput::tokenToInteger($INTEGER_LITERAL); }
1855 | MINUS_TOK INTEGER_LITERAL
1856 { $k = -AntlrInput::tokenToInteger($INTEGER_LITERAL); }
1860 * Similar to numeral but for strings.
1864 { s = AntlrInput::tokenText($STRING_LITERAL);
1865 /* strip off the quotes */
1866 s = s.substr(1, s.size() - 2);
1871 * Matches a hexadecimal constant.
1878 * Matches a binary constant.
1881 : '0bin' ('0' | '1')+
1885 * Matches a double quoted string literal. Escaping is supported, and
1886 * escape character '\' has to be escaped.
1888 STRING_LITERAL: '"' (ESCAPE | ~('"'|'\\'))* '"';
1891 * Matches any letter ('a'-'z' and 'A'-'Z').
1893 fragment ALPHA : 'a'..'z' | 'A'..'Z';
1896 * Matches the decimal digits (0-9)
1898 fragment DIGIT : '0'..'9';
1901 * Matches the hexidecimal digits (0-9, a-f, A-F)
1903 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
1906 * Matches and skips whitespace in the input and ignores it.
1908 WHITESPACE : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); };
1911 * Matches the comments and ignores them
1913 COMMENT : '%' (~('\n' | '\r'))* { SKIP(); };
1916 * Matches an allowed escaped character.
1918 fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');