diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 11ccb4935..7ef7edbbe 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1549,6 +1549,12 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] } expr = SOLVER->mkTuple(sorts, terms); } + | LPAREN_TOK TUPLE_PROJECT_TOK term[expr,expr2] RPAREN_TOK + { + std::vector<uint32_t> indices; + api::Op op = SOLVER->mkOp(api::TUPLE_PROJECT, indices); + expr = SOLVER->mkTerm(op, expr); + } | /* an atomic term (a term with no subterms) */ termAtomic[atomTerm] { expr = atomTerm; } ; @@ -1672,6 +1678,19 @@ identifier[CVC4::ParseOp& p] // put m in expr so that the caller can deal with this case p.d_expr = SOLVER->mkInteger(AntlrInput::tokenToUnsigned($m)); } + | TUPLE_PROJECT_TOK nonemptyNumeralList[numerals] + { + // we adopt a special syntax (_ tuple_project i_1 ... i_n) where + // i_1, ..., i_n are numerals + p.d_kind = api::TUPLE_PROJECT; + std::vector<uint32_t> indices(numerals.size()); + for(size_t i = 0; i < numerals.size(); ++i) + { + // convert uint64_t to uint32_t + indices[i] = numerals[i]; + } + p.d_op = SOLVER->mkOp(api::TUPLE_PROJECT, indices); + } | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] { p.d_op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals); @@ -2279,6 +2298,7 @@ EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp'; CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char'; TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple'; TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel'; +TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_project'; HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->'; HO_LAMBDA_TOK : { PARSER_STATE->isHoEnabled() }? 'lambda'; |