1 /* ******************* */
4 ** Original author: Christopher L. Conway
5 ** Major contributors: Morgan Deters
6 ** Minor contributors (to current version): Tim King, Andrew Reynolds, Dejan Jovanovic
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Parser for CVC presentation input language
14 ** Parser for CVC presentation input language.
23 // Skip the default error handling, just break with exceptions
24 // defaultErrorHandler = false;
26 // Only lookahead of <= k requested (disable for LL* parsing)
27 // Note that CVC4's BoundedTokenBuffer requires a fixed k !
28 // If you change this k, change it also in cvc_input.cpp !
35 ASSERT_TOK = 'ASSERT';
37 CHECKSAT_TOK = 'CHECKSAT';
38 OPTION_TOK = 'OPTION';
42 PUSH_SCOPE_TOK = 'PUSH_SCOPE';
43 POP_SCOPE_TOK = 'POP_SCOPE';
44 POPTO_SCOPE_TOK = 'POPTO_SCOPE';
46 DATATYPE_TOK = 'DATATYPE';
48 CONTEXT_TOK = 'CONTEXT';
49 FORGET_TOK = 'FORGET';
50 GET_TYPE_TOK = 'GET_TYPE';
51 CHECK_TYPE_TOK = 'CHECK_TYPE';
52 GET_CHILD_TOK = 'GET_CHILD';
53 GET_OP_TOK = 'GET_OP';
54 GET_VALUE_TOK = 'GET_VALUE';
55 SUBSTITUTE_TOK = 'SUBSTITUTE';
58 UNTRACE_TOK = 'UNTRACE';
60 TRANSFORM_TOK = 'TRANSFORM';
62 PRINT_TYPE_TOK = 'PRINT_TYPE';
66 INCLUDE_TOK = 'INCLUDE';
67 DUMP_PROOF_TOK = 'DUMP_PROOF';
68 DUMP_ASSUMPTIONS_TOK = 'DUMP_ASSUMPTIONS';
69 DUMP_SIG_TOK = 'DUMP_SIG';
70 DUMP_TCC_TOK = 'DUMP_TCC';
71 DUMP_TCC_ASSUMPTIONS_TOK = 'DUMP_TCC_ASSUMPTIONS';
72 DUMP_TCC_PROOF_TOK = 'DUMP_TCC_PROOF';
73 DUMP_CLOSURE_TOK = 'DUMP_CLOSURE';
74 DUMP_CLOSURE_PROOF_TOK = 'DUMP_CLOSURE_PROOF';
76 ASSERTIONS_TOK = 'ASSERTIONS';
77 ASSUMPTIONS_TOK = 'ASSUMPTIONS';
78 COUNTEREXAMPLE_TOK = 'COUNTEREXAMPLE';
79 COUNTERMODEL_TOK = 'COUNTERMODEL';
80 ARITH_VAR_ORDER_TOK = 'ARITH_VAR_ORDER';
85 BOOLEAN_TOK = 'BOOLEAN';
106 SUBTYPE_TOK = 'SUBTYPE';
108 FORALL_TOK = 'FORALL';
109 EXISTS_TOK = 'EXISTS';
110 PATTERN_TOK = 'PATTERN';
153 DISTINCT_TOK = 'DISTINCT';
157 BITVECTOR_TOK = 'BITVECTOR';
158 LEFTSHIFT_TOK = '<<';
159 RIGHTSHIFT_TOK = '>>';
160 BVPLUS_TOK = 'BVPLUS';
162 BVUDIV_TOK = 'BVUDIV';
163 BVSDIV_TOK = 'BVSDIV';
164 BVUREM_TOK = 'BVUREM';
165 BVSREM_TOK = 'BVSREM';
166 BVSMOD_TOK = 'BVSMOD';
168 BVASHR_TOK = 'BVASHR';
169 BVLSHR_TOK = 'BVLSHR';
170 BVUMINUS_TOK = 'BVUMINUS';
171 BVMULT_TOK = 'BVMULT';
175 BVNAND_TOK = 'BVNAND';
177 BVCOMP_TOK = 'BVCOMP';
178 BVXNOR_TOK = 'BVXNOR';
180 //BVTOINT_TOK = 'BVTOINT';
181 //INTTOBV_TOK = 'INTTOBV';
182 //BOOLEXTRACT_TOK = 'BOOLEXTRACT';
183 //IS_INTEGER_TOK = 'IS_INTEGER';
189 BVZEROEXTEND_TOK = 'BVZEROEXTEND';
190 BVREPEAT_TOK = 'BVREPEAT';
191 BVROTL_TOK = 'BVROTL';
192 BVROTR_TOK = 'BVROTR';
198 // these are parsed by special NUMBER_OR_RANGEOP rule, below
207 // Idea and code guidance from Sam Harwell,
208 // http://www.antlr.org/wiki/display/ANTLR3/Operator+precedence+parser
210 bool isRightToLeft(int type) {
211 // return true here for any operators that are right-to-left associative
213 case IMPLIES_TOK: return true;
214 default: return false;
216 }/* isRightToLeft() */
218 int getOperatorPrecedence(int type) {
220 case BITVECTOR_TOK: return 1;
223 case LBRACE: return 2;
224 case LBRACKET: return 3;
225 case ARROW_TOK: return 4;
226 //case IS_INTEGER_TOK: return 5;
230 case BVSGE_TOK: return 6;
234 case BVGE_TOK: return 7;
236 case RIGHTSHIFT_TOK: return 8;
238 case BVZEROEXTEND_TOK:
241 case BVROTR_TOK: return 9;
249 case BVLSHR_TOK: return 10;
252 case BVSUB_TOK: return 11;
253 case BVNEG_TOK: return 12;
254 case BVXNOR_TOK: return 13;
256 case BVCOMP_TOK: return 14;
257 case BVNAND_TOK: return 15;
258 case BVXOR_TOK: return 16;
259 case BVAND_TOK: return 17;
261 case CONCAT_TOK: return 19;
262 //case UMINUS_TOK: return 20;
263 case WITH_TOK: return 21;
264 case EXP_TOK: return 22;
268 case MOD_TOK: return 23;
270 case MINUS_TOK: return 24;
274 case GT_TOK: return 25;
276 case DISEQUAL_TOK: return 26;
277 case NOT_TOK: return 27;
278 case AND_TOK: return 28;
280 case XOR_TOK: return 29;
281 case IMPLIES_TOK: return 30;// right-to-left
282 case IFF_TOK: return 31;
284 case EXISTS_TOK: return 32;
286 case IN_TOK: return 33;
289 std::stringstream ss;
290 ss << "internal error: no entry in precedence table for operator " << CvcParserTokenNames[type];
291 throw ParserException(ss.str());
293 }/* getOperatorPrecedence() */
295 Kind getOperatorKind(int type, bool& negate) {
300 case IFF_TOK: return kind::IFF;
301 case IMPLIES_TOK: return kind::IMPLIES;
302 case OR_TOK: return kind::OR;
303 case XOR_TOK: return kind::XOR;
304 case AND_TOK: return kind::AND;
307 case EQUAL_TOK: return kind::EQUAL;
308 case DISEQUAL_TOK: negate = true; return kind::EQUAL;
309 case GT_TOK: return kind::GT;
310 case GEQ_TOK: return kind::GEQ;
311 case LT_TOK: return kind::LT;
312 case LEQ_TOK: return kind::LEQ;
315 case PLUS_TOK: return kind::PLUS;
316 case MINUS_TOK: return kind::MINUS;
317 case STAR_TOK: return kind::MULT;
318 case INTDIV_TOK: return kind::INTS_DIVISION;
319 case MOD_TOK: return kind::INTS_MODULUS;
320 case DIV_TOK: return kind::DIVISION;
321 case EXP_TOK: return kind::POW;
324 case CONCAT_TOK: return kind::BITVECTOR_CONCAT;
325 case BAR: return kind::BITVECTOR_OR;
326 case BVAND_TOK: return kind::BITVECTOR_AND;
329 std::stringstream ss;
330 ss << "internal error: no entry in operator-kind table for operator " << CvcParserTokenNames[type];
331 throw ParserException(ss.str());
333 }/* getOperatorKind() */
335 unsigned findPivot(const std::vector<unsigned>& operators,
336 unsigned startIndex, unsigned stopIndex) {
337 unsigned pivot = startIndex;
338 unsigned pivotRank = getOperatorPrecedence(operators[pivot]);
339 /*Debug("prec") << "initial pivot at " << pivot
340 << "(" << CvcParserTokenNames[operators[pivot]] << ") "
341 << "level " << pivotRank << std::endl;*/
342 for(unsigned i = startIndex + 1; i <= stopIndex; ++i) {
343 unsigned current = getOperatorPrecedence(operators[i]);
344 bool rtl = isRightToLeft(operators[i]);
345 if(current > pivotRank || (current == pivotRank && !rtl)) {
346 /*Debug("prec") << "new pivot at " << i
347 << "(" << CvcParserTokenNames[operators[i]] << ") "
348 << "level " << current << " rtl == " << rtl << std::endl;*/
356 Expr createPrecedenceTree(Parser* parser, ExprManager* em,
357 const std::vector<CVC4::Expr>& expressions,
358 const std::vector<unsigned>& operators,
359 unsigned startIndex, unsigned stopIndex) {
360 assert(expressions.size() == operators.size() + 1);
361 assert(startIndex < expressions.size());
362 assert(stopIndex < expressions.size());
363 assert(startIndex <= stopIndex);
365 if(stopIndex == startIndex) {
366 return expressions[startIndex];
369 unsigned pivot = findPivot(operators, startIndex, stopIndex - 1);
370 //Debug("prec") << "pivot[" << startIndex << "," << stopIndex - 1 << "] at " << pivot << std::endl;
372 Kind k = getOperatorKind(operators[pivot], negate);
373 Expr lhs = createPrecedenceTree(parser, em, expressions, operators, startIndex, pivot);
374 Expr rhs = createPrecedenceTree(parser, em, expressions, operators, pivot + 1, stopIndex);
375 if(k == kind::EQUAL && lhs.getType().isBoolean()) {
376 if(parser->strictModeEnabled()) {
377 WarningOnce() << "Warning: in strict parsing mode, will not convert BOOL = BOOL to BOOL <=> BOOL" << std::endl;
382 Expr e = em->mkExpr(k, lhs, rhs);
383 return negate ? em->mkExpr(kind::NOT, e) : e;
384 }/* createPrecedenceTree() recursive variant */
386 Expr createPrecedenceTree(Parser* parser, ExprManager* em,
387 const std::vector<CVC4::Expr>& expressions,
388 const std::vector<unsigned>& operators) {
389 if(Debug.isOn("prec") && operators.size() > 1) {
390 for(unsigned i = 0; i < expressions.size(); ++i) {
391 Debug("prec") << expressions[i];
392 if(operators.size() > i) {
393 Debug("prec") << ' ' << CvcParserTokenNames[operators[i]] << ' ';
396 Debug("prec") << std::endl;
399 Expr e = createPrecedenceTree(parser, em, expressions, operators, 0, expressions.size() - 1);
400 if(Debug.isOn("prec") && operators.size() > 1) {
401 Expr::setlanguage::Scope ls(Debug("prec"), language::output::LANG_AST);
402 Debug("prec") << "=> " << e << std::endl;
405 }/* createPrecedenceTree() base variant */
407 /** Add n NOTs to the front of e and return the result. */
408 Expr addNots(ExprManager* em, size_t n, Expr e) {
410 e = em->mkExpr(kind::NOT, e);
415 }/* @parser::members */
419 ** This file is part of CVC4.
420 ** Copyright (c) 2009-2013 New York University and The University of Iowa
421 ** See the file COPYING in the top-level source directory for licensing
428 /** This suppresses warnings about the redefinition of token symbols between different
429 * parsers. The redefinitions should be harmless as long as no client: (a) #include's
430 * the lexer headers for two grammars AND (b) uses the token symbol definitions. */
431 #pragma GCC system_header
433 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
434 /* This improves performance by ~10 percent on big inputs.
435 * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
436 * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
437 * Otherwise, we have to let the lexer detect the encoding at runtime.
439 # define ANTLR3_INLINE_INPUT_ASCII
440 # define ANTLR3_INLINE_INPUT_8BIT
441 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
443 #include "parser/antlr_tracing.h"
444 #include "util/integer.h"
445 #include "parser/antlr_input.h"
446 #include "parser/parser.h"
448 }/* @lexer::includes */
454 #include "expr/command.h"
455 #include "parser/parser.h"
456 #include "util/subrange_bound.h"
457 #include "parser/antlr_tracing.h"
465 * This class is just here to get around an unfortunate bit of Antlr.
466 * We use strings below as return values from rules, which require
467 * them to be constructible by a void*. So we derive the string
468 * class to provide just such a conversion.
470 class myString : public std::string {
472 myString(const std::string& s) : std::string(s) {}
473 myString(void*) : std::string() {}
474 myString() : std::string() {}
475 };/* class myString */
478 * Just exists to give us the void* construction that
481 class mySubrangeBound : public CVC4::SubrangeBound {
483 mySubrangeBound() : CVC4::SubrangeBound() {}
484 mySubrangeBound(void*) : CVC4::SubrangeBound() {}
485 mySubrangeBound(const Integer& i) : CVC4::SubrangeBound(i) {}
486 mySubrangeBound(const SubrangeBound& b) : CVC4::SubrangeBound(b) {}
487 };/* class mySubrangeBound */
490 * Just exists to give us the void* construction that
493 struct myExpr : public CVC4::Expr {
494 myExpr() : CVC4::Expr() {}
495 myExpr(void*) : CVC4::Expr() {}
496 myExpr(const Expr& e) : CVC4::Expr(e) {}
497 myExpr(const myExpr& e) : CVC4::Expr(e) {}
498 };/* struct myExpr */
500 }/* CVC4::parser::cvc namespace */
501 }/* CVC4::parser namespace */
502 }/* CVC4 namespace */
504 }/* @parser::includes */
506 @parser::postinclude {
508 #include "expr/expr.h"
509 #include "expr/kind.h"
510 #include "expr/type.h"
511 #include "parser/antlr_input.h"
512 #include "parser/parser.h"
513 #include "util/output.h"
519 #define REPEAT_COMMAND(k, CommandCtor) \
521 unsigned __k = (k); \
523 ? (Command*) new CommandCtor \
525 CommandSequence* __seq = new CommandSequence(); \
527 __seq->addCommand(new CommandCtor); \
533 using namespace CVC4;
534 using namespace CVC4::parser;
536 /* These need to be macros so they can refer to the PARSER macro, which will be defined
537 * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
539 #define PARSER_STATE ((Parser*)PARSER->super)
541 #define EXPR_MANAGER PARSER_STATE->getExprManager()
543 #define MK_EXPR EXPR_MANAGER->mkExpr
545 #define MK_CONST EXPR_MANAGER->mkConst
546 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
548 #define ENSURE_BV_SIZE(k, f) \
550 unsigned size = BitVectorType(f.getType()).getSize(); \
552 f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k - size)), f); \
553 } else if (k < size) { \
554 f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f); \
558 }/* @parser::postinclude */
561 * Parses an expression.
562 * @return the parsed expression
564 parseExpr returns [CVC4::Expr expr = CVC4::Expr()]
570 * Parses a command (the whole benchmark)
571 * @return the command of the benchmark
573 parseCommand returns [CVC4::Command* cmd = NULL]
574 : c=command { $cmd = c; }
576 { std::string s = AntlrInput::tokenText($IDENTIFIER);
577 if(s == "benchmark") {
578 PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv1 format detected. Use --lang smt1 for SMT-LIBv1 support.");
579 } else if(s == "set" || s == "get" || s == "declare" ||
580 s == "define" || s == "assert") {
581 PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIB format detected. Use --lang smt for SMT-LIB support.");
583 PARSER_STATE->parseError("A CVC4 presentation language command cannot begin with a parenthesis; expected command name.");
586 | EOF { $cmd = NULL; }
590 * Matches a command of the input. If a declaration, it will return an empty
593 command returns [CVC4::Command* cmd = NULL]
594 : ( mainCommand[cmd] SEMICOLON
596 | LET_TOK { PARSER_STATE->pushScope(); }
597 typeOrVarLetDecl[CHECK_DECLARED] ( COMMA typeOrVarLetDecl[CHECK_DECLARED] )*
600 PARSER_STATE->popScope();
604 cmd = new EmptyCommand();
609 typeOrVarLetDecl[CVC4::parser::DeclarationCheck check]
610 options { backtrack = true; }
611 : letDecl | typeLetDecl[check]
614 mainCommand[CVC4::Command*& cmd]
620 std::vector<CVC4::Datatype> dts;
621 Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl;
624 /* our bread & butter */
625 : ASSERT_TOK formula[f] { cmd = new AssertCommand(f); }
627 | QUERY_TOK formula[f] { cmd = new QueryCommand(f); }
628 | CHECKSAT_TOK formula[f]? { cmd = f.isNull() ? new CheckSatCommand() : new CheckSatCommand(f); }
632 ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
633 ( symbolicExpr[sexpr]
635 cmd = new SetBenchmarkLogicCommand(sexpr.getValue());
637 cmd = new SetOptionCommand(s, sexpr);
640 | TRUE_TOK { cmd = new SetOptionCommand(s, SExpr("true")); }
641 | FALSE_TOK { cmd = new SetOptionCommand(s, SExpr("false")); }
642 | { cmd = new SetOptionCommand(s, SExpr("true")); }
646 | PUSH_TOK ( k=numeral { cmd = REPEAT_COMMAND(k, PushCommand()); }
647 | { cmd = new PushCommand(); } )
648 | POP_TOK ( k=numeral { cmd = REPEAT_COMMAND(k, PopCommand()); }
649 | { cmd = new PopCommand(); } )
650 | POPTO_TOK k=numeral?
651 { UNSUPPORTED("POPTO command"); }
653 /* push / pop scopes */
654 | PUSH_SCOPE_TOK k=numeral?
655 { UNSUPPORTED("PUSH_SCOPE command"); }
656 | POP_SCOPE_TOK k=numeral?
657 { UNSUPPORTED("POP_SCOPE command"); }
658 | POPTO_SCOPE_TOK k=numeral?
659 { UNSUPPORTED("POPTO_SCOPE command"); }
662 { UNSUPPORTED("RESET command"); }
664 // Datatypes can be mututally-recursive if they're in the same
665 // definition block, separated by a comma. So we parse everything
666 // and then ask the ExprManager to resolve everything in one go.
668 { /* open a scope to keep the UnresolvedTypes contained */
669 PARSER_STATE->pushScope(); }
671 ( COMMA datatypeDef[dts] )*
673 { PARSER_STATE->popScope();
674 cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
677 ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
678 { UNSUPPORTED("CONTEXT command"); }
679 | { UNSUPPORTED("CONTEXT command"); }
682 | FORGET_TOK identifier[id,CHECK_NONE,SYM_VARIABLE]
683 { UNSUPPORTED("FORGET command"); }
685 | GET_TYPE_TOK formula[f]
686 { UNSUPPORTED("GET_TYPE command"); }
688 | CHECK_TYPE_TOK formula[f] COLON type[t,CHECK_DECLARED]
689 { UNSUPPORTED("CHECK_TYPE command"); }
691 | GET_CHILD_TOK formula[f] k=numeral
692 { UNSUPPORTED("GET_CHILD command"); }
694 | GET_OP_TOK formula[f]
695 { UNSUPPORTED("GET_OP command"); }
697 | GET_VALUE_TOK formula[f]
698 { cmd = new GetValueCommand(f); }
700 | SUBSTITUTE_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED] EQUAL_TOK
701 formula[f] LBRACKET identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[f] RBRACKET
702 { UNSUPPORTED("SUBSTITUTE command"); }
704 /* Like the --debug command line option, DBG turns on both tracing
707 ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
708 { Debug.on(s); Trace.on(s); }
709 | { Message() << "Please specify what to debug." << std::endl; }
713 ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
715 | { Message() << "Please specify something to trace." << std::endl; }
718 ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
720 | { Message() << "Please specify something to untrace." << std::endl; }
724 ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
725 { Message() << "No help available for `" << s << "'." << std::endl; }
726 | { Message() << "Please use --help at the command line for help." << std::endl; }
729 | TRANSFORM_TOK formula[f]
730 { cmd = new SimplifyCommand(f); }
732 | PRINT_TOK formula[f]
733 { UNSUPPORTED("PRINT command"); }
734 | PRINT_TYPE_TOK type[t,CHECK_DECLARED]
735 { UNSUPPORTED("PRINT_TYPE command"); }
737 | CALL_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] formula[f]
738 { UNSUPPORTED("CALL command"); }
741 ( simpleSymbolicExpr[sexpr]
742 { cmd = new EchoCommand(sexpr.getValue()); }
743 | { cmd = new EchoCommand(); }
747 { cmd = new QuitCommand(); }
750 ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
751 { UNSUPPORTED("INCLUDE command"); }
752 | { PARSER_STATE->parseError("No filename given to INCLUDE command"); }
756 { cmd = new GetProofCommand(); }
758 | ( DUMP_ASSUMPTIONS_TOK
761 | DUMP_TCC_ASSUMPTIONS_TOK
764 | DUMP_CLOSURE_PROOF_TOK
765 ) { UNSUPPORTED("DUMP* command"); }
767 /* these are all synonyms */
768 | ( WHERE_TOK | ASSERTIONS_TOK | ASSUMPTIONS_TOK )
769 { cmd = new GetAssertionsCommand(); }
772 { cmd = new GetModelCommand; }
774 { cmd = new GetModelCommand; }
776 | ARITH_VAR_ORDER_TOK LPAREN formula[f] ( COMMA formula[f] )* RPAREN
777 { UNSUPPORTED("ARITH_VAR_ORDER command"); }
779 | toplevelDeclaration[cmd]
782 simpleSymbolicExpr[CVC4::SExpr& sexpr]
788 { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
789 | MINUS_TOK INTEGER_LITERAL
790 { sexpr = SExpr(-Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
792 { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
794 { sexpr = SExpr(AntlrInput::tokenText($HEX_LITERAL)); }
796 { sexpr = SExpr(AntlrInput::tokenText($BINARY_LITERAL)); }
798 { sexpr = SExpr(s); }
800 { sexpr = SExpr(AntlrInput::tokenText($IDENTIFIER)); }
803 symbolicExpr[CVC4::SExpr& sexpr]
805 std::vector<SExpr> children;
807 : simpleSymbolicExpr[sexpr]
808 | LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN
809 { sexpr = SExpr(children); }
813 * Match a top-level declaration.
815 toplevelDeclaration[CVC4::Command*& cmd]
817 std::vector<std::string> ids;
819 Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl;
821 : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON
822 ( declareVariables[cmd,t,ids,true]
823 | declareTypes[cmd,ids] )
827 * A bound variable declaration.
829 boundVarDecl[std::vector<std::string>& ids, CVC4::Type& t]
830 : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[*(Command**)NULL,t,ids,false]
834 * A series of bound variable declarations.
838 std::vector<std::string> ids;
841 : boundVarDecl[ids,t] ( COMMA boundVarDecl[ids,t] )*
844 boundVarDeclsReturn[std::vector<CVC4::Expr>& terms,
845 std::vector<CVC4::Type>& types]
847 std::vector<std::string> ids;
852 : boundVarDeclReturn[terms,types] ( COMMA boundVarDeclReturn[terms,types] )*
855 boundVarDeclReturn[std::vector<CVC4::Expr>& terms,
856 std::vector<CVC4::Type>& types]
858 std::vector<std::string> ids;
860 // NOTE: do not clear the vectors here!
862 : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED]
863 { const std::vector<Expr>& vars = PARSER_STATE->mkBoundVars(ids, t);
864 terms.insert(terms.end(), vars.begin(), vars.end());
865 for(unsigned i = 0; i < vars.size(); ++i) {
872 * Match the right-hand-side of a type declaration. Unlike
873 * declareVariables[] below, don't need to return the Type, since it's
874 * always the KindType (the type of types). Also don't need toplevel
875 * because type declarations are always top-level, except for
876 * type-lets, which don't use this rule.
878 declareTypes[CVC4::Command*& cmd, const std::vector<std::string>& idList]
882 /* A sort declaration (e.g., "T : TYPE") */
884 { DeclarationSequence* seq = new DeclarationSequence();
885 for(std::vector<std::string>::const_iterator i = idList.begin();
888 // Don't allow a type variable to clash with a previously
889 // declared type variable, however a type variable and a
890 // non-type variable can clash unambiguously. Break from CVC3
892 PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT);
893 Type sort = PARSER_STATE->mkSort(*i);
894 Command* decl = new DeclareTypeCommand(*i, 0, sort);
895 seq->addCommand(decl);
900 /* A type alias "T : TYPE = foo..." */
901 | TYPE_TOK EQUAL_TOK type[t,CHECK_DECLARED]
902 { for(std::vector<std::string>::const_iterator i = idList.begin();
905 PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT);
906 PARSER_STATE->defineType(*i, t);
912 * Match the right-hand side of a variable declaration. Returns the
913 * type. Some IDs might have been declared previously, and are not
914 * re-declared if topLevel is true (CVC allows re-declaration if the
915 * types are compatible---if they aren't compatible, an error is
916 * thrown). Also if topLevel is true, variable definitions are
917 * permitted and "cmd" is output. If topLevel is false, bound vars
920 declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::string>& idList, bool topLevel]
923 Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
925 /* A variable declaration (or definition) */
926 : type[t,CHECK_DECLARED] ( EQUAL_TOK formula[f] )?
927 { DeclarationSequence* seq = NULL;
929 cmd = seq = new DeclarationSequence();
932 Debug("parser") << "working on " << idList.front() << " : " << t << std::endl;
933 // CVC language allows redeclaration of variables if types are the same
934 for(std::vector<std::string>::const_iterator i = idList.begin(),
935 i_end = idList.end();
938 if(PARSER_STATE->isDeclared(*i, SYM_VARIABLE)) {
939 Type oldType = PARSER_STATE->getType(*i);
940 Debug("parser") << " " << *i << " was declared previously "
941 << "with type " << oldType << std::endl;
943 std::stringstream ss;
944 ss << Expr::setlanguage(language::output::LANG_CVC4)
945 << "incompatible type for `" << *i << "':" << std::endl
946 << " old type: " << oldType << std::endl
947 << " new type: " << t << std::endl;
948 PARSER_STATE->parseError(ss.str());
950 Debug("parser") << " types " << t << " and " << oldType
951 << " are compatible" << std::endl;
954 Debug("parser") << " " << *i << " not declared" << std::endl;
956 Expr func = PARSER_STATE->mkVar(*i, t, ExprManager::VAR_FLAG_GLOBAL);
957 Command* decl = new DeclareFunctionCommand(*i, func, t);
958 seq->addCommand(decl);
960 PARSER_STATE->mkBoundVar(*i, t);
965 // f is not null-- meaning this is a definition not a declaration
967 // must be top-level; doesn't make sense to write something
968 // like e.g. FORALL(x:INT = 4): [...]
969 PARSER_STATE->parseError("cannot construct a definition here; maybe you want a LET");
971 assert(!idList.empty());
972 for(std::vector<std::string>::const_iterator i = idList.begin(),
973 i_end = idList.end();
976 Debug("parser") << "making " << *i << " : " << t << " = " << f << std::endl;
977 PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
978 Expr func = EXPR_MANAGER->mkVar(*i, t, ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
979 PARSER_STATE->defineFunction(*i, f);
980 Command* decl = new DefineFunctionCommand(*i, func, f);
981 seq->addCommand(decl);
988 * Matches a list of identifiers separated by a comma and puts them in the
990 * @param idList the list to fill with identifiers.
991 * @param check what kinds of check to perform on the symbols
993 identifierList[std::vector<std::string>& idList,
994 CVC4::parser::DeclarationCheck check,
995 CVC4::parser::SymbolType type]
1000 : identifier[id,check,type] { idList.push_back(id); }
1001 ( COMMA identifier[id,check,type] { idList.push_back(id); } )*
1005 * Matches an identifier and returns a string.
1007 identifier[std::string& id,
1008 CVC4::parser::DeclarationCheck check,
1009 CVC4::parser::SymbolType type]
1011 { id = AntlrInput::tokenText($IDENTIFIER);
1012 PARSER_STATE->checkDeclaration(id, check, type); }
1016 * Match the type in a declaration and do the declaration binding. If
1017 * "check" is CHECK_NONE, then identifiers occurring in the type need
1018 * not exist! They are created as "unresolved" types and linked up in
1019 * a type-substitution pass. Right now, only datatype definitions are
1020 * supported in this way (since type names can occur without any
1021 * forward-declaration in CVC language datatype definitions, we have
1022 * to create types for them on-the-fly). Before passing CHECK_NONE
1023 * you really should have a clear idea of WHY you need to parse that
1024 * way; then you should trace through Parser::mkMutualDatatypeType()
1025 * to figure out just what you're in for.
1028 CVC4::parser::DeclarationCheck check]
1032 std::vector<Type> args;
1034 /* a type, possibly a function */
1035 : restrictedTypePossiblyFunctionLHS[t,check,lhs]
1037 assert(t.isTuple());
1038 args = TupleType(t).getTypes();
1043 ( ARROW_TOK type[t2,check] { args.push_back(t2); } )?
1046 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?");
1049 t = EXPR_MANAGER->mkFunctionType(args);
1053 /* type-lets: typeLetDecl defines the types, we just manage the
1054 * scopes here. NOTE that LET in the CVC language is always
1056 | LET_TOK { PARSER_STATE->pushScope(); }
1057 typeLetDecl[check] ( COMMA typeLetDecl[check] )* IN_TOK type[t,check]
1058 { PARSER_STATE->popScope(); }
1061 // A restrictedType is one that is not a "bare" function type (it can
1062 // be enclosed in parentheses) and is not a type list. To support the
1065 // f : (nat, nat) -> nat;
1067 // we have to permit restrictedTypes to be type lists (as on the LHS
1068 // there). The "type" rule above uses restictedTypePossiblyFunctionLHS
1069 // directly in order to implement that; this rule allows a type list to
1070 // parse but then issues an error.
1071 restrictedType[CVC4::Type& t,
1072 CVC4::parser::DeclarationCheck check]
1076 : restrictedTypePossiblyFunctionLHS[t,check,lhs]
1077 { if(lhs) { PARSER_STATE->parseError("improperly-placed type list; maybe these parentheses were meant to be square brackets, to define a tuple type?"); } }
1081 * lhs is set to "true" on output if we have a list of types, so an
1082 * ARROW must follow. An ARROW can always follow; lhs means it MUST.
1084 restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
1085 CVC4::parser::DeclarationCheck check,
1091 std::vector<Type> types;
1092 std::vector< std::pair<std::string, Type> > typeIds;
1093 //SymbolTable* symtab;
1098 : identifier[id,check,SYM_SORT]
1099 parameterization[check,types]?
1101 if(check == CHECK_DECLARED ||
1102 PARSER_STATE->isDeclared(id, SYM_SORT)) {
1103 Debug("parser-param") << "param: getSort " << id << " " << types.size() << " " << PARSER_STATE->getArity( id )
1104 << " " << PARSER_STATE->isDeclared(id, SYM_SORT) << std::endl;
1105 if(types.size() != PARSER_STATE->getArity(id)) {
1106 std::stringstream ss;
1107 ss << "incorrect arity for symbol `" << id << "': expected "
1108 << PARSER_STATE->getArity( id ) << " type arguments, got "
1110 PARSER_STATE->parseError(ss.str());
1112 if(types.size() > 0) {
1113 t = PARSER_STATE->getSort(id, types);
1115 t = PARSER_STATE->getSort(id);
1119 t = PARSER_STATE->mkUnresolvedType(id);
1120 Debug("parser-param") << "param: make unres type " << id << std::endl;
1122 t = PARSER_STATE->mkUnresolvedTypeConstructor(id,types);
1123 t = SortConstructorType(t).instantiate( types );
1124 Debug("parser-param") << "param: make unres param type " << id << " " << types.size() << " "
1125 << PARSER_STATE->getArity( id ) << std::endl;
1131 | ARRAY_TOK restrictedType[t,check] OF_TOK restrictedType[t2,check]
1132 { t = EXPR_MANAGER->mkArrayType(t, t2); }
1135 | SUBTYPE_TOK LPAREN
1136 /* A bit tricky: this LAMBDA expression cannot refer to constants
1137 * declared in the outer context. What follows isn't quite right,
1138 * though, since type aliases and function definitions should be
1139 * retained in the set of current declarations. */
1140 { /*symtab = PARSER_STATE->getSymbolTable();
1141 PARSER_STATE->useDeclarationsFrom(new SymbolTable());*/ }
1142 formula[f] ( COMMA formula[f2] )? RPAREN
1143 { /*SymbolTable* old = PARSER_STATE->getSymbolTable();
1144 PARSER_STATE->useDeclarationsFrom(symtab);
1146 PARSER_STATE->unimplementedFeature("predicate subtyping not supported in this release");
1148 EXPR_MANAGER->mkPredicateSubtype(f) :
1149 EXPR_MANAGER->mkPredicateSubtype(f, f2);
1153 /* subrange types */
1154 | LBRACKET k1=bound DOTDOT k2=bound RBRACKET
1155 { if(k1.hasBound() && k2.hasBound() &&
1156 k1.getBound() > k2.getBound()) {
1157 std::stringstream ss;
1158 ss << "Subrange [" << k1.getBound() << ".." << k2.getBound()
1159 << "] inappropriate: range must be nonempty!";
1160 PARSER_STATE->parseError(ss.str());
1162 t = EXPR_MANAGER->mkSubrangeType(SubrangeBounds(k1, k2));
1165 /* tuple types / old-style function types */
1166 | LBRACKET ( type[t,check] { types.push_back(t); }
1167 ( COMMA type[t,check] { types.push_back(t); } )* )? RBRACKET
1168 { if(types.size() == 1 && types.front().isFunction()) {
1169 // old style function syntax [ T -> U ]
1170 PARSER_STATE->parseError("old-style function type syntax not supported anymore; please use the new syntax");
1172 // tuple type [ T, U, V... ]
1173 t = EXPR_MANAGER->mkTupleType(types);
1178 | SQHASH ( identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); }
1179 ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } )* )? HASHSQ
1180 { t = EXPR_MANAGER->mkRecordType(typeIds); }
1182 /* bitvector types */
1183 | BITVECTOR_TOK LPAREN k=numeral RPAREN
1185 PARSER_STATE->parseError("Illegal bitvector size: 0");
1187 t = EXPR_MANAGER->mkBitVectorType(k);
1191 | BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); }
1192 | REAL_TOK { t = EXPR_MANAGER->realType(); }
1193 | INT_TOK { t = EXPR_MANAGER->integerType(); }
1195 /* Parenthesized general type, or the lhs of an ARROW (a list of
1196 * types). These two things are combined to avoid conflicts in
1198 | LPAREN type[t,check] { types.push_back(t); }
1199 ( COMMA type[t,check] { lhs = true; types.push_back(t); } )* RPAREN
1200 { if(lhs) { t = EXPR_MANAGER->mkTupleType(types); }
1201 // if !lhs, t is already set up correctly, nothing to do..
1205 parameterization[CVC4::parser::DeclarationCheck check,
1206 std::vector<CVC4::Type>& params]
1210 : LBRACKET restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); }
1211 ( COMMA restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); } )* RBRACKET
1214 bound returns [CVC4::parser::cvc::mySubrangeBound bound]
1215 : UNDERSCORE { $bound = SubrangeBound(); }
1216 | k=integer { $bound = SubrangeBound(k.getNumerator()); }
1219 typeLetDecl[CVC4::parser::DeclarationCheck check]
1224 : identifier[id,CHECK_NONE,SYM_SORT] (COLON TYPE_TOK)? EQUAL_TOK restrictedType[t,check]
1225 { PARSER_STATE->defineType(id, t); }
1229 * Matches a CVC4 expression. Formulas and terms are not really
1230 * distinguished during parsing; please ignore the naming of the
1233 * @return the expression representing the formula/term
1235 formula[CVC4::Expr& f]
1237 Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
1239 std::vector<CVC4::Expr> expressions;
1240 std::vector<unsigned> operators;
1245 { f = addNots(EXPR_MANAGER, n, f); }
1247 { f = addNots(EXPR_MANAGER, n, f);
1248 expressions.push_back(f);
1250 morecomparisons[expressions,operators]?
1251 { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
1255 morecomparisons[std::vector<CVC4::Expr>& expressions,
1256 std::vector<unsigned>& operators] returns [size_t i = 0]
1260 $i = expressions.size();
1262 : booleanBinop[op] { operators.push_back(op); }
1265 { expressions.push_back(addNots(EXPR_MANAGER, n, f)); }
1267 { f = addNots(EXPR_MANAGER, n, f);
1268 expressions.push_back(f);
1270 morecomparisons[expressions,operators]?
1274 /** Matches 0 or more NOTs. */
1275 nots returns [size_t n = 0]
1276 : ( NOT_TOK { ++$n; } )*
1279 prefixFormula[CVC4::Expr& f]
1281 std::vector<std::string> ids;
1282 std::vector<Expr> terms;
1283 std::vector<Type> types;
1284 std::vector<Expr> bvs;
1290 : ( FORALL_TOK { k = kind::FORALL; } | EXISTS_TOK { k = kind::EXISTS; } )
1291 { PARSER_STATE->pushScope(); } LPAREN
1293 { for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) {
1294 bvs.push_back(PARSER_STATE->mkBoundVar(*i, t));
1298 ( COMMA boundVarDecl[ids,t]
1300 for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) {
1301 bvs.push_back(PARSER_STATE->mkBoundVar(*i, t));
1306 terms.push_back( EXPR_MANAGER->mkExpr( kind::BOUND_VAR_LIST, bvs ) ); }
1307 COLON instantiationPatterns[ipl]? formula[f]
1308 { PARSER_STATE->popScope();
1310 if(! ipl.isNull()) {
1311 terms.push_back(ipl);
1313 f = MK_EXPR(k, terms);
1316 /* lets: letDecl defines the variables and functionss, we just
1317 * manage the scopes here. NOTE that LET in the CVC language is
1318 * always sequential! */
1319 | LET_TOK { PARSER_STATE->pushScope(); }
1320 letDecl ( COMMA letDecl )*
1321 IN_TOK formula[f] { PARSER_STATE->popScope(); }
1324 | LAMBDA { PARSER_STATE->pushScope(); } LPAREN
1325 boundVarDeclsReturn[terms,types]
1326 RPAREN COLON formula[f]
1327 { PARSER_STATE->popScope();
1328 Type t = EXPR_MANAGER->mkFunctionType(types, f.getType());
1329 std::string name = "lambda";
1330 Expr func = PARSER_STATE->mkAnonymousFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
1331 Command* cmd = new DefineFunctionCommand(name, func, terms, f);
1332 PARSER_STATE->preemptCommand(cmd);
1336 /* array literals */
1337 | ARRAY_TOK { PARSER_STATE->pushScope(); } LPAREN
1338 boundVarDecl[ids,t] RPAREN COLON formula[f]
1339 { PARSER_STATE->popScope();
1340 UNSUPPORTED("array literals not supported yet");
1341 f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType()), ExprManager::VAR_FLAG_GLOBAL);
1345 instantiationPatterns[ CVC4::Expr& expr ]
1347 std::vector<Expr> args;
1349 std::vector<Expr> patterns;
1351 : ( PATTERN_TOK LPAREN formula[f] { args.push_back( f ); } (COMMA formula[f] { args.push_back( f ); } )* RPAREN COLON
1352 { patterns.push_back( EXPR_MANAGER->mkExpr( kind::INST_PATTERN, args ) );
1355 { if(! patterns.empty()) {
1356 expr = EXPR_MANAGER->mkExpr( kind::INST_PATTERN_LIST, patterns );
1362 * Matches (and defines) a single LET declaration.
1369 : identifier[name,CHECK_NONE,SYM_VARIABLE] EQUAL_TOK formula[e]
1370 { Debug("parser") << Expr::setlanguage(language::output::LANG_CVC4) << e.getType() << std::endl;
1371 PARSER_STATE->defineVar(name, e);
1372 Debug("parser") << "LET[" << PARSER_STATE->scopeLevel() << "]: "
1373 << name << std::endl
1374 << " ==>" << " " << e << std::endl;
1378 booleanBinop[unsigned& op]
1380 op = LT(1)->getType(LT(1));
1389 comparison[CVC4::Expr& f]
1391 std::vector<CVC4::Expr> expressions;
1392 std::vector<unsigned> operators;
1395 : term[f] { expressions.push_back(f); }
1396 ( comparisonBinop[op] term[f]
1397 { operators.push_back(op); expressions.push_back(f); } )*
1398 { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
1401 comparisonBinop[unsigned& op]
1403 op = LT(1)->getType(LT(1));
1415 std::vector<CVC4::Expr> expressions;
1416 std::vector<unsigned> operators;
1420 : storeTerm[f] { expressions.push_back(f); }
1421 ( arithmeticBinop[op] storeTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
1422 { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
1425 arithmeticBinop[unsigned& op]
1427 op = LT(1)->getType(LT(1));
1438 /** Parses an array/tuple/record assignment term. */
1439 storeTerm[CVC4::Expr& f]
1442 ( arrayStore[f] ( COMMA arrayStore[f] )*
1443 | DOT ( tupleStore[f] ( COMMA DOT tupleStore[f] )*
1444 | recordStore[f] ( COMMA DOT recordStore[f] )* ) )
1450 * Parses just part of the array assignment (and constructs
1453 arrayStore[CVC4::Expr& f]
1456 std::vector<Expr> dims;
1458 : ( LBRACKET formula[f2] { dims.push_back(f2); } RBRACKET )+
1459 ASSIGN_TOK uminusTerm[f3]
1460 { assert(dims.size() >= 1);
1461 // these loops are a bit complicated; they're only used for the
1462 // multidimensional ...WITH [a][b] :=... syntax
1463 for(unsigned i = 0; i < dims.size() - 1; ++i) {
1464 f = MK_EXPR(CVC4::kind::SELECT, f, dims[i]);
1466 // a[i][j][k] := v turns into
1467 // store(a, i, store(a[i], j, store(a[i][j], k, v)))
1468 for(unsigned i = dims.size() - 1; i > 0; --i) {
1469 f3 = MK_EXPR(CVC4::kind::STORE, f, dims[i], f3);
1470 // strip off one layer of the select
1474 // outermost wrapping
1475 f = MK_EXPR(CVC4::kind::STORE, f, dims[0], f3);
1480 * Parses just part of the tuple assignment (and constructs
1483 tupleStore[CVC4::Expr& f]
1487 : k=numeral ASSIGN_TOK uminusTerm[f2]
1489 Type t = f.getType();
1491 PARSER_STATE->parseError("tuple-update applied to non-tuple");
1493 size_t length = TupleType(t).getLength();
1495 std::stringstream ss;
1496 ss << "tuple is of length " << length << "; cannot update index " << k;
1497 PARSER_STATE->parseError(ss.str());
1499 f = MK_EXPR(MK_CONST(TupleUpdate(k)), f, f2);
1504 * Parses just part of the record assignment (and constructs
1507 recordStore[CVC4::Expr& f]
1512 : identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK uminusTerm[f2]
1514 Type t = f.getType();
1515 if(! t.isRecord()) {
1516 PARSER_STATE->parseError("record-update applied to non-record");
1518 const Record& rec = RecordType(t).getRecord();
1519 Record::const_iterator fld = rec.find(id);
1520 if(fld == rec.end()) {
1521 PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
1523 f = MK_EXPR(MK_CONST(RecordUpdate(id)), f, f2);
1527 /** Parses a unary minus term. */
1528 uminusTerm[CVC4::Expr& f]
1530 unsigned minusCount = 0;
1533 : (MINUS_TOK { ++minusCount; })+ bvBinaryOpTerm[f]
1534 { while(minusCount > 0) { --minusCount; f = MK_EXPR(CVC4::kind::UMINUS, f); } }
1538 /** Parses bitvectors. Starts with binary operators @, &, and |. */
1539 bvBinaryOpTerm[CVC4::Expr& f]
1541 std::vector<CVC4::Expr> expressions;
1542 std::vector<unsigned> operators;
1545 : bvNegTerm[f] { expressions.push_back(f); }
1546 ( bvBinop[op] bvNegTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
1547 { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
1549 bvBinop[unsigned& op]
1551 op = LT(1)->getType(LT(1));
1558 bvNegTerm[CVC4::Expr& f]
1560 : BVNEG_TOK bvNegTerm[f]
1561 { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
1566 * Parses an array select / bitvector extract / bitvector shift /
1567 * function or constructor application. These are all parsed the same
1568 * way because they are all effectively post-fix operators and can
1569 * continue piling onto an expression. Array selects and bitvector
1570 * extracts even share similar syntax with their use of [ square
1571 * brackets ], so we left-factor as much out as possible to make ANTLR
1574 postfixTerm[CVC4::Expr& f]
1577 bool extract = false, left = false;
1578 std::vector<Expr> args;
1583 ( /* array select / bitvector extract */
1585 ( formula[f2] { extract = false; }
1586 | k1=numeral COLON k2=numeral { extract = true; } )
1589 /* bitvector extract */
1590 f = MK_EXPR(MK_CONST(BitVectorExtract(k1, k2)), f);
1593 f = MK_EXPR(CVC4::kind::SELECT, f, f2);
1597 /* left- or right-shift */
1598 | ( LEFTSHIFT_TOK { left = true; }
1599 | RIGHTSHIFT_TOK { left = false; } ) k=numeral
1601 // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit
1603 f = MK_EXPR(kind::BITVECTOR_CONCAT, f, MK_CONST(BitVector(k)));
1605 unsigned n = BitVectorType(f.getType()).getSize();
1606 f = MK_EXPR(kind::BITVECTOR_CONCAT, MK_CONST(BitVector(k)),
1607 MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f));
1611 /* function/constructor application */
1612 | LPAREN { args.push_back(f); }
1613 formula[f] { args.push_back(f); }
1614 ( COMMA formula[f] { args.push_back(f); } )* RPAREN
1615 // TODO: check arity
1616 { Type t = args.front().getType();
1617 Debug("parser") << "type is " << t << std::endl;
1618 Debug("parser") << "expr is " << args.front() << std::endl;
1619 if(PARSER_STATE->isDefinedFunction(args.front())) {
1620 f = MK_EXPR(CVC4::kind::APPLY, args);
1621 } else if(t.isFunction()) {
1622 f = MK_EXPR(CVC4::kind::APPLY_UF, args);
1623 } else if(t.isConstructor()) {
1624 f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
1625 } else if(t.isSelector()) {
1626 f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args);
1627 } else if(t.isTester()) {
1628 f = MK_EXPR(CVC4::kind::APPLY_TESTER, args);
1630 PARSER_STATE->parseError("internal error: unhandled function application kind");
1634 /* record / tuple select */
1636 ( identifier[id,CHECK_NONE,SYM_VARIABLE]
1637 { Type t = f.getType();
1638 if(! t.isRecord()) {
1639 PARSER_STATE->parseError("record-select applied to non-record");
1641 const Record& rec = RecordType(t).getRecord();
1642 Record::const_iterator fld = rec.find(id);
1643 if(fld == rec.end()) {
1644 PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
1646 f = MK_EXPR(MK_CONST(RecordSelect(id)), f);
1649 { Type t = f.getType();
1651 PARSER_STATE->parseError("tuple-select applied to non-tuple");
1653 size_t length = TupleType(t).getLength();
1655 std::stringstream ss;
1656 ss << "tuple is of length " << length << "; cannot access index " << k;
1657 PARSER_STATE->parseError(ss.str());
1659 f = MK_EXPR(MK_CONST(TupleSelect(k)), f);
1663 | FLOOR_TOK LPAREN formula[f] RPAREN
1664 { f = MK_EXPR(CVC4::kind::TO_INTEGER, f); }
1665 | DISTINCT_TOK LPAREN
1666 formula[f] { args.push_back(f); }
1667 ( COMMA formula[f] { args.push_back(f); } )* RPAREN
1668 { f = (args.size() == 1) ? MK_CONST(bool(true)) : MK_EXPR(CVC4::kind::DISTINCT, args); }
1670 ( typeAscription[f, t]
1671 { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) {
1672 std::vector<CVC4::Expr> v;
1673 Expr e = f.getOperator();
1674 const DatatypeConstructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)];
1675 v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
1676 MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator() ));
1677 v.insert(v.end(), f.begin(), f.end());
1678 f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
1680 if(f.getType() != t) {
1681 PARSER_STATE->parseError("Type ascription not satisfied.");
1688 bvTerm[CVC4::Expr& f]
1691 std::vector<Expr> args;
1694 : BVXOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1695 { f = MK_EXPR(CVC4::kind::BITVECTOR_XOR, f, f2); }
1696 | BVNAND_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1697 { f = MK_EXPR(CVC4::kind::BITVECTOR_NAND, f, f2); }
1698 | BVNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1699 { f = MK_EXPR(CVC4::kind::BITVECTOR_NOR, f, f2); }
1700 | BVCOMP_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1701 { f = MK_EXPR(CVC4::kind::BITVECTOR_COMP, f, f2); }
1702 | BVXNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1703 { f = MK_EXPR(CVC4::kind::BITVECTOR_XNOR, f, f2); }
1705 /* BV unary minus */
1706 | BVUMINUS_TOK LPAREN formula[f] RPAREN
1707 { f = MK_EXPR(CVC4::kind::BITVECTOR_NEG, f); }
1709 | BVPLUS_TOK LPAREN k=numeral COMMA formula[f] { args.push_back(f); }
1710 ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN
1713 PARSER_STATE->parseError("BVPLUS(k,_,_) must have k > 0");
1715 for (unsigned i = 0; i < args.size(); ++ i) {
1716 ENSURE_BV_SIZE(k, args[i]);
1718 f = MK_EXPR(CVC4::kind::BITVECTOR_PLUS, args);
1720 /* BV subtraction */
1721 | BVSUB_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN
1724 PARSER_STATE->parseError("BVSUB(k,_,_) must have k > 0");
1726 ENSURE_BV_SIZE(k, f);
1727 ENSURE_BV_SIZE(k, f2);
1728 f = MK_EXPR(CVC4::kind::BITVECTOR_SUB, f, f2);
1730 /* BV multiplication */
1731 | BVMULT_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN
1734 PARSER_STATE->parseError("BVMULT(k,_,_) must have k > 0");
1736 ENSURE_BV_SIZE(k, f);
1737 ENSURE_BV_SIZE(k, f2);
1738 f = MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2);
1740 /* BV unsigned division */
1741 | BVUDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1742 { f = MK_EXPR(CVC4::kind::BITVECTOR_UDIV, f, f2); }
1743 /* BV signed division */
1744 | BVSDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1745 { f = MK_EXPR(CVC4::kind::BITVECTOR_SDIV, f, f2); }
1746 /* BV unsigned remainder */
1747 | BVUREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1748 { f = MK_EXPR(CVC4::kind::BITVECTOR_UREM, f, f2); }
1749 /* BV signed remainder */
1750 | BVSREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1751 { f = MK_EXPR(CVC4::kind::BITVECTOR_SREM, f, f2); }
1752 /* BV signed modulo */
1753 | BVSMOD_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1754 { f = MK_EXPR(CVC4::kind::BITVECTOR_SMOD, f, f2); }
1756 | BVSHL_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1757 { f = MK_EXPR(CVC4::kind::BITVECTOR_SHL, f, f2); }
1758 /* BV arithmetic right shift */
1759 | BVASHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1760 { f = MK_EXPR(CVC4::kind::BITVECTOR_ASHR, f, f2); }
1761 /* BV logical left shift */
1762 | BVLSHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1763 { f = MK_EXPR(CVC4::kind::BITVECTOR_LSHR, f, f2); }
1764 /* BV sign extension */
1765 | SX_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1766 { unsigned n = BitVectorType(f.getType()).getSize();
1767 // Sign extension in TheoryBitVector is defined as in SMT-LIB
1768 // which is different than in the CVC language
1769 // SX(BITVECTOR(k), n) in CVC language extends to n bits
1770 // In SMT-LIB, such a thing expands to k + n bits
1771 f = MK_EXPR(MK_CONST(BitVectorSignExtend(k - n)), f); }
1772 /* BV zero extension */
1773 | BVZEROEXTEND_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1774 { unsigned n = BitVectorType(f.getType()).getSize();
1775 // Zero extension in TheoryBitVector is defined as in SMT-LIB
1776 // which is the same as in CVC3, but different than SX!
1777 // SX(BITVECTOR(k), n) in CVC language extends to n bits
1778 // BVZEROEXTEND(BITVECTOR(k), n) in CVC language extends to k + n bits
1779 f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f); }
1780 /* BV repeat operation */
1781 | BVREPEAT_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1782 { f = MK_EXPR(MK_CONST(BitVectorRepeat(k)), f); }
1783 /* BV rotate right */
1784 | BVROTR_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1785 { f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); }
1786 /* BV rotate left */
1787 | BVROTL_TOK LPAREN formula[f] COMMA k=numeral RPAREN
1788 { f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); }
1790 /* BV comparisons */
1791 | BVLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1792 { f = MK_EXPR(CVC4::kind::BITVECTOR_ULT, f, f2); }
1793 | BVLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1794 { f = MK_EXPR(CVC4::kind::BITVECTOR_ULE, f, f2); }
1795 | BVGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1796 { f = MK_EXPR(CVC4::kind::BITVECTOR_UGT, f, f2); }
1797 | BVGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1798 { f = MK_EXPR(CVC4::kind::BITVECTOR_UGE, f, f2); }
1799 | BVSLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1800 { f = MK_EXPR(CVC4::kind::BITVECTOR_SLT, f, f2); }
1801 | BVSLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1802 { f = MK_EXPR(CVC4::kind::BITVECTOR_SLE, f, f2); }
1803 | BVSGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1804 { f = MK_EXPR(CVC4::kind::BITVECTOR_SGT, f, f2); }
1805 | BVSGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
1806 { f = MK_EXPR(CVC4::kind::BITVECTOR_SGE, f, f2); }
1809 | IS_INTEGER_TOK LPAREN formula[f] RPAREN
1810 { f = MK_EXPR(CVC4::kind::BITVECTOR_IS_INTEGER, f); }
1816 /** Parses a simple term. */
1817 simpleTerm[CVC4::Expr& f]
1820 std::vector<Expr> args;
1821 std::vector<std::string> names;
1823 Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
1829 /* parenthesized sub-formula / tuple literals */
1830 | LPAREN formula[f] { args.push_back(f); }
1831 ( COMMA formula[f] { args.push_back(f); } )* RPAREN
1832 { if(args.size() > 1) {
1833 /* If args has elements, we must be a tuple literal.
1834 * Otherwise, f is already the sub-formula, and
1835 * there's nothing to do */
1836 std::vector<Type> types;
1837 for(std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); ++i) {
1838 types.push_back((*i).getType());
1840 TupleType t = EXPR_MANAGER->mkTupleType(types);
1841 f = MK_EXPR(kind::TUPLE, args);
1845 /* empty tuple literal */
1847 { f = MK_EXPR(kind::TUPLE, std::vector<Expr>()); }
1848 /* empty record literal */
1849 | PARENHASH HASHPAREN
1850 { RecordType t = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >());
1851 f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), std::vector<Expr>());
1854 /* boolean literals */
1855 | TRUE_TOK { f = MK_CONST(bool(true)); }
1856 | FALSE_TOK { f = MK_CONST(bool(false)); }
1857 /* arithmetic literals */
1858 /* syntactic predicate: never match INTEGER.DIGIT as an integer and a dot!
1859 * This is a rational constant! Otherwise the parser interprets it as a tuple
1861 | DECIMAL_LITERAL { f = MK_CONST(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
1862 | INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
1863 /* bitvector literals */
1865 { assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 );
1866 std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4);
1867 f = MK_CONST( BitVector(hexString, 16) ); }
1869 { assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 );
1870 std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4);
1871 f = MK_CONST( BitVector(binString, 2) ); }
1872 /* record literals */
1873 | PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); }
1874 ( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN
1875 { std::vector< std::pair<std::string, Type> > typeIds;
1876 assert(names.size() == args.size());
1877 for(unsigned i = 0; i < names.size(); ++i) {
1878 typeIds.push_back(std::make_pair(names[i], args[i].getType()));
1880 RecordType t = EXPR_MANAGER->mkRecordType(typeIds);
1881 f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), args);
1884 /* variable / zero-ary constructor application */
1885 | identifier[name,CHECK_DECLARED,SYM_VARIABLE]
1886 /* ascriptions will be required for parameterized zero-ary constructors */
1887 { f = PARSER_STATE->getVariable(name); }
1888 { // datatypes: zero-ary constructors
1889 Type t2 = PARSER_STATE->getType(name);
1890 if(t2.isConstructor() && ConstructorType(t2).getArity() == 0) {
1891 // don't require parentheses, immediately turn it into an apply
1892 f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, f);
1898 * Matches (and performs) a type ascription.
1899 * The f arg is the term to check (it is an input-only argument).
1901 typeAscription[const CVC4::Expr& f, CVC4::Type& t]
1904 : COLON COLON type[t,CHECK_DECLARED]
1908 * Matches an entry in a record literal.
1910 recordEntry[std::string& name, CVC4::Expr& ex]
1911 : identifier[name,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[ex]
1915 * Parses an ITE term.
1917 iteTerm[CVC4::Expr& f]
1919 std::vector<Expr> args;
1920 Debug("parser-extra") << "ite: " << AntlrInput::tokenText(LT(1)) << std::endl;
1922 : IF_TOK formula[f] { args.push_back(f); }
1923 THEN_TOK formula[f] { args.push_back(f); }
1924 iteElseTerm[f] { args.push_back(f); }
1926 { f = MK_EXPR(CVC4::kind::ITE, args); }
1930 * Parses the else part of the ITE, i.e. ELSE f, or ELSIF b THEN f1 ...
1932 iteElseTerm[CVC4::Expr& f]
1934 std::vector<Expr> args;
1935 Debug("parser-extra") << "else: " << AntlrInput::tokenText(LT(1)) << std::endl;
1937 : ELSE_TOK formula[f]
1938 | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); }
1939 THEN_TOK iteThen = formula[f] { args.push_back(f); }
1940 iteElse = iteElseTerm[f] { args.push_back(f); }
1941 { f = MK_EXPR(CVC4::kind::ITE, args); }
1945 * Parses a datatype definition
1947 datatypeDef[std::vector<CVC4::Datatype>& datatypes]
1949 std::string id, id2;
1951 std::vector< Type > params;
1953 /* This really needs to be CHECK_NONE, or mutually-recursive
1954 * datatypes won't work, because this type will already be
1955 * "defined" as an unresolved type; don't worry, we check
1957 : identifier[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
1958 ( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] {
1959 t = PARSER_STATE->mkSort(id2, ExprManager::SORT_FLAG_PLACEHOLDER);
1960 params.push_back( t );
1962 ( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] {
1963 t = PARSER_STATE->mkSort(id2, ExprManager::SORT_FLAG_PLACEHOLDER);
1964 params.push_back( t ); }
1967 { datatypes.push_back(Datatype(id, params));
1968 if(!PARSER_STATE->isUnresolvedType(id)) {
1969 // if not unresolved, must be undeclared
1970 PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
1973 EQUAL_TOK constructorDef[datatypes.back()]
1974 ( BAR constructorDef[datatypes.back()] )*
1975 { PARSER_STATE->popScope(); }
1979 * Parses a constructor defintion for type
1981 constructorDef[CVC4::Datatype& type]
1984 CVC4::DatatypeConstructor* ctor = NULL;
1986 : identifier[id,CHECK_UNDECLARED,SYM_SORT]
1987 { // make the tester
1988 std::string testerId("is_");
1989 testerId.append(id);
1990 PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
1991 ctor = new CVC4::DatatypeConstructor(id, testerId);
1995 ( COMMA selector[*ctor] )*
1998 { // make the constructor
1999 type.addConstructor(*ctor);
2000 Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
2005 selector[CVC4::DatatypeConstructor& ctor]
2010 : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON type[t,CHECK_NONE]
2011 { ctor.addArg(id, t);
2012 Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
2017 * Matches an identifier from the input. An identifier is a sequence of letters,
2018 * digits and "_", "'", "." symbols, starting with a letter.
2020 IDENTIFIER : (ALPHA | '_') (ALPHA | DIGIT | '_' | '\'' | '\\' | '?' | '$' | '~')*;
2023 * Same as an integer literal converted to an unsigned int, but
2024 * slightly more convenient AND works around a strange ANTLR bug (?)
2025 * in the BVPLUS/BVMINUS/BVMULT rules where $INTEGER_LITERAL was
2026 * returning a reference to the wrong token?!
2028 numeral returns [unsigned k = 0]
2030 { $k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); }
2034 * Similar to numeral but for arbitrary-precision, signed integer.
2036 integer returns [CVC4::Rational k = 0]
2038 { $k = AntlrInput::tokenToInteger($INTEGER_LITERAL); }
2039 | MINUS_TOK INTEGER_LITERAL
2040 { $k = -AntlrInput::tokenToInteger($INTEGER_LITERAL); }
2044 * Similar to numeral but for strings.
2048 { s = AntlrInput::tokenText($STRING_LITERAL);
2049 /* strip off the quotes */
2050 s = s.substr(1, s.size() - 2);
2055 * Matches a hexadecimal constant.
2062 * Matches a binary constant.
2065 : '0bin' ('0' | '1')+
2069 * Matches a double quoted string literal. Escaping is supported, and
2070 * escape character '\' has to be escaped.
2072 STRING_LITERAL: '"' (ESCAPE | ~('"'|'\\'))* '"';
2075 * Matches any letter ('a'-'z' and 'A'-'Z').
2077 fragment ALPHA : 'a'..'z' | 'A'..'Z';
2080 * Matches the decimal digits (0-9)
2082 fragment DIGIT : '0'..'9';
2084 // This rule adapted from http://www.antlr.org/wiki/pages/viewpage.action?pageId=13828121
2085 // which reportedly comes from Tapestry (http://tapestry.apache.org/tapestry5/)
2087 // Special rule that uses parsing tricks to identify numbers and ranges; it's all about
2092 // INTEGER_LITERAL (digit+)
2093 // DECIMAL_LITERAL (digit* . digit+)
2094 // Has to watch out for embedded rangeop (i.e. "1..10" is not "1." and ".10").
2096 // This doesn't ever generate the NUMBER_OR_RANGEOP token, it
2097 // manipulates the $type inside to return the right token.
2101 { LA(2) != '.' }? => '.' DIGIT* { $type = DECIMAL_LITERAL; }
2102 | { $type = INTEGER_LITERAL; }
2105 ( '.' {$type = DOTDOT; }
2110 // these empty fragments remove "no lexer rule corresponding to token" warnings
2111 fragment INTEGER_LITERAL:;
2112 fragment DECIMAL_LITERAL:;
2117 * Matches the hexidecimal digits (0-9, a-f, A-F)
2119 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
2122 * Matches and skips whitespace in the input and ignores it.
2124 WHITESPACE : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); };
2127 * Matches the comments and ignores them
2129 COMMENT : '%' (~('\n' | '\r'))* { SKIP(); };
2132 * Matches an allowed escaped character.
2134 fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');